haskell - Agda:一对长度相同的向量

Question

在 Agda 中，如何定义一对长度必须相同的向量？

-- my first try, but need to have 'n' implicitly  
b : ∀ ( n : ℕ ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) 
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ [])
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])
b _ = _

-- how can I define VecSameLength correctly?
VecSameLength : Set
VecSameLength = _

c : VecSameLength
c = (1 ∷ 2 ∷ []) , (1 ∷ 2 ∷ [])

d : VecSameLength
d = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])

-- another try
VecSameLength : Set
VecSameLength = Σ (Vec ℕ ?) (λ v → Vec ℕ (len v)) 

Answer 1

如果你想保留长度作为类型的一部分，你只需要打包两个具有相同大小索引的向量。先导入必要的:

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是 A 的向量对的类型s，两者都带有 n元素。请注意，我借此机会将其推广到任意宇宙级别 - 这意味着您可以拥有 Set 的向量。 s，例如。

要注意的第二个有用的事情是我使用了 _×_ ，这是一个普通的非依赖对。它是根据 Σ 定义的作为第二个组件不依赖于第一个的值的特殊情况。

在我转到我们希望隐藏大小的示例之前，这里有一个这种类型的值的示例:

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 ，这意味着这两种表示是同构的。