什么是存在型？
我通读维基百科文章存在的types 。 由于存在操作符（∃），我认为它们被称为存在types（existential types）。 不过，我不确定它的意义。 有什么区别
T = ∃X { X a; int f(X); } 和
T = ∀x { X a; int f(X); }
？
当某人定义了一个通用types∀X他们说： 你可以插入任何你想要的types，我不需要知道任何关于types的任何事情，我只会把它称为X
当某人定义一个存在types∃X他们会说： 我将在这里使用任何我想要的types; 你不会知道types的任何东西，所以你只能将它不透明地称为X
通用types让你写下如下的东西：
void copy<T>(List<T> source, List<T> dest) { ... }
copy函数不知道T实际上是什么，但是它不需要。
存在types会让你写下如下的东西：
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); } }
列表中的每个虚拟机实现可以具有不同的字节码types。 runAllCompilers函数不知道字节码types是什么，但它不需要; 它所做的只是将VirtualMachine.compile的字节码转发给VirtualMachine.run 。
Javatypes通配符（例如： List<?> ）是一种非常有限的存在types。
更新：忘了提及你可以用通用types来模拟存在types。 首先，包装你的通用types来隐藏types参数。 其次，倒置控制（这有效地互换了上面定义中的“你”和“我”部分，这是存在与普遍之间的主要区别）。
// 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 ，它具有通用types的handle函数。 净效果是一样的，我们的代码必须把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)这样的存在types的值∃x. F(x) ∃x. F(x) 是包含某种types x和F(x)types值的对。 而像∀x. F(x)这样的多态types的值∀x. F(x) ∀x. F(x)是一个函数 ，它接受某种types的x并产生一个types为F(x) 。 在这两种情况下，typesclosures在某种types的构造函数F 。
请注意，这个视图混合了types和值。 存在certificate是一种types和一种价值。 通用certificate是按types（或从types到值的映射）索引的整个值族。
所以你指定的两种types的区别如下：
T = ∃X { X a; int f(X); }
这意味着：typesT的值包含一个名为X的types，一个值a:X和一个函数f:X->int 。 Ttypes值的生产者可以select任何types的X ，消费者不可能知道X 除了有一个叫做a例子，并且这个值可以通过赋给f来变成一个int 。 换句话说，typesT的值知道如何以某种方式产生一个int 。 那么，我们可以消除中间typesX ，只是说：
T = int
普遍量化的有点不同。
T = ∀X { X a; int f(X); }
这意味着：typesT的值可以被赋予任何types的X ，并且无论X是什么 ，都会产生一个值a:X和一个函数f:X->int 。 换句话说：typesT的值的消费者可以为Xselect任何types。 而Ttypes值的生产者根本不知道X任何内容，但是必须能够为X任何select产生一个值a ，并且能够把这个值转化为一个int 。
显然实现这种types是不可能的，因为没有任何程序可以产生每种可想象的types的值。 除非你允许荒谬像null或底部。
由于存在主义是一对，所以存在主义论证可以通过柯里化转化为普遍主义论证。
(∃b. F(b)) -> Int
是相同的：
∀b. (F(b) -> Int)
前者是一个二级存在。 这导致以下有用的属性：
每个存在量化types的秩
n+1是一个普遍量化types的秩n。
有一个标准的algorithm将存在转化为共相，称为Skolemization 。
我认为解释存在主义types和普遍types是有意义的，因为这两个概念是互补的，即一个是另一个的“相反”。
我不能回答关于存在types的每一个细节（比如给出一个确切的定义，列出所有可能的用途，它们与抽象数据types的关系等），因为我根本就不够知识。 我只会演示（使用Java） HaskellWiki这篇文章所说的存在types的主要作用：
存在types可以用于几个不同的目的。 但他们所做的是在右侧“隐藏”一个typesvariables。 通常情况下，右侧出现的任何typesvariables也必须出现在左侧[…]
设置示例：
下面的伪代码并不是非常有效的Java，尽pipe它很容易解决这个问题。 事实上，这正是我要做的这个答案！
class Tree<α> { α value; Tree<α> left; Tree<α> right; } int height(Tree<α> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; }
让我简单地为你解释这一点。 我们正在界定…
-
表示二叉树中的节点的recursiontypes
Tree<α>。 每个节点存储一些types为α的value，并引用相同types的可选right子树。 -
函数
height返回从任何叶节点到根节点t的最远距离。
现在，让我们把上面的伪代码转换成适当的Java语法！ （为了简洁起见，我将继续省略一些样板，比如面向对象和可访问性修饰符）。我将展示两种可能的解决scheme。
1.通用型解决scheme：
最明显的解决方法是通过在其签名中引入types参数α来简单地生成height通用：
<α> int height(Tree<α> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; }
这将允许你声明variables，并在该函数内部创buildtypesα的expression式，如果你想的话。 但…
2.存在型解决scheme：
如果你看看我们的方法的身体，你会注意到我们实际上并没有访问或使用任何types的α ！ 没有这种types的expression式，也没有用这种types声明的任何variables…那么，为什么我们必须做height通用呢？ 为什么我们不能简单的忘记α ？ 事实certificate，我们可以：
int height(Tree<?> t) { return (t != null) ? 1 + max( height(t.left), height(t.right) ) : 0; }
正如我在这个答案一开始所写的那样，存在主义和普遍主义是互补的/双重的。 因此，如果通用types的解决scheme是使height 更通用，那么我们应该期望存在types具有相反的效果：使其不那么通用，即通过隐藏/去除types参数α 。
因此，在这个方法中你不能再引用t.value的types，也不能操作这个types的任何expression式，因为没有标识符被绑定到它。 （ ?通配符是一个特殊的标记，而不是“捕获”一个types的标识符。） 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 | =====================+=====================================
这些都是很好的例子，但我select回答有点不同。 从math中回想起那个∀x。 P（x）的意思是“对于所有的x，我可以certificateP（x）”。 换句话说，这是一种function，你给我一个x，我有一个方法来certificate你的。
在types理论中，我们不是在谈论证据，而是在谈论types。 所以在这个空间中，我们的意思是“对于任何typesX你给我，我会给你一个特定的typesP”。 现在，由于除了它是一个types的事实之外，我们没有给出关于X的许多信息，所以P不能用它做很多事情，但是也有一些例子。 P可以创build“相同types的所有对”的types： P<X> = Pair<X, X> = (X, X) 。 或者我们可以创build选项types： P<X> = Option<X> = X | Nil P<X> = Option<X> = X | Nil ，其中Nil是空指针的types。 我们可以列出它： List<X> = (X, List<X>) | Nil List<X> = (X, List<X>) | Nil 。 请注意，最后一个是recursion的， List<X>值或者是第一个元素是X的元素，第二个元素是List<X> ，否则它是空指针。
现在，在math∃x。 P（x）的意思是“我可以certificate有一个特定的x使得P（x）是真的”。 可能有许多这样的x，但是为了certificate这一点，就足够了。 另一种考虑的方法是必须存在一组非空的证据和certificate对{（x，P（x））}。
转化为types论：族中的一个types∃XP<X>是一个typesX和相应的typesP<X> 。 注意，在我们给X给P之前（这样我们知道关于X的一切，但是P很less），现在恰恰相反。 P<X>不保证给出有关X的任何信息，只是有一个，而且确实是一个types。
这有用吗？ 那么，P可能是一种暴露其内部typesX的方式。一个例子是隐藏其状态X的内部表示的对象。虽然我们没有办法直接操纵它，但我们可以通过在P上戳。可能有很多这种types的实现，但是无论select哪一种，都可以使用所有这些types。
存在型是一种不透明的types。
想一想Unix中的文件句柄。 你知道它的types是int，所以你可以很容易地伪造它。 例如，你可以尝试从句柄43中读取。如果程序有这个特定句柄打开的文件，你可以从中读取。 你的代码不必是恶意的，只是马虎（例如，句柄可能是一个未初始化的variables）。
一个存在types是从你的程序隐藏的。 如果fopen返回一个存在types，你所能做的就是将它与一些接受这个存在types的库函数一起使用。 例如，下面的伪代码将被编译：
让exfile = fopen（“foo.txt”）; //没有types的exfile！ 读取（exfile，buf，size）;
接口“read”被声明为：
有一个typesT，这样：
size_t read（T exfile，char * buf，size_t size）;
variablesexfile不是一个int，不是一个char *，不是一个结构文件 – 你可以在types系统中expression任何东西。 你不能声明一个types未知的variables，也不能将一个指针转换成未知types的指针。 语言不会让你。
要直接回答你的问题：
对于通用types， T使用必须包含types参数X 例如T<String>或T<Integer> 。 对于T的存在types使用，不包含该types参数，因为它是未知的或不相关的 – 只要使用T （或在Java T<?> ）。
更多信息：
通用/抽象types和存在types是对象/function的消费者/客户与其生产者/实施者之间透视的双重性。 当一方看到一个普遍types时，另一个看到一个存在types。
在Java中，您可以定义一个generics类：
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();
- 从
MyClass客户端的angular度来看，T是通用的，因为当你使用这个类时，你可以用T代替任何types的T，而且当你使用MyClass的实例时，你必须知道T的实际types - 从
MyClass本身的实例方法来看，T是存在的，因为它不知道T的真实types - 在Java中，
?代表存在主义的types – 因此，当你在课堂上时，T基本上是?。 如果你想用T存在处理MyClass一个实例，你可以在上面的secretMessage()例子中声明MyClass<?>。
存在types有时用于隐藏某些东西的实现细节，正如其他地方所讨论的那样。 这个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并不是。 但是这里要指出的是，你正在捕获某种状态以及在该状态下操作的函数列表，而且你不知道状态部分的实际types，但是函数已经与该types匹配。
现在，在Java中，所有非最终的非原始types都是部分存在的。 这可能听起来很奇怪，但是因为声明为Object的variables可能是Object的子类，所以不能声明特定的types，只能是“this type or subclass”。 因此，对象被表示为一个状态位加上一个在该状态下运行的函数列表 – 确切地说哪个函数是在运行时通过查找来确定的。 这与使用上面的存在types非常相像，在这个types中存在一个存在状态部分和一个在该状态下运行的函数。
在没有子types和强制types的静态types编程语言中，存在types允许pipe理不同types对象的列表。 T<Int>列表不能包含T<Long> 。 但是， T<?>的列表可以包含T任何变体，允许将许多不同types的数据放入列表中，并根据需要将它们全部转换为int（或者在数据结构内部进行任何操作）。
一个人几乎总是可以将一个存在types的logging转换成一个logging而不使用闭包。 闭包也是存在的types，因为closures的自由variables对调用者是隐藏的。 因此，一种支持闭包而不是存在types的语言可以让你创build共享隐藏状态的闭包，这些隐藏状态将放入对象的存在部分。
似乎我来得晚了一点，但无论如何，这个文件增加了对存在types的另一种观点，虽然不是专门语言不可知的，但是理解存在types应该是相当容易的： http：//www.cs.uu .nl / groups / ST / Projects / ehc / ehc-book.pdf （第8章）
普遍存在和存在量化types之间的差异可以通过以下观察来表征：
具有量化types的值的使用决定了量化typesvariables实例化时要select的types。 例如，身份函数“id ::∀aa→a”的调用者为这个特定的id应用程序确定为typesvariablesaselect的types。 对于函数应用程序“id 3”，这个types等于Int。
具有量化types的值的创build决定并隐藏了量化typesvariables的types。 例如，“∃a。（a，a→Int）”的创build者可能已经从“（3，λx→x）”构造了该types的值。 另一个创build者已经从“（'x'，λx→ord x）”构造了一个相同types的值。 从用户的angular度来看，这两个值具有相同的types，因此可以互换。 该值具有为typesvariablesaselect的特定types，但是我们不知道哪种types，所以这个信息不能再被利用。 这个价值特定types的信息已经被“遗忘”了。 我们只知道它存在。
对抽象数据types和信息隐藏的研究将存在types引入了编程语言。 使数据types抽象隐藏有关该types的信息，所以这种types的客户端不能滥用它。 假设你有一个对象的引用…一些语言允许你把这个引用强制转换为对字节的引用，并对你想要的内存做任何事情。 为了保证程序的行为，对于一种语言来说，强制执行的操作是非常有用的，即只能通过对象的devise者所提供的方法来操作对象的引用。 你知道types的存在，但没有更多。
看到：
抽象types有存在types，MITCHEL和PLOTKIN
所有types参数的值都存在通用types。 存在types仅存在满足存在types的约束的types参数的值。
例如，在Scala中，expression存在types的一种方式是被限制在一些上限或下限的抽象types。
trait Existential { type Parameter <: Interface }
相当于一个受约束的通用types是一个存在types，如下例所示。
trait Existential[Parameter <: Interface]
任何使用站点都可以使用Interface因为Existential任何可实例化的子types必须定义必须实现Interface的type Parameter 。
Scala中一个存在types的退化情况是一个从不被引用的抽象types，因此不需要被任何子types定义。 这实际上有一个Scala中的List[_]和Java中的List[?]的简写符号。
我的回答受到奥德斯基（Martin Odersky） 关于统一抽象和存在types的提议的启发。 随附的幻灯片帮助理解。
据我所知，这是一个描述接口/抽象类的math方法。
至于T =∃X{X a; int f（X）; }
对于C＃它将转化为一个通用的抽象types：
abstract class MyType<T>{ private T a; public abstract int f(T x); }
“存在”只是意味着某种types服从于这里定义的规则。
