Коммутативное свойство для операторов Haskell?

Question

Есть ли способ заявить, что оператор является коммутативным, чтобы мне не приходилось давать одинаковые определения для обоих направлений? Например:

data Nat = Zero | Succ Nat

(+) :: Nat -> Nat -> Nat
Zero + x = x
x + Zero = x
...

Здесь, есть ли способ, которым мне не пришлось бы давать оба эти определения, чтобы одно из них подразумевалось от другого? Есть ли способ заявить, что fn = flip fn?

Answer 1

Это необязательно для этого оператора сложения, но в целом вы можете сделать функцию коммутативной, не реализуя все перевернутые случаи, добавив окончательное уравнение, которое переворачивает аргументы:

data X = A | B | C

adjacent A B = True
adjacent B C = True
adjacent A C = False
adjacent x y = adjacent y x  -- covers B A, C B, and C A

Однако недостатком является то, что если вы забудете обработать регистр, это легко приведет к бесконечному циклу:

adjacent A B = True
adjacent B C = True
adjacent x y = adjacent y x

Вот, adjacent A C назвал бы adjacent C A, который бы назвал adjacent A C, и так далее. И проверка соответствия шаблону GHC (-fwarn-incomplete-patterns или же -Wall) здесь тебе не поможет.

Я думаю, вы могли бы добавить дополнительный аргумент для предотвращения зацикливания:

data Commute = Forward | Reverse

adjacent = go Forward
  where
    go _ A B = True
    go _ B C = True
    go Forward x y = go Reverse y x  -- try to commute
    go Reverse _ _ = False           -- commuting failed

Теперь GHC будет жаловаться, если вы не добавите go Reverse Уравнение для обработки случая, когда вы добирались, но не было совпадения.

Но я думаю, что это подходит только для функций с большим количеством случаев, в противном случае гораздо проще просто перечислить их все.

Answer 2

Чтобы выразить это как ответ: Да, если вы реализуете регулярное добавление, вы автоматически получаете коммутативную операцию:

(+) :: UInt -> UInt -> UInt
Zero + x = x
(Succ s) + x = s + (Succ x)

Эта операция является коммутативной, хотя она неэффективна в обоих направлениях, а это означает, что "big number as UInt" + Zero занимает больше времени, чем Zero + "big number as UInt" потому что оператор сложения определен таким образом.

ghci> :set +s
ghci> bignum + Zero
number as uint
(0.01 secs, 4,729,664 bytes) -- inefficient O(n) operation
ghci> Zero + bignum
number as uint
(0.00 secs, 0 bytes) -- instant constant operation

Простой способ исправить это - определить сложение так, как вы это делали, явно определяя коммутативность.