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