编程语言基础：Agda 描述

module plfa.part2.Inference where

在本书至此的进展中，项的类型推导是如法令一般直接给出的。在 Lambda 章节，类型推导以外在于项的形式给出，而在 DeBruijn 章节，类型推导以内在于项的形式给出，但在两者均要求我们将类型推导完全写出。

在实践中，我们一般可以给项加上一些装饰，然后运用算法来推理（Infer）出类型推导。的确，Agda 中也是这样：我们给顶层的函数声明指定类型，而其余可由给出的信息推理而来。 Agda 使用的这种推理被称为双向（Bidirectional）类型推理，我们将在本章中进行展示。

本章中，我们讲之前的进展结合在一起。我们首先由带有类型注释的项开始，其与 Lambda 章节中的源项相似，从此我们计算出内在类型的项，如同 DeBruijn 章节中那样。

绪论：推理规则作为算法

在我们至此使用的演算中，一个项可以有多于一个类型。例如，

(ƛ x ⇒ x) ⦂ (A ⇒ A)

对于任意类型 A 成立。我们首先考虑一个带有 λ 项的小语言，其每一项有其唯一的类型。我们只需要给抽象加上参数的类型。这样我们可以得到如下的语法：

L, M, N ::=                         带装饰的项
  x                                   变量
  ƛ x ⦂ A ⇒ N                         抽象（装饰后）
  L · M                               应用

每一条相关的赋型规则可以被读作类型检查的算法。对于每一条赋型规则，我们将每个位置标记如输入（Input）或者输出（Output）。

对于下面的判断

Γ ∋ x ⦂ A

我们将语境 Γ 和变量 x 作为输入，类型 A 作为输出。考虑下面的规则：

----------------- Z
Γ , x ⦂ A ∋ x ⦂ A

Γ ∋ x ⦂ A
----------------- S
Γ , y ⦂ B ∋ x ⦂ A

从输入中，我们可以决定应用哪一条规则：如果语境中最后一个变量与给定的变量一致，那么应用第一条规则，否则应用第二条。（对于 de Bruijn 因子来说，这更加简单：零对应第一条，后继对应第二条。）对于第一条，输出类型可以直接从语境中得到。对于第二条，结论中的输入可以作为假设的输入，而假设的输出决定了结论的输出。

对于下面的判断：

Γ ⊢ M ⦂ A

我们将语境 Γ 和项 M 作为输入，类型 A 作为输出。考虑下面的规则：

