7

I'm new to dependent types (I'm trying both Idris and Coq, despite their big differences).

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

That is, a vector of k vectors, whose lengths are given by a parameter. Is this possible?

3 Answers 3

7

You can do this with a heterogeneous list, as follows.

Require Vector.
Require Import List.
Import ListNotations.

Inductive hlist {A : Type} (B : A -> Type) : list A -> Type :=
| hnil : hlist B []
| hcons : forall a l, 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 with will the type you describe.

For example, we can construct an element of 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 notations for vectors that you can set up like this:

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.
3
  • 1
    Or you can Import Vector.VectorNotations. Commented Aug 17, 2017 at 17:12
  • 1
    Good point. Unfortunately, VectorNotations has a bug where the notation for Vector.nil is declared as [] instead of [ ], which is how it's declared for List.nil. This confuses Coq into thinking [] is a token rather than two separate tokens and interferes with my use of [] for List.nil. So I've gotten in the sad habit of never importing VectorNotations. This bug is fixed in master, so I will get to unlearn this habit someday. Commented Aug 17, 2017 at 17:18
  • 1
    It looks like they fixed it for Coq 8.6.1. Commented Aug 17, 2017 at 21:15
5

In Idris, besides 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
4

For completeness, here is a solution in Idris inspired by the one posted by James Wilcox:

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 n t -> VecVec v t -> VecVec (n :: v) t

val: VecVec [3, 2, 3] Bool
val = [[False, True, False], [False, True], [True, False, True]]

This example uses the automatic translation of bracketed lists to the basic constructors Nil and :: of whatever data type defines them.

1
  • 2
    You could've also used a list as the index of the VecVec type, since you don't really use the variable k: data VecVec : List Nat -> Type -> Type where Nil : VecVec [] t (::) : Vect n t -> VecVec v t -> VecVec (n :: v) t. Commented Aug 17, 2017 at 21:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.