haskell – 从属类型：依赖对类型如何类似于不相交联合？
|
我一直在研究依赖类型，我理解以下：
>为什么universal quantification表示为依赖函数类型。 ?(x：A).B(x)表示“对于类型A的所有x，存在类型B(x)的值”。因此，它被表示为一个函数，当给定任何类型A的值x返回类型B(x)的值。 Aside：有趣的是，通用量化始终用于material implication，而存在量化始终用于logical conjunction。 无论如何，维基百科的文章dependent types指出：
一个对类型(通常是一个产品类型)是如何类似于一个不相交的联合(它是一个和类型)？这一直困惑我。 此外，依赖函数类型如何与产品类型类似？
混淆起因于对Σ类型的结构使用类似的术语以及它的值如何看起来像。
Σ(x：A)B(x)的值是一对(a，b)，其中a∈A和b∈B(a)。第二个元素的类型取决于第一个元素的值。 如果我们看一下Σ(x：A)B(x)的结构，对于所有可能的x∈A，它是B(x)的一个不相交的联合(联产)。 如果B(x)是常数(与x无关)，则Σ(x：A)B将只是| A | B的副本，即A?B(2种类型的产品)。 如果我们看看Π(x：A)B(x)的结构，它是所有可能的x∈A的B(x)的乘积。其值可以被视为| A | -tuple，其中第a个分量是类型B(a)。 如果B(x)是常数(独立于x)，那么Π(x：A)B将只是A→B – 从A到B的函数，即使用集理论符号B?的| A |的副本。 因此，Σ(x∈A)B(x)是由A的元素索引的| A | – 联合序列，而Π(x∈A)B(x)一个。 （编辑：李大同） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |