Fixed point of n-mutually recursive functors
gonflores@guay.com
gonflores@guay.com
Wed, 22 May 2002 00:01:56 +0200 (CEST)
------=_Part_3605_7651686.1022018516599
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
------=_Part_3605_7651686.1022018516599--