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

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Sun Feb 10 11:43:40 EST 2008

```Am Sonntag, 10. Februar 2008 05:14 schrieben Sie:
> […]

> Now some functions which I wasn't able to define
>
> Concat function. This would be the naive implementation, but it fails
> to compile.
>
> (<+>) :: Add s1 s2 s3 => FSVec s1 a -> FSVec s2 a -> FSVec s3 a
> NullV  <+> ys  = ys
> (x:>xs) <+> ys = x :> (xs <+> ys)

Hmm, we would have to find a way to implement lemmas.  In this case, the lemma
that succ (x + y) = succ x + y.  At the moment, I’ve no good idea how to do
that.

> Tail function, which is also incorrect.
>
> tailV :: Succ s' s => FSVec s a -> FSVec s' a
> tailV (x :> xs) = xs

Maybe this problem is similar to the one I came across earlier.  See my mail
the replies to it.

> 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.

> […]

Some remark concerning spelling: Would it be possible to drop the V at the end
of the function names?  I think the fact that those functions are
about “vectors” is better expressed by qualification:

import Data.List as List
import Data.TypeLevel.Vector as Vector

-- Usage: Vector.last, List.last, …

Compare this to the functions in Data.Map, Data.Set, etc.  They also use
insert, etc. instead of insertM, insertS, etc.  Note that the latter would
quickly lead to ambiguities because insertM would stand for map insertion as
well as for multiset insertion.  Similar with sets and sequences.

Best wishes,
Wolfgang
```