Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to define the free monad generated by a functor?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to define the free monad generated by a functor?


chronological Thread 
  • 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 where
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)
   I want to define it in such a way that the induction principle for free monad is available, how am I supposed to do?
  

Many thanks
--
Best regards


                               Li Yong-ji              



Archive powered by MhonArc 2.6.16.

Top of Page