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

[Alfonso Acosta]

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