[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Dan Licata]

> > And finally, vector, which is supposed to build a fixed-sized vector
> > out of a list.
> >
> > The ideal type for the function would be:
> >
> > vector :: [a] -> FSVec s a
> >
> > But there is no apparent way in which to obtain s based on the length
> > of the input list.
> >
> > [1] shows a way in which to create vector using CPS style and a
> > reification function:
> >
> > reifyInt :: Int -> (forall s . Nat s => FSVect s a -> w) -> w
> >
> > The result would be a function with the following type:
> >
> > vector :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w
> >
> > Nevertheless, I'm not fully satisfied by it.
> 
> I suppose, it’s the best we can get without having dependent types.  Others 
> might correct me.

The type 

vector :: [a] -> FSVec s a

doesn't make sense here: because s is universally quantified at the
outside, this says "for all lengths s, given a list, I can produce a
vector of length s".

And indeed, in the second version, it looks like you're using the
continuation to curry an existential:

vector :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w

is the same as

vector :: [a] -> ((exists s . Nat s and FSVec s a) -> w) -> w

So why not just do

vector :: [a] -> (exists s . Nat s and FSVec s a)

I.e.

data UnknownLengthVec a where
  U :: Nat s => FsVec s a -> UnknownLengthVec a

vector :: [a] -> UnknownLengthVec a

I haven't tried, but I'd be surprised if you couldn't write this
function by recuring on the list.

Of course, this type does not relate the size of the vector to the
output of the length function on lists; it just says you get a vector
some size.  But maybe that's good enough for many uses?

-Dan