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 的产物