The Coq mailing list

["Igor Zhirkov" <igorjirkov AT gmail.com>]

Hello, 

I wonder whether it is possible to define the Mu  combinator in Coq in a general way. 

In Haskell it can be defined like that: 

>>>

newtype Fix f = Fx (f (Fix f ) )

<<<

Or like that (using records syntax):

>>>

newtype Mu f = In {out :: f (Mu f)}

<<<

When translated directly into Coq it fails with "Non strictly positive occurrence of Mu":

>>>

Inductive Mu f := MIn {MOut: f ( Mu f) }.   

<<<

Maybe I need to throw in some axioms to work around the termination issues?

It seems, however, that for an arbitrary recursive type one can always write a definition that corresponds to the Mu application to the corresponding functor:

>>>

Inductive exprf a :=

| add : a -> a -> exprf a

| lit: nat -> exprf a.

Inductive expr := In { Out: exprf expr }.

<<<

While doing a little research I have only stepped on the work of Arthur Chargueraud  (A Practical Fixed Point Combinator for Type Theory), but it does not seem to me that it is relevant.

What I am trying to achieve is the separation of the recursion schema and the computable part (algebra) for catamorphisms and anamorphisms.

BR

Igor