存在类型是什么?

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

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

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

abstract class MyType<T>{
private T a;


public abstract int f(T x);
}

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

对抽象数据类型和信息隐藏的研究将存在类型引入了编程语言。使数据类型抽象隐藏了关于该类型的信息，因此该类型的客户端不能滥用它。假设你有一个对象的引用…有些语言允许您将该引用转换为对字节的引用，并对该内存块执行任何操作。为了保证程序的行为，语言强制只通过对象设计器提供的方法对对象的引用进行操作是很有用的。你只知道这种类型存在，仅此而已。

看到的:

抽象类型有存在类型，MITCHEL &普罗金

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

当有人定义一个通用类型∀X时，他们说:你可以插入任何你想要的类型，我不需要知道任何类型来完成我的工作，我只会不透明地将它称为X。

当有人定义存在类型∃X时，他们说:我想用什么类型都行;你将不知道任何关于类型的信息，所以你只能模糊地将它引用为X。

通用类型让你可以这样写:

void copy<T>(List<T> source, List<T> dest) {
...
}

copy函数不知道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<?>)是存在类型的一种非常有限的形式。

更新:忘了说你可以用泛型类型来模拟存在类型。首先，包装通用类型以隐藏类型参数。第二，反转控制(这有效地将&;you&;和“我这是存在和共相之间的主要区别)。

// 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，它有一个通用类型的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);
}
}

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

