Fixed point of n-mutually recursive functors
Wed, 22 May 2002 15:50:12 +0200 (CEST)
Content-Type: text/plain; charset=us-ascii
> I don't think this is possible in plain Haskell 98.
> It is possible in Generic Haskell, see:
> 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