¿Cuáles son algunos casos de uso convincentes para los tipos de métodos dependientes?

Los tipos de métodos dependientes, que solían ser una característica experimental antes, ahora se han habilitado por defecto en el tronco , y aparentemente esto parece haber creado algo de emoción en la comunidad Scala.

A primera vista, no es inmediatamente obvio para qué esto podría ser útil. Heiko Seeberger publicó un ejemplo simple de tipos de métodos dependientes aquí , que como se puede ver en el comentario allí, se puede reproducir fácilmente con parámetros de tipo en los métodos. Así que ese no fue un ejemplo muy convincente. (Puede que me falte algo obvio. Corríjame si es así).

¿Cuáles son algunos ejemplos prácticos y útiles de casos de uso para tipos de métodos dependientes donde son claramente ventajosos sobre las alternativas?

¿Qué cosas interesantes podemos hacer con ellos que antes no eran posibles / fáciles?

¿Qué nos compran sobre las características existentes del sistema de tipos?

Además, ¿los tipos de métodos dependientes son análogos o se inspiran en alguna de las características que se encuentran en los sistemas de tipos de otros lenguajes de escritura avanzados como Haskell, OCaml?

Más o menos cualquier uso de tipos de miembros (es decir, anidados) puede dar lugar a la necesidad de tipos de métodos dependientes. En particular, mantengo que sin tipos de métodos dependientes, el patrón de pastel clásico está más cerca de ser un antipatrón.

¿Entonces, cuál es el problema? Los tipos anidados en Scala dependen de su instancia de cierre. En consecuencia, en ausencia de tipos de métodos dependientes, los intentos de usarlos fuera de esa instancia pueden ser frustrantemente difíciles. Esto puede convertir diseños que inicialmente parecen elegantes y atractivos en monstruosidades que son terriblemente rígidas y difíciles de refactorizar.

Ilustraré eso con un ejercicio que doy durante mi curso de entrenamiento Advanced Scala ,

trait ResourceManager {
  type Resource <: BasicResource
  trait BasicResource {
    def hash : String
    def duplicates(r : Resource) : Boolean
  }
  def create : Resource

  // Test methods: exercise is to move them outside ResourceManager
  def testHash(r : Resource) = assert(r.hash == "9e47088d")  
  def testDuplicates(r : Resource) = assert(r.duplicates(r))
}

trait FileManager extends ResourceManager {
  type Resource <: File
  trait File extends BasicResource {
    def local : Boolean
  }
  override def create : Resource
}

class NetworkFileManager extends FileManager {
  type Resource = RemoteFile
  class RemoteFile extends File {
    def local = false
    def hash = "9e47088d"
    def duplicates(r : Resource) = (local == r.local) && (hash == r.hash)
  }
  override def create : Resource = new RemoteFile
}

Es un ejemplo del patrón de pastel clásico: tenemos una familia de abstracciones que se refinan gradualmente a través de una jerarquía ( ResourceManager/ Resourcese refinan por FileManager/ Fileque a su vez se refinan por NetworkFileManager/RemoteFile ). Es un ejemplo de juguete, pero el patrón es real: se usa en todo el compilador Scala y se usó ampliamente en el complemento Scala Eclipse.

Aquí hay un ejemplo de la abstracción en uso,

val nfm = new NetworkFileManager
val rf : nfm.Resource = nfm.create
nfm.testHash(rf)
nfm.testDuplicates(rf)

Tenga en cuenta que la dependencia de la ruta significa que el compilador garantizará que los métodos testHashy solo se puedan invocar con argumentos que le correspondan, es decir. es propio y nada más.testDuplicatesNetworkFileManagerRemoteFiles

Es indudablemente una propiedad deseable, pero ¿y si quisiéramos mover este código de prueba a un archivo fuente diferente? Con los tipos de métodos dependientes es trivialmente fácil redefinir esos métodos fuera de la ResourceManagerjerarquía,

def testHash4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.hash == "9e47088d")

def testDuplicates4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.duplicates(r))

Tenga en cuenta los usos de los tipos de métodos dependientes aquí: el tipo del segundo argumento ( rm.Resource) depende del valor del primer argumento ( rm).

Es posible hacer esto sin tipos de métodos dependientes, pero es extremadamente incómodo y el mecanismo es bastante poco intuitivo: he estado enseñando este curso durante casi dos años, y en ese momento, a nadie se le ha ocurrido una solución de trabajo inesperada.

Pruébalo por ti mismo ...

