類型（類型理論）

在被稱為類型理論的數理邏輯和計算機科學領域，類型是一個類型構造器的類型，或者不那么常見的是一個高階類型操作符的類型。一個類型系統本質上是一個簡單類型的lambdacalculus，它有一個原始的類型，表示為并稱為類型，它是任何不需要任何類型參數的數據類型的類型。類型有時被混亂地描述為（數據）類型的類型，但它實際上更像是一個算術指定器。在語法上，我們很自然地認為多態類型是類型構造器，因此非多態類型是空態類型構造器。但是所有的空類型構造器，也就是所有的單態類型，都有相同的、最簡單的種類；即由于高階類型操作符在編程語言中并不常見，在大多數編程實踐中，種類被用來區分數據類型和用于實現參數化多態性的構造函數的類型。類型出現在語言中，無論是明確的還是隱含的，這些語言的類型系統以程序可訪問的方式解釋參數多態性，例如C++、Haskell和Scala。，發音為type，是所有數據類型的種類，被視為空類型構造器，在這里也被稱為適當類型。這通常包括函數式編程語言中的函數類型。{displaystyle*rightarrow*}是單數類型的種類。是二元類型構造函數的種類，例如一對類型構造函數，也是函數類型構造函數的種類，不要與它的應用結果相混淆，它本身是一個函數類型，因此是種類是指從單數類型構造器到適當類型的高階類型運算符的種類。Haskell中的種類。Haskell98的類型系統正好包括兩種類型。發音的類型是所有數據類型的種類。

{displaystylek_{1}rightarrowk_{2}}是單數類型構造函數的種類。是一個單數類型構造函數的類型，它接收一個類型為一個居住的類型（在Haskell中稱為適當的類型）是一個有值的類型。例如，忽略那些使情況復雜化的類型，4是一個Int類型的值，而[1,2,3]是一個[Int]類型的值（Ints的列表）。因此，Int和[Int]有種但任何函數類型也是如此，例如，Int->Bool或甚至Int->Int->Bool。一個類型構造函數接受一個或多個類型參數，當提供足夠的參數時產生一個數據類型，也就是說，由于currying，它支持部分應用。

標準Haskell不允許多態的種類。這與類型上的參數化多態性相反，在Haskell中支持這種多態性。例如，在下面的例子中。，除非類型明確指出了其他情況。因此，類型檢查器將拒絕以下對Tree的使用。GHC有一個擴展PolyKinds，它和KindSignatures一起，允許多態的類型。