什么是存在主义类型？

Question

我阅读了维基百科文章的存在类型.我认为,由于存在运算符(∃),它们被称为存在类型.不过,我不确定它的重点是什么.有什么区别

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

和

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

？

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

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

Answer 2

的值的存在的类型等?x. F(x) 是一对含有一些类型 x和值的类型F(x).而像多态类型的值?x. F(x)是一个取一些类型并产生类型值的函数.在这两种情况下,类型都会关闭某些类型的构造函数.xF(x)F

请注意,此视图混合了类型和值.存在证明是一种类型和一种价值.通用证明是按类型索引的整个值系列(或从类型到值的映射).

因此,您指定的两种类型之间的区别如下:

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

这意味着:type的值T包含一个名为X,值a:X和函数的类型f:X->int.类型值的生产者T可以选择任何类型,X消费者也无法了解任何类型X.除了它有一个被调用的例子,a并且这个值可以int通过赋予它来变成a f.换句话说,类型的值T知道如何以int某种方式产生.好吧,我们可以消除中间类型,X然后说:

T = int

普遍量化的一个有点不同.

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

这意味着:类型的值T可以被赋予任何类型X,并且它将产生一个值a: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.

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<?>,表示二叉树中的节点.每个节点存储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   |                  
=====================+=====================================

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,第二个元素是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.可能有很多这种类型的实现,但无论选择哪一种,都可以使用所有这些类型.

Answer 5

存在类型是不透明类型.

想想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,不是a char*,不是struct File - 你可以在类型系统中表达任何东西.您不能声明类型未知的变量,也不能将指针转换为该未知类型.语言不会让你.

Answer 6

直接回答你的问题:

使用通用类型时,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(或在数据结构内部提供任何操作).

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

Answer 7

似乎我来得有点迟了,但无论如何,这个文档增加了另一种关于存在类型的看法,虽然不是特定于语言不可知的,但应该更容易理解存在类型: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选择的特定类型,但我们不知道哪种类型,因此无法再利用此信息.该值特定类型信息已被"遗忘"; 我们只知道它存在.

Answer 8

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

例如，在 Scala 中，表达存在类型的一种方式是抽象类型，该类型受限于某些上限或下限。

trait Existential {
  type Parameter <: Interface
}

等效地，受约束的通用类型是存在类型，如下例所示。

trait Existential[Parameter <: Interface]

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

甲退化情况Scala中一种存在类型的是一种抽象的类，其从未提及，因此不需要由任何亚型来定义。这List[_] 在 Scala和List<?>Java 中有一个有效的速记符号。

我的回答受到 Martin Odersky提议的统一抽象类型和存在类型的启发。在伴随滑动有助于理解。