Why do Haskell's typeclass laws have to be verified manually?

user_4622575 0
Viewed 158

Why does one need to explicitly write checks (possibly using quickcheck) for type class laws in Haskell?

For example for testing associativity of the String monoid:

leftIdcheck :: Monoid a => a -> Bool
leftIdcheck a = a <> mempty == a

quickCheck (leftIdcheck :: String -> Bool)

But this is so much work! Why can't the haskell complier just check all this by default on its own and tell me that my instance of monoid on my type doesn't satisfy the identity law ?

Is there any library or language extension that allows us to have these checks built in as we write the program instead of having to write them separately? This seems very error prone.

On a related note, does Agda let us have these checks/proofs for free or do we have to write them manually there too?

typeclass haskell
1 Answers

Haskell is a non-total language without dependent types, therefore most properties you might want to prove a) can't even be formulated exactly b) aren't really strictly speaking true, if you consider ⊥.

In Coq and Agda, that is a different story, and indeed a Coq class will normally contain not only the methods its Haskell pendant has, but also the laws:

Class Monoid (m: Type) : Type :=
  { mempty : m
  ; mappend : m -> m -> m
  ; mempty_left : forall (p: m), mappend mempty p = p
  ; mempty_right : forall (p: m), mappend p mempty = p
  ; mappend_assoc : forall (p q r: m)
                  , mappend p (mappend q r) = mappend (mappend p q) r
  }.

Still that doesn't mean the compiler will just automatically prove those for you, when you declare an instance. As Willem Van Onsem commented, that is in general impossible. You need to write the proof yourself, and that is much, much more laborious than writing a QuickCheck property. Of course if you've managed to do it, it is a bit more reassuring, however in practice QuickCheck is usually enough to catch >90% of all bugs. Proper formal verification is great, but it's only worthwhile for really important / safety-critical code and even then it's quite a good idea to first let QuickCheck confirm that there's even any hope of proving what you're trying to prove.

user_7459030
Related