Fixed point of n-mutually recursive functors

Johan Jeuring
Wed, 22 May 2002 07:56:27 +0200

> I can also define the fixed-point of 2 mutually recursive bifunctors =
>> data Fix21 f g =3D In21 (f (Fix21 f g) (Fix22 f g))
>> data Fix22 f g =3D 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?

I don't think this is possible in plain Haskell 98.

It is possible in Generic Haskell, see:


Ralf Hinze. Polytypic values possess polykinded types. In Roland=20
Backhouse, J.N. Oliveira, editors, Proceedings of the Fifth=20
International Conference on Mathematics of Program Construction (MPC=20
2000), Ponte de Lima, Portugal, July 3-5, 2000, =A9 Springer-Verlag.

> If it isn't, what kind of type system would I need?

Generic Haskell's type system is sufficient.

> Is it possible using dependent types?

I would expect so.

A pointer to mutually recursive cata's (and functors):

Swierstra, S.D. and Azero Alcocer, P.R. and Saraiava, J., Designing and=20=

Implementing Combinator Languages, In: Advanced Functional Programming,=20=

Third International School, AFP'98, Springer-Verlag, LNCS 1608,=20

-- Johan Jeuring