主體類型

在類型理論, 類型系統有主體類型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算法用到。然而，一些ML的擴展，如polymorphic recursion，會令主體類型喪失（undecidable）。其他一些擴展，如Haskell的generalized algebraic data type，也令主體類型喪失（destroy）。要麼開發人員使用類型註解，要麼編譯器猜測類型。

主體類型與主體定型不同。主體定型意思是，對於表達式e，類型環境A和類型t為主體定型對，當且僅當對於任意的類型環境B和類型u（A、B有相同的變量），都可從(A,t)推導到(B,u)。該推導過程一般使用變量具體化和子類替換。

一般來說，有主體定型一定有主體類型；反之則不成立，例子是ML的let多態。