我通读了维基百科上关于存在类型的文章。我认为它们之所以被称为存在类型是因为存在操作符(∃)。但我不知道这有什么意义。有什么区别

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

and

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

?


当前回答

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

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

trait Existential {
  type Parameter <: Interface
}

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

trait Existential[Parameter <: Interface]

任何使用站点都可以使用接口,因为存在的任何可实例化子类型必须定义必须实现接口的类型Parameter。

在Scala中,存在类型的退化情况是一种抽象类型,它永远不会被引用,因此不需要由任何子类型定义。这在Scala中有效地简化了List[_]和List<?Java中的>。

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

其他回答

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

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

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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

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

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

trait Existential {
  type Parameter <: Interface
}

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

trait Existential[Parameter <: Interface]

任何使用站点都可以使用接口,因为存在的任何可实例化子类型必须定义必须实现接口的类型Parameter。

在Scala中,存在类型的退化情况是一种抽象类型,它永远不会被引用,因此不需要由任何子类型定义。这在Scala中有效地简化了List[_]和List<?Java中的>。

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

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

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