[Haskell-cafe] Re: How to convert a list to a vector encoding its length in its type?

[John Lato]

> From: David Menendez <dave at zednenem.com>
>
> or, equivalently, by using a higher-order function.
>
>    toPeano :: Int -> (forall n. Nat n => n -> t) -> t
>

Incidentally, this is the approach used in the type-level library [1],
which provides the function:

  reifyIntegral :: Integral i => i -> (forall n. Nat n => n -> r) -> r

The docs describe this as "In CPS style (best possible solution),"
although I didn't see any reference for that assertion.

Bas, if you'd like some examples, the ForSyDe project [2] has a
tutorial on using type-level vectors, which I found helpful when faced
with the same problem recently [3], [4].

Cheers,
John Lato

[1] http://hackage.haskell.org/package/type-level
[2] http://www.ict.kth.se/forsyde/files/tutorial/apa.html
[3] http://inmachina.net/~jwlato/haskell/iter-audio/src/Sound/Iteratee/Channelized.hs
[4] http://inmachina.net/~jwlato/haskell/iter-audio/examples/channelized_reader.hs