How can I specify that two operations commute in a typeclass?

Question

I started reading this paper on CRDTs, which is a way of sharing modifiable data concurrently by ensuring that the operations that modify the data are commutative. It seemed to me that this would be a good candidate for abstraction in Haskell - provide a typeclass for CRDTs that specifies a datatype and operations that commute on that type, then work on making library to actually share the updates between concurrent processes.

What I can't figure is how to phrase the contract that operations must commute in the specification of the typeclass.

For a simple example:

class Direction a where
  turnLeft :: a -> a
  turnRight :: a -> a

There's no guarantee that turnLeft . turnRight is the same as turnRight . turnLeft. I suppose the fallback is to specify the equivalent of the monad laws - use a comment to specify constraints that aren't enforced by the type system.

Answer 1

What you want is a type class that includes a proof burden, something like the below pseudo-Haskell:

class Direction a where
    turnLeft  :: a -> a
    turnRight :: a -> a
    proofburden (forall a. turnLeft (turnRight a) === turnRight (turnLeft a))

Here all instance must provide both functions and proof(s) for the compiler to type check. This is wishful thinking (for Haskell) as Haskell has no (well, limited) notion of proof.

OTOH, Coq is a proof assistant for a dependently typed language that can extract to Haskell. While I've never used Coq's type classes before, a quick search is fruitful, with the example:

Class EqDec (A : Type) := {
   eqb : A -> A -> bool ;
   eqb_leibniz : forall x y, eqb x y = true -> x = y }.

So it looks like advanced languages can do this, but there is arguably much work to do in lowering the learning curve for your standard developer.