Coq and The Maybe Monad

In the spirit of Coq and The Monad Laws, I here is a quick (and easy) proof that Maybe (known in Coq/OCaml as option) satisfies the three Monad Laws.


Section MaybeMonad.

Definition retO (A:Set) (a:A) := Some a.
Definition bindO (A B : Set) (m:option A) (f:A -> option B)
:= match m with Some m' => f m' | None => None end.

(* return a >>= f = f a *)
Theorem first_law_opt :
forall (A B : Set) (a:A) (f:A -> option B),
bindO A B (retO A a) f = f a.

intros A B a f.
unfold bindO.
unfold retO.
reflexivity.
Qed.

(* (m >>= return) = m *)
Theorem second_law_opt :
forall (A:Set) (m : option A), bindO A A m (retO A) = m.

intros A m.
unfold bindO.
induction m.
unfold retO.
reflexivity.
reflexivity.
Qed.

(* (m >>= f) >>= g = m >>= (\x -> f x >>= g) *)
Theorem third_law_opt:
forall (A B C : Set) (m:option A) (a:A)
(f : A -> option B) (g : B -> option C),
bindO B C (bindO A B m f) g
= bindO A C m (fun x => bindO B C (f x) g).

intros A B C m a f g.

induction m.
unfold bindO.
reflexivity.

unfold bindO.
reflexivity.
Qed.

End MaybeMonad.


I reiterate my statement that Coq is the best computer game I've ever played.

Powered by ScribeFire.

Arrows?

Gwern Branwen replied to my announcement of the still-incomplete Software Tools in Haskell on the haskell-cafe mailing list with a neat article describing run-length-decoding, which included a pointer to another article in Don Stewart's blog on Arrows and RLE in Haskell.

Don has the following encoding function:

encode = map (length &&& head) . group

which, of course, implies that computing the average of a list of numbers would be:

uncurry (/) . (sum &&& fromIntegral . length)

Arrows are weird.

(Don't forget to include Control.Arrow, by the way.)