Dependent Types: Vector Vectors

Question

I am new to dependent types (I try Idris and Kok, despite their big differences).

I am trying to express the following type: a given type T and a sequence k nats n1, n2, ... nk, a type consisting of k sequences T with length n1, n2, ... nk, respectively.

That is, the vector of k vectors whose lengths are specified by the parameter. Is it possible?

Answer 1

You can do this with a heterogeneous list, as shown below.

Require Vector. Require Import List. Import ListNotations. Inductive hlist {A : Type} (B : A -> Type) : list A -> Type := | hnil : hlist B [] | hcons : forall al, B a -> hlist B l -> hlist B (a :: l). Definition vector_of_vectors (T : Type) (l : list nat) : Type := hlist (Vector.t T) l. 

Then, if l is your list of lengths, the type vector_of_vectors T l s will describe the type.

For example, we can build the element vector_of_vectors bool [2; 0; 1] vector_of_vectors bool [2; 0; 1] vector_of_vectors bool [2; 0; 1] :

 Section example. Definition ls : list nat := [2; 0; 1]. Definition v : vector_of_vectors bool ls := hcons [false; true] (hcons [] (hcons [true] hnil)). End example. 

This example uses some notation for vectors, which you can configure as follows:

 Arguments hnil {_ _}. Arguments hcons {_ _ _ _} _ _. Arguments Vector.nil {_}. Arguments Vector.cons {_} _ {_} _. Delimit Scope vector with vector. Bind Scope vector with Vector.t. Notation "[ ]" := (@Vector.nil _) : vector. Notation "a :: v" := (@Vector.cons _ a _ v) : vector. Notation " [ x ] " := (Vector.cons x Vector.nil) : vector. Notation " [ x ; y ; .. ; z ] " := (Vector.cons x (Vector.cons y .. (Vector.cons z Vector.nil) ..)) : vector. Open Scope vector. 

Answer 2

In Idris, in addition to creating a custom inductive type, we can reuse the standard type of heterogeneous vectors - HVect :

 import Data.HVect VecVec : Vect k Nat -> Type -> Type VecVec shape t = HVect $ map (flip Vect t) shape val : VecVec [3, 2, 1] Bool val = [[False, False, False], [False, False], [False]] -- the value is found automatically by Idris' proof-search facilities 

Answer 3

For completeness, here is a solution in Idris, inspired by what James Wilcox wrote:

 module VecVec import Data.Vect data VecVec: {k: Nat} -> Vect k Nat -> (t: Type) -> Type where Nil : VecVec [] t (::): {k, n: Nat} -> {v: Vect k Nat} -> Vect nt -> VecVec vt -> VecVec (n :: v) t val: VecVec [3, 2, 3] Bool val = [[False, True, False], [False, True], [True, False, True]] 

In this example, automatic translation of lists in square brackets into the base constructors Nil and :: any data type defines them.