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 `Int`

s. 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 `FSVec`

type using Haskell plus a few GHC extensions.