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

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

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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

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

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

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

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

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

存在类型是不透明类型。

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