主体类型与主体定型 principle type and principle typing

2020年3月3日

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

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

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

ML语言具有主体类型属性,ML表达式可以通过Robinson’s unification algorithm求出主体类型,该主体类型被Hindley–Milner type inference算法用到。然而,一些ML的扩展,如polymorphic recursion,会令主体类型丧失。其他一些扩展,如[[Haskell]]的generalized algebraic data type,也令主体类型丧失。要么开发人员使用类型注解,要么编译器猜测类型。

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

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

本文依照CC-BY-SA 3.0协议发布
作者:爱让一切都对了

参考资料

https://en.wikipedia.org/wiki/Principal_type