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