价值的存在量化 [英] Existential Quantification over Values

问题描述

我遇到了Scala语言中关于值的存在性量化 规范(3.2.10现有类型).

x: y.Inner forSome{val y : Outer}

有人有说明性的用例吗?

T forSome {val x: S}被定义为T forSome { type t <: S with Singleton }.在规范(3.2.1单例类型)中提到了Singletron特性，但是我在Scaladoc中找不到它.在哪里定义?

解决方案

它与类型名称中提到的内部类一起使用非常有用.例如，请参见在 Scala之行:内部类中定义的Graph和Node类.通过某个值的现有量化来写一些未指定图的节点类型.

type SomeNode = g.Node forSome { val g: Graph }

如果您想拥有一个将两个节点作为必须来自同一图的参数的方法，这可能会很有用.

def somethingWithTwoNodes[N <: g.Node forSome { val g: Graph }](n1: N, n2: N) = (n1,n2)

请注意2.7将不接受该方法定义，因为它认为N中存在某种递归.

那么就拥有

val g1 = new Graph
val g2 = new Graph

然后将其编译

somethingWithTwoNodes(g1.newNode, g1.newNode)
somethingWithTwoNodes(g2.newNode, g2.newNode)

但这些不是

somethingWithTwoNodes(g1.newNode, g2.newNode)
somethingWithTwoNodes(g2.newNode, g1.newNode)

对于Singleton特性，它并不是以典型方式真正定义的，即没有用于它的类文件.就像类型Any，AnyVal，AnyRef和Null.它在src/compiler/scala/tools/nsc/symtab/Definitions.scala中与其他类型一起定义，但是我怀疑这是否是非常有用的信息.这也是一个奇怪的野兽，它是最终的特征，这意味着您不能在定义特征或类时将其混入其中，实际上，它更像是编译器将其归因于某种类型的标记，以表示该类型与任何其他类型都是唯一的./p>

I came across existential quantification over values in the Scala Language Specification (3.2.10 Existential Types).

x: y.Inner forSome{val y : Outer}

Does someone have illustrative use cases for it?

T forSome {val x: S} is defined as T forSome { type t <: S with Singleton }. The Singletron trait is mentioned in the Specification (3.2.1 Singleton Types) but I could not find it in the Scaladoc. Where is it defined?

解决方案

It is useful along with inner classes as alluded in the type names. See for example the Graph and Node classes defined in A Tour of Scala: Inner Classes. Existential quantification over a value is used to write the type of the nodes of some unspecified graph.

type SomeNode = g.Node forSome { val g: Graph }

This might be useful if you wanted to have a method that took two nodes as arguments that had to come from the same graph.

def somethingWithTwoNodes[N <: g.Node forSome { val g: Graph }](n1: N, n2: N) = (n1,n2)

Note that 2.7 will not accept that method definition because it thinks there's some sort of recursion in N.

Then if you have

val g1 = new Graph
val g2 = new Graph

then these compile

somethingWithTwoNodes(g1.newNode, g1.newNode)
somethingWithTwoNodes(g2.newNode, g2.newNode)

but these doesn't

somethingWithTwoNodes(g1.newNode, g2.newNode)
somethingWithTwoNodes(g2.newNode, g1.newNode)

As for the Singleton trait, it's not really defined in the typical way, i.e. there isn't a class file for it. It's like the types Any, AnyVal, AnyRef and Null. It is defined in src/compiler/scala/tools/nsc/symtab/Definitions.scala along with these other types, but I doubt that is very useful information to have. It's also an odd beast being a final trait which means you can't mix it in when defining a trait or class, it's really more of a marker that the compiler ascribes to a type to say that it is unique from any other type.

这篇关于价值的存在量化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！