KnownNat-indexed vectors

There’s also approach from fixed-vector. It works with Church-encoded products. For example ordinary haskell data type data V2 a = V2 a a is isomorphic to: newtype Church2 a = Church2 (forall r. (a -> a -> r) -> r) inspect :: V2 a -> Church2 a inspect (V2 x y) = Church2 $ \f -> f x y construct :: Church2 a -> V2 a construct (Church2 f) = f V2 next trick is notice that it’s possible to define N-dimensional Church vectors inductively. But one has to define standard Peano numerals since type level naturals don’t support induction. data Nat = Z | S Nat type family Fn n a b where Fn Z a b = b Fn (S n) a b = a -> Fn n a b newtype Fun n a b = Fun (Fn n a b) newtype Church n a = Church (forall r. Fun n a r -> r) Then it’s possible to define all operations on Church encoded vectors. And single missing piece is to define type class that establish isomorphism between Church encoding and whatever representation one wants to use. Naturally this approach only works with small vectors. It is possible to define vector that are generic in length.