NOTE: 型別論中的指數意義

首先定義型別 \(1\) 是只有唯一一個元素的型別，我們不關心這個元素到底叫做什麼。同理 Bool 就會是 \(2\)，因為它有兩個元素，而其他一樣有兩個元素的型別是同構。

1. 乘法

那麼乘法可以視為 Pair ，記作 \(A \times B\)。可以由檢查 \(1 \times A\) 跟 \(A \times 1\) 是否跟 \(A\) 同構來檢驗這個想法。

1.1. 檢驗

以下的 Haskell 程式裡， () 是 \(1\) 型別，小寫的型別則是型別變數，恰巧方便讓兩個定義適用於任何型別參數。

pairOf1A :: ((), a) -> a
pairOf1A ((), v) = v

pairOfA1 :: (a, ()) -> a
pairOfA1 (v, ()) = v

可以發現兩個函數的反轉都很容易實現，因此現在我們可以說 \(1 \times A\) 確實跟 \(A\) 同構。

2. 指數

有了乘法，就可以按照 \(a^b = a \times \cdots \times a(重複 b 次)\) 定義出指數。關鍵是這樣的型別雖然存在，但是意義為何呢？舉實際案例，\(bool^3\) 要代表什麼？一個可行的方案就是按照元素數量的想法，認為 \(bool^3\) 就是 8bits 的資料型別。 Ada 實際採用的 modular type，就是類似的定義。