haskell - 依赖类型 : How is the dependent pair type analogous to a disjoint union?

Question

我一直在研究依赖类型，并且了解以下内容:

1. 为什么 universal quantification被表示为依赖函数类型。 ∀(x:A).B(x)表示“对于所有人x类型 A有一个类型为 B(x) 的值”。因此，它被表示为一个函数，当给定任何值时 x类型 A返回 B(x) 类型的值.
2. 为什么 existential quantification被表示为依赖对类型。 ∃(x:A).B(x)表示“存在一个 x类型 A其中有一个类型为 B(x) 的值”。因此，它表示为一对，其第一个元素是特定值 x类型 A其第二个元素是 B(x) 类型的值.

旁白:值得注意的是，通用量化始终与 material implication 一起使用。而存在量化总是与 logical conjunction 一起使用.

无论如何，维基百科关于 dependent types 的文章指出:

The opposite of the dependent type is the dependent pair type, dependent sum type or sigma-type. It is analogous to the coproduct or disjoint union.

pair 类型(通常是乘积类型)与不相交并集(sum 类型)有何相似之处？这一直让我很困惑。

此外，依赖功能类型与产品类型有何相似之处？

Answer 1

混淆是由于对 Σ 类型的结构及其值的外观使用类似的术语而引起的。

Σ(x:A) B(x) 的值是一个对(a,b) em> 其中a∈A 和b∈B(a)。第二个元素的类型取决于第一个元素的值。

如果我们看Σ(x:A) B(x)的结构，它是以下的不相交并(余积) B(x) 对于所有可能的x∈A。

如果B(x)是常数(独立于x)，那么Σ(x:A) B将只是 |A| B 的副本，即 A⨯B(两种类型的乘积)。

<小时/>

如果我们看Π(x:A) B(x)的结构，它是B的乘积 (x) 对于所有可能的x∈A。它的值可以被视为|A|元组，其中a个组件的类型为B(a).

如果B(x)是常数(独立于x)，那么Π(x:A) B将只是 A→B - 从A到B的函数，即Bᴬ(B到B>A)使用集合论符号 - |A| B 副本的乘积。

<小时/>

因此 Σ(x∈A) B(x) 是一个由 A 元素索引的 |A| 元余积，而 Π(x∈A) B(x) 是一个 |A| 元乘积，由 A 的元素索引。