我认为将存在类型与普遍类型一起解释是有意义的，因为这两个概念是互补的，即一个是另一个的“相反”。

我无法回答关于存在类型的每一个细节(比如给出一个确切的定义，列出所有可能的用法，它们与抽象数据类型的关系，等等)，因为我在这方面的知识不够丰富。我将只演示(使用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<α>，表示二叉树中的一个节点。每个节点存储一个α类型的值，并引用相同类型的可选左右子树。 一个函数高度，它返回从任何叶节点到根节点t的最远距离。

现在，让我们把上面关于高度的伪代码转换成正确的Java语法!(为了简洁起见，我将继续省略一些样板文件，例如面向对象和可访问性修饰符。)我将展示两种可能的解决方案。

1. 通用型解决方案:

最明显的解决方法是通过在其签名中引入类型参数α来简单地使height成为泛型:

<α> int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

这将允许您在该函数中声明变量并创建α类型的表达式(如果您愿意的话)。但是…

2. 存在型解:

如果你看一下我们的方法体，你会注意到我们实际上并没有访问或使用任何α类型的东西!没有那种类型的表达式，也没有那种类型声明的变量……那么，为什么我们要让身高通用呢?为什么我们不能简单地忘记α?事实证明，我们可以:

int height(Tree<?> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

正如我在回答的一开始所写的，存在型和普遍型在本质上是互补/双重的。因此，如果通用类型解决方案是使高度更加泛型，那么我们应该期望存在类型具有相反的效果:通过隐藏/删除类型参数α，使它不那么泛型。

因此，您不能再在此方法中引用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   |                  
=====================+=====================================

直接回答你的问题:

对于通用类型，T的使用必须包括类型参数x。例如T<String>或T<Integer>。对于存在类型使用T不包括该类型参数，因为它是未知的或不相关的-只需使用T(或在Java中T<?>)。

进一步的信息:

通用/抽象类型和存在类型是对象/函数的消费者/客户和它的生产者/实现之间的二元视角。一方看到的是普遍类型，另一方看到的是存在类型。

在Java中，你可以定义一个泛型类:

public class MyClass<T> {
   // T is existential in here
   T whatever; 
   public MyClass(T w) { this.whatever = w; }

   public static MyClass<?> secretMessage() { return new MyClass("bazzlebleeb"); }
}

// T is universal from out here
MyClass<String> mc1 = new MyClass("foo");
MyClass<Integer> mc2 = new MyClass(123);
MyClass<?> mc3 = MyClass.secretMessage();

From the perspective of a client of MyClass, T is universal because you can substitute any type for T when you use that class and you must know the actual type of T whenever you use an instance of MyClass From the perspective of instance methods in MyClass itself, T is existential because it doesn't know the real type of T In Java, ? represents the existential type - thus when you are inside the class, T is basically ?. If you want to handle an instance of MyClass with T existential, you can declare MyClass<?> as in the secretMessage() example above.

存在类型有时用于隐藏某些东西的实现细节，如在其他地方讨论的那样。Java版本如下所示:

public class ToDraw<T> {
    T obj;
    Function<Pair<T,Graphics>, Void> draw;
    ToDraw(T obj, Function<Pair<T,Graphics>, Void>
    static void draw(ToDraw<?> d, Graphics g) { d.draw.apply(new Pair(d.obj, g)); }
}

// Now you can put these in a list and draw them like so:
List<ToDraw<?>> drawList = ... ;
for(td in drawList) ToDraw.draw(td);

要正确地捕获这一点有点棘手，因为我正在假装使用某种函数式编程语言，而Java不是。但这里的重点是，您正在捕获某种状态加上对该状态进行操作的函数列表，并且您不知道状态部分的真实类型，但函数知道，因为它们已经与该类型匹配。

Now, in Java all non-final non-primitive types are partly existential. This may sound strange, but because a variable declared as Object could potentially be a subclass of Object instead, you cannot declare the specific type, only "this type or a subclass". And so, objects are represented as a bit of state plus a list of functions that operate on that state - exactly which function to call is determined at runtime by lookup. This is very much like the use of existential types above where you have an existential state part and a function that operates on that state.

在没有子类型和类型转换的静态类型编程语言中，存在类型允许管理不同类型对象的列表。T<Int>的列表不能包含T<Long>。然而，T<?>可以包含T的任何变体，允许将许多不同类型的数据放入列表中，并根据需要将它们全部转换为int(或执行数据结构内部提供的任何操作)。

几乎总是可以将具有存在类型的记录转换为不使用闭包的记录。闭包也是存在类型的，因为它关闭的自由变量对调用者是隐藏的。因此，一种支持闭包但不支持存在类型的语言可以允许您创建闭包，这些闭包共享与放入对象的存在部分相同的隐藏状态。

存在类型是不透明类型。

想想Unix中的文件句柄。你知道它的类型是int，所以你可以很容易地伪造它。例如，您可以尝试从句柄43读取。如果恰好程序打开了一个带有这个特定句柄的文件，那么您将从中读取。你的代码不必是恶意的，只是草率的(例如，句柄可以是一个未初始化的变量)。

存在类型对程序隐藏。如果fopen返回一个存在类型，你所能做的就是将它与一些接受这种存在类型的库函数一起使用。例如，下面的伪代码可以编译:

let exfile = fopen("foo.txt"); // No type for exfile!
read(exfile, buf, size);

接口“read”声明为:

存在一种类型T，这样:

size_t read(T exfile, char* buf, size_t size);

变量exfile不是int，不是char*，也不是struct file——在类型系统中没有任何可以表示的东西。你不能声明一个未知类型的变量，你也不能强制转换，比如说，一个指针到那个未知类型。语言不允许你这么做。

Research into abstract datatypes and information hiding brought existential types into programming languages. Making a datatype abstract hides info about that type, so a client of that type cannot abuse it. Say you've got a reference to an object... some languages allow you to cast that reference to a reference to bytes and do anything you want to that piece of memory. For purposes of guaranteeing behavior of a program, it's useful for a language to enforce that you only act on the reference to the object via the methods the designer of the object provides. You know the type exists, but nothing more.

看到的: 抽象类型有存在类型，MITCHEL和PLOTKIN http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf

我认为将存在类型与普遍类型一起解释是有意义的，因为这两个概念是互补的，即一个是另一个的“相反”。

我无法回答关于存在类型的每一个细节(比如给出一个确切的定义，列出所有可能的用法，它们与抽象数据类型的关系，等等)，因为我在这方面的知识不够丰富。我将只演示(使用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<α>，表示二叉树中的一个节点。每个节点存储一个α类型的值，并引用相同类型的可选左右子树。 一个函数高度，它返回从任何叶节点到根节点t的最远距离。

现在，让我们把上面关于高度的伪代码转换成正确的Java语法!(为了简洁起见，我将继续省略一些样板文件，例如面向对象和可访问性修饰符。)我将展示两种可能的解决方案。

1. 通用型解决方案:

最明显的解决方法是通过在其签名中引入类型参数α来简单地使height成为泛型:

<α> int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

这将允许您在该函数中声明变量并创建α类型的表达式(如果您愿意的话)。但是…

2. 存在型解:

如果你看一下我们的方法体，你会注意到我们实际上并没有访问或使用任何α类型的东西!没有那种类型的表达式，也没有那种类型声明的变量……那么，为什么我们要让身高通用呢?为什么我们不能简单地忘记α?事实证明，我们可以:

int height(Tree<?> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

正如我在回答的一开始所写的，存在型和普遍型在本质上是互补/双重的。因此，如果通用类型解决方案是使高度更加泛型，那么我们应该期望存在类型具有相反的效果:通过隐藏/删除类型参数α，使它不那么泛型。

因此，您不能再在此方法中引用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   |                  
=====================+=====================================

存在类型的值，例如∃x。F(x)是一个包含x类型和F(x)类型值的对。而像∀x这样的多态类型的值。F(x)是一个接受x类型并产生F(x)类型值的函数。在这两种情况下，类型在某个类型构造函数F上关闭。

注意，这个视图混合了类型和值。存在证明是一种类型和一个值。通用证明是由类型(或从类型到值的映射)索引的一整套值。

所以你指定的两种类型的区别如下:

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

这意味着:类型T的值包含名为X的类型、值A:X和函数f:X->int。T类型值的生产者可以为X选择任何类型，而消费者对X一无所知，除了有一个叫做A的例子，并且这个值可以通过将它交给f来转换成int型。换句话说，T类型的值知道如何以某种方式生成int型。我们可以排除中间类型X，然后说

T = int

而普遍量化的则略有不同。

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

这意味着:类型T的值可以给定任何类型X，它将生成一个值A:X，以及一个函数f:X->int，无论X是什么。换句话说:T类型值的消费者可以为X选择任何类型，而T类型值的生产者完全不可能知道X的任何信息，但它必须能够为任何X选择产生一个值a，并能够将这样的值转换为int型。

显然，实现这种类型是不可能的，因为没有程序可以产生所有可以想象的类型的值。除非你允许像null或底部这样的荒谬。

由于存在主义论点是一对，存在主义论点可以通过套用转换为普遍论点。

(∃b. F(b)) -> Int

等于:

∀b. (F(b) -> Int)

前者是二级存在主义。这将导致以下有用的属性:

秩n+1的每一个存在量化类型都是秩n的普遍量化类型。

有一个将存在性转化为共相的标准算法，叫做Skolemization。