# The Maybe monad in Coq

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

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:

Inductive option (A : Type) :=
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 any Haskell text that the monad laws are, in order:

• 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!