Agda: пара векторов одинаковой длины

Если вы хотите сохранить длину как часть типа, вам просто нужно упаковать два вектора с одинаковым индексом размера. Необходимый импорт в первую очередь:

open import Data.Nat
open import Data.Product
open import Data.Vec

Ничего особенного: так же, как вы пишете свой обычный вектор размером n, вы можете сделать это:

2Vec : ∀ {a} → Set a → ℕ → Set a
2Vec A n = Vec A n × Vec A n

То есть 2Vec A n - это тип пары векторов As, оба с n элементами. Обратите внимание, что я воспользовался возможностью обобщить это до уровня произвольной вселенной - что означает, например, что у вас могут быть векторы Sets.

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

И прежде чем я перейду к примеру, где мы хотели бы сохранить размер скрытым, вот пример значения этого типа:

test₁ : 2Vec ℕ 3
-- We can also infer the size index just from the term:
-- test₁ : 2Vec ℕ _    
test₁ = 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

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

Скрытие индексов - это работа, которая как раз подходит для зависимой пары. Для начала вот как можно скрыть длину одного вектора:

data SomeVec {a} (A : Set a) : Set a where
  some : ∀ n → Vec A n → SomeVec A

someVec : SomeVec ℕ
someVec = some _ (0 ∷ 1 ∷ [])

Индекс размера хранится вне сигнатуры типа, поэтому мы знаем только, что вектор внутри имеет некоторый неизвестный размер (фактически предоставляя вам список). Конечно, писать новый тип данных каждый раз, когда нам нужно было скрыть индекс, было бы утомительно, поэтому стандартная библиотека дает нам Σ.

someVec : Σ ℕ λ n → Vec ℕ n
-- If you have newer version of standard library, you can also write:
-- someVec : Σ[ n ∈ ℕ ] Vec ℕ n
-- Older version used unicode colon instead of ∈
someVec = _ , 0 ∷ 1 ∷ []

Теперь мы можем легко применить это к типу 2Vec, указанному выше:

∃2Vec : ∀ {a} → Set a → Set a
∃2Vec A = Σ[ n ∈ ℕ ] 2Vec A n

test₂ : ∃2Vec ℕ
test₂ = _ , 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

copumpkin поднимает отличный вопрос: вы можете получить такую ​​же гарантию, просто используя список пар. Эти два представления кодируют одну и ту же информацию, давайте посмотрим.

Здесь мы будем использовать другой список импорта, чтобы предотвратить конфликты имен:

open import Data.List
open import Data.Nat
open import Data.Product as P
open import Data.Vec as V
open import Function
open import Relation.Binary.PropositionalEquality

Переход от двух векторов к одному списку - это вопрос объединения двух векторов:

vec⟶list : ∀ {a} {A : Set a} → ∃2Vec A → List (A × A)
vec⟶list (zero  , []     , [])     = []
vec⟶list (suc n , x ∷ xs , y ∷ ys) = (x , y) ∷ vec⟶list (n , xs , ys)

-- Alternatively:
vec⟶list = toList ∘ uncurry V.zip ∘ proj₂

Вернуться - это просто разархивировать - взять список пар и создать пару списков:

list⟶vec : ∀ {a} {A : Set a} → List (A × A) → ∃2Vec A
list⟶vec [] = 0 , [] , []
list⟶vec ((x , y) ∷ xys) with list⟶vec xys
... | n , xs , ys = suc n , x ∷ xs , y ∷ ys

-- Alternatively:
list⟶vec = ,_ ∘ unzip ∘ fromList

Теперь мы знаем, как перейти от одного представления к другому, но нам еще нужно показать, что эти два представления дают нам одинаковую информацию.

Во-первых, мы показываем, что если мы возьмем список, преобразуем его в вектор (через list⟶vec), а затем обратно в список (через vec⟶list), то мы получим тот же список обратно.

pf₁ : ∀ {a} {A : Set a} (xs : List (A × A)) → vec⟶list (list⟶vec xs) ≡ xs
pf₁ []       = refl
pf₁ (x ∷ xs) = cong (_∷_ x) (pf₁ xs)

А затем наоборот: сначала список векторов, а затем список векторов:

pf₂ : ∀ {a} {A : Set a} (xs : ∃2Vec A) → list⟶vec (vec⟶list xs) ≡ xs
pf₂ (zero  , []     , [])     = refl
pf₂ (suc n , x ∷ xs , y ∷ ys) =
  cong (P.map suc (P.map (_∷_ x) (_∷_ y))) (pf₂ (n , xs , ys))

Если вам интересно, что делает cong:

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

Мы показали, что list⟶vec вместе с vec⟶list образуют изоморфизм между List (A × A) и ∃2Vec A, что означает, что эти два представления изоморфны.