> From: David Menendez <d...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe