Coq and The Monad Laws: Introduction
Over the past few months I've been spending some time with Coq, the proof assistant. I am still very much a beginner, so as an exercise I decided to try and prove the three Monad laws for the implementation of the List Monad.
In Haskell, the List Monad looks like this:
instance Monad  where
return x = [x]
m >>= f = concatMap f m
Coq is a proof-assistant for a constructive logic, so it can also be used as a (dependently-typed) functional programming language.
You can open an interactive session and type the lines in using
coqtop. However, I use the ProofGeneral Emacs-based interface and save my code in a file like "listmonad.v". You can then step through the lines using
C-c C-n. There also exists a custom GUI called CoqIDE.
In Coq, I defined the Monad methods like so:
Require Import List.
Definition ret (A : Set) (a : A) := a :: nil.
Definition bind (A B : Set) (m : list A) (f : A -> list B) :=
flat_map f m.
I opened up a new section (but did not close it yet). The definitions are fairly unremarkable, except that now the types A and B are explicit parameters. In Coq, a single colon is used for type annotations, and a double colon is used for list consing.
flat_map is Coq's version of
concatMap. I did not know that before, but found it by using
SearchAbout list. at the interactive Coq prompt.
I can see what Coq thinks of my definitions:
Coq < Check ret.
: forall A : Set, A -> list A
Coq < Check bind.
: forall A B : Set, list A -> (A -> list B) -> list B
Now we are ready to state the three Monad Laws. First, in Haskell notation:
1. return a >>= f = f a
2. m >>= return = m
3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)
The first two Monad laws, in essence, assert that return is an identity operation on the left and right sides of bind. The third says that bind is associative.
Theorem first_law :
forall (A B : Set) (a : A) (f : A -> list B),
bind A B (ret A a) f = f a.
Theorem second_law :
forall (A : Set) (m : list A),
bind A A m (ret A) = m.
Theorem third_law :
forall (A B C : Set) (m : list A)
(f : A -> list B) (g : B -> list C),
bind B C (bind A B m f) g =
bind A C m (fun x => bind B C (f x) g).
Entering any of these Theorems into Coq will engage the interactive proof mode. In the next article, I will examine the proofs of the first two laws.