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.

Riedel

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.

Cathar

The funny thing is C++0x Concepts (dropped proposal) had such support, they were called axioms. – Coumarin

@snk_kid: C++ axioms don't statically ensure that the specified invariant is actually true. – Expose

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.

Leach

Agda also gives the minor benefit in this case of a more Haskell-ish flavor and a direct FFI to Haskell--i.e., potentially a smaller learning curve for a Haskell programmer new to dependently typed languages. – Cameroun

I do find while programming Agda feels more Haskell, the code extracted from Coq is more like the Haskell I would write. Swings and roundabouts. – Leach

I'd suppose it depends on whether the goal is to extract a small library to use in Haskell, or to write mostly in Agda while calling into Haskell libraries. But I've used Agda little and Coq never, so I can't say for sure... – Cameroun

That is true. I believe people are working on the Agda-to-Haskell compiler this year to make it a bit less verbose. Excellent work done by all those involved. – Leach

I've had a little fiddle with She and I'd like to clarify my answer as you might be able to but She isn't quite there yet and you probably still don't want to. If you're interested, see my blog post containing my working. You've inspired me. Thanks. – Leach

"Most functional programmers are hesitant to program with dependent types. It is said that type checking becomes undecidable; the type checker will always loop; and that dependent types are just really, really, hard. The same programmers, however, are perfectly happy to program with a ghastly hodgepodge of complex type system extensions. [...] to go to great lengths just to avoid dependent types." -- Tutorial Implementation of a Dependently Typed Lambda Calculus. N.B.: Compare author list with the perpetrator of SHE. :) – Cameroun

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.

Cameroun

Answer 4

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.

Expose

I'm willing to believe that - can you provide any link to a discussion on the topic? – Riedel

I believe the reason is the separation between values and their types. In Haskell's type system, there is an impassable barrier between their worlds. I quite like Conor McBride's analogy to an "established social order" in strictlypositive.org/winging-jpgs and strictlypositive.org/a-case. – Leach

The "established social order" slides are hilarious (and informative). McBride also published the paper "Why Dependent Types Matter" on Epigram, which is dependently typed. It's syntax looks fairly similar to Haskell's. – Audriaaudrie