Fixed point of n-mutually recursive functors
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
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?
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 Backhouse, J.N. Oliveira, editors, Proceedings of the Fifth International Conference on Mathematics of Program Construction (MPC 2000), Ponte de Lima, Portugal, July 3-5, 2000, © 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 Implementing Combinator Languages, In: Advanced Functional Programming, Third International School, AFP'98, Springer-Verlag, LNCS 1608, 150-206,1999. -- Johan Jeuring
participants (2)
-
gonflores＠guay.com -
Johan Jeuring