The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

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)?