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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe