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