Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Instantiate a parameter of a module type with an inductive type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Instantiate a parameter of a module type with an inductive type


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page