# 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.

``` 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 ```

``` 1. return a >>= f = f a 2. m >>= return = m 3. (m >>= f) >>= g = m >>= (\x -> f x >>= g) ```
``` 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). ```