[Haskell-cafe] Re: How to convert a list to a vector encoding its
length in its type?
jwlato at gmail.com
Fri Aug 21 18:57:14 EDT 2009
> 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 ,
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  has a
tutorial on using type-level vectors, which I found helpful when faced
with the same problem recently , .
More information about the Haskell-Cafe