依赖类型:依赖对类型如何类似于不相交联合？

Question

我一直在研究依赖类型,我理解以下内容:

1. 为什么通用量化表示为依赖函数类型.?(x:A).B(x)表示"对于所有x类型,A都有类型的值B(x)".因此它表示为其中,当给定一个功能的任何值x类型的A返回类型的值B(x).
2. 为什么存在量化表示为依赖对类型.?(x:A).B(x)表示"存在有x类型A值的类型B(x)".因此,它表示为一对,其第一个元素是类型的特定值x,A其第二个元素是类型的值B(x).

旁白:值得注意的是,通用量化总是与物质含义一起使用,而存在量化始终与逻辑联合使用.

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

与从属类型相反的是从属对类型,从属和类型或西格玛类型.它类似于副产品或不相交的联合.

对类型(通常是产品类型)是如何类似于不相交的联合(这是一种和型)？这一直困扰着我.

此外,依赖函数类型如何与产品类型类似？

Answer 1

混淆源于对Σ类型的结构使用类似的术语以及它的值如何.

甲值的Σ(X:A)B(x)的是一对 (A,B)其中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 | 元组,其中一个组分是类型B(A) .

如果B(x)是常数(与x无关)那么Π(x:A)B将只是A→B - 从A到B的函数,即使用集合理论符号的Bᴬ(B到A) - 产品的| A | B的副本.

所以Σ(x∈A)B(x)是| A | -al副产品由A的元素索引,而Π(x∈A)B(x)是a | A | - 由A元素索引的产品.

Answer 2

依赖对使用类型和函数键入,从该类型的值到另一种类型.从属对具有第一类型的值和应用于第一值的第二类型的值的对的值.

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

我们可以通过展示Either规范表达为西格玛类型来重新获得总和类型:它就在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

Answer 3

在PetrPudlák的答案的基础上,另一个以纯粹非依赖方式看待这一点的角度是注意到类型Either a a与该类型同构(Bool, a).虽然后者乍一看是一种产品,但有理由说这是一种和型,因为它是两种情况的总和a.

我必须用这个例子来Either a a代替Either a b,因为后者被表达为产品,我们需要 - 依赖良好的类型.

Answer 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是产品的因素之一.