haskell – 从属类型:依赖对类型如何类似于不相交联合?

前端之家收集整理的这篇文章主要介绍了haskell – 从属类型:依赖对类型如何类似于不相交联合?前端之家小编觉得挺不错的,现在分享给大家,也给大家做个参考。
我一直在研究依赖类型,我理解以下:

>为什么universal quantification表示为依赖函数类型。 ∀(x:A).B(x)表示“对于类型A的所有x,存在类型B(x)的值”。因此,它被表示为一个函数,当给定任何类型A的值x返回类型B(x)的值。
>为什么existential quantification表示为依赖对类型。 ∃(x:A).B(x)表示“存在类型A的x,其中存在类型B(x)的值”。因此,它被表示为一对,其第一元素是类型A的特定值x,并且其第二元素是类型B(x)的值。

Aside:有趣的是,通用量化始终用于material implication,而存在量化始终用于logical conjunction

无论如何,维基百科的文章dependent types指出:

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.

一个对类型(通常是一个产品类型)是如何类似于一个不相交的联合(它是一个和类型)?这一直困惑我。

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

混淆起因于对Σ类型的结构使用类似的术语以及它的值如何看起来像。

Σ(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)一个。

原文链接:https://www.f2er.com/javaschema/282504.html

猜你在找的设计模式相关文章