Зависимые типы: вектор векторов

Я новичок в зависимых типах (я пробую и Idris, и Coq, несмотря на их большие различия).

Я пытаюсь выразить следующий тип: задан тип T и последовательность k НАТОВ n1, n2, ... nk, тип, состоящий из K последовательностей T длиной n1, n2, ... nk соответственно .

, то есть вектор из k векторов, длины которых задаются параметром. Возможно ли это?

3 7
coq

3 ответа:

Вы можете сделать это с гетерогенным списком следующим образом.

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.

Тогда, если l - это ваш список длин, Тип vector_of_vectors T l С будет типом, который вы описываете.

Например, мы можем построить элемент 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.

В этом примере используются некоторые обозначения векторов, которые можно настроить следующим образом: 

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.
7

В Idris, помимо создания пользовательского индуктивного типа, мы можем повторно использовать стандартный тип гетерогенных векторов -- 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
5

Для полноты, вот решение в Идрисе, вдохновленное тем, что написал Джеймс Уилкокс: 

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]]

В этом примере используется автоматический перевод списков в квадратных скобках в базовые конструкторы Nil и :: любого типа данных, определяющего их.

4