主体类型与主体定型 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协议发布
作者:爱让一切都对了
作者:爱让一切都对了
say thanks to so much for your site it assists a lot.