Γ ∋ x ⦂ A
-----------
Γ ⊢ ` x ⦂ A

Γ , x ⦂ A ⊢ N ⦂ B
---------------------------
Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ (A ⇒ B)

Γ ⊢ L ⦂ A ⇒ B
Γ ⊢ M ⦂ A′
A ≡ A′
-------------
Γ ⊢ L · M ⦂ B

输入项决定了应用哪一条规则：变量使用第一条，抽象使用第二条，应用使用第三条。我们把这样的规则叫做语法导向的（Syntax directed）规则。对于变量的规则，结论的输入决定了结论的输出。抽象的规则也是一样——约束变量和参数从结论的输入流向假设中的语境；这得以实现，因为我们在抽象中加入了参数的类型。对于应用的规则，我们加入第三条假设来检查函数类型中的作用域是否与参数的类型一致；这条判断是在两个类型已知时是可判定的。结论的输入决定了前两个假设的输入，而前两个假设的输出决定了第三个假设的输入，而第一个假设的输出决定了结论的输出。

我们可以直接地把上述内容转换成一个算法，加入自然数和不动点也很直接。我们省略其明细。取而代之的是，我们考虑一种需要更少装饰的表示方法。其核心思想是将普通的赋型判断拆分成两个判断，一个生成类型作为输出，另一个取类型作为输入。

生成和继承类型

我们保留之前的变量的查询判断。除此之外，我们有两种联系类型和项的判断：

Γ ⊢ M ↑ A
Γ ⊢ M ↓ A

第一类判断生成（Synthesise）项的类型，如上，而第二类继承（Inherit）类型。在第一类中，语境和项作为输入，类型作为输出；而在第二类中，语境、项和类型三者都作为输入。

什么项生成类型，什么项继承类型的？我们的宗旨是解构子中的主项使用生成来赋型，而构造子使用继承。比如，函数应用中的函数由生成来赋型，而抽象是由继承来赋型。抽象中继承的类型和之前我们为参数额外增加的注解起到一样的作用。

解构某一类型的值的项总有一个主项（提供一个所需类型的参数），且经常有副项。对于函数应用来说，主项提供了函数，副项提供了参数。对于分情况讨论来说，主项提供了自然数，副项则是两种情况不同的情况。在解构子中，主项使用生成进行赋型，而副项使用继承进行赋型。我们将看到，这自然地导致函数应用作为整体由生成进行赋型，而分情况讨论作为整体则使用继承进行赋型。变量一般使用生成进行赋型，因为我们可以直接从语境中查询其类型。不动点自然是用继承来赋型。

为了达成赋型系统的语法导向性，我们将项分为两类： Term⁺ 和 Term⁻，分别用生成和继承来赋型。由生成赋型的子项可能出现在由继承赋型的子项中，反之亦然，这给我们带来两种新形式。

例如，我们之前提到函数应用的参数由继承赋型，而变量由生成赋型。在参数是变量时会出现不匹配的情况。因此，我们需要一种把生成的项当作继承的项的方法。我们引入 M ↑ 这种新的形式来达成此目的。它的赋型判断即为检查其生成和继承的类型是否一致。

同样，函数应用的函数部分由生成来赋型，而抽象是由继承来赋型。在函数是抽象时会出现不匹配的情况。因此，我们需要一种把继承的项当作生成的项的方法。我们引入 M ↓ A 这种新的形式来达成此目的。它的赋型判断返回 A 作为生成的类型，并把它作为 M 继承的类型。

M ↓ A 这种形式表示了我们唯一需要用类型来装饰的项。它只在从生成切换成继承时出现，即当一个解构某一类型的值的项的主项中包含了一个构造某一类型的值的时候，也就是说，这是在 β 归约发生的地方出现。一般来说，我们只需要在顶层声明中需要这样的装饰。

我们可以从上文中提取出项的语法：

L⁺, M⁺, N⁺ ::=                      带有生成类型的项
  x                                   变量
  L⁺ · M⁻                             应用
  M⁻ ↓ A                              切换至继承

L⁻, M⁻, N⁻ ::=                      带有继承类型的项
  ƛ x ⇒ N⁻                            抽象
  `zero                               零
  `suc M⁻                             后继
  case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ]     分情况讨论
  μ x ⇒ N⁻                            不动点
  M⁺ ↑                                切换至生成

我们将在下文中形式化上述定义。

可靠性和完备性

我们试图证明赋型判断是可判定的：

synthesize : ∀ (Γ : Context) (M : Term⁺)
    ------------------------------------
  → Dec (∃[ A ] Γ ⊢ M ↑ A)

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
          --------------------------------------
        → Dec (Γ ⊢ M ↓ A)

给定语境 Γ 和生成项 M，我们必须判定是否存在一个类型 A 使得 Γ ⊢ M ↑ A 成立，或者其否定。同样，给定语境 Γ 、继承项 M 和类型 A，我们必须判定 Γ ⊢ M ↓ A 成立，或者其否定。

我们的证明是构造性的。在生成的情况中，它要么给出一个包括类型 A 和 Γ ⊢ M ↓ A 成立的证明的有序对，或是一个将上述有序对转换成矛盾的函数。在继承的情况中，它要么给出 Γ ⊢ M ↑ A 成立的证明，或是一个将上述证明转换成矛盾的函数。成立的情况被称为可靠性（Soundness）——生成和继承只在对应关系成立时成功。不成立的情况被称为完备性（Completeness）——生成和继承只在对应关系无法成立时失败。

另一种实现方法可能在生成或继承成功时返回其推导，并在失败时返回一条错误信息——例如，参见 Agda 用户手册中讨论语法糖的章节。这样的方法可以实现可靠性，而不是完备性。如果其返回一个推导，那么我们知道它是正确的；但没有人阻挡我们来给出一个总是返回错误的函数，即使正确的推导存在。证明可靠性和完备性两者比起单独证明可靠性一者更加有力。其反向的证明可以被看作是一个语义上验证过的错误信息，即便它本身比仔细撰写的错误信息更让人难懂。

我们现在可以开始正式的形式化了：

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (False; toWitnessFalse)

当我们有一个赋型推导时，从它构造出内在类型的表示方法更加方便。为了与我们之前的结果进行比较，我们导入模块 plfa.part2.More：

import plfa.part2.More as DB

as DB 这个词组让我们可以用例如 DB._⊢_ 的方法来指代其中的定义，我们用 Γ DB.⊢ A 来使用它，其中 Γ 的类型是 DB.Context， A 的类型是 DB.Type。

语法

首先，我们来定义中缀声明。我们将判断和项的运算符分别列出：

infix   4  _∋_⦂_
infix   4  _⊢_↑_
infix   4  _⊢_↓_
infixl  5  _,_⦂_

infixr  7  _⇒_

infix   5  ƛ_⇒_
infix   5  μ_⇒_
infix   6  _↑
infix   6  _↓_
infixl  7  _·_
infix   8  `suc_
infix   9  `_

标识符、类型和语境与之前一样：

Id : Set
Id = String

data Type : Set where
  `ℕ    : Type
  _⇒_   : Type → Type → Type

