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:

In Haskell the Maybe monad is part of the standard library.

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

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