The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sun, 5 Jun 2011 20:33:10 +0000,
frank maltman 
<frank.maltman AT googlemail.com>
 a écrit :

> Hello.
> 
> I've written a simple monad module type and an implementation using
> 'option' but have come up against an issue when trying to actually
> use the module:
> 
> --
> 
> Module Type Base.
>   Parameter M : Type -> Type.
> 
>   Parameter monad_bind   : forall {A B : Type}, M A -> (A -> M B) ->
> M B. Parameter monad_return : forall {A : Type}, A -> M A.
> 
>   Parameter monad_left_identity : forall (A B : Type) (x : A) (f : A
> -> M B), monad_bind (monad_return x) f = f x.
> 
>   Parameter monad_right_identity : forall (A : Type) (m : M A),
>     monad_bind m monad_return = m.
>   
>   Parameter monad_associativity : forall (A B C : Type) (f : A -> M
> B) (g : B -> M C) (m : M A), monad_bind (monad_bind m f) g =
> monad_bind m (fun z => monad_bind (f z) g). End Base.
> 
> Module Monad_Option : Base.
>   Definition M := option.
> 
>   Definition monad_bind {A B : Type} (m : option A) (f : A -> option
> B) : option B := match m with
>       | Some x => f x
>       | None   => None
>     end.
> 
>   Definition monad_return {A : Type} (x : A) : option A := Some x.
> 
>   Definition monad_left_identity : forall (A B : Type) (x : A) (f : A
> -> option B), monad_bind (monad_return x) f = f x.
>   Proof.
>     intros A B x f.
>     reflexivity.
>   Defined.
> 
>   Definition monad_right_identity : forall (A : Type) (m : option A),
>     monad_bind m monad_return = m.
>   Proof.
>     intros A m.
>     destruct m as [|m'].
>     reflexivity.
>     reflexivity.
>   Defined.
> 
>   Definition monad_associativity : forall {A B C : Type} (f : A ->
> option B) (g : B -> option C) (m : option A), monad_bind (monad_bind
> m f) g = monad_bind m (fun z => monad_bind (f z) g). Proof.
>     intros A B C f g m.
>     destruct m as [|m'].
>     reflexivity.
>     reflexivity.
>   Defined.
> End Monad_Option.
> 
> --
> 
> > Check Monad_Option.monad_bind (Some 1).
> >                                ^^^^^^
> Error: The term "Some 1" has type "option nat"
>  while it is expected to have type "Monad_Option.M ?68".
> 
> I believe the problem is that Monad_Option.M is considered a distinct
> type from 'option'. I think I may need to add something in the same
> manner as I would in O'Caml (unless I'm mistaken):
> 
> module Base : Monad.Base with type 'a monad = 'a option = ...
> 
> Does coq have something similar (or am I looking at a different
> problem entirely)?

If I am not mistaken, you should have RTFM, since this part has a
correct documentation unlike many coq features.

Module Monad_option: Base
with Definition M := option.
…
End Monad_option.

should have done the trick in the OCaml way.

In a way it is better than the <:, since it abstracts exactly the parts
you want.