我一直在研究依赖类型，我了解以下内容：
- Why 通用量化 https://en.wikipedia.org/wiki/Universal_quantification被表示为依赖函数类型。
∀(x:A).B(x) means “对全部x类型的A有一个类型的值B(x)”。因此，它被表示为一个函数，当给定时any value x类型的A返回类型的值B(x).
- Why 存在量化 https://en.wikipedia.org/wiki/Existential_quantification被表示为依赖对类型。
∃(x:A).B(x) means “存在一个x类型的A有一个 type 的值B(x)”。因此它被表示为一对，其第一个元素是一个特定的 value x类型的A并且其第二个元素是类型的值B(x).
Aside:同样有趣的是，通用量化总是与实质性影响 https://en.wikipedia.org/wiki/Material_conditional而存在量化总是与逻辑连接 https://en.wikipedia.org/wiki/Logical_conjunction.
不管怎样，维基百科上的文章依赖类型 https://en.wikipedia.org/wiki/Dependent_type指出：
与依赖类型相反的是依赖对类型, 依赖和类型 or 西格玛型。它类似于余积或不相交并。
配对类型（通常是乘积类型）如何类似于不相交联合（这是求和类型）？这一直让我很困惑。
另外，依赖功能类型与产品类型有何相似之处？
混淆是由于对 Σ 类型的结构及其值的外观使用类似的术语而引起的。
A value of Σ(x:A) B(x) is a pair (a,b) where a∈A and b∈B(a)。第二个元素的类型取决于第一个元素的值。
如果我们看一下结构 of Σ(x:A) B(x)， 它是不相交的联合（副产品）B(x)为了一切可能x∈A.
If B(x)是常数（独立于x) then Σ(x:A) B将只是|A|的副本B， 那是A⨯B（两种类型的产品）。
如果我们看一下结构 of Π(x:A) B(x)， 它是product of B(x)为了一切可能x∈A. Its values可以被视为|A|-元组，其中a-th 组件的类型B(a).
If B(x)是常数（独立于x) then Π(x:A) B将只是A→B- 函数来自A to B， 那是Bᴬ (B to A）使用集合论符号 - 的乘积|A|的副本B.
So Σ(x∈A) B(x) is a |A|-ary 余积由以下元素索引A, while Π(x∈A) B(x) is a |A|- 由以下元素索引的乘积A.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
