The Maybe monad is pretty useful whenever you’re dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.

The first idea is a to lift the codomain of a partial function $f : A \rightharpoonup B$ by including a special value $\bot$ such that $f^\prime : A \rightarrow B \cup \{\bot\}$ is a total function. In Haskell you’ll find that the type Maybe B plays the role of the lifted codomain $B \cup \{\bot\}$. But enough mathematical foreplay, let’s get to it:

data Maybe t = Just t | Nothing   instance Monad Maybe where return = Just (Just x) >>= k = k x Nothing >>= k = Nothing

Coq’s standard library also includes the datatype Maybe, but there it is called option.

Inductive option (A : Type) := | Some : A -> option A | None : option A.

In order to make working with this type a little more enjoyable and the resulting code more readable, we declare the type argument of its constructors to be implicit which means that they should be inferred from the context:

Arguments Some [A] _. Arguments None [A].

Now we can define the monad operations return (which we’ll call ret to avoid confusion with the keyword of the same name) and >>= (which is also called bind).

Definition ret {A : Type} (x : A) := Some x.   Definition bind {A B : Type} (a : option A) (f : A -> option B) : option B := match a with | Some x => f x | None => None end.

We can also define the usual notations for use in monadic code. First, the familiar infix operator for the bind operation.

Notation "A >>= F" := (bind A F) (at level 42, left associativity).

Followed by the beloved do-notation from Haskell.

Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200).

We could stop here, but because Coq is also a thereom prover and not only a fancy dependently typed functional programming language, we go right on and prove the three laws that each monad has to satisfy in order to be called a monad at all. Recall from

• left identity: $\mathrm{return}\;a \gg\!= f = f\;a$
• right identity: $a \gg\!= \mathrm{return} = a$
• associativity: $(a \gg\!= f) \gg\!= g = a \gg\!= (\lambda x\,.\, f\;x \gg\!= g)$

These laws correspond directly to the Coq lemmata mon_left_id, mon_right_id, and
mon_assoc below. As you can see, the proofs in all three cases are rather trivial.

Lemma mon_left_id : forall (A B : Type) (a : A) (f : A -> option B), ret a >>= f = f a. intros. reflexivity. Qed.   Lemma mon_right_id : forall (A : Type) (a : option A), a >>= ret = a. intros. induction a; repeat reflexivity. Qed.   Lemma mon_assoc : forall (A B C : Type) (a : option A) (f : A -> option B) (g : B -> option C), (a >>= f) >>= g = a >>= (fun x => f x >>= g). intros. induction a; repeat reflexivity. Qed.

That’s is, have some fun with the Maybe monad in Coq!

This entry was posted in Coq, Haskell and tagged . Bookmark the permalink.

8 Responses to The Maybe monad in Coq

1. mikerosss says:

nice post. thanks.

2. erus says:

Definition ret {A : Type} (x : A) := Some x. is a type error

• This definition is perfectly typeable as it is. Perhaps you could elaborate on the specifics of your problem. Perhaps you are using an older Coq version than 8.3?

• Chris Perivolaropoulos says:

Same here. I am getting:

Error:
In environment
A : Type
x : A
The term “x” has type “A” while it is expected to have type “Type”.

• Thomas Strathmann says:

You probably forgot to declare the arguments to the constructors of option implicit.

3. mdgeorge says:

Shouldn’t bind read “… | Some x -> Some f x …”?

• Thomas Strathmann says:

No, Some f x is not even type correct in that context and Some (f x) has type option (option B) but this is not what we want. Actually, the code I presented is just a transliteration from Haskell to Gallina with the proofs added just because we can. 😉

But your comment made me reexamine the code and I found that I did forget to set the argument to the constructors of option as implicit which breaks the definition of bind. Should work now (tested with the current version Coq 8.4).

This site uses Akismet to reduce spam. Learn how your comment data is processed.