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

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

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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

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

对于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

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

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

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

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

trait Existential {
  type Parameter <: Interface
}

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

trait Existential[Parameter <: Interface]

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

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

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