Moving on to the implementation of fixed-sized vectors themselves ... I have been trying to implement them as a GADT but I have run into quite few problems. As a result, I'm considering to implement them using the more-traditional phantom type-parameter approach. Anyhow, I'd like to share those problems with the list, just in case someone comes with a solution. Here are some examples of what I was able to define without problems (although, for some cases, I was forced to "break" the safety layer of the GADT by using the toInt reflection function). Save this email as FSVec.lhs to test them.
{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, KindSignatures #-} module Data.Param.FSVec where
import Data.TypeLevel.Num
The Fixed Sized Vector data type. I know Wolfgang would prefer something more closely named to LiSt to, but let's avoid getting into that discussion now.
data FSVec :: * -> * -> * where NullV :: FSVec D0 a (:>) :: Succ s s' => a -> FSVec s a -> FSVec s' a
infixr :>
Some successful examples
headV :: Pos s => FSVec s a -> a headV (x :> xs) = x
lastV :: Pos s => FSVec s a -> a lastV = lastV' -- trusted function without the Pos constraint, otherwise the compiler would complain about -- the Succ constraint of :> not being met. where lastV' :: FSVec s a -> a lastV' (x :> NullV) = x lastV' (x :> xs) = lastV' xs
atV :: (Pos s, Nat n, n :<: s) => FSVec s a -> n -> a atV v n = atV' v (toInt n) -- Reflecting the index breaks checking that the recursive call -- verifies the atV constraints, however I couldn't find another way. -- atV' is to be trusted regarding the recursive call where atV' :: FSVec s a -> Int -> a atV' (x :> xs) n | n == 0 = x | otherwise = atV' xs (n-1) -- this defition is nicer but doesn't typecheck -- atV (x :> xs) n -- | toInt n == 0 = x -- | otherwise = atV xs (predRef n)
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) Tail function, which is also incorrect. tailV :: Succ s' s => FSVec s a -> FSVec s' a tailV (x :> xs) = xs 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. Another alternative would be forcing the user to provide the size explicitly (which is ugly as well) vector' :: Nat s => s -> [a] -> FSVec s a The Succ constraint in the definition of :> doesn't allow me to do such a thing. The following implementation does not typecheck: vector' :: Nat s => s -> [a] -> FSVec s a vector' s l | toInt s == length l = vector' l | otherwise = error "dynamic/static size mismatch" where vector'' :: [a] -> FSVec s a vector'' [] = NullV vector'' (x : xs) = x :> vector' xs The problem is that I don't know a way in which to "bypass" the Succ constraint of :> . Using a traditional phantom type-parameter to express the size is the only solution I can think of (which would also solve the problems of init and tail). However, that would mean losing the ability of pattern matching with (:>). Any comments/suggestions would be very much appreciated. Cheers, Fons [1] http://ofb.net/~frederik/vectro/draft-r2.pdf