Heterogenous sized vectors where the types "work elsewhere"

Question

Suppose I have a function that works on a vector with size known at compile-time (these are provided by the vector-sized package):

{-# LANGUAGE DataKinds, GADTs #-}
module Test where
import Data.Vector.Sized

-- Processes vectors known at compile time to have size 4.
processVector :: Vector 4 Int -> String
processVector = undefined

Fine, but what if I don't want to process vector of ints, but a vector of vectors?

-- Same thing but has subvectors of size 3.
processVector2 :: Vector 4 (Vector 3 Int) -> String
processVector2 = undefined

Fine, but there each sub-vector is of a fixed size. I want a function where the subvectors can each be of a different size but still known at compile time.

We can do this with existential quantifications:

data InnerVector = forall n. InnerVector (Vector n Int)
processVector3 :: Vector 4 InnerVector -> String
processVector3 = undefined

Fine, but what if I want to return not a String but a vector of the same dimensions?

processVector4 :: Vector 4 InnerVector -> Vector 4 InnerVector
processVector4 = undefined

This does not work because the second vector might have differently sized subvectors from the input subvectors! I want them known to be same at compile time. (So the subvectors at index 0 have same size, subvectors at index 1 have the same size, and so on.)

Is this possible to achieve? If not, do you know of (or can you create) a data structure that makes this possible?

I am avoiding tuples because:

• My vectors will have size over 100.
• Vectors make general processing easy (using 0-based indexes), so my processing functions continue to work even if I add more items to my vector.
• I do indeed only want values of one type within the inner vectors (Int in the example).

Answer 1

By using existential quantification you effectively hide the sizes of the inner vectors. But if you want to write code with types that convey that you are preserving those sizes, you don't want them hidden. Instead you want your types to be loud and clear about them.

So, let's define some types that broadcast these inner sizes. Essentially, you need your "vector-of-vectors" type to be a type of heterogenous lists that restricts the elements of these lists to be vectors. For sure, there are some libraries out there that can help you put together such a type, but here we'll roll our own. Just because it's more fun to do so.

Let's start with enabling some language extensions and then writing some types for the inner vectors and their sizes:

{-# LANGUAGE DataKinds, GADTs, InstanceSigs, KindSignatures, TypeOperators #-}

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
  VNil  :: Vector Zero a
  VCons :: a -> Vector n a -> Vector (Succ n) a

instance Functor (Vector n) where
  fmap f VNil         = VNil
  fmap f (VCons x xs) = VCons (f x) (fmap f xs)

Next up is our type of "jagged" matrices (i.e., a vector of variable-size vectors). As said, this is just a specific type of heterogeneous lists:

data JaggedMatrix :: [Nat] -> * -> * where
  MNil  :: JaggedMatrix '[] a
  MCons :: Vector n a -> JaggedMatrix ns a -> JaggedMatrix (n : ns) a

There, that's it. The type of jagged matrices is indexed by a list that contains the sizes of the inner vectors. The outer dimension is not explicated in the type, but can simply be derived from the length of the inner-dimensions list.

Let's put it to work and write a dimensions-preservering function. Here's an obvious one:

instance Functor (JaggedMatrix ns) where
  fmap :: (a -> b) -> JaggedMatrix ns a -> JaggedMatrix ns b
  fmap f MNil           = MNil
  fmap f (MCons xs xss) = MCons (fmap f xs) (fmap f xss)