Fixed point of n-mutually recursive functors

[gonflores@guay.com]

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

> I don't think this is possible in plain Haskell 98. 
> It is possible in Generic Haskell, see: 
> http://www.generic-haskell.org/ 
> [...]
> Generic Haskell's type system is sufficient. 
> 
> Is it possible using dependent types? 
>
> I would expect so. 

I have been looking to Generic Haskell and it may be possible to define a generic map function like:

mapN :: (a1 -> b1) -> ... -> (aN -> bN) -> f a1 ... aN -> f b1 ... bN

However, I still don't know how could I define something like:

> data FixN1 f1 ... fN = InN1 (f1 (FixN1 f1 ... fN) ... (FixNN f1 ... fN)) 
> ... 
> data FixNN f1 ... fN = InNN (fN (FixN1 f1 ... fN) ... (FixNN f1 ... fN)) 

I think that I would need dependent types, because I want to define a number of data types that depend on a given natural...any suggestions?

Best regards, Gonzalo Flores
------=_Part_3676_5539854.1022075412963--