Cuantificación existencial sobre los valores

Question

Encontré la cuantificación existencial sobre los valores en el lenguaje Scala Especificación (3.2.10 Tipos existenciales).

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

¿Alguien tiene casos de uso ilustrativos para él?

T forSome {val x: S} se define como T forSome { type t <: S with Singleton }. El rasgo de Singletron se menciona en la Especificación (3.2.1 Tipos de Singleton) pero no pude encontrarlo en el Scaladoc. ¿Dónde está definido?

Answer 1

Es útil junto con las clases internas como se alude en los nombres de tipo. Ver por ejemplo las clases Graph y Node definidas en A Tour of Scala: Inner Classes. La cuantificación existencial sobre un valor se usa para escribir el tipo de los nodos de algún gráfico no especificado.

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

Esto podría ser útil si se quería tener un método que tuvo dos nodos como argumentos que tenían que venir de la misma gráfica.

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

Tenga en cuenta que 2,7 no aceptará que la definición del método, ya que cree que hay algún tipo de recursividad en N.

Entonces, si usted tiene

val g1 = new Graph 
val g2 = new Graph 

entonces estos compilar

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

pero estos no lo hacen

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

En cuanto al rasgo de Singleton, no está realmente definido de la manera típica, es decir, no hay un archivo de clase para él. Es como los tipos Any, AnyVal, AnyRef y Null. Se define en src/compiler/scala/tools/nsc/symtab/Definitions.scala junto con estos otros tipos, pero dudo que sea una información muy útil. También es una bestia extraña que es un rasgo final que significa que no se puede mezclar cuando se define un rasgo o clase, en realidad es más un marcador que el compilador atribuye a un tipo para decir que es único de cualquier otro tipo.

Answer 2

La primera mitad de this paper usa esta técnica para generar un tipo de secuencia.