text: 在型別理論, 型別系統有主體型別t，當且僅當對於任意的型別環境A和表示式e，codice_1，都可以從t推導到u。例如λ演算codice_2，其主體型別t=α -&gt; α，α為型別變數，類似Java或C#的泛型型別變數。若有A|-λx.x: int -&gt; int，令α=int，則可以從主體型別t具體化為int -&gt; int。型別系統希望具有主體型別，因為它可以對錶達式確定一種單一型別，該單一型別可演化為該表示式的所有可能型別。如果型別系統沒有主體型別，則一個表示式可能有多個互不相容的型別。型別推導傾向於推導主體型別。ML具有主體型別屬性，ML表示式可以透過求出主體型別，該主體型別被演算法用到。然而，一些ML的擴充套件，如，會令主體型別喪失。要麼開發人員使用型別註解，要麼編譯器猜測型別。主體型別與主體定型不同。主體定型意思是，對於表示式e，型別環境A和型別t為主體定型對，當且僅當對於任意的型別環境B和型別u，都可從(A,t)推導到(B,u)。該推導過程一般使用變數具體化和子類替換。一般來說，有主體定型一定有主體型別；反之則不成立，例子是ML的let多型。
metadata: erhwenkuo/wikipedia-zhtw
metadata: 主體型別
metadata: https://zh.wikipedia.org/wiki?curid=6941762