Hask 中的型別產品

分類產品

在類別理論中，兩個物體 X ， Y 的乘積是另一個具有兩個投影的物體 Z ： π1：Z→X 和 π2：Z→Y ; 使得來自另一個物體的任何其他兩個態射通過這些投射唯一地分解。換句話說，如果存在 f 1：W→X 和 f 2：W→Y ，則存在唯一的態射 g：W→Z ，使得 π1○g = f 1 和 π2○g = f 2 。

哈斯克的產品

這轉化為 Hask Haskell 的型別的類別如下，Z 是 A，B 時的產品：

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

按照上述規律**，兩種型別** A，B 的產品型別是 (A,B) 的兩種型別的元組，兩個投影是 fst 和 snd。我們可以檢查它是否符合上述規則，如果我們有兩個函式 f1 :: W -> A 和 f2 :: W -> B 我們可以唯一地分解它們如下：

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

我們可以檢查分解是否正確：

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

同構性的唯一性

(A,B) 作為 A 和 B 的產品的選擇並不是唯一的。另一個合乎邏輯的等價選擇是：

data Pair a b = Pair a b

而且，我們也可以選擇 (B,A) 作為產品，甚至是 (B,A,())，我們也可以按照規則找到類似上面的分解函式：

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

這是因為產品不是唯一的，而是同構的獨特之處。A 和 B 的每兩個產品不必相等，但它們應該是同構的。舉個例子，我們剛剛定義的兩個不同的產品 (A,B) 和 (B,A,()) 是同構的：

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

分解的唯一性

值得注意的是，分解函式也必須是唯一的。有些型別遵循產品所需的所有規則，但分解並不是唯一的。舉個例子，我們可以嘗試使用 (A,(B,Bool)) 作為 A 和 B 的產品：fst fst . snd：

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

我們可以檢查它是否有效：

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

但問題是我們可以編寫另一個分解，即：

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

並且，由於分解不是唯一的，(A,(B,Bool)) 不是 Hask 中的 A 和 B 的產物