什么是存在类型?

我通读了Wikipedia文章存在类型。我发现由于存在运算符(∃),它们被称为存在类型。不过,我不确定它的意义是什么。之间有什么区别


T = ∃X { X a; int f(X); }


T = ∀x { X a; int f(X); }


神不在的星期二
浏览 495回答 3
3回答

慕神8447489

存在类型的值,例如,∃x. F(x) 是包含某种类型 x和该类型的值的一对F(x)。而like多态类型的值∀x. F(x)是一个具有某种类型并产生 type值的函数。在这两种情况下,类型都会关闭某个类型构造器。xF(x)F请注意,此视图混合了类型和值。存在证明是一种类型和一种价值。通用证明是按类型(或从类型到值的映射)索引的整个值系列。因此,您指定的两种类型之间的区别如下:T = ∃X { X a; int f(X); }这意味着:类型的值T包含一个称为的类型X,一个值a:X和一个函数f:X->int。类型值的生产者T可以选择任何类型,X消费者对此一无所知X。除了调用它的一个示例,a并且可以通过将其int赋予来将其转换为一个值f。换句话说,类型的值T知道如何产生int某种方式。好吧,我们可以消除中间类型,X而只是说:T = int普遍量化的数字有些不同。T = ∀X { X a; int f(X); }这意味着:类型的值T可以给出任何类型的X,它会产生一个值a:X,和功能f:X->int 不管是什么X是。换句话说:类型值的使用者T可以为选择任何类型X。类型值的产生者T一无所知X,但是它必须能够a为任何选择产生一个值X,并能够将这样的值转化为一个值int。显然,实现这种类型是不可能的,因为没有程序可以产生每种可以想象的类型的值。除非您允许荒谬之类的话null。由于一个存在性参数是一对,因此可以通过currying将一个存在性参数转换为通用参数。(∃b. F(b)) -> Int是相同的:∀b. (F(b) -> Int)前者是2级生存者。这导致以下有用的属性:等级的每个存在量化类型都是等级n+1普遍量化类型n。有一种标准的算法可以将存在物转换为通用物,称为Skolemization。

繁花如伊

我认为将存在性类型与通用类型一起解释是有意义的,因为这两个概念是互补的,即一个概念与另一个概念“相对”。我无法回答有关存在性类型的每一个细节(例如给出确切的定义,列出所有可能的用途,它们与抽象数据类型的关系等),因为我对此没有足够的了解。我将仅演示(使用Java)HaskellWiki文章声明存在类型的主要作用:存在类型可以用于多种不同目的。但是他们要做的是在右侧“隐藏”一个类型变量。通常,出现在右侧的任何类型变量也必须出现在左侧[…]设置示例:以下伪代码不是完全有效的Java,即使很容易修复它也是如此。实际上,这正是我要在此答案中执行的操作!class Tree<α>{&nbsp; &nbsp; α&nbsp; &nbsp; &nbsp; &nbsp;value;&nbsp; &nbsp; Tree<α> left;&nbsp; &nbsp; Tree<α> right;}int height(Tree<α> t){&nbsp; &nbsp; return (t != null)&nbsp; ?&nbsp; 1 + max( height(t.left), height(t.right) )&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; :&nbsp; 0;}让我为您简要说明一下。我们正在定义...Tree<α>表示二叉树中的节点的递归类型。每个节点存储value某种类型的α,并引用相同类型的可选树left和right子树。该函数height返回从任何叶节点到根节点的最远距离t。现在,让我们将上面的伪代码height转换为正确的Java语法!(为简洁起见,我将继续省略一些样板,例如面向对象和可访问性修饰符。)我将展示两种可能的解决方案。1.通用型解决方案:最明显的解决方法是height通过将类型参数α引入其签名来简单地实现泛型:<α> int height(Tree<α> t){&nbsp; &nbsp; return (t != null)&nbsp; ?&nbsp; 1 + max( height(t.left), height(t.right) )&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; :&nbsp; 0;}如果需要,这将允许您声明变量并在该函数内创建类型为α的表达式。但...2.现有类型解决方案:如果查看我们方法的主体,您会注意到我们实际上并没有访问或使用α类型的任何东西!没有那种类型的表达式,也没有用那种类型声明的变量……那么,为什么我们必须使height泛型成为根本呢?为什么我们不能简单地忘记α?事实证明,我们可以:int height(Tree<?> t){&nbsp; &nbsp; return (t != null)&nbsp; ?&nbsp; 1 + max( height(t.left), height(t.right) )&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; :&nbsp; 0;}正如我在回答之初所写的那样,存在和通用类型本质上是互补/双重的。因此,如果通用类型的解决方案要使通用性height 更高,那么我们应该期望存在性类型具有相反的效果:使其不通用,即通过隐藏/删除类型参数α。结果,您将无法再引用t.value此方法的类型,也不能操作该类型的任何表达式,因为没有标识符绑定到该方法。(?通配符是一个特殊的令牌,而不是“捕获”类型的标识符。)t.value实际上已经变得不透明了;也许您唯一仍能做的就是将其类型转换为Object。摘要:===========================================================&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;|&nbsp; &nbsp; universally&nbsp; &nbsp; &nbsp; &nbsp;existentially&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;|&nbsp; quantified type&nbsp; &nbsp; quantified type---------------------+-------------------------------------&nbsp;calling method&nbsp; &nbsp; &nbsp; |&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp;&nbsp;needs to know&nbsp; &nbsp; &nbsp; &nbsp;|&nbsp; &nbsp; &nbsp; &nbsp; yes&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; no&nbsp;the type argument&nbsp; &nbsp;|&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;---------------------+-------------------------------------&nbsp;called method&nbsp; &nbsp; &nbsp; &nbsp;|&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp;&nbsp;can use / refer to&nbsp; |&nbsp; &nbsp; &nbsp; &nbsp; yes&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; no&nbsp;&nbsp;&nbsp;the type argument&nbsp; &nbsp;|&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp;
打开App,查看更多内容
随时随地看视频慕课网APP