主体类型

在类型理论, 类型系统有主体类型t，当且仅当对于任意的类型环境A和表达式e，A |- e :u，都可以从t推导到u。

例如λ演算λx.x，其主体类型t=α -> α，α为类型变量，类似Java或C#的泛型类型变量。若有A|-λx.x: int -> int，令α=int，则可以从主体类型t具体化为int -> int。

类型系统希望具有主体类型，因为它可以对表达式确定一种单一类型，该单一类型可演化为该表达式的所有可能类型。如果类型系统没有主体类型，则一个表达式可能有多个互不兼容的类型。类型推导倾向于推导主体类型。

ML具有主体类型属性，ML表达式可以通过合一求出主体类型，该主体类型被Hindley–Milner type inference（英语：Hindley–Milner type inference）算法用到。然而，一些ML的扩展，如polymorphic recursion（英语：polymorphic recursion），会令主体类型丧失（undecidable）。其他一些扩展，如Haskell的generalized algebraic data type（英语：generalized algebraic data type），也令主体类型丧失（destroy）。要么开发人员使用类型注解，要么编译器猜测类型。

主体类型与主体定型不同。主体定型意思是，对于表达式e，类型环境A和类型t为主体定型对，当且仅当对于任意的类型环境B和类型u（A、B有相同的变量），都可从(A,t)推导到(B,u)。该推导过程一般使用变量具体化和子类替换。^[1]

一般来说，有主体定型一定有主体类型；反之则不成立，例子是ML的let多态。