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 FSVec type using Haskell plus a few GHC extensions.