Fixed point of n-mutually recursive functors
Wed, 22 May 2002 00:01:56 +0200 (CEST)

Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

I am able to define the fixed point of a functor as

> data Fix f = In (f (Fix f))

where I can also define the type class

> class Functor1 f  
>   where map1 :: (a -> b) -> f a -> f b

I can also define the fixed-point of 2 mutually recursive bifunctors as:

> data Fix21 f g = In21 (f (Fix21 f g) (Fix22 f g))
> data Fix22 f g = In22 (g (Fix21 f g) (Fix22 f g))

where bifunctors can be captured in the type class 

> class Functor2 f 
>  where map2 :: (a1 -> b1) -> (a2 -> b2) -> f a1 a2 -> f b1 b2

Now, I would like to generalize those definitions to n-functors. 

Is it possible?
If it isn't, what kind of type system would I need? 
Is it possible using dependent types?

I would also appreciate any points to literature using n-mutually recursive functors.

Best regards, Gonzalo Flores