依赖类型：依赖对类型如何与不相交联合类似？ [英] Dependent Types: How is the dependent pair type analogous to a disjoint union?

问题描述

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

1. 为什么 universal quantification 被表示为一个依赖函数类型。 ∀（x：A）.B（x）表示所有 x 类型 A 有一个 B（x） 类型的值。因此，它被表示为一个函数，当给定任何值 x 类型 A 返回一个类型的值 B（x）。


2. 为什么存在量化表示为从属对类型。 ∃（x：A）.B（x）表示存在一个 x 类型 A ，其中存在类型 B（x）rdquo; 的值。因此它被表示为一对，它的第一个元素是特定的值 x 类型 A 第二个元素是 B（x）类型的值。
   

另外：另外值得注意的是，通用量化总是与重要含义，而存在量化总是与逻辑连词一起使用。

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

与依赖类型相反的是相关对类型，相关和类型或Σ-型即可。它类似于coproduct或不相交的联合。

它是怎样一个对类型（通常是产品类型）是类似的到一个不相交的联盟（这是一个总和类型）？这一直困扰着我。

另外，依赖函数类型如何与产品类型类似？

解决方案

使用类似的术语来描述Σ类型的结构以及它的值如何变得混乱。

A < （x：A）B（x）是 pair （a，b），其中a∈A和b∈B（a）。第二个元素的类型取决于第一个元素的值。

如果我们看一下Σ（x）的结构 ：A）B（x），它是 B（x）的一个不相交的联合（coproduct），适用于所有可能的x∈A B（x）是常数（独立于 x ），那么Σ（x ：A）B 将只是 B 的副本 A ，即A⨯B（两种产品）。

---

如果我们看看Π（x：A）的结构 ）B（x），它是所有可能的x∈A的 B（x）的产品。它的 values 可以被看作是 | A | -tuples，其中 a -th分量的类型是 B（a） B（x）是常量（独立于 x ），那么Π（x ：A）B 就是 A→B - 从 A 到 B ，即 B （ B 转换为 A ）使用set-theory表示法 - | A | 副本 B 。

---

所以Σ（x∈A）B（x）是一个 | A | -ary coproduct由 A 的元素索引，而Π（x∈A）B（x）是一个 | A | - 由 A 元素索引的产品。

I've been studying dependent types and I understand the following:

1. Why universal quantification is represented as a dependent function type. ∀(x:A).B(x) means “for all x of type A there is a value of type B(x)”. Hence it's represented as a function which when given any value x of type A returns a value of type B(x).
2. Why existential quantification is represented as a dependent pair type. ∃(x:A).B(x) means “there exists an x of type A for which there is a value of type B(x)”. Hence it's represented as a pair whose first element is a particular value x of type A and whose second element is a value of type B(x).

Aside: It's also interesting to note that universal quantification is always used with material implication while existential quantification is always used with logical conjunction.

Anyway, the Wikipedia article on dependent types states that:

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.

How is it that a pair type (which is normally a product type) is analogous to a disjoint union (which is a sum type)? This has always confused me.

In addition, how is the dependent function type analogous to the product type?

解决方案

The confusion arises from using similar terminology for the structure of a Σ type and for how its values look like.

A value of Σ(x:A) B(x) is a pair (a,b) where a∈A and b∈B(a). The type of the second element depends on the value of the first one.

If we look at the structure of Σ(x:A) B(x), it's a disjoint union (coproduct) of B(x) for all possible x∈A.

If B(x) is constant (independent of x) then Σ(x:A) B will be just |A| copies of B, that is A⨯B (a product of 2 types).

---

If we look at the structure of Π(x:A) B(x), it's a product of B(x) for all possible x∈A. Its values could be viewed as |A|-tuples where a-th component is of type B(a).

If B(x) is constant (independent of x) then Π(x:A) B will be just A→B - functions from A to B, that is Bᴬ (B to A) using the set-theory notation - the product of |A| copies of B.

---

So Σ(x∈A) B(x) is a |A|-ary coproduct indexed by the elements of A, while Π(x∈A) B(x) is a |A|-ary product indexed by the elements of A.

这篇关于依赖类型：依赖对类型如何与不相交联合类似？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！