UP | HOME

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,就是類似的定義。

Date: 2022-10-18 Tue 00:00
Author: Lîm Tsú-thuàn