Coq and The Monad Laws: Introduction

Submitted by mrd on Wed, 08/15/2007 - 2:26pm.

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:

Section ListMonad. 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. ret : forall A : Set, A -> list A Coq < Check bind. 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.

In Coq:

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.