类型代数中的自然数

我们可以在 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