Types dépendants: Vecteur de vecteurs

Question

Je suis nouveau pour les types dépendants (j'essaie à la fois Idris et Coq, malgré leurs grandes différences). J'essaye d'exprimer le type suivant: donné un type T et une séquence de k nats n1, n2, ... nk, un type composé de k séquences de T de longueur n1, n2, .. .nk respectivement.

C'est-à-dire, un vecteur de k vecteurs, dont les longueurs sont données par un paramètre. Est-ce possible?

Answer 1

Vous pouvez le faire avec une liste hétérogène, comme suit.

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. 

Ensuite, si l est votre liste de longueurs, le type vector_of_vectors T l avec la volonté du type que vous décrivez.

Par exemple, nous pouvons construire un élément de 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. 

Cet exemple utilise des notations pour les vecteurs que vous pouvez configurer comme ceci:

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

Pour être complet, voici une solution dans Idris inspiré par celui posté par 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]] 

Cet exemple utilise la traduction automatique de listes entre crochets pour les constructeurs de base Nil et :: de n'importe quel type de données les définit.

Answer 3

Dans Idris, en plus de créer un type personnalisé par induction, nous pouvons réutiliser le type standard de vecteurs hétérogènes - 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