[Haskell-cafe] Re: number-parameterized types and heterogeneous lists

[oleg at okmij.org]

Luke Palmer wrote in response to Harald ROTTER
> > I also wonder if there is some kind of "generalized" foldr such that, e.g.
> >      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
> > I think that this foldr must be some "special" foldr that augments the data
> > type of the result in each foldr step.
> > Would this be possible or am I just chasing phantoms ?

> Mostly I believe you are.  What you are describing is firmly in the
> realm of dependent types, far beyond Haskell's type system. See
> Epigram or Agda for languages which have attempted to tackle this
> problem.

First of all, Haskell (as implemented by released versions of GHC for
at least two years) already permits dependent types, in the
strict sense of a type of an expression being determined by the value
of one argument of that expression:

	http://okmij.org/ftp/Computation/tagless-typed.html#tc-GADT-tc

Second, (values of) types like D0 and D1 can be collected in a
heterogenous list (HList), which does have the corresponding fold
operator, called HFoldr in

	http://darcs.haskell.org/HList/Data/HList/HListPrelude.hs