¿Qué se entiende por tipos dependientes de la ruta de Scala?

type-systems path-dependent-type

Question

Escuché que Scala tiene tipos dependientes de la ruta. Tiene algo que ver con las clases internas, pero ¿qué significa esto realmente y por qué me importa?

Answer 1

Mi ejemplo favorito:

case class Board(length: Int, height: Int) {
  case class Coordinate(x: Int, y: Int) { 
    require(0 <= x && x < length && 0 <= y && y < height) 
  }
  val occupied = scala.collection.mutable.Set[Coordinate]()
}

val b1 = Board(20, 20)
val b2 = Board(30, 30)
val c1 = b1.Coordinate(15, 15)
val c2 = b2.Coordinate(25, 25)
b1.occupied += c1
b2.occupied += c2
// Next line doesn''t compile
b1.occupied += c2

Por lo tanto, el tipo de Coordinate depende de la instancia de la Board desde la que se creó la instancia. Hay todo tipo de cosas que se pueden lograr con esto, dando un tipo de seguridad que depende de los valores y no solo de los tipos.

Esto puede sonar como tipos dependientes, pero es más limitado. Por ejemplo, el tipo de occupied depende del valor de la Board . Arriba, la última línea no funciona porque el tipo de c2 es b2.Coordinate , mientras que el tipo de occupied es Set[b1.Coordinate] . Tenga en cuenta que uno puede usar otro identificador con el mismo tipo de b1 , por lo que no es el identificador b1 que está asociado con el tipo. Por ejemplo, los siguientes trabajos:

val b3: b1.type = b1
val c3 = b3.Coordinate(10, 10)
b1.occupied += c3