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

[Wolfgang Jeltsch]

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 
on <http://www.haskell.org/pipermail/haskell/2007-September/019757.html> and 
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