我无法回答关于存在类型的每一个细节(比如给出一个确切的定义，列出所有可能的用法，它们与抽象数据类型的关系，等等)，因为我在这方面的知识不够丰富。我将只演示(使用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<α>，表示二叉树中的一个节点。每个节点都存储了一个类型为α的value，并引用了相同类型的可选left和right子树。

• 函数height，返回从任意叶节点到根节点t的最远距离。

现在，让我们把上面的height伪代码转换成正确的Java语法!(为了简洁起见，我将继续省略一些样板文件，例如面向对象和可访问性修饰符。)我将展示两种可能的解决方案。

1. 通用型解决方案:

最明显的修复方法是通过将类型参数α引入到其签名中，使height成为泛型:

<α> int height(Tree<α> t)
{
return (t != null)  ?  1 + max( height(t.left), height(t.right) )
:  0;
}

这将允许你在该函数中声明变量并创建α类型的表达式，如果你愿意的话。但是…

2. 存在型解:

如果你看一下我们的方法体，你会注意到我们实际上并没有访问或使用任何类型为α!没有那种类型的表达式，也没有那种类型声明的变量……那么，为什么我们必须让height是泛型的呢?为什么我们不能简单地忘记α?事实证明，我们可以:

int height(Tree<?> t)
{
return (t != null)  ?  1 + max( height(t.left), height(t.right) )
:  0;
}

正如我在回答的一开始所写的，存在型和普遍型在本质上是互补/双重的。因此，如果通用类型解决方案是使height 更多的为泛型，那么我们应该期望存在类型具有相反的效果:使其为少为泛型，即通过隐藏/删除类型参数α。

因此，您不能再在此方法中引用t.value的类型，也不能操作该类型的任何表达式，因为没有标识符绑定到它。(?通配符是一个特殊的令牌，而不是“捕获”类型的标识符。)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   |
=====================+=====================================

一个存在类型的值，如∃x. F(x) 是一对，包含一些类型 x和类型为F(x)的x0。而像∀x. F(x)这样的多态类型的值是x1，它接受某种类型的x，而x2则接受类型为F(x)的值。在这两种情况下，类型在一些类型构造函数F上关闭。

注意，这个视图混合了类型和值。存在证明是一种类型和一个值。通用证明是由类型(或从类型到值的映射)索引的一整套值。

所以你指定的两种类型的区别如下:

T = ∃X { X a; int f(X); }

这意味着:类型为T的值包含名为X的类型、值为a:X的值和函数f:X->int。T类型值的生产者可以为X选择X3类型，而消费者不能知道有关X的任何信息。除了有一个名为a的例子，并且这个值可以通过将其赋给f来转换为int。换句话说，类型为T的值知道如何以某种方式生成int。好吧，我们可以去掉中间类型X，只说:

T = int

而普遍量化的则略有不同。

T = ∀X { X a; int f(X); }

这意味着:类型为T的值可以赋给任何类型为X的值，它将生成值a:X和函数f:X->int X2。换句话说:类型为T的值的消费者可以为X选择任何类型。并且类型为T的值的生产者不能知道关于X的任何事情，但是它必须能够为任何X的选择生成值a，并且能够将这样的值转换为X1。

显然，实现这种类型是不可能的，因为没有程序可以产生所有可以想象的类型的值。除非你允许荒谬的null或底部。

由于存在实参是一对，所以存在实参可以通过局部套用转换为通用实参。

(∃b. F(b)) -> Int

等于:

∀b. (F(b) -> Int)

前者是2存在型。这将导致以下有用的属性:

秩n+1的每一个存在量化类型都是秩n的普遍量化类型。

有一个将存在式转化为共相的标准算法，称为< em > Skolemization < / em >。

这些都是很好的例子，但我选择稍微不同的答案。回想一下数学，∀x。P(x)表示"对于所有x，我可以证明P(x)"换句话说，它是一种函数，你给我一个x，我有一个方法来证明它。

在类型论中，我们讨论的不是证明，而是类型。所以在这里，我们的意思是“对于任何类型的X，你给我，我会给你一个特定类型的P”。现在，由于我们没有给P太多关于X的信息，除了它是一个类型的事实，P不能用它做什么，但有一些例子。P可以创建“所有相同类型的对”类型:P<X> = Pair<X, X> = (X, X)。或者我们可以创建选项类型:P<X> = Option<X> = X | Nil，其中Nil是空指针的类型。我们可以用它做一个列表:List<X> = (X, List<X>) | Nil。注意，最后一个是递归的，List<X>的值要么是第一个元素是X，第二个元素是List<X>的对，要么是一个空指针。

现在，在数学∃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。例如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();

• 从MyClass的客户端的角度来看，T是通用的，因为当你使用T类时，你可以用任何类型替换T，并且当你使用MyClass的实例时，你必须知道T的实际类型
• 从MyClass本身的实例方法的角度来看，T是存在的，因为它不知道T的真正类型
• 在Java中，?表示存在类型——因此当你在类内部时，T基本上就是?。如果你想用T存在来处理MyClass的实例，你可以像上面的secretMessage()例子一样声明MyClass<?>。

存在类型有时用于隐藏某些东西的实现细节，如在其他地方讨论的那样。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不是。但这里的重点是，您正在捕获某种状态加上对该状态进行操作的函数列表，并且您不知道状态部分的真实类型，但函数知道，因为它们已经与该类型匹配。

现在，在Java中，所有非最终的非原始类型都是部分存在类型。这听起来可能很奇怪，但因为声明为Object的变量可能是Object的子类，所以不能声明具体的类型，只能声明“此类型或子类”。因此，对象被表示为一个状态位加上一个对该状态进行操作的函数列表——确切地调用哪个函数是在运行时通过查找确定的。这非常类似于上面使用的存在类型，其中有一个存在状态部分和一个对该状态进行操作的函数。

在没有子类型和类型转换的静态类型编程语言中，存在类型允许管理不同类型对象的列表。T<Int>的列表不能包含T<Long>。然而，T<?>的列表可以包含T的任何变体，允许将许多不同类型的数据放入列表中，并根据需要将它们全部转换为int(或执行数据结构内部提供的任何操作)。

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

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

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

trait Existential {
type Parameter <: Interface
}

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

trait Existential[Parameter <: Interface]

任何使用站点都可以使用Interface，因为Existential的任何可实例化子类型必须定义必须实现Interface的type Parameter。

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

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

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

普遍量化的类型和存在量化的类型之间的区别可以用以下观察来描述:

• 使用具有∀量化类型的值决定了量化类型变量实例化所选择的类型。例如，标识函数“id::∀”的调用者。A→A”决定为id的这个特定应用选择类型变量A的类型。对于函数应用程序“id 3”，此类型等于Int。

• 具有∃量化类型的值的创建确定并隐藏了量化类型变量的类型。例如，“∃a.”的创建者。(a, a→Int) "可以从" (3，λx→x) "构造出该类型的值;另一个创建者从“(' x '， λx→ord x)”构造了一个具有相同类型的值。从用户的角度来看，这两个值具有相同的类型，因此是可互换的。该值为类型变量a选择了特定的类型，但我们不知道是哪种类型，因此不能再利用该信息。这种特定于值的类型信息已经被“遗忘”了;我们只知道它的存在。