什么是存在类型？

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<α>

{

    α       value;

    Tree<α> left;

    Tree<α> right;

}

int height(Tree<α> t)

{

    return (t != null)  ?  1 + max( height(t.left), height(t.right) )

                        :  0;

}

让我为您简要说明一下。我们正在定义...

Tree<α>表示二叉树中的节点的递归类型。每个节点存储value某种类型的α，并引用相同类型的可选树left和right子树。

该函数height返回从任何叶节点到根节点的最远距离t。

现在，让我们将上面的伪代码height转换为正确的Java语法！（为简洁起见，我将继续省略一些样板，例如面向对象和可访问性修饰符。）我将展示两种可能的解决方案。

1.通用型解决方案：

最明显的解决方法是height通过将类型参数α引入其签名来简单地实现泛型：

<α> int height(Tree<α> t)

{

    return (t != null)  ?  1 + max( height(t.left), height(t.right) )

                        :  0;

}

如果需要，这将允许您声明变量并在该函数内创建类型为α的表达式。但...

2.现有类型解决方案：

如果查看我们方法的主体，您会注意到我们实际上并没有访问或使用α类型的任何东西！没有那种类型的表达式，也没有用那种类型声明的变量……那么，为什么我们必须使height泛型成为根本呢？为什么我们不能简单地忘记α？事实证明，我们可以：

int height(Tree<?> t)

{

    return (t != null)  ?  1 + max( height(t.left), height(t.right) )

                        :  0;

}

正如我在回答之初所写的那样，存在和通用类型本质上是互补/双重的。因此，如果通用类型的解决方案要使通用性height 更高，那么我们应该期望存在性类型具有相反的效果：使其不通用，即通过隐藏/删除类型参数α。

结果，您将无法再引用t.value此方法的类型，也不能操作该类型的任何表达式，因为没有标识符绑定到该方法。（?通配符是一个特殊的令牌，而不是“捕获”类型的标识符。）t.value实际上已经变得不透明了；也许您唯一仍能做的就是将其类型转换为Object。

摘要：

===========================================================

                     |    universally       existentially

                     |  quantified type    quantified type

---------------------+-------------------------------------

 calling method      |                  

 needs to know       |        yes                no

 the type argument   |                 

---------------------+-------------------------------------

 called method       |                  

 can use / refer to  |        yes                no  

 the type argument   |