简化归纳族

简化归纳族是使用模式匹配的语法来定义归纳族的手法. 它失去了定义相等类型及类似情况的能力, 换来了更简单的语义 (更加接近函数).

1定义

定义 1.1. $\Gamma ⊢p:A$ 在满足以下条件时是一个匹配子:

•	不含消去规则、形成规则或函数类型的构造规则,

•

允许出现自由变量,

•	自由变量是线性的, 即没有重复的变量.

此处只考虑了有归纳类型、宇宙、$\Pi$ 类型、$\Sigma$ 类型的类型论. 若对类型论进行扩展, 则这些限制可能也需要进行对应的调整.

定义 1.2. 简化归纳族由如下数据组成:

•	一个类型 $\Gamma ⊢D:A\to \mathcal{U}$, 类似归纳族, 其中 $A$ 是任意类型,

•	一组构造子 $\Gamma ⊢p\mapsto \mathrm{co}{\mathrm{n}}_{\mathrm{i}}{C}_i$, 其中: ∘ $\Gamma ,FV(p)$ 为将 $\Gamma$ 扩展后的某个新语境, ∘ $\Gamma ,FV(p)⊢p:A$ 是一个匹配子 (1.1), ∘ $\Gamma ,FV(p)⊢C_i$ 为满足严格正性的类型. 定义构造子的类型如下: $$\Gamma ⊢\mathrm{co}{\mathrm{n}}_{\mathrm{i}}:\prod _{x:FV(p)}\prod _{y:C_i}D(p)$$

•	模式匹配作为消去子.

2例子

定义 2.1. 如下类型是简化归纳族版本的有限集合类型:

•	$\mathrm{Fin}:\mathbb{N}\to \mathcal{U}$ 为类型,

•	$s(n)\mapsto f01$ 为构造子之一, 其中 $1$ 是单位类型,

•	$s(n)\mapsto \mathrm{fs}(\mathrm{Fin}n)$ 为构造子之二.

3性质

引理 3.1. 任何能用简化归纳族表达的类型, 都可以转化为另一个等价的归纳族.

这意味着归纳族的语义可以应用到简化归纳族上.

4参考资料

•	Tesla Zhang (2021). “A Simpler Encoding of Indexed Types”. arXiv: 2103.15408. (doi)

术语翻译

简化归纳族 • 英文 simpler indexed types

匹配子 • 英文 pattern