函数 (类型论)
函数类型是映射在类型论中的类比 (见 集合论类比), 一般记作 , 它在简单类型论和依值类型论里都可以定义, 且定义是一样的. 注意函数类型不是 类型, 即使有时我们认为函数类型是 类型的特例. 可以用 “函数” 指代函数类型的实例.
在线性类型论中, 线性的函数记作 , 这个记号叫做 “棒棒糖”, 又见线性逻辑.
1类型规则
从类型 到 的函数记作 .
构造规则
该规则又叫抽象或 -抽象.
有时我们省略变量名 (尤其是在讨论范畴语义的时候) , 写成:
消去规则
该规则又叫应用或 -应用.
其中:
该规则又叫计算规则或者 规则.
记号 代表替换操作.
除此之外, 还有如下唯一性规则, 又叫 规则:
2性质
集合论类比
集合论中的 “映射” 和类型论中的函数有一个本质的不同, 即集合论中的映射是由 “函数关系” 定义的, 而类型论中的函数是由表达式 (或者说 “公式”) 来定义的. 如果把类型类比为集合, 那么类型论函数总是能转换成函数关系, 但函数关系却并不总是能转换成表达式. 这意味着类型论函数不具备集合论函数中的两个重要性质:
• | 函数外延性, 即对应每个函数关系的函数是唯一的. 在类型论中, 该性质不直接成立, 比如 和 在类型论中依然是可以区分的函数. 某些性质很好的类型论中, 可以将这些函数视为在相等类型意义上相等的. 同伦类型论的相关研究用多种方法解决了这个问题, 见泛等公理和立方类型论. |
• | 函数概括性, 即对应每个函数关系都存在 (至少) 一个函数. 在类型论中, 可以通过如下公理来拥有这个性质: 对于二元关系 , 若则这个 便是那个至少存在的函数, 但因为这是公理, 所以它不能像普通的类型论函数一样计算. |
3范畴语义
• |
• |
4相关概念
• | 类型是依值类型论中函数类型的升级. |
• | 积类型可以借助函数类型定义消去规则. |
术语翻译
函数类型 • 英文 function type • 法文 type des fonctions • 拉丁文 typus functionum
抽象 • 英文 abstraction
应用 • 英文 application
函数概括性 • 英文 function comprehension