什么是存在类型？

Question

我阅读了维基百科文章存在类型。我了解到它们被称为存在类型，因为它们使用了存在运算符（∃）。但是我不确定它的意义是什么。那么，如何区分

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

并且

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

?

- Claudiu

---

你在询问“有一些狗”和“一切都是狗”之间的区别。 - Jim Balter

Answer 1

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

- Kannan Goundan

---

@Kannan，非常有用的回答，但有点难以理解：1. 我认为如果您可以更明确地说明存在性和普遍性类型的双重性质会更有帮助。我只是偶然发现了您非常相似地表述了前两段；直到后来您才明确指出两个定义基本上是相同的，只是用"I"和"you"颠倒过来。此外，我不立即明白"I"和"you"应该指什么。 - stakx - no longer contributing

我使用∃B明确量词的作用范围。使用通配符语法时，量词被隐含（实际上List<List<?>>意味着∃T:List<List<T>>而不是List<∃T:List<T>>）。 此外，显式量化使您可以引用类型（我修改了示例以利用这一点，通过将类型B的字节码存储在临时变量中来实现）。 - Kannan Goundan

这里使用的数学符号非常草率，但我认为这不是回答者的错（这是标准）。尽管如此，最好不要滥用存在量词和普遍量词... - Noldorin

@Kannan_Goundan，我想知道是什么让你说Java通配符是这个版本的很有限。你知道你可以用纯Java实现你的first runAllCompilers示例函数（使用一个辅助函数来检索（给出一个名称）通配符参数吗？ - Lionel Parreaux

Java会隐式地将限定词放在最内层的类型表达式上。List<List<?>>的意思是List<∃T:List<T>>。在Java中没有办法指定∃T:List<List<T>>。runAllCompilers能够工作是因为在这种情况下限制恰好合适。 - Kannan Goundan

Answer 2

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

- Apocalisp

---

这实际上是更好的解释。 - johnrubythecat

Answer 3

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

关于存在类型的每个细节（例如给出精确定义、列出所有可能的用途、它们与抽象数据类型的关系等），我无法回答，因为我对此并不了解。我只会演示（使用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<α>，它表示二叉树中的一个节点。每个节点存储某种类型α的值，并具有对相同类型的可选左和右子树的引用。

一个函数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   |                  
=====================+=====================================

- stakx - no longer contributing

---

好的解释。您不需要将t.value强制转换为Object，您可以直接将其称为Object。我认为存在类型使该方法更加通用，因为如此。您所知道的关于t.value的唯一信息就是它是一个Object，而您可以对α说一些特定的东西（例如α扩展Serializable） 。 - Craig P. Motlin

我现在认为我的答案并没有真正解释什么是存在类型，所以我考虑写另一个答案，更像Kannan Goudan的答案的前两段，我认为那更接近“真相”。话虽如此，@Craig：将泛型与Object进行比较非常有趣：虽然两者都类似于使您能够编写静态类型独立的代码，但前者（泛型）并不会为了实现这个目标而丢弃几乎所有可用的类型信息。在这个特定意义上，泛型在我看来是对Object的一种补救。 - stakx - no longer contributing

在这段代码（来自Effective Java）中，public static void swap(List<?> list, int i, int j) { swapHelper(list, i, j); } private static <E> void swapHelper(List<E> list, int i, int j) { list.set(i, list.set(j, list.get(i))); }，E是一个通用类型，而?代表的是一个存在类型？ - Kevin Meredith

这个答案是不正确的。在类型 int height(Tree<?> t) 中的 ? 仍然未知，并且仍然由调用者确定，因为调用者可以选择传递哪棵树。即使人们称之为 Java 中的存在类型，它也不是。? 占位符可以在某些情况下用于实现 Java 中的存在类型，但这不是其中之一。 - Peter Hall

Answer 4

这些都是好的例子，但我选择用稍微不同的方式来回答。从数学上回想一下，∀x.P(x)意味着“对于所有的x，我可以证明P(x)”。换句话说，它是一种函数，你给我一个x，我有一种方法来证明它。

在类型理论中，我们讨论的不是证明，而是类型。因此，在这个空间中，我们的意思是“对于你给我的任何类型X，我将给你一个特定的类型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 的信息，只是确定存在一个 X 类型。

这有什么用处呢？P 可能是一种具有公开其内部类型 X 的方法的类型。例如，一个对象隐藏了其状态 X 的内部表示。虽然我们不能直接操作它，但可以通过观察 P 的影响来了解其效果。可能会有许多实现这种类型的方式，但无论选择哪个特定的实现，都可以使用所有这些类型。

- Rogon

---

知道它是一个P<X>而不是P，这个函数会获得什么好处呢？（假设其功能和容器类型相同，但你不知道它是否包含X） - Claudiu

严格来说，“∀x.P(x)”并不涉及到“P(x)”的可证明性，只涉及到其真假。 - R.. GitHub STOP HELPING ICE

