In Idris, what's the type of a list of lists of doubles, where all the lengths are known?

Question

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.

András Kovács András Kovács · Accepted Answer · 2018-09-21T19:41:09

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)

In Idris, what's the type of a list of lists of doubles, where all the lengths are known?

1 Answers