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

relacion de uso

Question

Los tipos de métodos dependientes, que solían ser una función experimental anterior, ahora se han habilitado de forma predeterminada en el tronco , y aparentemente esto parece haber creado cierto entusiasmo en la comunidad de Scala.

A primera vista, no es inmediatamente obvio para qué podría ser útil. Heiko Seeberger publicó un ejemplo simple de tipos de métodos dependientes here , que como se puede ver en el comentario, se puede reproducir fácilmente con parámetros de tipo en los métodos. Entonces ese no era un ejemplo muy convincente. (Puede que me esté perdiendo algo obvio. Por favor corrígeme 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 del sistema de tipos existentes?

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

Answer 1

Esta nueva característica es necesaria cuando se usan miembros de tipo abstracto concreto en lugar de parámetros de tipo . Cuando se usan parámetros de tipo, la dependencia del tipo de polimorfismo familiar se puede expresar en la última 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, "")
^

Answer 2

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

El problema relevante es que los valores de estado se almacenan en un mapa hash y se referencian mediante un valor de clave hash. Las funciones ingresan argumentos inmutables que son valores del entorno, pueden llamar a otras funciones y escribir el estado 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, permanece declarativo en ese sentido). ¿Cómo se escribe esto en Scala?

La clase de entorno debe tener un método sobrecargado que ingrese dicha función 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 público de lectura a los valores (por lo tanto, según sea necesario, denegar funciones la capacidad de leer valores del entorno).

Pero si estas claves hash son cadenas o valores hash enteros, la tipificación estática del tipo de elemento de mapa hash subsumes a Any o AnyRef (el código de código hash no se muestra a continuación), y así podría producirse un desajuste en tiempo de ejecución, es decir, sería posible para poner cualquier tipo de valor en un mapa hash para una determinada clave hash.

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 classOf lo siguiente, en teoría puedo obtener las claves hash de los nombres de clase en tiempo de ejecución empleando classOf , así que una clave hash es un nombre de clase en lugar de una cadena (usando los trazos 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í que se logra seguridad de tipo estático.

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

Answer 3

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

¿Entonces, cuál es el problema? Los tipos anidados en Scala dependen de su instancia adjunta. 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.

Lo ilustraré con un ejercicio que doy durante mi curso de capacitación 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 clásico de tortas: tenemos una familia de abstracciones que se refinan gradualmente a través de una jerarquía ( ResourceManager / Resource son refinados por FileManager / File que a su vez son refinados por NetworkFileManager / RemoteFile ). Es un ejemplo de juguete, pero el patrón es real: se usa en todo el compilador de Scala y se usó extensamente 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 ruta significa que el compilador garantizará que los métodos testHash y testDuplicates en NetworkFileManager solo pueden testDuplicates con los argumentos que le corresponden, es decir. son sus propios RemoteFiles , y nada más.

Es indudablemente una propiedad deseable, pero supongamos que quisiéramos mover este código de prueba a un archivo fuente diferente. Con los tipos de métodos dependientes es muy fácil redefinir esos métodos fuera de la jerarquía de ResourceManager ,

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 intuitivo: he estado enseñando este curso durante casi dos años, y en ese momento, nadie ha presentado una solución de trabajo espontánea.

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 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) llamo a esto la panadería de la perdición.

Edición: el consenso es que Bakery of Doom fue la moneda de David MacIver ...

Por la bonificación: 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 débilmente convencional que tenga tipos dependientes en esta forma. Los lenguajes como Coq, Cayenne, Epigram y Agda tienen una forma diferente de tipado dependiente, que en cierto modo es más general, pero que difiere significativamente al formar parte de sistemas de tipo que, a diferencia de Scala, no tienen subtipado.

Answer 4

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 definió dentro de Graph , pero dice que no podemos modificar Graph y estamos escribiendo una extensión "pimp my library" para ello.

Acerca de la segunda pregunta: los tipos habilitados por esta característica son mucho más débiles que los tipos dependientes completos (para más información, consulte la Programación de Dependiente Escrito en Agda ). No creo haber visto una analogía anteriormente.