存在类型是不透明类型。

想想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——在类型系统中没有任何可以表示的东西。你不能声明一个未知类型的变量，你也不能强制转换，比如说，一个指针到那个未知类型。语言不允许你这么做。

类型参数的所有值都存在一个通用类型。存在类型仅适用于满足存在类型约束的类型参数值。

例如，在Scala中，表示存在类型的一种方法是抽象类型，它被限制在某个上界或下界。

trait Existential {
  type Parameter <: Interface
}

同样，受约束的通用类型是存在类型，如下例所示。

trait Existential[Parameter <: Interface]

任何使用站点都可以使用接口，因为存在的任何可实例化子类型必须定义必须实现接口的类型Parameter。

在Scala中，存在类型的退化情况是一种抽象类型，它永远不会被引用，因此不需要由任何子类型定义。这在Scala中有效地简化了List[_]和List<?Java中的>。

我的回答受到Martin Odersky关于统一抽象类型和存在类型的建议的启发。随附的幻灯片有助于理解。

直接回答你的问题:

对于通用类型，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(或执行数据结构内部提供的任何操作)。

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

我画了这个图。我不知道它是否严谨。但如果有帮助的话，我很高兴。

这些都是很好的例子，但我选择稍微不同的答案。回想一下数学，∀x。P(x)表示"对于所有x，我可以证明P(x)"换句话说，它是一种函数，你给我一个x，我有一个方法来证明它。

In type theory, we are not talking about proofs, but of types. So in this space we mean "for any type X you give me, I will give you a specific type P". Now, since we don't give P much information about X besides the fact that it is a type, P can't do much with it, but there are some examples. P can create the type of "all pairs of the same type": P<X> = Pair<X, X> = (X, X). Or we can create the option type: P<X> = Option<X> = X | Nil, where Nil is the type of the null pointers. We can make a list out of it: List<X> = (X, List<X>) | Nil. Notice that the last one is recursive, values of List<X> are either pairs where the first element is an X and the second element is a List<X> or else it is a null pointer.

现在，在数学∃x。P(x)表示“我可以证明存在一个特定的x，使得P(x)为真”。这样的x可能有很多，但要证明它，一个就足够了。另一种思考方法是，必须存在一个非空的证据-证明对{(x, P(x))}集合。

转换为类型理论:家族中的类型∃X。P<X>为类型X，对应类型P<X>。注意，在我们把X给P之前，(所以我们知道关于X的一切，但对P知之甚少)现在正好相反。P<X>并没有承诺给出任何关于X的信息，只是说有一个，而且它确实是一个类型。

这有什么用呢?嗯，P可以是一种类型，它有办法暴露其内部类型x。一个例子是一个对象，它隐藏了其状态x的内部表示。虽然我们没有办法直接操作它，但我们可以通过戳P来观察它的效果。这种类型可以有很多实现，但无论选择哪一种，您都可以使用所有这些类型。

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