为什么Haskell中没有简单的语法来表示余积类型？

Question

为什么Haskell中没有简单的语法来表示余积类型？

haskellfunctional-programmingcomputer-sciencecategory-theory

11

Haskell中的产品类型易于定义：

data Person String String

是两种类型的乘积。两种类型的余积是

type Shape=Either Circle Rectangle

但是，尽管该产品很容易扩展到三种或更多种类型，但对于余积来说似乎并不那么简单。这种差异背后是否有理论基础，还是纯粹的技术原因？

- Mozibur Ullah

1

也许我想错了，但我认为余积类型也很简单：data Foo = Bar Int | Baz String。 - Owen

1

@MoziburUllah：那不是重点。Int和String是类型，而Foo是Int和String的余积。 - Dietrich Epp

@owen：我注意到的另一点是，你使用了“Either”作为余积，正如你和Dietrich指出的语法是我首先想到的。在Haskell类型系统中，“undefined”的确切状态是什么，我刚刚接触它（我对范畴论比对Haskell更熟悉）。 - Mozibur Ullah

@Dietrich：你说(Int,Int)包含未定义是什么意思？你所说的“包含”，我知道它的朴素含义。但从理论上讲，我希望它是从终端元素的同态，但根据那个维基页面，它也没有这个。 - Mozibur Ullah

@MoziburUllah：是的，那是一个标记联合。如果忽略 ⊥，标记联合就是余积。 - Dietrich Epp

显示剩余13条评论

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Dietrich Epp · Accepted Answer

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的余积¹。

请注意，非标记联合体不是余积。

¹: 嗯，有点。 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（在Set中）。

因此，您可以看到类型构造函数(,)与笛卡尔积不同，因为它包含一个额外的成员⊥。我们可以重复异构并集的论证：

⊥ ∈ Either Int Int（在Hask中），但是
⊥ ∉ Int ⊔ Int（在Set中）。

在每种情况下，Hask中的结构包含一个额外的元素⊥，而Set中的等效结构则没有。

Hask与指向集合的区别

Hask也不是指向集合的范畴。首先，Hask包含不是指向集合的态射。

对于 Hask 中的每种类型 T，我们可以构造一个函数 T -> T，使得对于所有的 x，都有 f x = ⊥。因此，如果 Hask 中的对象是指向集合（pointed sets），那么 ⊥ 必须是基点。请注意，所有这样的 f 都是严格函数。
然而，让 g 成为任何惰性（正确的术语实际上是“非严格”）函数。根据严格性的定义，g ⊥ ≠ ⊥。但是，根据第一条，这与 Hask 是指向集合范畴的前提相矛盾。

另外，积和余积结构不同，类似于 Set 的结构不同。对于积：

(⊥, ⊥) ∈ (Int, Int)（在 Hask 中），但是
(⊥, ⊥) ∉ Int ⊗ Int（在 Pointed Set 中）。

这是由于态射的问题引起的：在指向集合中，所有函数都是严格的——包括构造函数，如(,)。余积也有同样的问题：

Left ⊥ ∈ Either Int Int（在Hask中），但
Left ⊥ ∉ Int ⊕ Int（在指向集合中）。

结论

因此，集合和指向集合都不完全等同于范畴Hask。正如Haskell Wiki上Hask页面所述，在Haskell中，“乘积”和“余积”类型根本不符合范畴乘积和余积的定义。因此，严格来说，在Haskell中不存在乘积和余积。

这是坏消息。好消息是还有救。

考虑 Hask 中的所有严格函数和严格构造函数。结果是 Hask 的子范畴，也是 Pointed Set 的子范畴。这个子范畴是笛卡尔闭范畴。

考虑 Hask 中的所有全函数，并将两个函数视为相同的态射，如果它们产生除 ⊥ 以外的每个输入相同的输出。（根据“总”的定义，这些输出必须不是 ⊥）。结果是 Set 的子范畴。这个子范畴是笛卡尔闭范畴。

只要遵守正确的规则，您仍然可以使用笛卡尔闭范畴。您甚至可以选择两个不同的类别来使用！但是，如果您按照这些规则操作，则正在使用 Haskell 的子集。

严格函数可以修改为惰性函数，而不会改变整个程序的输出，假设程序的严格版本终止。因此，您可以假装 ⊥ 不存在，并使用范畴论完成一些工作，但仍然编写利用惰性评估的程序。

懒人摘要：可以使用笛卡尔闭范畴，可以选择两个不同的类别，可以假装 ⊥ 不存在并使用范畴论完成一些工作，但仍然编写利用惰性评估的程序。

假设Hask有产品和余积，不会给你带来麻烦。