On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit<da...@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 <d...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
