记名类型论

记名类型论指那些通过类型的名字来区分类型的类型论. 这常见于那些支持归纳类型的类型论. 例如, 两个名字不同但定义一模一样的归纳类型若被认为是不同的, 那么该类型论就是记名的.

如果类型论总是按照类型的定义来确定类型是否相等, 则可以说它是不记名类型论. 若将某类型论中的所有归纳类型翻译为 W 类型, 则该类型论对于归纳类型就是不记名的, 因为这个翻译过程中类型的名字丢失了.

在有复杂的类型递归、或者存在难以进行翻译的复杂类型的类型论中, 很难实现判断类型相等的算法. 直接通过名字来判断类型等价是更经济的行为.

在描述类型论时, 可以将记名、不记名的区分具体到每个形成规则上, 因为大部分记名类型论都只有一部分 (而不是全部) 形成规则是涉及记名的.

1相关概念

•	注意区分 “名字” 和变量: 后者可以视为 “用于被替换” 的名字, 而前者不强调这点.

•	记名集是研究名字的形式理论,

•	局部无名表示是混合 De Bruijn 编号和记名方法的变量实现方式.

术语翻译

记名类型论 • 英文 nominal type theory

不记名类型论 • 英文 structural type theory