data Context : Set where
  ∅     : Context
  _,_⦂_ : Context → Id → Type → Context

项的语法由共同递归来定义。我们用 Term⁺ 和 Term⁻ 来分别表示生成和继承的项。注意我们包括了变向的形式 M ↓ A 和 M ↑：

data Term⁺ : Set
data Term⁻ : Set

data Term⁺ where
  `_                       : Id → Term⁺
  _·_                      : Term⁺ → Term⁻ → Term⁺
  _↓_                      : Term⁻ → Type → Term⁺

data Term⁻ where
  ƛ_⇒_                     : Id → Term⁻ → Term⁻
  `zero                    : Term⁻
  `suc_                    : Term⁻ → Term⁻
  `case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
  μ_⇒_                     : Id → Term⁻ → Term⁻
  _↑                       : Term⁺ → Term⁻

至于每个项是由继承或者生成来赋型，我们在上文中已经讨论过，并且可以直接上文的非形式化语法中直接得来。解构子中的主项由生成赋型，解构子中的构造子和副项由继承赋型。

项的例子

我们重新给出前几章中的例子。首先，计算自然数二加二：

two : Term⁻
two = `suc (`suc `zero)

plus : Term⁺
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
          `case (` "m") [zero⇒ ` "n" ↑
                        |suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
            ↓ (`ℕ ⇒ `ℕ ⇒ `ℕ)

2+2 : Term⁺
2+2 = plus · two · two

唯一的变化是我们需要在需要时加入上下箭头。唯一的类型注释出现在 plus。

接下来，计算 Church 数的二加二：

Ch : Type
Ch = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ

twoᶜ : Term⁻
twoᶜ = (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · (` "z" ↑) ↑) ↑)

