From: David Menendez
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/Channeliz... [4] http://inmachina.net/~jwlato/haskell/iter-audio/examples/channelized_reader....