我通读了维基百科上关于存在类型的文章。我认为它们之所以被称为存在类型是因为存在操作符(∃)。但我不知道这有什么意义。有什么区别
T = ∃X { X a; int f(X); }
and
T = ∀x { X a; int f(X); }
?
当前回答
当有人定义一个通用类型∀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。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来观察它的效果。这种类型可以有很多实现，但无论选择哪一种，您都可以使用所有这些类型。
据我所知，这是一种描述接口/抽象类的数学方法。
对于T =∃X {X a;int f (X);｝
对于c#，它可以转换为泛型抽象类型:
abstract class MyType<T>{
private T a;
public abstract int f(T x);
}
"存在主义"的意思是有某种类型服从这里定义的规则。
当有人定义一个通用类型∀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。例如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(或执行数据结构内部提供的任何操作)。
几乎总是可以将具有存在类型的记录转换为不使用闭包的记录。闭包也是存在类型的，因为它关闭的自由变量对调用者是隐藏的。因此，一种支持闭包但不支持存在类型的语言可以允许您创建闭包，这些闭包共享与放入对象的存在部分相同的隐藏状态。
存在类型是不透明类型。
想想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——在类型系统中没有任何可以表示的东西。你不能声明一个未知类型的变量，你也不能强制转换，比如说，一个指针到那个未知类型。语言不允许你这么做。