plusᶜ : Term⁺
plusᶜ = (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
           ` "m" · (` "s" ↑) · (` "n" · (` "s" ↑) · (` "z" ↑) ↑) ↑)
             ↓ (Ch ⇒ Ch ⇒ Ch)

sucᶜ : Term⁻
sucᶜ = ƛ "x" ⇒ `suc (` "x" ↑)

2+2ᶜ : Term⁺
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero

唯一的类型注释出现在 plusᶜ。 sucᶜ 甚至不需要类型注释，因为它从 plusᶜ 的参数中继承了类型。

双向类型检查

变量的赋型规则与 Lambda 章节中一致：

data _∋_⦂_ : Context → Id → Type → Set where

  Z : ∀ {Γ x A}
      -----------------
    → Γ , x ⦂ A ∋ x ⦂ A

  S : ∀ {Γ x y A B}
    → x ≢ y
    → Γ ∋ x ⦂ A
      -----------------
    → Γ , y ⦂ B ∋ x ⦂ A

与语法一样，生成和继承的赋型判断也是共同递归的：

data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set

data _⊢_↑_ where

  ⊢` : ∀ {Γ A x}
    → Γ ∋ x ⦂ A
      -----------
    → Γ ⊢ ` x ↑ A

  _·_ : ∀ {Γ L M A B}
    → Γ ⊢ L ↑ A ⇒ B
    → Γ ⊢ M ↓ A
      -------------
    → Γ ⊢ L · M ↑ B

  ⊢↓ : ∀ {Γ M A}
    → Γ ⊢ M ↓ A
      ---------------
    → Γ ⊢ (M ↓ A) ↑ A

data _⊢_↓_ where

  ⊢ƛ : ∀ {Γ x N A B}
    → Γ , x ⦂ A ⊢ N ↓ B
      -------------------
    → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B

  ⊢zero : ∀ {Γ}
      --------------
    → Γ ⊢ `zero ↓ `ℕ

  ⊢suc : ∀ {Γ M}
    → Γ ⊢ M ↓ `ℕ
      ---------------
    → Γ ⊢ `suc M ↓ `ℕ

  ⊢case : ∀ {Γ L M x N A}
    → Γ ⊢ L ↑ `ℕ
    → Γ ⊢ M ↓ A
    → Γ , x ⦂ `ℕ ⊢ N ↓ A
      -------------------------------------
    → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A

  ⊢μ : ∀ {Γ x N A}
    → Γ , x ⦂ A ⊢ N ↓ A
      -----------------
    → Γ ⊢ μ x ⇒ N ↓ A

  ⊢↑ : ∀ {Γ M A B}
    → Γ ⊢ M ↑ A
    → A ≡ B
      -------------
    → Γ ⊢ (M ↑) ↓ B

我们用和 Lambda 中一样的命名规则，把 ⊢ 加在构造子之前，来当作对应赋型规则的名称。

这些规则和 Lambda 章节中相似，修改成支持生成和继承类型的样式。其中有两条新规则 ⊢↓ 和 ⊢↑。前者把类型装饰当作继承的类型，并将其返回作为生成的类型。后者取其生成的类型，并检查是否与继承的类型一致——这应该让你回忆起第一部分中函数应用规则的相等性测试。

练习 `bidirectional-mul` （推荐）

将你在 Lambda 章节中乘法的定义重写，将其装饰至支持类型推理的形式。

-- 请将代码写在此处。

练习 `bidirectional-products` （推荐）

扩充你的双向赋型规则，来包括 More 章节中的积。

-- 请将代码写在此处。

练习 `bidirectional-rest` （延伸）

扩充你的双向赋型规则，来包括 More 章节中的其余构造。

-- 请将代码写在此处。

前置需求

M ↑ 规则需要我们有能力来判定两个类型是否相等。我们可以直接地给出代码：

_≟Tp_ : (A B : Type) → Dec (A ≡ B)
`ℕ      ≟Tp `ℕ              =  yes refl
`ℕ      ≟Tp (A ⇒ B)         =  no λ()
(A ⇒ B) ≟Tp `ℕ              =  no λ()
(A ⇒ B) ≟Tp (A′ ⇒ B′)
  with A ≟Tp A′ | B ≟Tp B′
...  | no A≢    | _         =  no λ{refl → A≢ refl}
...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
...  | yes refl | yes refl  =  yes refl

我们也会需要一些显然的引理；作用域和值域相等的函数类型相等：

dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
dom≡ refl = refl

rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
rng≡ refl = refl

我们也需要知道 `ℕ 和 A ⇒ B 这两个类型不相等：

ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
ℕ≢⇒ ()

唯一的类型

从语境查询一个类型是唯一的。给定两个推导，其一证明 Γ ∋ x ⦂ A，另一个证明 Γ ∋ x ⦂ B，那么 A 和 B 一定是一样的：

uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
uniq-∋ Z Z                 =  refl
uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′

如果两个推导都使用 Z 规则，那么唯一性即可直接得出；如果两个推导都使用 S 规则，那么唯一性可以由归纳得出。如果一个使用了 Z 规则，另一个使用了 S 规则，这则是一个矛盾，因为 Z 要求我们查询的变量是语境中的最后一个，而 S 要求不是这样。

生成的类型也是唯一的。给定两个推导，其一证明 Γ ⊢ M ↑ A，另一个证明 Γ ⊢ M ↑ B，那么 A 和 B 一定是一样的：

uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl

有三种项的形式。如果项是变量，那么生成的唯一性从查询的唯一性中直接得出。如果项是函数应用，那么唯一性由应用中的函数之上的归纳得出，因为值域相等的类型相等。如果项是变向，两者装饰的类型相等，从此可得唯一性。

查询语境中变量的类型

给定 Γ 和两个不同的变量 x 和 y，如果不存在类型 A 使得 Γ ∋ x ⦂ A 成立，那么也不存在类型 A 使得 Γ , y ⦂ B ∋ x ⦂ A 成立：

ext∋ : ∀ {Γ B x y}
  → x ≢ y
  → ¬ (∃[ A ] Γ ∋ x ⦂ A)
    ----------------------------
  → ¬ (∃[ A ] Γ , y ⦂ B ∋ x ⦂ A)
ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
ext∋ _   ¬∃ ⟨ A , S _ ∋x ⟩  =  ¬∃ ⟨ A , ∋x ⟩

给定类型 A 和 Γ , y ⦂ B ∋ x ⦂ A 成立的证明，我们必须构造一个矛盾。如果判断由 Z 成立，那么 x 和 y 一定是一样的，与第一个假设矛盾。如果判断由 S _ ∋x 成立，那么 ∋x 提供了 Γ ∋ x ⦂ A 成立的证明，与第二个假设矛盾。

给定语境 Γ 和变量 x，我们可判断是否存在一个类型 A 使得 Γ ∋ x ⦂ A 成立，或者其反命题：

lookup : ∀ (Γ : Context) (x : Id)
         ------------------------
       → Dec (∃[ A ] Γ ∋ x ⦂ A)
lookup ∅ x                        =  no  (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl                    =  yes ⟨ B , Z ⟩
... | no x≢y with lookup Γ x
...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
...             | yes ⟨ A , ∋x ⟩  =  yes ⟨ A , S x≢y ∋x ⟩

考虑语境的情况：

如果语境为空，那么平凡地，我们没有任何可能的推导。

如果语境非空，比较给定的变量和最新的绑定：
- 如果它们一致，我们完成了判定，使用 Z 作为对应的推导。
- 如果它们不一致，我们递归：
  - 如果查询失败了，我们使用 ext∋ 将变量不存在于内部的语境中的证明扩充至扩充后的语境。
  - 如果查询成功了，我们对返回的推导使用 S。

提升否定

对于每一个可能的项的形式，我们需要证明：如果其内部的子项无法被赋型，那么整个项无法被赋型。大多数情况下，我们可以直接在行中直接完成所需的证明，但有一些困难的情况，我们提供一些帮助函数。

如果 Γ ⊢ L ↑ A ⇒ B 成立而 Γ ⊢ M ↓ A 不成立，那么不存在使得 Γ ⊢ L · M ↑ B′ 成立的类型 B′：

¬arg : ∀ {Γ A B L M}
  → Γ ⊢ L ↑ A ⇒ B
  → ¬ Γ ⊢ M ↓ A
    --------------------------
  → ¬ (∃[ B′ ] Γ ⊢ L · M ↑ B′)
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′

让 ⊢L 作为 Γ ⊢ L ↑ A ⇒ B 成立的证明、 ¬⊢M 作为 Γ ⊢ M ↓ A 不成立的证明。给定类型 B′ 和 Γ ⊢ L · M ↑ B′ 成立的证明，我们必须构造一个矛盾。这样的证明一定是 ⊢L′ · ⊢M′ 的形式，其中 ⊢L′ 是 Γ ⊢ L ↑ A′ ⇒ B′ 成立的证明、⊢M′ 是 Γ ⊢ M ↓ A′ 成立的证明。将 uniq-↑ 应用于 ⊢L 和 ⊢L′，我们知道 A ⇒ B ≡ A′ ⇒ B′，所以可得 A ≡ A′，这意味着 ¬⊢M 和 ⊢M′ 可以构造出一个矛盾。不使用 rewrite 语句的话，Agda 不会让我们从 ¬⊢M 和 ⊢M′ 中构造出一个矛盾，因为其中的类型分别是 A 和 A′。

如果 Γ ⊢ M ↑ A 成立且 A ≢ B，那么 Γ ⊢ (M ↑) ↓ B 不成立：

¬switch : ∀ {Γ M A B}
  → Γ ⊢ M ↑ A
  → A ≢ B
    ---------------
  → ¬ Γ ⊢ (M ↑) ↓ B
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B

让 ⊢M 作为 Γ ⊢ M ↑ A 成立的证明、A≢B 作为 A ≢ B 成立的证明。给定 Γ ⊢ (M ↑) ↓ B 成立的证明，我们必须构造一个矛盾。这样的证明一定是 ⊢↑ ⊢M′ A′≡B 的形式，其中 ⊢M′ 是 Γ ⊢ M ↑ A′ 成立的证明、A′≡B 是 A′ ≡ B 成立的证明。将 uniq-↑ 应用于 ⊢M 和 ⊢M′，我们知道 A ≡ A′，这意味着 A≢B 和 A′≡B 可以构造出一个矛盾。不使用 rewrite 语句的话，Agda 不会让我们从 A≢B 和 A′≡B 中构造出一个矛盾，因为其中的类型分别是 A 和 A′。

生成和继承类型

餐桌已经布置好了，我们已经准备好享用今天的主菜了。我们定义两个共同递归的函数，一个用于生成，一个用于继承。生成在给定语境 Γ 和生成项 M 时，要么返回一个类型 A 和 Γ ⊢ M ↑ A 成立的证明，或者其/否定。继承在给定语境 Γ 、继承项 M 和类型 A 时要么返回 Γ ⊢ M ↓ A 成立的证明，或者其否定：

synthesize : ∀ (Γ : Context) (M : Term⁺)
             ---------------------------
           → Dec (∃[ A ] Γ ⊢ M ↑ A )

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
    ---------------
  → Dec (Γ ⊢ M ↓ A)

我们首先考虑生成的代码：

synthesize Γ (` x) with lookup Γ x
... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
synthesize Γ (L · M) with synthesize Γ L
... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩

有三种情况来考虑：

如果项是变量 ` x，我们使用之前定义的查询：
- 如果失败了，那么 ¬∃ 是不存在使得 Γ ∋ x ⦂ A 成立的类型 A 的证明。 Γ ⊢ ` x ↑ A 成立的证明一定是 ⊢` ∋x 的形式，其中 ∋x 是 Γ ∋ x ⦂ A 成立的证明，这构成了一个矛盾。
- 如果成功了，那么 ∋x 是 Γ ∋ x ⦂ A 成立的证明，所以 ⊢` ∋x 是 Γ ⊢ ` x ↑ A 成立的证明。

如果项是函数应用 L · M，我们递归于函数项 L：
- 如果失败了，那么 ¬∃ 是不存在任何类型 Γ ⊢ L ↑ _ 成立的证明。 Γ ⊢ L · M ↑ _ 成立的证明一定是 ⊢L · _ 的形式，其中 ⊢L 是 Γ ⊢ L ↑ _ 成立的证明，这构成了一个矛盾。
- 如果成功了，那么有两种情况：
  - 其一是 ⊢L 是 Γ ⊢ L ⦂ `ℕ 成立的证明。 Γ ⊢ L · M ↑ _ 成立的证明一定是 ⊢L′ · _ 的形式，其中 ⊢L′ 是 Γ ⊢ L ↑ A ⇒ B 对于一些类型 A 和 B 成立的证明。将 uniq-↑ 应用于 ⊢L 和 ⊢L′ 构成了一个矛盾，因为 `ℕ 无法与 A ⇒ B 相等。
  - 另一是 ⊢L 是 Γ ⊢ L ↑ A ⇒ B 成立的证明，那么我们在参数项 M 上递归：
    - 如果失败了，那么 ¬⊢M 是 Γ ⊢ M ↓ A 不成立的证明。将 ¬arg 应用于 ⊢L 和 ¬⊢M，我们可得 Γ ⊢ L · M ↑ B 不成立。
    - 如果成功了，那么 ⊢M 是 Γ ⊢ M ↓ A 成立的证明，且 ⊢L · ⊢M 提供了 Γ ⊢ L · M ↑ B 成立的证明。

如果项是从生成到继承的变向项 M ↓ A，我们在子项 M 上递归，并向继承提供类型 A：
- 如果失败了，那么 ¬⊢M 是 Γ ⊢ M ↓ A 不成立的证明。 Γ ⊢ (M ↓ A) ↑ A 成立的证明一定是 ⊢↓ ⊢M 的形式，其中 ⊢M 是 Γ ⊢ M ↓ A 成立的证明，这构成了一个矛盾。
- 如果成功了，那么 ⊢M 是 Γ ⊢ M ↓ A 成立的证明，且 ⊢↓ ⊢M 提供了 Γ ⊢ (M ↓ A) ↑ A 成立的证明。

我们接下来考虑继承的代码：

inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢ƛ ⊢N)
inherit Γ `zero `ℕ          =  yes ⊢zero
inherit Γ `zero (A ⇒ B)     =  no  (λ())
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
... | yes ⊢M                =  yes (⊢suc ⊢M)
inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢μ ⊢N)
inherit Γ (M ↑) B with synthesize Γ M
... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)

