LEAN 类型理论之注解（Annotations of LEAN Type Theory）—— 归纳类型（Inductive Type）浅析

        归纳类型（Inductive Type）的核心是，该类型是基于归纳原则（Inductive principle，base case & inductive step）来定义的。简单来说，在定义归纳类型时，会使用其归纳类型自身。如下图的类型等式（Type Equation），K 是其定义体（The body of Definition），调用其类型自身：        

        这个类型等式（Type Equation）是理解归纳类型（Inductive Type）的最关键。

        该类型等式的意思是，有这么一个类型，记为 μt:F.K， 与  其定义体 K 中的类型变量 t 替换（substitute）成自身后的类型，记为 K [ μt:F.K / t ]，等价（Equivalence）。

        要解该类型等式，即找到该等式的解（Solution），就是要找到一个类型，能满足该等式。 那么，分析上述类型等式（Type Equation），有：

        1. μ，抽象出一个类型为F 的 类型变量 t，（Type variable），如 λ 的作用，是抽象出一个值变量（variable）。

        2. K，可以看作是一个类型函数（Type Function）的函数体，其内部使用了类型为F 的 类型变量 t。

        3. 在等式的右边可以看出，类型变量 t 所引用的类型就是正在被定义的类型本身，即 μt:F.K 。

        因此，当要定义的类型，是归纳类型（Inductive Type）时，就可以满足上述类型等式。

        严格来说，上述类型等式，定义了递归类型（Recursive Type），包括了归纳类型（Inductive Type），以及共归纳类型（Coinductive Type），在LEAN的语境里，统称为归纳类型（Inductive Type）。

        其区别在于，归纳类型（Inductive Type）必须存在基本构建函数（Base case constructor），即不需要依赖被定义的归纳类型的本身即可以构建其正规元素（Canonical Element），以此作为其归纳步骤（Inductive step）的出发点或落脚点，如自然数类型（Nat)。

        而，共归纳类型（Coinductive Type）则没有基本构建函数（Base case constructor），如 流类型（Stream）。

        在正式研究LEAN对归纳类型（Inductive Type）的定义前，我们先通过自然数的例子，直观感受一下。

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

        上面代码是LEAN对自然数（Nat）的定义:

        1. inductive，关键字，申明这是一个归纳类型的定义，该归纳类型的名字叫 Nat。

        2. where，关键字，引出后面的内容，是该类型的定义体。

        3. 符号 |， 指示这是该类型的构建函数（constructor），用以构建该类型的正规元素（Canonical Element）。

        4. zero : Nat，这个自然数归纳类型的基本构建函数（Base case constructor），其没有输入，即无输入函数，表示一个常量，其类型为自然数，即正在定义的类型本身。

        5. succ (n : Nat) : Nat，这是其归纳步骤的构建函数（constructor of inductive step），其输入是自然数，即正在定义的类型的值；其输出是另一个自然数。succ 是 successor的缩写，即其含义是，给定的输入的自然数的下一个自然数。

        通过，上面的说明，可以清晰的看到，该归纳类型在定义自己的时候，使用了自己本身，尤其，体现在归纳步骤（Inductive Step）上，即 succ 构建函数（constructor）。

        将 K 定义为  （ zero : t ） + （ succ (n : t ) : t  ），μt:F.K ≡ Nat，就有

                μt:F.K ≃ K [ μt:F.K / t ]

                   =>  Nat ≃ K [ Nat / t ]

                   =>  Nat ≃ （（ zero : t ） + （ succ (n : t ) : t  ）） [ Nat / t ]

                   =>  Nat ≃ （（ zero : Nat ） + （ succ (n : Nat ) : Nat  ））

        此时，可以清楚看到，类型等式的左边是正在定义的归纳类型 Nat；右边是其构建函数（constructor）。且与LEAN中定义归纳类型（Inductive Type）Nat 的语法结构相对应。这是，因为 LEAN的语法 是为了 完整地 表达 LEAN类型理论。

口

        顺便给个共归纳类型（Coinductive Type），流类型（Stream）：

inductive Stream t where
| cons (head: t) (tail: Stream t): Stream t