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?

Epileptoid

You could define addition normally and would get (slow) commutativity for free. – Dream

Also, this already has an answer here. (It is more general than your use case, so you probably need to do some research how to use the suggested package) – Dream

If you take into account lazyness almost no operation is completely commutative because typically f undefined x can be different than f x undefined due to the fact that pattern matching is essentially sequential. This is the reason why it's so hard to obtain full abstraction between operational and denotational semantics of functional languages: in denotational semantics you include functions like parallel or etc which cannot actually be defined in the language. – Mendive

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.

Rizika

Perfect and simple, thanks! Don't know why I didn't think of this myself. – Epileptoid

Also, GHC is very wary of inlining recursive functions (because it might never stop!) so using this technique could interfere with compiler optimizations. Although of course it's also possible that GHC will figure out it's really not recursive, and end up inlining, but I'm not sure it's quite that clever. – Cardiovascular

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.

Dream

What happens with a greater than comparison when one of the arguments is bottom at some point. Eg, 3 >=(Succ (Succ (undefined)) + Succ Zero). You should get either undefined both ways or True both ways if it's commutative. – Sonnysonobuoy

In general you are correct, however in some (either beginner or very theoretical) views we ignore undefined sometimes. In the theoretical view undefined brings a lot of complications, and sometimes it is easier to work in an idealized model. – Dream

Why not get it right instead of idealized? make Succ be strict in its argument so you have undefined both ways and it's both commutative and idealised instead of idealised but not commutative when the requirement is commutative and idealism is not requested. – Sonnysonobuoy

In general you don't want to enforce strictness for every function since you miss out some nice optimizations the compiler may be able to perform (Short-cut fusion is one example where laziness helps the compiler a lot). Of course in this toy example you may as well make it strict - it doesn't matter. – Dream

good point, what about making the addition function strict in both arguments? – Sonnysonobuoy