我们在此只考虑抽象和从继承变向至生成的情况：

如果项是 ƛ x ⇒ N，而继承的类型是 `ℕ，那么平凡地， Γ ⊢ (ƛ x ⇒ N) ↓ `ℕ 无法成立。

如果项是 ƛ x ⇒ N，而继承的类型是 A ⇒ B，我们用语境 Γ , x ⦂ A 递归至子项 N 继承类型 B：
- 如果失败了，那么 ¬⊢N 是 Γ , x ⦂ A ⊢ N ↓ B 不成立的证明。 Γ ⊢ (ƛ x ⇒ N) ↓ A ⇒ B 成立的证明一定是 ⊢ƛ ⊢N 的形式，其中 ⊢N 是 Γ , x ⦂ A ⊢ N ↓ B 成立的证明，这构成了一个矛盾。
- 如果成功了，那么 ⊢N 是 Γ , x ⦂ A ⊢ N ↓ B 成立的证明，且 ⊢ƛ ⊢N 提供了 Γ ⊢ (ƛ x ⇒ N) ↓ A ⇒ B 成立的证明。

如果项是从继承到生成的变向项 M ↑，我们在子项 M 上递归：
- 如果失败了，那么 ¬∃ 是不存在使得 Γ ⊢ M ↑ A 成立的类型 A 的证明。 Γ ⊢ (M ↑) ↓ B 成立的证明一定是 ⊢↑ ⊢M _ 的形式，其中 ⊢M 是 Γ ⊢ M ↑ _ 成立的证明，这构成了一个矛盾。
- 如果成功了，那么 ⊢M 是 Γ ⊢ M ↑ A 成立的证明。我们应用 _≟Tp_ 来判定 A 和 B 是否相等：
  - 如果失败了，那么 A≢B 是 A ≢ B 的证明。将 ¬switch 应用于 ⊢M 和 A≢B，我们可得 Γ ⊢ (M ↑) ↓ B 无法成立。
  - 如果成功了，那么 A≡B 是 A ≡ B 的证明，且 ⊢↑ ⊢M A≡B 提供了 Γ ⊢ (M ↑) ↓ B 成立的证明。

