coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yongji Li <dragonlyj AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] How to define the free monad generated by a functor?
- Date: Mon, 2 Mar 2009 11:33:47 +0800
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=aaAMF1Mg9d/z6D6U6bNewwmRNr8fisnWnK9y4pIshbFkbr3GWb3eQHziflovNuanU/ bO1zJIQmaZNKDFIgdOoQfN/nEU4UxOpHfettgJdW4sY7OTD78gArJ+cjPdsfUsISjMAP pIQbFARRJ4ycbGLBGTAA6DLxs+qs6pDsicP64=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear all:
When I try to define the free monad generated by a functor F:Type->Type (ignoring the mapping of morphisms), the following definition is rejected by Coq:
Inductive FreeMonad (F:Type->Type)(X:Type): Type:=
| eta: X -> FreeMonad F X
| mu: F (FreeMonad F X) -> FreeMonad F X.
Error: Non strictly positive occurrence of "FreeMonad" in
"F (FreeMonad F X) -> FreeMonad F X".
I don't understand that why positive condition rejects such a definition. I have searched in google and found no hints at all. But it seems that a similar definition is accepted in Haskell:
data FreeM (e : Set -> Set) (a : Set) : Set whereI want to define it in such a way that the induction principle for free monad is available, how am I supposed to do?
return : a -> FreeM e a
effect : e (FreeM e a) -> FreeM e a
(obtained from FP lunch: http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=89)
Many thanks
--
Best regards
Li Yong-ji
- [Coq-Club] How to define the free monad generated by a functor?, Yongji Li
- Re: [Coq-Club] How to define the free monad generated by a functor?, Andre . HIRSCHOWITZ
- Re: [Coq-Club] How to define the free monad generated by a functor?,
Conor McBride
- Re: [Coq-Club] How to define the free monad generated by a functor?, Andre . HIRSCHOWITZ
Archive powered by MhonArc 2.6.16.