On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit<dagit@codersbase.com> wrote:
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 <dave@zednenem.com> <http://www.eyrie.org/~zednenem/>