剩余的情况类似，它们的代码可以由对应的赋型规则直接对应得来。

测试项的例子

首先，我们复制之前介绍过的智能构造子 S′，使得访问语境中的变量更加便利：

S′ : ∀ {Γ x y A B}
   → {x≢y : False (x ≟ y)}
   → Γ ∋ x ⦂ A
     ------------------
   → Γ , y ⦂ B ∋ x ⦂ A

S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) x

下面是给自然数二加二赋型的结果：

⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ
⊢2+2 =
  (⊢↓
   (⊢μ
    (⊢ƛ
     (⊢ƛ
      (⊢case (⊢` (S′ Z)) (⊢↑ (⊢` Z) refl)
       (⊢suc
        (⊢↑
         (⊢`
          (S′
           (S′
            (S′ Z)))
          · ⊢↑ (⊢` Z) refl
          · ⊢↑ (⊢` (S′ Z)) refl)
         refl))))))
   · ⊢suc (⊢suc ⊢zero)
   · ⊢suc (⊢suc ⊢zero))

我们可以确认，对相应的项生成类型返回了自然数类型，和上述的推导：

_ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩
_ = refl

的确，上述的推导是用左边的项求值所得的，再加上一些微小的修改。所需的修改只是使用智能构造子 S′ 来获取两个变量名（使用字符串）不同的证明（其无法打印或阅读）。

下面是给 Church 数二加二赋型的结果：

⊢2+2ᶜ : ∅ ⊢ 2+2ᶜ ↑ `ℕ
⊢2+2ᶜ =
  ⊢↓
  (⊢ƛ
   (⊢ƛ
    (⊢ƛ
     (⊢ƛ
      (⊢↑
       (⊢`
        (S′
         (S′
          (S′ Z)))
        · ⊢↑ (⊢` (S′ Z)) refl
        ·
        ⊢↑
        (⊢`
         (S′
          (S′ Z))
         · ⊢↑ (⊢` (S′ Z)) refl
         · ⊢↑ (⊢` Z) refl)
        refl)
       refl)))))
  ·
  ⊢ƛ
  (⊢ƛ
   (⊢↑
    (⊢` (S′ Z) ·
     ⊢↑ (⊢` (S′ Z) · ⊢↑ (⊢` Z) refl)
     refl)
    refl))
  ·
  ⊢ƛ
  (⊢ƛ
   (⊢↑
    (⊢` (S′ Z) ·
     ⊢↑ (⊢` (S′ Z) · ⊢↑ (⊢` Z) refl)
     refl)
    refl))
  · ⊢ƛ (⊢suc (⊢↑ (⊢` Z) refl))
  · ⊢zero

我们可以确认，对相应的项生成类型返回了自然数类型，和上述的推导：

_ : synthesize ∅ 2+2ᶜ ≡ yes ⟨ `ℕ , ⊢2+2ᶜ ⟩
_ = refl

同样，上面的推导使用对左手边的项求值所得，加上一些修改。

测试错误的例子

很重要的是，不仅要检查代码是否按照意图工作，以及代码是否按照意图不工作。下面是检查不同种类错误的例子：

未约束的变量：

_ : synthesize ∅ ((ƛ "x" ⇒ ` "y" ↑) ↓ (`ℕ ⇒ `ℕ)) ≡ no _
_ = refl

函数应用的参数不是良类型的：

_ : synthesize ∅ (plus · sucᶜ) ≡ no _
_ = refl

函数应用的函数不是良类型的：

_ : synthesize ∅ (plus · sucᶜ · two) ≡ no _
_ = refl

函数应用的函数是自然数类型：

_ : synthesize ∅ ((two ↓ `ℕ) · two) ≡ no _
_ = refl

抽象继承了自然数类型：

_ : synthesize ∅ (twoᶜ ↓ `ℕ) ≡ no _
_ = refl

零继承了函数类型：

_ : synthesize ∅ (`zero ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl

后继继承了函数类型：

_ : synthesize ∅ (two ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl

非良类型项的后继：

_ : synthesize ∅ (`suc twoᶜ ↓ `ℕ) ≡ no _
_ = refl

对函数类型的项分情况讨论：

_ : synthesize ∅
      ((`case (twoᶜ ↓ Ch) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl

对不良类型的项分情况讨论：

_ : synthesize ∅
      ((`case (twoᶜ ↓ `ℕ) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl

变向时继承与生成的项不一致：

_ : synthesize ∅ (((ƛ "x" ⇒ ` "x" ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ))) ≡ no _
_ = refl

擦除

从装饰过的项拥有正确的类型的证明中，我们可以简单地提取出对应的内在类型的项。我们使用 DB 来指代 DeBruijn 章节中的代码。我们可以简单地定义一个擦除（Erasure）从外在的赋型判断，至对应的内在类型的项的函数。

首先，我们给出擦除类型的代码：

∥_∥Tp : Type → DB.Type
∥ `ℕ ∥Tp             =  DB.`ℕ
∥ A ⇒ B ∥Tp          =  ∥ A ∥Tp DB.⇒ ∥ B ∥Tp

它简单地把对应的构造子重命名至 DB 模块中。

接下来，我们给出擦除语境的代码：

∥_∥Cx : Context → DB.Context
∥ ∅ ∥Cx              =  DB.∅
∥ Γ , x ⦂ A ∥Cx      =  ∥ Γ ∥Cx DB., ∥ A ∥Tp

它简单地丢弃了变量名。

接下来，我们给出擦除查询判断的代码：

∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
∥ Z ∥∋               =  DB.Z
∥ S x≢ ∋x ∥∋         =  DB.S ∥ ∋x ∥∋

它简单地丢弃了变量名不同的证明。

最后，我们给出擦除赋型判断的代码。正如由两个共同递归的赋型判断，我们有两个共同递归的擦除函数：

∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp

∥ ⊢` ⊢x ∥⁺           =  DB.` ∥ ⊢x ∥∋
∥ ⊢L · ⊢M ∥⁺         =  ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ ⊢↓ ⊢M ∥⁺           =  ∥ ⊢M ∥⁻

∥ ⊢ƛ ⊢N ∥⁻           =  DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢zero ∥⁻           =  DB.`zero
∥ ⊢suc ⊢M ∥⁻         =  DB.`suc ∥ ⊢M ∥⁻
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻  =  DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
∥ ⊢μ ⊢M ∥⁻           =  DB.μ ∥ ⊢M ∥⁻
∥ ⊢↑ ⊢M refl ∥⁻      =  ∥ ⊢M ∥⁺

擦除将每个赋型判断中的构造子替换成 DB 中对应的项构造子。对应变向的构造子被丢弃。

我们证实本章中的赋型判断擦除后，与之前使用内在类型项章节中的那些一致：

_ : ∥ ⊢2+2 ∥⁺ ≡ DB.2+2
_ = refl

_ : ∥ ⊢2+2ᶜ ∥⁺ ≡ DB.2+2ᶜ
_ = refl

因此，我们证实了双向类型推理把装饰后的 Lambda 章节的 λ 项转换至 DeBruijn 章节中内在类型的项。

练习 `inference-multiplication` （推荐）

对你在 bidirectional-mul 练习中的乘法项应用双向推理，并证明推理得到的赋型可以擦除至 DeBruijn 章节中你的定义。

-- 请将代码写在此处。

练习 `inference-products` （推荐）

使用你在 bidirectional-mul 练习中的赋型规则，将双向推理扩充至包括积。此外扩充对应的擦除。

-- 请将代码写在此处。

练习 `inference-rest` （延伸）

使用你从练习 bidirectional-rest 中得到的规则，扩充双向推导规则，来包括 More 章节的剩余构造。此外扩充对应的擦除。

-- 请将代码写在此处。

Agda 中的双向推理

Agda 本身也使用双向推理。这解释了为什么构造子可以被重载，而其他定义的名称不可以——此处的重载指的是我们可以给不同类型的构造子使用相同的名称。构造子是由继承来赋型，而变量由生成来赋型，因此每个变量必须有唯一的类型。

Agda 中多数的顶层声明时函数，其由继承来赋型，也就是为什么 Agda 会对这些定义要求类型声明。一个由生成赋型的右手边的定义，比如说函数应用，则不需要类型声明。

answer = 6 * 7

Unicode

本章中使用了以下 Unicode：

↓  U+2193:  DOWNWARDS ARROW (\d)
↑  U+2191:  UPWARDS ARROW (\u)
∥  U+2225:  PARALLEL TO (\||)

绪论：推理规则作为算法

生成和继承类型

可靠性和完备性

导入

语法

项的例子

双向类型检查

练习 bidirectional-mul （推荐）

练习 bidirectional-products （推荐）

练习 bidirectional-rest （延伸）

前置需求

唯一的类型

查询语境中变量的类型

提升否定

生成和继承类型

测试项的例子

测试错误的例子

擦除

练习 inference-multiplication （推荐）

练习 inference-products （推荐）

练习 inference-rest （延伸）

Agda 中的双向推理

Unicode

练习 `bidirectional-mul` （推荐）

练习 `bidirectional-products` （推荐）

练习 `bidirectional-rest` （延伸）

练习 `inference-multiplication` （推荐）

练习 `inference-products` （推荐）

练习 `inference-rest` （延伸）