我通读了维基百科上关于存在类型的文章。我认为它们之所以被称为存在类型是因为存在操作符(∃)。但我不知道这有什么意义。有什么区别
T = ∃X { X a; int f(X); }
and
T = ∀x { X a; int f(X); }
?
我通读了维基百科上关于存在类型的文章。我认为它们之所以被称为存在类型是因为存在操作符(∃)。但我不知道这有什么意义。有什么区别
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关于统一抽象类型和存在类型的建议的启发。随附的幻灯片有助于理解。
其他回答
这些都是很好的例子,但我选择稍微不同的答案。回想一下数学,∀x。P(x)表示"对于所有x,我可以证明P(x)"换句话说,它是一种函数,你给我一个x,我有一个方法来证明它。
In type theory, we are not talking about proofs, but of types. So in this space we mean "for any type X you give me, I will give you a specific type P". Now, since we don't give P much information about X besides the fact that it is a type, P can't do much with it, but there are some examples. P can create the type of "all pairs of the same type": P<X> = Pair<X, X> = (X, X). Or we can create the option type: P<X> = Option<X> = X | Nil, where Nil is the type of the null pointers. We can make a list out of it: List<X> = (X, List<X>) | Nil. Notice that the last one is recursive, values of List<X> are either pairs where the first element is an X and the second element is a List<X> or else it is a null pointer.
现在,在数学∃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来观察它的效果。这种类型可以有很多实现,但无论选择哪一种,您都可以使用所有这些类型。
我认为将存在类型与普遍类型一起解释是有意义的,因为这两个概念是互补的,即一个是另一个的“相反”。
我无法回答关于存在类型的每一个细节(比如给出一个确切的定义,列出所有可能的用法,它们与抽象数据类型的关系,等等),因为我在这方面的知识不够丰富。我将只演示(使用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<α>,表示二叉树中的一个节点。每个节点存储一个α类型的值,并引用相同类型的可选左右子树。 一个函数高度,它返回从任何叶节点到根节点t的最远距离。
现在,让我们把上面关于高度的伪代码转换成正确的Java语法!(为了简洁起见,我将继续省略一些样板文件,例如面向对象和可访问性修饰符。)我将展示两种可能的解决方案。
1. 通用型解决方案:
最明显的解决方法是通过在其签名中引入类型参数α来简单地使height成为泛型:
<α> int height(Tree<α> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
这将允许您在该函数中声明变量并创建α类型的表达式(如果您愿意的话)。但是…
2. 存在型解:
如果你看一下我们的方法体,你会注意到我们实际上并没有访问或使用任何α类型的东西!没有那种类型的表达式,也没有那种类型声明的变量……那么,为什么我们要让身高通用呢?为什么我们不能简单地忘记α?事实证明,我们可以:
int height(Tree<?> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
正如我在回答的一开始所写的,存在型和普遍型在本质上是互补/双重的。因此,如果通用类型解决方案是使高度更加泛型,那么我们应该期望存在类型具有相反的效果:通过隐藏/删除类型参数α,使它不那么泛型。
因此,您不能再在此方法中引用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 |
=====================+=====================================
据我所知,这是一种描述接口/抽象类的数学方法。
对于T =∃X {X a;int f (X);}
对于c#,它可以转换为泛型抽象类型:
abstract class MyType<T>{
private T a;
public abstract int f(T x);
}
"存在主义"的意思是有某种类型服从这里定义的规则。
直接回答你的问题:
对于通用类型,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();
From the perspective of a client of MyClass, T is universal because you can substitute any type for T when you use that class and you must know the actual type of T whenever you use an instance of MyClass From the perspective of instance methods in MyClass itself, T is existential because it doesn't know the real type of T In Java, ? represents the existential type - thus when you are inside the class, T is basically ?. If you want to handle an instance of MyClass with T existential, you can declare MyClass<?> as in the secretMessage() example above.
存在类型有时用于隐藏某些东西的实现细节,如在其他地方讨论的那样。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不是。但这里的重点是,您正在捕获某种状态加上对该状态进行操作的函数列表,并且您不知道状态部分的真实类型,但函数知道,因为它们已经与该类型匹配。
Now, in Java all non-final non-primitive types are partly existential. This may sound strange, but because a variable declared as Object could potentially be a subclass of Object instead, you cannot declare the specific type, only "this type or a subclass". And so, objects are represented as a bit of state plus a list of functions that operate on that state - exactly which function to call is determined at runtime by lookup. This is very much like the use of existential types above where you have an existential state part and a function that operates on that state.
在没有子类型和类型转换的静态类型编程语言中,存在类型允许管理不同类型对象的列表。T<Int>的列表不能包含T<Long>。然而,T<?>可以包含T的任何变体,允许将许多不同类型的数据放入列表中,并根据需要将它们全部转换为int(或执行数据结构内部提供的任何操作)。
几乎总是可以将具有存在类型的记录转换为不使用闭包的记录。闭包也是存在类型的,因为它关闭的自由变量对调用者是隐藏的。因此,一种支持闭包但不支持存在类型的语言可以允许您创建闭包,这些闭包共享与放入对象的存在部分相同的隐藏状态。
存在类型的值,例如∃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。