42

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

  1. 为什么全称量化被表示为依赖函数类型。∀(x:A).B(x)意思是“对于所有x类型A，都有一个类型的值B(x)”。因此，它被表示为一个函数，当给定任何x类型的值时，它返回一个类型的A值B(x)。
  2. 为什么存在量化被表示为依赖对类型。∃(x:A).B(x)意思是“存在一个x类型的类型A，它有一个类型的值B(x)”。因此，它表示为一对，其第一个元素是type的特定值，其第二个元素是 type 的值。xAB(x)

旁白：有趣的是，普遍量化总是与物质暗示一起使用，而存在量化总是与逻辑连词一起使用。

无论如何，关于依赖类型的维基百科文章指出：

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

对类型（通常是乘积类型）如何类似于不相交的联合（总和类型）？这一直让我感到困惑。

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

4

6 回答 6

32
于 2014-10-24T07:21:01.353 回答
12

依赖对使用类型和从该类型的值到另一种类型的函数进行类型化。从属对具有应用于第一值的第一类型值和第二类型值的对的值。

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)在哪里

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
于 2014-10-24T07:16:15.097 回答
11

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

我必须用Either a a代替来做这个例子Either a b，因为为了将后者表示为产品，我们需要 - 嗯 - 依赖类型。

于 2014-10-24T07:57:21.097 回答
9

好问题。该名称可能源自 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 是乘积的因素之一。

于 2014-10-24T07:05:58.813 回答
2

在这一点上，这可能与其他答案是多余的，但这是问题的核心：

对类型（通常是乘积类型）如何类似于不相交的联合（总和类型）？这一直让我感到困惑。

但是，什么是乘积而不是相等数字的总和？例如 4 × 3 = 3 + 3 + 3 + 3。

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

于 2014-10-26T18:12:14.973 回答
0

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

联产品是所有对象 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 次注入。

于 2014-10-25T09:46:00.127 回答