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

For some reason I never saw David's reply to my email. On Fri, Aug 21, 2009 at 11:16 AM, Daniel Peebles wrote:

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.

Isn't this the case every time you open open up the AnyVector type? The only way you can use the vector's size is when you want to do something that works with all sizes unless you're willing to walk the vector back to Nil? For example, if you started with two equal size vectors, wrap them in an AnyVector, then pass them off to a function that can append them, the type system won't know that you have a vector which is twice the original size.

Dan

On Fri, Aug 21, 2009 at 2:03 PM, David Menendez wrote:

...

On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit 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

Yes, that's exactly what I meant by my verbage above :) Guess I should have explicitly used the forall/exists terminology.

...

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

Okay, that's what we did with AnyVector. What I don't understand is how you'll actually use this. Once you create SomeNat, the type system no longer remembers which Nat. So to me, you're back where you started.

...

or, equivalently, by using a higher-order function.

   toPeano :: Int -> (forall n. Nat n => n -> t) -> t

This looks a bit more promising. For those unfamiliar with this form, it is the logical "negation" of the previous type. One description is here [1], where it is mentioned that the type of t cannot depend on n. So you could not for example, return Vector a n or do, "toPeano 5 id". I guess you end up writing your program inside out in a sense which is fine, but then how do you address the forgetfulness? Everything has to be inside one scope where you never wrap things in an existential type? Perhaps via the negated existential encoding your last version of toPeano? I have a hard time wrapping my head around it at this point. Jason [1] http://www.ofb.net/~frederik/vectro/draft-r2.pdf