haskell - 为什么 Haskell 中的联积类型没有简单的语法？

Question

Haskell 中的产品类型很容易定义:

data Person String String 

是两种类型的产品。两种类型的联积是

type Shape=Either Circle Rectangle

但是，虽然产品很容易扩展到三种或更多类型，但对于联产品来说似乎并不那么简单。这种差异背后是否有理论依据，还是纯粹是技术原因？

Answer 1

data Apple = Gala | Fuji | PinkLady
data Orange = Navel | Blood
data Berry = Blueberry | Cranberry | Raspberry

data Fruit = Apple Apple
           | Orange Orange
           | Berry Berry

在这里， Fruit是 Apple 的联产品, Orange , 和 Berry 1.
请注意，未标记的联合不是副产品。
1:嗯，有点。 Fruit还包含一个额外的元素， ⊥ .见下文。
回复已编辑的问题

data Shape = Either Circle Rectangle

你可能的意思是:

type Shape = Either Circle Rectangle

如果您使用 data ，您已经使用名为 Either 的单个构造函数定义了一个产品类型。 .这是完全合法的。如果您使用 type ，您已经定义了 Shape作为 Either Circle Rectangle 的另一个名称，它是 Circle 的联积和 Rectangle .
Hask 与 Set
我们把 Haskell 中的类型和函数的范畴叫做 Hask。这是它的常用名称。它确实符合类别的定义，假设您不太仔细地观察这些我们称为计算机的有限事物。
让我们将 Hask 与类别 Set 进行比较。这是很自然的，因为 Hask 是一个具体的类别。比较 (,)在 Hask 中键入构造函数，在 Set 中使用笛卡尔积。如果我们想要 Int的产品和 Int ，我们得到:

⊥ ∈ (Int, Int) (在 Hask 中)，但是

⊥ ∉ Int ⨯ Int (在集合中)。

所以你可以看到类型构造函数 (,)与笛卡尔积不同，因为它包含一个额外的成员， ⊥ .我们可以重复不相交联合的论证:

⊥ ∈ Either Int Int (在 Hask 中)，但是

⊥ ∉ Int ⊔ Int (在集合中)。

在每种情况下，Hask 中的结构都包含一个附加元素， ⊥ ，Set 中的等效结构不具有。
Hask 与 Pointed 集
Hask 也不是指向集的范畴。首先，Hask 包含非指向集态射的态射。

对于每种类型 T在 Hask 中，我们可以构造一个函数 T -> T使得 f x = ⊥所有 x .因此，⊥必须是基点，如果 Hask 中的对象是指向集。请注意，所有此类 f是严格的函数。

然而，让g是任何懒惰的(这里的正确术语实际上是“非严格”)函数。根据严格性的定义，g ⊥ ≠ ⊥ .然而，对于#1，这与 Hask 是指向集的范畴的前提相矛盾。

此外，乘积和联积结构不同，类似于结构与 Set 结构的不同方式。对于产品，

(⊥, ⊥) ∈ (Int, Int) (在 Hask 中)，但是

(⊥, ⊥) ∉ Int ⊗ Int (在指向集合中)。

这源于态射的问题:在指向集合中，所有函数都是严格的——这包括构造函数，例如 (,) .联积也有同样的问题:

Left ⊥ ∈ Either Int Int (在 Hask 中)，但是

Left ⊥ ∉ Int ⊕ Int (在指向集合中)。

结论
因此，Set 和 Pointed Set 都不完全等同于类别 Hask。如 Hask 中所述在 Haskell Wiki 上的页面上，Haskell 中的“产品”和“副产品”类型根本不符合分类产品和副产品的定义。所以严格来说，Haskell 中不存在积和副积。
这就是坏消息。有好消息。

考虑 Hask 中的所有严格函数和严格构造函数。结果是 Hask 的一个子类别，它也是 Pointed Set 的一个子类别。该子类别是笛卡尔封闭类别。

考虑 Hask 中的所有全函数，如果两个函数对除 ⊥ 之外的每个输入产生相同的输出，则将它们视为相同的态射。 . (根据“total”的定义，这些输出不一定是 ⊥。)结果是 Set 的一个子类别。该子类别是笛卡尔封闭类别。

因此，只要您遵循正确的规则集，您仍然可以使用笛卡尔封闭类别。您甚至可以从两个不同的类别中进行选择!但是，如果您遵守这些规则，那么您正在使用 Haskell 的一个子集。
最后还有一个好消息。可以将严格函数修改为惰性函数，而无需更改整个程序的输出，假设程序的严格版本终止。所以你可以假装 ⊥不存在并使用类别理论完成一些工作，但仍然编写利用惰性求值的程序。
懒人总结
假装 Hask 有产品和副产品不会给你带来麻烦。