Existential Quantification over Values

Question

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?

Answer 1

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.

Answer 2

The first half of this paper uses this technique to build a stream type.