Commutative Property for Haskell Operators?

Question

Is there a way to state that an operator is commutative, so that I don't have to give identical definitions for both directions? For instance:

data Nat = Zero | Succ Nat

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

Here, is there a way such that I wouldn't have to give both of those definitions, that one of them would be implied from the other? Is there some way to state that fn = flip fn?

Answer 1

It’s not necessary for this addition operator, but in general you can make a function commutative without implementing all the flipped cases by adding a final equation that flips the arguments:

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

However, the downside is that if you forget to handle a case, this easily leads to an infinite loop:

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

Here, adjacent A C would call adjacent C A, which would call adjacent A C, and so on. And GHC’s pattern match exhaustivity checking (-fwarn-incomplete-patterns or -Wall) won’t help you here.

I guess you could add an additional argument to prevent looping:

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

Now GHC will complain if you don’t add the go Reverse equation to handle the case where you commuted but there was still no match.

But I think this is only suitable for functions with a large number of cases—otherwise, it’s much clearer to simply enumerate them all.

Answer 2

To put it as an answer: Yes, if you implement regular addition, you automatically end up with a commutative operation:

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

This operation is commutative, although it isn't efficient both ways, meaning that "big number as UInt" + Zero takes longer than Zero + "big number as UInt" because the addition operator is defined that way.

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

An easy way to fix this is to define addition the way you did, explicitly defining commutativity.