We would like to numerically parameterize vectors using their
length in order to implement fixed-sized vectors
FSVec). Ideally, we would like to be able to
implement something similar to this:
v :: FSVec 23 Int -- Not Haskell
v would be a a vector containing 23
Ints. Note it
is not possible to directly do this in Haskell.
The vector concatenation function would be something along the lines of:
(++) :: FSVec s1 a -> FSVec s2 a -> FSVec (s1+s2) a -- Again, not valid Haskell
We would also like to establish static security constraints on functions. Those constrains would be checked at compile time guaranteeing a correct behaviour during runtime. For instance.
head :: FSVec (s > 0) a -> FSVec (s - 1) a -- Not Haskell
However, Haskell does not support dependent types (a numerically
parameterized-vector is in practice a dependent type) nor type-level
lambdas directly. Yet, it is still possible to implement our
type using Haskell plus a few GHC extensions.