什么是存在类型？

Question

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

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

和

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

？

Answer 1

存在类型的值，例如，∃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。

Answer 2

我认为将存在性类型与通用类型一起解释是有意义的，因为这两个概念是互补的，即一个概念与另一个概念“相对”。我无法回答有关存在性类型的每一个细节（例如给出确切的定义，列出所有可能的用途，它们与抽象数据类型的关系等），因为我对此没有足够的了解。我将仅演示（使用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;