型別代數中的自然數

我們可以在 Haskell 型別和自然數之間建立連線。可以將這種連線分配給每種型別的居民數量。

有限聯合型別

對於有限型別，只要看到我們可以根據建構函式的數量為每個數字指定一個自然型別就足夠了。例如：

type Color = Red | Yellow | Green

將是 3 。而 Bool 型別將是 2 。

type Bool = True | False

同構性的唯一性

我們已經看到多個型別對應於單個數字，但在這種情況下，它們將是同構的。這就是說會有一對態射 f 和 g，其構成將是連線這兩種型別的身份。

f::a -> b
g::b -> a

f . g == id == g . f

在這種情況下，我們會說型別是同構的。只要它們是同構的，我們將在代數中考慮兩種相等的型別。

例如，第二個的兩個不同表示是完全同構的：

type Bit  = I    | O
type Bool = True | False

bitValue::Bit -> Bool
bitValue I = True
bitValue O = False

booleanBit::Bool -> Bit
booleanBit True  = I
booleanBit False = O

因為我們可以看到 bitValue . booleanBit == id == booleanBit . bitValue

一和零

數字 1 的表示顯然是隻有一個建構函式的型別。在 Haskell 中，這種型別的規範是 ()，稱為 Unit。只有一個建構函式的每個其他型別都與 () 同構。

我們的 0 表示將是一個沒有建構函式的型別。這是 Haskell 中的 Void 型別，如 Data.Void 中所定義。這相當於一個無人值守的型別，沒有資料建構函式：

data Void