函数 (类型论)

函数类型是映射在类型论中的类比 (见 集合论类比), 一般记作 $A\to B$, 它在简单类型论和依值类型论里都可以定义, 且定义是一样的. 注意函数类型不是 $\Pi$ 类型, 即使有时我们认为函数类型是 $\Pi$ 类型的特例. 可以用 “函数” 指代函数类型的实例.

在线性类型论中, 线性的函数记作 $A⊸B$, 这个记号叫做 “棒棒糖”, 又见线性逻辑.

1类型规则

从类型 $A$ 到 $B$ 的函数记作 $A\to B$.

$$\frac{\Gamma ⊢A\mathrm{type}\Gamma ⊢B\mathrm{type}}{\Gamma ⊢(A\to B)\mathrm{type}}$$

构造规则

该规则又叫抽象或 $\lambda$-抽象.

$$\frac{\Gamma ,x:A⊢u:B}{\Gamma ⊢\lambda x.u:A\to B}$$

有时我们省略变量名 (尤其是在讨论范畴语义的时候) , 写成:

$$\frac{\Gamma ,A⊢u:B}{\Gamma ⊢\lambda .u:A\to B}$$

消去规则

该规则又叫应用或 $\lambda$-应用.

$$\frac{\Gamma ⊢u:A\to B\Gamma ⊢v:A}{\Gamma ⊢\mathrm{ap}(u,v):B}$$

其中:

$$\frac{\Gamma ,x:A⊢u:B\Gamma ⊢v:A}{\Gamma ⊢\mathrm{ap}(\lambda .u,v)=u[x\mapsto v]:B}$$

该规则又叫计算规则或者 $\beta$ 规则.

记号 $u[x\mapsto v]$ 代表替换操作.

除此之外, 还有如下唯一性规则, 又叫 $\eta$ 规则:

$$\frac{\Gamma ⊢f:A\to B}{\Gamma ⊢f=\lambda x.fx:A\to B}$$

2性质

集合论类比

集合论中的 “映射” 和类型论中的函数有一个本质的不同, 即集合论中的映射是由 “函数关系” 定义的, 而类型论中的函数是由表达式 (或者说 “公式”) 来定义的. 如果把类型类比为集合, 那么类型论函数总是能转换成函数关系, 但函数关系却并不总是能转换成表达式. 这意味着类型论函数不具备集合论函数中的两个重要性质:

•	函数外延性, 即对应每个函数关系的函数是唯一的. 在类型论中, 该性质不直接成立, 比如 $\lambda x.x+1$ 和 $\lambda x.1+x$ 在类型论中依然是可以区分的函数. 某些性质很好的类型论中, 可以将这些函数视为在相等类型意义上相等的. 同伦类型论的相关研究用多种方法解决了这个问题, 见泛等公理和立方类型论.

•	函数概括性, 即对应每个函数关系都存在 (至少) 一个函数. 在类型论中, 可以通过如下公理来拥有这个性质: 对于二元关系 $R$, 若$$\forall (a:A),\exists !(b:B),R(a,b)$$则$$\exists f:A\to B,\forall (a:A),R(a,f(a))$$这个 $f$ 便是那个至少存在的函数, 但因为这是公理, 所以它不能像普通的类型论函数一样计算.

3范畴语义

•	在简单类型论的范畴语义中, 函数类型对应 积闭范畴里的内态射, 函数应用的规则对应求值映射.

•	在依值类型论的范畴语义中, 函数类型对应局部积闭范畴里的俯范畴的内态射.

4相关概念

•	$\Pi$ 类型是依值类型论中函数类型的升级.
•	积类型可以借助函数类型定义消去规则.

术语翻译

函数类型 • 英文 function type • 法文 type des fonctions • 拉丁文 typus functionum

抽象 • 英文 abstraction

应用 • 英文 application

函数概括性 • 英文 function comprehension