依赖类型：依赖对类型如何类似于不相交的联合？答案

【问题标题】：Dependent Types: How is the dependent pair type analogous to a disjoint union?依赖类型：依赖对类型如何类似于不相交的联合？
【发布时间】：2023-03-22 09:23:01
【问题描述】：

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

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

旁白：有趣的是，普遍量化总是与material implication一起使用，而存在量化总是与logical conjunction一起使用。

无论如何，dependent types 上的*文章指出：

依赖类型的对立面是依赖对类型、依赖和类型或sigma-type。它类似于联积或不相交并集。

pair 类型（通常是 product 类型）如何类似于不相交的 union（sum 类型）？这一直让我很困惑。

另外，依赖函数类型与产品类型有何相似之处？

【问题讨论】：

标签： haskell agda dependent-type idris curry-howard

【解决方案1】：

混淆源于对 Σ 类型的结构及其值的外观使用类似的术语。

Σ(x:A) B(x)的值是pair (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（2种的乘积）。

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

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

所以 Σ(x∈A) B(x) 是由 A 的元素索引的 |A|-ary coproduct，而 Π(x∈A) B(x) 是由 A 的元素索引的 |A| 元积。

【讨论】：

Σ(x:A) B(x) 类型不能被看作是 all possible x∈A 的 B(x) 的不相交并集。如果你为所有可能的 x∈A产生B(x)，你得到Π(x:A) B(x)。
@SassaNF：但不相交并集不需要您为所有可能的 x 生成 B(x)，就像 Either a b 不需要同时持有 a 和 @ 987654324@.
@Vitus 是的，这就是为什么“B(x) for all possible x∈A”需要澄清
@SassaNF：是吗？我觉得它很清楚地表明（例如） Σ(x∈Nat) B(x) 可以看作 B(0) ∨ B(1) ∨ B(2) ∨ ...
@SassaNF 将类型作为一个整体来讨论和它们的值是有区别的。让我们将类型视为集合。为了构造一个disjoint union 的集合，我们需要所有个索引。例如，由 B(1)={a,b}, B(2)={b,c}, B(3)={a,b} 索引的集合的不相交并集 A={1, 2, 3} 将是 {(a,1),(b,1), (b,2), (c,2), (a,3), (b,3)}。这样一个集合的每个成员只是一个索引和一个值。但是他们 product 的每个成员当然包含 all 值：{(a,b,a), (a,b,b), (a, c,a), (a,c,b), ...}.

【解决方案2】：

依赖对是用一个类型和一个从该类型的值到另一个类型的函数来键入的。从属对具有应用于第一个值的第一种类型的值和第二种类型的值的对的值。

data Sg (S : Set) (T : S -> Set) : Set where
  Ex : (s : S) -> T s -> Sg S T

我们可以通过展示 Either 如何规范地表示为 sigma 类型来重新捕获 sum 类型：它只是 Sg Bool (choice a b) where

choice : a -> a -> Bool -> a
choice l r True  = l
choice l r False = r

是布尔值的规范消除器。

eitherIsSg : {a b : Set} -> Either a b -> Sg Bool (choice a b)
eitherIsSg (Left  a) = Sg True  a
eitherIsSg (Right b) = Sg False b

sgIsEither : {a b : Set} -> Sg Bool (choice a b) -> Either a b
sgIsEither (Sg True  a) = Left  a
sgIsEither (Sg False b) = Right b

【讨论】：

我期待 choice l r True = r，匹配 Haskell 的 bool。

【解决方案3】：

以 Petr Pudlák 的回答为基础，以纯粹非依赖的方式看待这一点的另一个角度是注意类型 Either a a 与类型 (Bool, a) 同构。尽管后者乍一看是一个产品，但说它是 sum 类型是有道理的，因为它是 a 的两个实例的总和。

我必须使用Either a a 而不是Either a b 来做这个示例，因为要将后者表示为产品，我们需要——嗯——依赖类型。

【讨论】：

【解决方案4】：

好问题。该名称可能源自 Martin-Löf，他使用术语“集合族的笛卡尔积”来表示 pi 类型。例如，请参阅以下注释： http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf 关键是，虽然 pi 类型原则上类似于指数，但您始终可以将指数视为 n 元乘积，其中 n 是指数。更具体地说，非依赖函数 A -> B 可以看作是指数型 B^A 或无限积 Pi_{a in A} B = B x B x B x ... x B (A 次)。从这个意义上说，从属乘积是一个潜在的无限乘积 Pi_{a in A} B(a) = B(a_1) x B(a_2) x ... x B (a_n)（对于 A 中的每个 a_i 一次）。

依赖和的推理可能类似，因为您可以将乘积视为 n 元和，其中 n 是乘积的因素之一。

【讨论】：

【解决方案5】：

此时这可能与其他答案是多余的，但这是问题的核心：

pair 类型（通常是 product 类型）如何类似于不相交的 union（sum 类型）？这一直让我很困惑。

但是，除了相等数字的总和之外，什么是乘积？例如4 × 3 = 3 + 3 + 3 + 3。

同样的关系也适用于类型、集合或类似事物。事实上，非负整数只是有限集的反分类。选择数字上的加法和乘法的定义，使得不相交的集合的基数是集合的基数之和，并且集合乘积的基数等于集合的基数的乘积。事实上，如果你用“羊群”代替“集合”，这可能就是算术的发明方式。

【讨论】：

【解决方案6】：

首先，看看什么是联产品。

联产品是所有对象 B_i 的终端对象 A，因此对于所有箭头 B_i -> X，有一个箭头 B_i -> A，以及一个唯一的 A -> X，因此相应的三角形可以交换。

您可以将其视为带有 B_i 的 Haskell 数据类型 A -> A 是一组具有单个 B_i 类型参数的构造函数。很明显，对于每个 B_i -> X 都可以从 A -> X 提供一个箭头，这样通过模式匹配您可以将该箭头应用于 B_i 以获得 X。

与 sigma 类型的重要联系是 B_i 中的索引 i 可以是任何类型，而不仅仅是自然数类型。

与上述答案的重要区别在于，对于该类型的每个值 i，它不必具有 B_i：一旦定义了 B_i ∀ i，您就有了一个总函数。

从 Petr Pudlak 的回答中可以看出，Π 和 Σ 之间的区别在于，对于 Σ，元组中的某些值 B_i 可能缺失 - 对于某些 i，可能没有对应的 B_i。

Π 和 Σ 之间的另一个明显区别是 Π 通过提供从乘积 Π 到每个 B_i 的第 i 个投影来表征 B_i 的乘积（这就是函数 i -> B_i 的含义），但 Σ 提供箭头反过来 - 它提供从 B_i 到 Σ 的第 i 次注入。

【讨论】：