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 by including a special value such that is a total function. In Haskell you’ll find that the type `Maybe B`

plays the role of the lifted codomain . 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:

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:****right identity:****associativity:**

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!

nice post. thanks.

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?

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

You probably forgot to declare the arguments to the constructors of

`option`

`implicit.`

Shouldn’t bind read “…

`| Some x ->`

…”?Somef xNo,

`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).Pingback: When null is not enough: an option type for C# | Twisted Oak Studios Blog