我通读了 Wikipedia 文章Existential types。我收集到它们被称为存在类型是因为存在运算符 (∃)。不过，我不确定这有什么意义。有什么区别
T = ∃X { X a; int f(X); }
和
T = ∀x { X a; int f(X); }
?
Claudiu
问问题
30063 次
11 回答
219
当有人定义通用类型∀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<?>是一种非常有限的存在类型。
更新：忘了提到你可以用通用类型模拟存在类型。首先，包装您的通用类型以隐藏类型参数。其次，反转控制（这有效地交换了上述定义中的“你”和“我”部分，这是存在主义和普遍主义之间的主要区别）。
// 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);
}
}
于 2011-04-02T00:26:42.093 回答
115
存在类型的值就像∃x. F(x) 是一对包含某种类型 x和类型的值F(x)。而多态类型的值 like∀x. F(x)是一个接受某种类型并产生type 值的函数。在这两种情况下，类型都关闭了一些类型构造函数。xF(x)F
请注意，此视图混合了类型和值。存在性证明是一种类型和一种值。通用证明是按类型索引的整个值族（或从类型到值的映射）。
所以你指定的两种类型的区别如下：
T = ∃X { X a; int f(X); }
这意味着： type 的值T包含一个名为 的类型X、一个 valuea:X和一个 function f:X->int。类型值的生产者T可以选择任何类型，X而消费者对X. 除了有一个调用它的例子，a并且这个值可以通过将int其转换为f. 换句话说，一个类型的值T知道如何以int某种方式产生一个。好吧，我们可以消除中间类型X，然后说：
T = int
普遍量化的有点不同。
T = ∀X { X a; int f(X); }
这意味着： type 的值T可以被赋予任何 type X，它会产生一个 valuea:X和一个函数，f:X->int 不管X它是什么。换句话说：类型值的消费者T可以为X. 类型值的生产者T根本不知道任何关于 的内容X，但它必须能够a为 的任何选择生成一个值X，并且能够将这样的值转换为int。
显然实现这种类型是不可能的，因为没有程序可以产生所有可以想象的类型的值。除非你允许像null或底部这样的荒谬。
由于存在论是一对，所以存在论论点可以通过柯里化转换为普遍论点。
(∃b. F(b)) -> Int
是相同的：
∀b. (F(b) -> Int)
前者是二级存在主义。这导致以下有用的属性：
每个存在量化的等级类型
n+1都是普遍量化的等级类型n。
有一种标准算法可以将存在主义转化为普遍主义，称为Skolemization。
于 2012-02-27T22:06:50.913 回答
41
我认为将存在类型与通用类型一起解释是有意义的，因为这两个概念是互补的，即一个是另一个的“对立面”。
我无法回答有关存在类型的每一个细节（例如给出准确的定义、列出所有可能的用途、它们与抽象数据类型的关系等），因为我对此不够了解。我将仅演示（使用 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某种类型α的 a，并具有对相同类型的可选子树left和子树的引用。rightheight返回从任何叶节点到根节点的最远距离的函数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在此方法中引用 of 的类型，也不能操作该类型的任何表达式，因为没有标识符绑定到它。（?通配符是一个特殊的标记，而不是“捕获”一个类型的标识符。）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 |
=====================+=====================================
于 2011-12-31T03:52:41.887 回答
17
这些都是很好的例子，但我选择稍微不同的回答。回想一下数学，∀x。P(x) 的意思是“对于所有的 x，我可以证明 P(x)”。换句话说，它是一种函数，你给我一个 x，我有一个方法可以为你证明。
在类型论中，我们不是在谈论证明，而是在谈论类型。所以在这个空间里，我们的意思是“对于你给我的任何 X 类型，我会给你一个特定的 P 类型”。现在，由于除了 X 是一种类型之外，我们没有给 P 提供太多关于 X 的信息，所以 P 不能用它做很多事情，但是有一些例子。P 可以创建“所有相同类型的对”的类型：P<X> = Pair<X, X> = (X, X). 或者我们可以创建选项 type: P<X> = Option<X> = X | Nil，其中 Nil 是空指针的类型。我们可以从中列出一个清单：List<X> = (X, List<X>) | Nil. 请注意，最后一个是递归的，值List<X>要么是第一个元素是 X，第二个元素是 a 的对，要么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。这种类型可能有很多实现，但无论选择哪一个，您都可以使用所有这些类型。
于 2012-09-08T01:18:41.347 回答
15
直接回答你的问题：
对于通用类型，使用的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 - 从实例方法
MyClass本身的角度来看，T是存在的，因为它不知道真正的类型T - 在 Java 中，
?表示存在类型 - 因此当您在类中时，T基本上是?. 如果你想处理一个存在的实例MyClass，T你可以MyClass<?>像secretMessage()上面的例子一样声明。
如其他地方所讨论的，存在类型有时用于隐藏某些东西的实现细节。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（或执行数据结构内提供的任何操作）。
几乎总是可以在不使用闭包的情况下将具有存在类型的记录转换为记录。闭包也是存在类型的，因为它被关闭的自由变量对调用者是隐藏的。因此，支持闭包但不支持存在类型的语言可以允许您创建共享相同隐藏状态的闭包，就像您将放入对象的存在部分一样。
于 2012-11-30T19:31:10.960 回答
12
存在类型是不透明类型。
想想 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——在类型系统中没有什么可以表达的。您不能声明类型未知的变量，也不能将指针转换为该未知类型。语言不会让你。
于 2009-04-13T01:12:29.683 回答
9
似乎我来晚了，但无论如何，本文档添加了另一种关于存在类型的观点，虽然不是特别与语言无关，但应该更容易理解存在类型：http://www.cs.uu .nl/groups/ST/Projects/ehc/ehc-book.pdf（第 8 章）
普遍和存在量化类型之间的差异可以通过以下观察来表征：
使用具有 ∀ 量化类型的值决定了为量化类型变量的实例化选择的类型。例如，标识函数“id :: ∀aa → a”的调用者确定为这个特定的 id 应用程序选择的类型变量 a 的类型。对于函数应用程序“id 3”，此类型等于 Int。
具有 ∃ 量化类型的值的创建确定并隐藏了量化类型变量的类型。例如，“∃a.(a, a → Int)”的创建者可能已经从“(3, λx → x)”构造了该类型的值；另一个创建者从“('x', λx → ord x)”构造了一个相同类型的值。从用户的角度来看，这两个值具有相同的类型，因此可以互换。该值具有为类型变量 a 选择的特定类型，但我们不知道是哪种类型，因此无法再利用此信息。此值特定类型信息已被“忘记”；我们只知道它存在。
于 2015-11-04T00:33:05.793 回答
5
类型参数的所有值都存在通用类型。存在类型仅存在于满足存在类型约束的类型参数的值。
例如，在 Scala 中，表达存在类型的一种方法是抽象类型，它被限制在某些上限或下限。
trait Existential {
type Parameter <: Interface
}
等效地，受约束的通用类型是存在类型，如下例所示。
trait Existential[Parameter <: Interface]
任何使用站点都可以使用 ，Interface因为任何可实例化的子类型都Existential必须定义type Parameter必须实现Interface.
Scala 中存在类型的退化情况是一种抽象类型，它从不被引用，因此不需要由任何子类型定义。List[_] 这在 Scala和List<?>Java中有效地具有简写符号。
于 2015-06-15T04:01:10.747 回答
3
对抽象数据类型和信息隐藏的研究将存在类型带入了编程语言。将数据类型抽象化会隐藏有关该类型的信息，因此该类型的客户端不能滥用它。假设你有一个对象的引用……有些语言允许你将该引用转换为对字节的引用，并对那块内存做任何你想做的事情。为了保证程序的行为，语言强制您仅通过对象设计者提供的方法对对象的引用进行操作是很有用的。你知道类型存在，但仅此而已。
看：
抽象类型有存在类型，MITCHEL & PLOTKIN
于 2008-11-24T06:48:32.723 回答
2
我创建了这个图表。不知道是不是很严谨。但如果有帮助，我很高兴。
于 2018-12-05T06:43:17.197 回答
-6
据我了解，这是一种描述接口/抽象类的数学方法。
至于 T = ∃X { X a; 整数 f(X); }
对于 C#，它将转换为通用抽象类型：
abstract class MyType<T>{
private T a;
public abstract int f(T x);
}
“存在”只是意味着有某种类型遵守此处定义的规则。
于 2008-11-15T08:04:16.507 回答