mixphix:
Are there libraries where this kind of vector has been implemented?
There exist several packages that define a family of finite types indexed by type-level naturals, e.g. finite-typelits, data-fin, fin-int or fin. For each natural number n, there is a type Finite n that has exactly n elements. Then you can define
newtype V n x = V (Finite n -> x)
and derive a lot of…
