The Coq mailing list

[Yongji Li <dragonlyj AT gmail.com>]

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