[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
Martijn van Steenbergen
martijn at van.steenbergen.nl
Tue Aug 25 14:45:42 EDT 2009
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!
More information about the Haskell-Cafe