The Coq mailing list

[Andre.HIRSCHOWITZ AT unice.fr]

Hello Conor,

Thanks for your nice contribution which perfectly illustrated what I 
meant by a clever answer. Fortunately unclever questions and answers are 
still welcome on this list.
BTW, I also enjoy your address.

> 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).
Marco and I have recently revisited a proposal of Matthes-Uustalu about 
such a
"signature of operations and laws your F COULD come packaged
with". More precisely, they (and we) start from a higher-order functor
F : (Type ->Type )-> (Type->Type).
Hence we are certainly interested in your thoughts.

andré