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