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

Luke Palmer lrpalmer at gmail.com
Mon Jun 23 04:05:33 EDT 2008


On Mon, Jun 23, 2008 at 6:50 AM, Harald ROTTER <harald.rotter at sagem.com> wrote:
> Hello,
>
> sorry for the late answer, I was off for the weekend :-)
>
> The paper "Number-parameterized types" by Oleg Kielyov is located at
>
>      http://okmij.org/ftp/papers/number-parameterized-types.pdf
>
> It impressively shows what one can do with Haskell's type system.
> What I am after is the replacement of a "chain" of digits, like e.g.
>      D1 $ D0 $ D0 $ Sz
> by a list
>      [D1,D0,D0]
> so I can effectively use list operations on those "typed numbers". 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.

Luke


More information about the Haskell-Cafe mailing list