// Reimplement the testHash and testDuplicates methods outside
// the ResourceManager hierarchy without using dependent method types
def testHash        // TODO ... 
def testDuplicates  // TODO ...

testHash(rf)
testDuplicates(rf)

Después de un corto tiempo luchando con él, probablemente descubrirá por qué yo (o tal vez fue David MacIver, no podemos recordar cuál de nosotros acuñó el término) lo llamo la panadería de la fatalidad.

Editar: el consenso es que Bakery of Doom fue la moneda de David MacIver ...

Para el extra: la forma de Scala de tipos dependientes en general (y los tipos de métodos dependientes como parte de ella) se inspiró en el lenguaje de programación Beta ... surgen naturalmente de la semántica de anidamiento consistente de Beta. No conozco ningún otro lenguaje de programación incluso débilmente convencional que tenga tipos dependientes en esta forma. Los idiomas como Coq, Cayenne, Epigram y Agda tienen una forma diferente de tipeo dependiente, que de alguna manera es más general, pero que difiere significativamente al ser parte de sistemas de tipos que, a diferencia de Scala, no tienen subtipos.

trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}

En otro lugar, podemos garantizar estáticamente que no estamos mezclando nodos de dos gráficos diferentes, por ejemplo:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 

Por supuesto, esto ya funcionó si se define dentro Graph, pero digamos que no podemos modificar Graphy estamos escribiendo una extensión "pimp my library" para ello.

Acerca de la segunda pregunta: los tipos habilitados por esta función son mucho más débiles que los tipos dependientes completos (consulte Programación de tipo dependiente en Agda para obtener una idea de eso). No creo haber visto una analogía antes.

Esta nueva característica es necesaria cuando se utilizan miembros de tipo abstracto concreto en lugar de parámetros de tipo . Cuando se utilizan parámetros de tipo, la dependencia del tipo de polimorfismo familiar se puede expresar en la última versión y algunas versiones anteriores de Scala, como en el siguiente ejemplo simplificado.

trait C[A]
def f[M](a: C[M], b: M) = b
class C1 extends C[Int]
class C2 extends C[String]

f(new C1, 0)
res0: Int = 0
f(new C2, "")
res1: java.lang.String = 
f(new C1, "")
error: type mismatch;
 found   : C1
 required: C[Any]
       f(new C1, "")
         ^

Estoy desarrollando un modelo para la interoperabilidad de una forma de programación declarativa con el estado ambiental. Los detalles no son relevantes aquí (por ejemplo, detalles sobre devoluciones de llamada y similitud conceptual con el modelo de actor combinado con un serializador).

El problema relevante es que los valores de estado se almacenan en un mapa hash y se hace referencia a ellos mediante un valor de clave hash. Las funciones introducen argumentos inmutables que son valores del entorno, pueden llamar a otras funciones y escribir estados en el entorno. Pero las funciones no pueden leer valores del entorno (por lo que el código interno de la función no depende del orden de los cambios de estado y, por lo tanto, sigue siendo declarativo en ese sentido). ¿Cómo escribir esto en Scala?

La clase de entorno debe tener un método sobrecargado que ingrese una función de este tipo para llamar e ingrese las claves hash de los argumentos de la función. Por lo tanto, este método puede llamar a la función con los valores necesarios del mapa hash, sin proporcionar acceso de lectura pública a los valores (por lo tanto, según sea necesario, negando a las funciones la capacidad de leer valores del entorno).

Pero si estas claves hash son cadenas o valores hash enteros, el tipeo estático del tipo de elemento de mapa hash subsume a Any o AnyRef (el código de mapa hash no se muestra a continuación) y, por lo tanto, podría producirse una falta de coincidencia en tiempo de ejecución, es decir, sería posible para poner cualquier tipo de valor en un mapa hash para una clave hash dada.

trait Env {
...
  def callit[A](func: Env => Any => A, arg1key: String): A
  def callit[A](func: Env => Any => Any => A, arg1key: String, arg2key: String): A
}

Aunque no probé lo siguiente, en teoría puedo obtener las claves hash de los nombres de clase en tiempo de ejecución empleando classOf, por lo que una clave hash es un nombre de clase en lugar de una cadena (usando los backticks de Scala para incrustar una cadena en un nombre de clase).

trait DependentHashKey {
  type ValueType
}
trait `the hash key string` extends DependentHashKey {
  type ValueType <: SomeType
}

Así se logra la seguridad de tipo estático.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A