[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[David Menendez]

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
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 at zednenem.com>
<http://www.eyrie.org/~zednenem/>