[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
dave at zednenem.com
Fri Aug 21 14:03:17 EDT 2009
On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit<dagit at 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
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 at zednenem.com>
More information about the Haskell-Cafe