An example value: [[1, 2], [1]]
Here, I would know that there are 2 lists, and that the first list has length 2, while the second one has length 1. Ideally, this function would compute those types:
func : (n ** Vect n Nat) -> Type
But I don't know how to write it. I'm pretty sure it's something to do with dependent pairs, but I'm not sure how to write it.
To clarify, I know it'd be possible to simply use (n ** Vect n (p ** Vect p Double)) as the type of the example value. However, n only constrains the number of lists, not the number of their elements, because inside the list, p could be anything. I would most likely need something where the first element of the dependent pair is a vector of lengths, not just the number of lists. So something like (Vect n Nat ** Vect n (Vect m Double))--where each m is the corresponding element of the first vector.
You could define a new vector type which contains possibly differently indexed elements of an indexed type at each position:
import Prelude
import Data.Vect
-- heterogeneously indexed vector
data IVect : Vect n ix -> (ix -> Type) -> Type where
Nil : IVect Nil b
(::) : b i -> IVect is b -> IVect (i :: is) b
-- of which a special case is a vector of vectors
VVect : Vect n Nat -> Type -> Type
VVect is a = IVect is (flip Vect a)
test1 : VVect [2, 2, 2] Nat
test1 = [[1, 2], [3, 4], [5, 6]]
test2 : VVect [0, 1, 2] Bool
test2 = [[], [True], [False, True]]
Alternatively, you can define VVect using dependent pairs and map, but this is more cumbersome to use:
VVect' : Vect n Nat -> Type -> Type
VVect' {n = n} is a = (xs : Vect n (m ** Vect m a) ** (map fst xs = is))
test3 : VVect' [0, 1, 2] Bool
test3 = ([(_ ** []), (_ ** [True]), (_ ** [False, False])] ** Refl)
You have some choice though whether to use lists or vectors. With lists as the inner container, values look more compact:
VVect'' : Vect n Nat -> Type -> Type
VVect'' {n = n} is a = (xs : Vect n (List a) ** (map length xs = is))
test4 : VVect'' [0, 1, 2] Bool
test4 = ([[], [True], [False, True]] ** Refl)