How can I specify that two operations commute in a

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 I can't figure is how to phrase the contract that operations must commute in the specification of the typeclass.

The reason that you can't figure it out is that it's not possible. You can't encode this kind of property in types - not in Haskell at least.

Answer 2

Further to TomMD's answer, you can use Agda to the same effect. Although it doesn't have typeclasses, you get most of the functionality (apart from dynamic dispatch) from records.

record Direction (a : Set) : Set₁ where
  field
    turnLeft  : a → a
    turnRight : a → a
    commLaw   : ∀ x → turnLeft (turnRight x) ≡ turnRight (turnLeft x)

---

I thought I'd edit the post and answer the question of why you can't do this in Haskell.

In Haskell (+ extensions), you can represent equivalence as used in the Agda code above.

{-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}

data (:=:) a :: * -> * where
  Refl :: a :=: a  

This represents theorems about two types being equal. E.g. a is equivalent to b is a :=: b.

Where we they are equivalent, we can use the constructor Refl. Using this, we can perform functions on the proofs (values) of the theorems (types).

-- symmetry
sym :: a :=: b -> b :=: a
sym Refl = Refl

-- transitivity
trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl

These are all type-correct, and therefore true. However this;

wrong :: a :=: b
wrong = Refl

is clearly wrong and does indeed fails on type checking.

However, through all this, the barrier between values and types has not been broken. Values, value-level functions and proofs still live on one side of the colon; types, type-level functions and theorems live on the other. Your turnLeft and turnRight are value-level functions and therefore cannot be involved in theorems.

Agda and Coq are dependently-typed languages, where the barrier does not exist or things are allowed to cross over. The Strathclyde Haskell Enhancement (SHE) is a preprocessor for Haskell code that can cheat some of the effects of DTP into Haskell. It does this by duplicating data from the value world in the type world. I don't think it handles duplicating value-level functions yet and if it did, my hunch is this might be too complicated for it to handle.

Answer 3

As has been stated already, there's no way to enforce this directly in Haskell using the type system. But if merely specifying constraints in comments isn't satisfying enough, as a middle ground you could provide QuickCheck tests for the desired algebraic properties.

Something along these lines can already be found in the checkers package; you may want to consult it for inspiration.

Answer 4

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.