Является ли эксклюзивный или моноид для Bools?

Я сделал для xor-функции оператор, он выглядит так:

op :: Integer -> Integer -> Maybe Integer
op x y
  | x == 0 && y == 0 = Just 0
  | x == 0 && y == 1 = Just 1
  | x == 1 && y == 0 = Just 1
  | x == 1 && y == 1 = Just 0
  | otherwise = Nothing

Я использовал 0 и 1 вместо True и False, но это не должно повлиять на результат. Я читал, что это моноид, но не понимаю почему. Ассоциативность очевидна и не требует доказательства (доказательство я уже сделал сам), но что такое элемент идентичности и почему?

Изменить: вот без цифр:

xor :: Bool -> Bool -> Bool
xor x y | x == True && y == False = True
        | x == False && y == True = True
        | otherwise = False

haskell xor monoids
person Vajk    schedule 06.07.2017    source источник
comment
Я бы сказал наоборот: идентичность банально ложна, потому что False ^ x == x, что вы легко можете исчерпывающе подтвердить. Но менее очевидно, что ассоциативность имеет место, и это может потребовать доказательства. Кроме того, это, возможно, целые числа - очень странный способ кодирования bools.   -  person amalloy    schedule 06.07.2017
comment
Подсказка: если у вас есть целые числа x и y, то x `xor` y является младшим битом x + y. Отдельно вам следует посмотреть на Data.Bits, а также не использовать Integer для представления логического значения.   -  person dfeuer    schedule 06.07.2017
comment
Это не может образовывать моноид (с элементом идентичности), поскольку функция должна иметь тип X -> X -> X с X набором, над которым определен моноид.   -  person Willem Van Onsem    schedule 06.07.2017
comment
(Xor, False) действительно является моноидом (и даже группой с очевидным оператором обращения). Однако ваш код не имеет дело с логическими значениями. Непонятно, почему вы думаете, что это не должно иметь значения. Очевидно, да. Из-за этого вам пришлось представить Maybe.   -  person n. 1.8e9-where's-my-share m.    schedule 06.07.2017
comment
Почему бы тебе просто не сделать это как xor :: Eq a => a -> a -> Bool xor x y = x /= y   -  person Redu    schedule 06.07.2017
comment
@Redu: или просто xor = (/=).   -  person Willem Van Onsem    schedule 06.07.2017
comment
@Redu, потому что это глупо. Data.Bits правильно понял: xor :: Bits a => a -> a -> a.   -  person dfeuer    schedule 06.07.2017
comment
@dfeuer вы говорите глупо, но именно так xor определено в Data.Bits пакете.   -  person Redu    schedule 06.07.2017
comment
@Redu только для Bool, а не для всех типов Eq.   -  person Li-yao Xia    schedule 06.07.2017

Ответы (1)


arrow_upward
1
arrow_downward

Я допустил глупую ошибку в своем доказательстве, поскольку amalloy сказал, что личность ложная. Вот полное доказательство, надеюсь, теперь оно верное.

mempty <> p = p
xor False p = p
-- For p = True:
xor False True = True
True = True
-- For p = False:
xor False False = False
False = False
-- Q.E.D
person Vajk    schedule 06.07.2017