agda - 在 Agda 中使用依赖对的问题

Question

我在学习 Agda by tutorial ，现在我正在阅读有关依赖对的信息。

所以，这是代码片段:

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → (b : B a) → Σ A B

infixr 4 _,_

Σprojₗ : {A : Set}{B : A → Set} → Σ A B → A
Σprojₗ (a , b) = a

data _∈_ {A : Set}(x : A) : List A → Set where
  first : {xs : List A} → x ∈ x ∷ xs
  later : {y : A}{xs : List A} → x ∈ xs → x ∈ y ∷ xs

infix 4 _∈_

_!_ : ∀{A : Set} → List A → ℕ → Maybe A
  [] ! _           = nothing
  x ∷ xs ! zero    = just x
  x ∷ xs ! (suc n) = xs ! n

infix 5 _!_

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)

_,_是依赖对的构造函数， Σprojₗ返回对的第一部分， _∈_是隶属关系， lst ! i返回 just $(i-th element)如果 list的长度大于或等于 i， nothing - 除此以外。我想写一个 lookup获取列表的函数 xs , 成员(member)证明 x ∈ xs , 并返回自然数和函数的依赖对，对于自然数 n返回列表的第 n 个元素是 just x 的证据(或反证) .现在函数看起来像

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≣ just x)
lookup {A} {x} .(x ∷ xs) (inHead {xs}) = 0 , refl
lookup .(y ∷ xs) (inTail {y} {xs} proof) = (1 + Σprojₗ (lookup xs proof)) , ?

我想我应该写一些像 Σprojᵣ 这样的函数(它应该返回对的第二个元素，带有签名的函数 A → Set )用于填充孔，但我不知道如何编写它。唯一经过类型检查的变体是

Σprojᵣ : {A : Set}{B : A → Set} → Σ A B → (A → Set)
Σprojᵣ {A} {B} (a , b) = B

，但我没有设法完成 lookup用这个功能。我如何解决这个练习？

Answer 1

事实上，假设 Σprojᵣ投影该对的第二个元素，Σprojᵣ (lookup xs proof)是适合孔的正确解决方案。问题是，这个投影怎么写？

如果我们有普通的非依赖对，写两个投影很容易:

data _×_ (A B : Set) : Set where
  _,′_ : A → B → A × B

fst : ∀ {A B} → A × B → A
fst (a ,′ b) = a

snd : ∀ {A B} → A × B → B
snd (a ,′ b) = b

当我们使用依赖对时，是什么让它如此困难？提示隐藏在名称中:第二个组件取决于 first 的值，我们必须以某种方式在我们的类型中捕获它。

所以，我们开始:

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

为左组件编写投影很容易(请注意，我称它为 proj₁ 而不是 Σprojₗ ，这是标准库所做的):

proj₁ : {A : Set} {B : A → Set} → Σ A B → A
proj₁ (a , b) = a

现在，第二个投影应该看起来像这样:

proj₂ : {A : Set} {B : A → Set} → Σ A B → B ?
proj₂ (a , b) = b

但是 B什么？由于第二个组件的类型取决于第一个组件的值，我们需要以某种方式通过 B 走私它。 .

我们需要能够引用我们的对，让我们这样做:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B ?

现在，我们对的第一个组件是 proj₁ pair ，所以让我们填写:

proj₂ : {A : Set} {B : A → Set} (pair : Σ A B) → B (proj₁ pair)

事实上，这种类型检查!

然而，有比写 proj₂ 更简单的解决方案用手。

而不是定义 Σ作为 data ，我们可以将其定义为 record .记录是 data 的特例只有一个构造函数的声明。好消息是记录可以免费为您提供预测:

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ  -- opens the implicit record module

这(以及其他有用的东西)为您提供预测 proj₁和 proj₂ .

我们也可以用 with 解构这对声明并避免这种情况 proj业务全:

lookup : ∀ {A} {x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup {x = x} .(x ∷ xs) (first {xs}) = 0 , refl
lookup         .(y ∷ xs) (later {y} {xs} p) with lookup xs p
... | n , p′ = suc n , p′

with不仅可以对函数的参数进行模式匹配，还可以对中间表达式进行模式匹配。如果您熟悉 Haskell，它类似于 case .

现在，这几乎是理想的解决方案，但仍然可以做得更好。请注意，我们必须带上隐式 {x} , {xs}和 {y}进入范围只是为了我们可以写下点模式。点模式不参与模式匹配，它们被用作断言该特定表达式是唯一适合的表达式。

例如，在第一个等式中，圆点图案告诉我们列表一定看起来像 x ∷ xs - 我们知道这一点，因为我们在证明上进行了模式匹配。由于我们只对证明进行模式匹配，因此列表参数有点多余:

lookup : ∀ {A} {x : A} (xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup ._ first = 0 , refl
lookup ._ (later p) with lookup _ p
... | n , p′ = suc n , p′

编译器甚至可以推断递归调用的参数!如果编译器可以自己计算这些东西，我们可以安全地将其标记为隐式:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup first = 0 , refl
lookup (later p) with lookup p
... | n , p′ = suc n , p′

现在，最后一步:让我们引入一些抽象。第二个等式将一对分开，应用一些函数( suc )并重建对 - 我们在对上映射函数!

现在， map 的完全依赖类型相当复杂。不懂就不要气馁!当你以后带着更多的知识回来时，你会发现它很有趣。

map : {A C : Set} {B : A → Set} {D : C → Set}
      (f : A → C) (g : ∀ {a} → B a → D (f a)) →
      Σ A B → Σ C D
map f g (a , b) = f a , g b

与之比较:

map′ : {A B C D : Set}
       (f : A → C) (g : B → D) →
       A × B → C × D
map′ f g (a ,′ b) = f a ,′ g b

我们以非常简洁的方式结束:

lookup : ∀ {A} {x : A} {xs : List A} → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)
lookup first     = 0 , refl
lookup (later p) = map suc id (lookup p)

也就是说，我们映射 suc在第一个组件上并保持第二个不变( id )。