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

David Menendez wrote:

data SomeNat where SomeNat :: (Nat n) => n -> SomeNat toPeano :: Int -> SomeNat

or, equivalently, by using a higher-order function.

toPeano :: Int -> (forall n. Nat n => n -> t) -> t

Nice! I thought the only way to create them was with a new datatype, but this works too. I guess the nontrivial bit to think of is the introduction of a fresh type (t in this case). Thanks for this insight! Martijn.