Fixed point of n-mutually recursive functors

Johan Jeuring johanj@cs.uu.nl
Wed, 22 May 2002 07:56:27 +0200


> I can also define the fixed-point of 2 mutually recursive bifunctors =
as:
>
>> 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:

http://www.generic-haskell.org/

or

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
150-206,1999.

-- Johan Jeuring