¿Alguna razón por la cual scala no admite explícitamente tipos dependientes?

path-dependent-type dependent-type

Question

Hay tipos dependientes de la ruta y creo que es posible expresar casi todas las características de lenguajes como Epigram o Agda en Scala, pero me pregunto por qué Scala no admite this más explícita, como lo hace muy bien en otras áreas (por ejemplo, , DSL)? ¿Algo que me falta como "no es necesario"?

Answer 1

Asumo que es porque (como sé por experiencia, habiendo usado tipos dependientes en el asistente de pruebas de Coq, que los admite completamente pero no de una manera muy conveniente) los tipos dependientes son una característica de lenguaje de programación muy avanzada que es muy difícil acierte, y puede causar una explosión exponencial en la complejidad en la práctica. Todavía son un tema de investigación en ciencias de la computación.

Answer 2

Conveniencia sintáctica a un lado, la combinación de tipos singleton, tipos dependientes de ruta y valores implícitos significa que Scala tiene un soporte sorprendentemente bueno para tipeo dependiente, como he intentado demostrar shapeless .

El soporte intrínseco de Scala para tipos dependientes es a través de tipos dependientes de ruta . Esto permite que un tipo dependa de una ruta de selector a través de un gráfico de objeto (es decir, valor) como tal,

scala> class Foo { class Bar }
defined class Foo
scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658
scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757
scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>
scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
implicitly[foo1.Bar =:= foo2.Bar]

En mi opinión, lo anterior debería ser suficiente para responder la pregunta "¿Es Scala un lenguaje dependiente de tipado?" en positivo: está claro que aquí tenemos tipos que se distinguen por los valores que son sus prefijos.

Sin embargo, a menudo se objeta que Scala no es un lenguaje de tipo "completamente" dependiente porque no tiene suma dependiente y tipos de productos como los que se encuentran en Agda o Coq o Idris como intrínsecos. Creo que esto refleja una fijación en la forma sobre los fundamentos hasta cierto punto, sin embargo, intentaré y mostraré que Scala está mucho más cerca de estos otros idiomas de lo que normalmente se reconoce.

A pesar de la terminología, los tipos de suma dependientes (también conocidos como tipos de Sigma) son simplemente un par de valores donde el tipo del segundo valor depende del primer valor. Esto es directamente representable en Scala,

scala> trait Sigma {
| val foo: Foo
| val bar: foo.Bar
| }
defined trait Sigma
scala> val sigma = new Sigma {
| val foo = foo1
| val bar = new foo.Bar
| }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

y, de hecho, esta es una parte crucial de la codificación de tipos de métodos dependientes que se necesita para escapar de la ''panadería de la fatalidad'' en Scala antes de 2.10 (o antes a través de la opción de compilador de Scala de tipos de método experimental-independiente).

Los tipos de productos dependientes (también conocidos como tipos de Pi) son esencialmente funciones de valores a tipos. Son clave para la representación de vectores de tamaño estático y los otros niños de póster para lenguajes de programación de tipos dependientes. Podemos codificar tipos de Pi en Scala usando una combinación de tipos dependientes de ruta, tipos de singleton y parámetros implícitos. Primero definimos un rasgo que va a representar una función desde un valor de tipo T a un tipo U,

scala> trait Pi[T] { type U }
defined trait Pi

Podemos definir un método polimórfico que use este tipo,

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

(tenga en cuenta el uso del tipo de ruta dependiente pi.U en el tipo de resultado List[pi.U] ). Dado un valor de tipo T, esta función devolverá una lista (n vacía) de valores del tipo correspondiente a ese valor T particular.

Ahora vamos a definir algunos valores adecuados y testigos implícitos para las relaciones funcionales que queremos mantener,

scala> object Foo
defined module Foo
scala> object Bar
defined module Bar
scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11
scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

Y ahora aquí está nuestra función de uso de tipo Pi en acción,

scala> depList(Foo)
res2: List[fooInt.U] = List()
scala> depList(Bar)
res3: List[barString.U] = List()
scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>
scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
implicitly[res2.type <:< List[String]]
^
scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>
scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
implicitly[res3.type <:< List[Int]]

(nótese que aquí usamos el operador de testificación de subtipo <:< Scala en lugar de =:= porque res2.type y res3.type son tipos de singleton y por lo tanto más precisos que los tipos que estamos verificando en el RHS).

En la práctica, sin embargo, en Scala no comenzaríamos codificando los tipos Sigma y Pi y luego procederíamos desde allí como lo haríamos en Agda o Idris. En cambio, usaríamos tipos dependientes de ruta, tipos de singleton e implícitos directamente. Puede encontrar numerosos ejemplos de cómo esto se desarrolla en forma informe: tipos de tamaño , registros extensibles , HLists integrales , chatarra , repisas genéricas , etc.

La única objeción restante que puedo ver es que en la codificación anterior de tipos Pi requerimos que los tipos únicos de los valores dependientes sean expresables. Desafortunadamente, en Scala esto solo es posible para valores de tipos de referencia y no para valores de tipos que no son de referencia (especialmente, por ejemplo, Int). Esto es una lástima, pero no una dificultad intrínseca: el verificador de tipos de Scala representa los tipos únicos de valores no de referencia internamente, y ha habido un couple de experiments al hacerlos directamente expresables. En la práctica, podemos solucionar el problema con una codificación de nivel natural bastante estándar de los números naturales .

En cualquier caso, no creo que esta ligera restricción de dominio pueda usarse como una objeción al estado de Scala como un lenguaje dependiente. Si es así, entonces podría decirse lo mismo para ML dependiente (que solo permite dependencias en valores numéricos naturales), lo que sería una conclusión extraña.

Answer 3

Creo que los tipos dependientes de ruta de Scala solo pueden representar tipos Σ, pero no tipos path. Esta:

trait Pi[T] { type U }

no es exactamente un tipo Π. Por definición, el tipo,, o producto dependiente, es una función cuyo tipo de resultado depende del valor del argumento, que representa el cuantificador universal, es decir, ∀x: A, B (x). En el caso anterior, sin embargo, depende solo del tipo T, pero no de algún valor de este tipo. El rasgo Pi mismo es un tipo Σ, un cuantificador existencial, es decir, ∃x: A, B (x). La autorreferencia del objeto en este caso actúa como variable cuantificada. Sin embargo, cuando se pasa como un parámetro implícito, se reduce a una función de tipo ordinario, ya que se resuelve en términos de tipo de letra. La codificación del producto dependiente en Scala puede verse como la siguiente:

trait Sigma[T] {
val x: T
type U //can depend on x
}
// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won''t compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U

La pieza que falta aquí es la capacidad de restringir estáticamente el campo x al valor esperado t, formando efectivamente una ecuación que representa la propiedad de todos los valores que habitan el tipo T. Junto con nuestros tipos,, usados ​​para expresar la existencia del objeto con la propiedad dada, el se forma la lógica, en la cual nuestra ecuación es un teorema que debe ser probado.

En una nota lateral, en el caso real, el teorema puede ser altamente no trivial, hasta el punto en que no puede derivarse automáticamente del código o resolverse sin una cantidad significativa de esfuerzo. Incluso se puede formular la Hipótesis de Riemann de esta manera, solo para encontrar que la firma es imposible de implementar sin probarla, haciendo un ciclo para siempre o lanzando una excepción.