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

[Jason Dagit]

For some reason I never saw David's reply to my email.

On Fri, Aug 21, 2009 at 11:16 AM, Daniel Peebles<pumpkingod at gmail.com> 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<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

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