这些都是很好的例子，但我选择稍微不同的答案。回想一下数学，∀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来观察它的效果。这种类型可以有很多实现，但无论选择哪一种，您都可以使用所有这些类型。

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

当有人定义一个通用类型∀X时，他们是在说:你可以插入任何你想要的类型，我不需要知道任何类型来完成我的工作，我只会不透明地将它称为X。

当有人定义存在类型∃X时，他们在说:我将在这里使用我想要的任何类型;你不会知道任何关于类型的信息，所以你只能模糊地把它称为X。

通用类型让你可以这样写:

void copy<T>(List<T> source, List<T> dest) {
   ...
}

复制函数不知道T是多少，但它不需要知道。

存在类型可以让你这样写:

interface VirtualMachine<B> {
   B compile(String source);
   void run(B bytecode);
}

// Now, if you had a list of VMs you wanted to run on the same input:
void runAllCompilers(List<∃B:VirtualMachine<B>> vms, String source) {
   for (∃B:VirtualMachine<B> vm : vms) {
      B bytecode = vm.compile(source);
      vm.run(bytecode);
   }
}

列表中的每个虚拟机实现都可以有不同的字节码类型。runAllCompilers函数不知道字节码类型是什么，但它不需要知道;它所做的就是将字节码从VirtualMachine.compile传递到VirtualMachine.run。

Java类型通配符(例如:List<?>)是存在类型的一种非常有限的形式。

更新:忘了说你可以用通用类型来模拟存在类型。首先，包装通用类型以隐藏类型参数。第二，反向控制(这有效地交换了上面定义中的“你”和“我”部分，这是存在和共相之间的主要区别)。

// A wrapper that hides the type parameter 'B'
interface VMWrapper {
   void unwrap(VMHandler handler);
}

// A callback (control inversion)
interface VMHandler {
   <B> void handle(VirtualMachine<B> vm);
}

现在，我们可以让VMWrapper调用我们自己的VMHandler，它有一个通用类型的句柄函数。最终效果是一样的，我们的代码必须将B视为不透明的。

void runWithAll(List<VMWrapper> vms, final String input)
{
   for (VMWrapper vm : vms) {
      vm.unwrap(new VMHandler() {
         public <B> void handle(VirtualMachine<B> vm) {
            B bytecode = vm.compile(input);
            vm.run(bytecode);
         }
      });
   }
}

虚拟机实现示例:

class MyVM implements VirtualMachine<byte[]>, VMWrapper {
   public byte[] compile(String input) {
      return null; // TODO: somehow compile the input
   }
   public void run(byte[] bytecode) {
      // TODO: Somehow evaluate 'bytecode'
   }
   public void unwrap(VMHandler handler) {
      handler.handle(this);
   }
}

据我所知，这是一种描述接口/抽象类的数学方法。

对于T =∃X {X a;int f (X);｝

对于c#，它可以转换为泛型抽象类型:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"存在主义"的意思是有某种类型服从这里定义的规则。

似乎我来晚了一点，但无论如何，这篇文档增加了关于存在类型是什么的另一种观点，尽管不是特别的语言不可知，这样应该更容易理解存在类型:http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf(第8章)

The difference between a universally and existentially quantified type can be characterized by the following observation: The use of a value with a ∀ quantified type determines the type to choose for the instantiation of the quantified type variable. For example, the caller of the identity function “id :: ∀a.a → a” determines the type to choose for the type variable a for this particular application of id. For the function application “id 3” this type equals Int. The creation of a value with a ∃ quantified type determines, and hides, the type of the quantified type variable. For example, a creator of a “∃a.(a, a → Int)” may have constructed a value of that type from “(3, λx → x)”; another creator has constructed a value with the same type from “(’x’, λx → ord x)”. From a users point of view both values have the same type and are thus interchangeable. The value has a specific type chosen for type variable a, but we do not know which type, so this information can no longer be exploited. This value specific type information has been ‘forgotten’; we only know it exists.

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

我无法回答关于存在类型的每一个细节(比如给出一个确切的定义，列出所有可能的用法，它们与抽象数据类型的关系，等等)，因为我在这方面的知识不够丰富。我将只演示(使用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   |                  
=====================+=====================================