Programmatic proofs for monad laws

Question

In haskell, the users do not have to prove that their monads satisfy the monad laws.

return a >>= k                  =  k a
m        >>= return             =  m
m        >>= (\x -> k x >>= h)  =  (m >>= k) >>= h

If I understand correctly, even if they want, there's no way for the compiler could read such a proof.

Questions

1. What technology is missing in haskell for there to be a way to implement such proof checkable by a compiler?
2. Which functional language supports such a functionality (i.e. can check if a claim-to-be monad satisfies the monad laws)?

Answer 1

In practice, laws usually aren't proven in Haskell, but they may very well be tested. If you throw lots of random inputs to the expressions on both sides of the equation for your monad, and the result always comes out the same on both sides, that may not guarantee anything but it does make it quite likely that any law-violating behaviour would be caught. That is, provided you generate the inputs in a sufficiently representative way. QuickCheck is usually pretty good at this.

If you do want to prove laws then, well, Haskell isn't really the right tool. You'd want the proof to be checked at compile time, but Haskell makes it rather difficult to express complicated values in the type level. If you do it at runtime instead, then first of all: no good if the deployed executable crashes because of a mistake. But more importantly, since Haskell isn't total you could “prove” any proposition by just giving undefined as the result – or some other ⊥ value, more typically this might be some subtle infinite loop.

The right tool is a dependently typed language. The most popular are Coq and Lean, which resemble ML more than Haskell, and Agda. These are primarily intended to be proof assistants rather that general programming languages which also allow you to formulate theorems; Idris goes more in that direction.

All that said, modern Haskell is now also have somewhat capable of dependently-typed programming. The key tool is to have your functions as type families, and use singletons to get value-level standins to the type-level values, and then use either GADTs or constrained CPS to pass around the proofs.

It's still really awkward to use this to specify laws for a type class, but it can be used quite nicely to Curry-Howard-express concrete theorems. The singletons-base package contains a lot of standard functions in type-lifted form, thus suitable for proving stuff about. For example, here's how you could formulate that the list concatenation operator is associative:

{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, PolyKinds, TypeOperators #-}

import Data.List.Singletons

listConcatAssoc :: ∀ k l m ρ . Sing k -> Sing l -> Sing m
            -> (((k++l)++m ~ k++(l++m)) => ρ) -> ρ
listConcatAssoc SNil SNil SNil φ = φ
...

The complete proof will be quite annoying to write, but TBH proofs are annoying to write even in Coq, though that is specifically its job. Coq does make it a lot nicer to really express typeclasses with laws etc., though.