The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Yongji

(Hi Andre -- sorry, yours is another beast entirely...)

On 2 Mar 2009, at 03:33, Yongji Li wrote:

> 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.

Are you sure you should call that mu? Is it the multiplication?

> Error: Non strictly positive occurrence of "FreeMonad" in
> "F (FreeMonad F X) -> FreeMonad F X".

And so it should be. Are all *functions* F from type to type
functors in the sense you mean?

>   I don't understand that why positive condition rejects such a  
> definition. I have searched in google and found no hints at all.

Consider F X = X -> X, and you get a classic example of a
datatype which causes problems.

> 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)

Sure, but Haskell has lower standards. It certainly permits
datatypes which have no induction principles.

>   I want to define it in such a way that the induction principle for  
> free monad is available,
Can you at least state this induction principle? I suspect
you may find this hard without knowing more about F.

> how am I supposed to do?
There are lots of things you might do. The simplest is to
exploit the fact that every strictly positive functor can be
expressed (up to isomorphism) in *container form*. You could
try this (a minor variation on the W-type)

> Inductive FreeMonad (C:Type)(R : C -> Type)(X:Type): Type:=
>          | ret: X -> FreeMonad C R X
>          | eff: forall c:C, R c -> FreeMonad C R X.


This presents the traces of effectful programs as trees where
each node issues a command c from signature C and receives a
suitable response in R c. For more on this way of looking at
interaction, see papers by Peter Hancock, Anton Setzer, and
others.

A more expensive, but perhaps more rewarding approach is to
define a *universe* of strictly positive functors, interpreted
via an inductive family. You can read more about this approach
in papers by Peter Morris and colleagues.

Both of these provide ways to workaround the positivity
criterion. (What is the positivity criterion these days?)
However, it would be nice in the long run if we could replace
the positivity criterion with a more semantic criterion --- a
signature of operations and laws your F should come packaged
with to qualify as strictly positive, the way in Haskell you
need to know Functor e to show Monad (FreeM e). Then we could
replace positivity checking by type checking. I do not know
what the whole of this signature should be (but I'm trying to
find out). I know at least some of it: F should come with

 F_Everywhere : forall X:Type, (X -> Type) -> (F X -> Type)
 F_everywhere : forall X:Type, forall P : X -> Type,
                (forall x:X, P x) ->
                (forall xs : F X, F_Everywhere P xs)

These two allow you to state the induction principle you need
and equip it with operational behaviour. More on "Everywhere"
and its little friend "Somewhere" in Peter Morris's thesis,
and several other places, if only I could remember.

So there you have it:
 (1) a reason why Coq is right to reject your definition
 (2) some suggestions for workarounds
 (3) some reason to believe that your original intuition
       was a good one, and that it should be reflected by
       a more type-based criterion in the future

Hope this helps.

All the best

Conor