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