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

[Daniel Peebles]

Just to expand on David's higher-order function for the original
Vector type, we can do:

data AnyVec a where
  AnyVec :: Vec a n -> AnyVec a

listToVec :: [a] -> AnyVec a
listToVec = worker AnyVec

worker :: (forall n. Nat n => Vec a n -> t) -> [a] -> t
worker f [] = f Nil
worker f (x:xs) = worker (f . (Cons x)) xs

and have it behave as you'd expect. Note that in a sense this is
"forgetful" of the original length of the list.

Dan

On Fri, Aug 21, 2009 at 2:03 PM, David Menendez<dave at zednenem.com> wrote:
> 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/>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>