On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit
Even with a type class for our type level numbers I'm at a loss. I just don't understand how to convert an arbitrary int into an arbitrary but fixed type. Perhaps someone else on the list knows. I would like to know, if it's possible, how to do it.
toPeano :: Nat n => Int -> n
The problem is that the parameter, n, is part of the input to toPeano,
but you need it to be part of the output. To rephrase slightly, you
have
toPeano :: forall n. (Nat n) => Int -> n
but you need,
toPeano :: Int -> exists n. (Nat n) => n
which states that toPeano determines the type of its return value. In
Haskell, you can encode this with an existential data type,
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
--
Dave Menendez