The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

Hi Frank,

changing

> Module Monad_Option : Base.

to

> Module Monad_Option <: Base.

does the trick. The former masks the computational content of the
module, while the latter just asks Coq to check that the signature of
Monad_Option is a subtype of the signature Base.

Regards,

-- Mathieu


On Sun, Jun 05, 2011 at 08:33:10PM +0000, frank maltman wrote:
> 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)?