coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Helmut Brandl <helmut.brandl AT gmx.net>
- To: Coq-Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Instantiate a parameter of a module type with an inductive type
- Date: Mon, 11 Sep 2017 14:36:46 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
- Ironport-phdr: 9a23:LL/4Px8uINOQkf9uRHKM819IXTAuvvDOBiVQ1KB+2uMcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS46tL2HV91a19Hs5Hgj1fV5+If2wEYrPhey20fqz8tvdeVMbvjelZaJOK0C2oAHUq9VQi5FrLKo14hTMsj1OdvgF63lvIAezkhL5+9v41oRq9ShU86Yh+spFTLm8db4xS7BcJDsjIyYz6dG95kqLdheG+nZJCjZeqRFPGQWQtBw=
Dear list,
I have the following module types
Module Type MONAD.
Parameter t: Type -> Type.
Parameter apply: forall A B:Type, (A->B) -> t A -> t B.
Parameter map: forall A B:Type, (A->B) -> t A -> t B.
Parameter bind: forall A B:Type, t A -> (A -> t B) -> t B.
End MONAD.
Module Type MONAD0.
Parameter t: Type -> Type.
Parameter make: forall A:Type, A -> t A.
Parameter bind: forall A B:Type, t A -> (A -> t B) -> t B.
End MONAD0.
and the module functor
Module Monad_of (M:MONAD0).
Definition t := M.t.
Definition bind := M.bind.
Definition make := M.make.
Arguments bind {A} {B} _ _.
Arguments make {A} _.
Definition map {A B:Type} (f:A->B) (m:t A): t B :=
bind m (fun a => make (f a)).
Definition apply {A B:Type} (f: t (A->B)) (m: t A): t B :=
bind f (fun f0 => map f0 m).
End Monad_of.
I wanted to use the following module as a module argument for the previous functor
Module Option.
Inductive t (A:Type) :=
| None: t A
| Some: A -> t A.
Check t.
Arguments None {A}.
Arguments Some {A} _.
Definition make {A:Type} (a:A): t A :=
Some a.
Definition bind {A:Type} (m:t A) (f:A->t A): t A :=
match m with
| None =>
None
| Some v =>
f v
end.
Check make.
End Option.
Module Option1 := Monad_of(Option).
With the last line the compiler complains with the message "The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name."
Can anybody help me to understand this error message and give me a hint on how to fix this problem?
Thanks
Helmut
- [Coq-Club] Instantiate a parameter of a module type with an inductive type, Helmut Brandl, 09/11/2017
- Re: [Coq-Club] Instantiate a parameter of a module type with an inductive type, Frédéric Besson, 09/12/2017
Archive powered by MHonArc 2.6.18.