似乎我来晚了一点，但无论如何，这篇文档增加了关于存在类型是什么的另一种观点，尽管不是特别的语言不可知，这样应该更容易理解存在类型: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.

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

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

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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

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

存在类型是不透明类型。

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

似乎我来晚了一点，但无论如何，这篇文档增加了关于存在类型是什么的另一种观点，尽管不是特别的语言不可知，这样应该更容易理解存在类型: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.

当有人定义一个通用类型∀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);
   }
}