"∀x. P(x)"的意思是“对于所有的x，我可以证明P(x)”。-- 呃，不，这完全不是它的意思。它是一个关于所有x的P(x)的断言。换句话说，它是一种函数，你给我一个x，我有一种方法来为你证明它。-- 这些是无意义的话语。 - Jim Balter

Answer 5

直接回答您的问题：

使用通用类型时，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，但你必须知道每次使用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中，所有非final的非原始类型都部分存在性。这可能听起来很奇怪，但因为声明为Object的变量可以潜在地是Object的子类，所以你不能声明特定的类型，只能是“该类型或其子类”。因此，对象表示为一些状态加上一个操作该状态的函数列表 - 要调用哪个函数由查找在运行时确定。这非常像上面使用存在类型的情况，其中你有一个存在性状态部分和一个操作该状态的函数。

在没有子类型和强制转换的静态类型编程语言中，存在类型允许管理不同类型对象的列表。列表T不能包含T。然而，T列表可以包含任何T的变体，从而使您可以将许多不同类型的数据放入列表中，并按需将它们全部转换为int（或执行提供在数据结构内的任何操作）。

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

- Dobes Vandermeer

---

很棒的解释！这个答案应该得到更多的赞。 - Yogesh Umesh Vaity

Answer 6

看起来我来晚了，但不管怎样，这篇文档提供了另一种关于存在类型的视角，虽然不是特别与语言无关，但应该相对容易理解存在类型：Dijkstra, Atze - Essential Haskell（第8章）。

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

- 使用具有∀量化类型的值确定要选择哪种类型来实例化量化类型变量。例如，identity函数“id :: ∀a.a → a”的调用者确定了要为此特定应用程序选择哪种类型变量a的类型。对于函数应用“id 3”，此类型等于Int。 - 具有∃量化类型的值的创建确定并隐藏了量化类型变量的类型。例如，“∃a。（a，a→Int）”的创建者可能已经从“(3，λx→x)”构造了该类型的值；另一个创建者已经从“(’x’，λx→ord x)”构造了具有相同类型的值。从用户的角度来看，这两个值具有相同的类型，因此可以互换使用。该值具有为类型变量a选择的特定类型，但我们不知道是哪种类型，因此无法再利用此信息。该值特定类型信息已被“遗忘”；我们只知道它存在。

- themarketka

Answer 7

存在类型是一种不透明类型。

想象一下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类型——在类型系统中无法表达。你不能声明一个类型未知的变量，也不能将指针转换为该未知类型。语言不允许这样做。

- Bartosz Milewski

---

这样行不通。如果read的签名是∃T.read(T file, ...)，那么你无法将任何东西作为第一个参数传递。可行的方法是让fopen返回文件句柄和一个由相同存在范围限定的读取函数：∃T.(T, read(T file, ...))。 - Kannan Goundan

这似乎只是在谈论ADT。 - kizzx2

"没有 exfile 的类型！" - 那么你如何将其传递给 read？你如何将其与其他“无类型”的变量区分开来？“在类型系统中无法表达的任何内容” - 那么你的语言设计是有问题的。 - Jim Balter

Answer 8

一种通用类型适用于类型参数的所有值。存在类型仅适用于满足存在类型限制的类型参数的值。

例如，在Scala中表达存在类型的一种方式是将抽象类型约束为某些上界或下界。

trait Existential {
  type Parameter <: Interface
}

等价地，受限的通用类型是存在类型，如以下示例所示。

trait Existential[Parameter <: Interface]

任何使用站点都可以使用“接口”，因为“存在类型”的任何可实例化子类型都必须定义“类型参数”，该类型参数必须实现“接口”。

在Scala中，存在类型的退化情况是一个抽象类型，它从未被引用，因此不需要由任何子类型定义。这有效地具有List[_]在Scala中和Java中的List<?>的速记符号。

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

- Shelby Moore III

---

阅读了上面的一些材料后，我觉得你已经很好地总结了我的理解：通用类型 ∀x.f(x) 对其接收函数是不透明的，而存在类型 ∃x.f(x) 则被限制为具有某些属性。通常，所有参数都是存在类型，因为它们的函数将直接操作它们；但是，通用参数可能具有通用类型，因为该函数不会在基本通用操作之外管理它们，例如获取引用，如：∀x.∃array.copy(src:array[x] dst:array[x]){...}。 - George

如此描述：https://stackoverflow.com/a/19413755/3195266，类型成员可以通过身份类型模拟全称量化。当然，对于类型参数存在量化，有“forSome”。 - Netsu

Answer 9

研究抽象数据类型和信息隐藏将存在类型引入了编程语言。使数据类型抽象化可以隐藏关于该类型的信息，因此该类型的客户端无法滥用它。假设您有一个对象的引用...一些语言允许您将该引用强制转换为字节的引用并对该内存块执行任何操作。为了保证程序行为的目的，语言强制仅通过对象设计者提供的方法来操作对象的引用。您知道类型存在，但不知道更多信息。

参见：抽象类型具有存在类型，MITCHEL＆PLOTKIN http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf

- ja

Answer 10

我创建了这个图表。我不知道它是否严谨，但如果它有帮助的话，我很高兴。

- v.oddou