Подтвердить что ты не робот

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

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

data Nat = Zero | Succ Nat

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

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

Ответ 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 и т.д. И проверка соответствия шаблону соответствия GHCs (-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 для обработки случая, когда вы заменили, но совпадения не было.

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

Ответ 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

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