主类型

在类型理论中，如果给定一个术语和一个环境，这个术语在这个环境中存在一个主类型，也就是一个类型，使得这个术语在这个环境中的所有其他类型都是主类型的实例，那么这个类型系统就被称为具有主类型属性。主类型属性对于类型系统来说是一个理想的属性，因为它提供了一种方法，使表达式在给定环境中的类型包含所有表达式的可能类型，而不是有几个不可比拟的可能类型。具有主类型属性的系统的类型推断通常会试图推断出主类型。例如，ML系统具有主类型属性，表达式的主类型可以通过Robinson的统一算法来计算，Hindley-Milner类型推理算法就使用了该算法。然而，对ML类型系统的许多扩展，如多态递归，可以使主类型的推理变得不可判定。

其他的扩展，如Haskell的广义代数数据类型，破坏了语言的主类型属性，需要使用类型注释或由编译器从几个选项中猜测出预定的类型。主类型属性要求，给定一个术语，存在一个类型（即一对上下文和一个类型），它是该术语所有可能类型的实例。主体类型属性可能会与原则类型属性相混淆，但两者是不同的。原则类型属性依靠上下文作为输入来确定类型，而原则类型属性则将上下文作为结果输出。