什么是存在类型? [英] What is an existential type?

问题描述

我通读了Wikipedia文章 现有类型 .我发现由于存在运算符(∃)，它们被称为存在类型.不过，我不确定它的意义是什么.

I read through the Wikipedia article Existential types. I gathered that they're called existential types because of the existential operator (∃). I'm not sure what the point of it is, though. What's the difference between

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

和

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

?

推荐答案

当有人定义通用类型∀X时，他们说:您可以插入所需的任何类型，我不需要知道关于要执行工作的类型的任何内容，我只会将其不透明地称为X .

When someone defines a universal type ∀X they're saying: You can plug in whatever type you want, I don't need to know anything about the type to do my job, I'll only refer to it opaquely as X.

当某人定义存在类型∃X时，他们说:在这里我将使用所需的任何类型；您不会对类型一无所知，因此只能将其不透明地称为X .

When someone defines an existential type ∃X they're saying: I'll use whatever type I want here; you wont know anything about the type, so you can only refer to it opaquely as X.

通用类型使您可以编写以下内容:

Universal types let you write things like:

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

copy函数不知道T实际是什么，但不需要.

The copy function has no idea what T will actually be, but it doesn't need to.

现有类型可以让您编写如下内容:

Existential types would let you write things like:

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.

Each virtual machine implementation in the list can have a different bytecode type. The runAllCompilers function has no idea what the bytecode type is, but it doesn't need to; all it does is relay the bytecode from VirtualMachine.compile to VirtualMachine.run.

Java类型通配符(例如:List<?>)是存在类型的一种非常有限的形式.

Java type wildcards (ex: List<?>) are a very limited form of existential types.

更新:忘记了您可以使用通用类型模拟存在类型.首先，包装通用类型以隐藏type参数.其次，反转控制(这有效地交换了以上定义中的"you"和"I"部分，这是存在性和通用性之间的主要区别).

Update: Forgot to mention that you can sort of simulate existential types with universal types. First, wrap your universal type to hide the type parameter. Second, invert control (this effectively swaps the "you" and "I" part in the definitions above, which is the primary difference between existentials and universals).

// 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视为不透明.

Now we can have the VMWrapper call our own VMHandler which has a universally typed handle function. The net effect is the same, our code has to treat B as opaque.

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);
         }
      });
   }
}

VM实现示例:

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);
   }
}

这篇关于什么是存在类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！