coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- To: frank maltman <frank.maltman AT googlemail.com>
- Cc: <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "Transparent" module types, ala O'Caml?
- Date: Mon, 6 Jun 2011 10:04:23 +0200
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.
- [Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?,
Mathieu Boespflug
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, AUGER Cedric
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, Damien Pous
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?,
Mathieu Boespflug
Archive powered by MhonArc 2.6.16.