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

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 esto de manera más explícita como lo hace muy bien en otras áreas (digamos , DSL)? ¿Algo que me falta como "no es necesario"?

Dejando de lado la conveniencia sintáctica, la combinación de tipos singleton, tipos dependientes de la ruta y valores implícitos significa que Scala tiene un soporte sorprendentemente bueno para la escritura dependiente, como he intentado demostrar en informe .

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

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 a la pregunta "¿Es Scala un lenguaje de escritura dependiente?" 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 "totalmente" dependiente porque no tiene tipos de producto y suma dependientes 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é mostrar que Scala está mucho más cerca de estos otros lenguajes de lo que normalmente se reconoce.

A pesar de la terminología, los tipos de suma dependientes (también conocidos como tipos Sigma) son simplemente un par de valores donde el tipo del segundo valor depende del primer valor. Esto se puede representar directamente 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 los tipos de métodos dependientes que se necesita para escapar de 'Bakery of Doom' en Scala antes de 2.10 (o antes a través de la opción del compilador Scala de tipos de métodos dependientes experimentales).

Los tipos de productos dependientes (también conocidos como tipos Pi) son esencialmente funciones de valores a tipos. Son clave para la representación de vectores de tamaño estático y los otros elementos secundarios del cartel para los lenguajes de programación de tipo dependiente. Podemos codificar tipos Pi en Scala usando una combinación de tipos dependientes de ruta, tipos 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 entonces definir un método polimórfico que utilice 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 dependiente de la ruta pi.Uen 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 en particular.

Ahora definamos algunos valores adecuados y testigos implícitos de 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]]

(tenga en cuenta que aquí usamos el <:<operador testigo de subtipos de Scala en lugar de =:=porque res2.typey res3.typeson tipos 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 desde allí como lo haríamos en Agda o Idris. En su lugar, usaríamos tipos dependientes de la ruta, tipos singleton e implícitos directamente. Puede encontrar numerosos ejemplos de cómo se desarrolla esto en informes sin forma: tipos de tamaño , registros extensibles , listas H completas , desecho de su plantilla , cremalleras 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 singleton 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 pena, pero no una dificultad intrínseca: el verificador de tipos de Scala representa los tipos singleton de valores no de referencia internamente, y ha habido un par de experimentos para hacerlos directamente expresables. En la práctica, podemos solucionar el problema con una codificación a nivel de tipo bastante estándar de los números naturales .

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

Asumiría que se debe a que (como sé por experiencia, habiendo utilizado tipos dependientes en el asistente de prueba de Coq, que los admite completamente pero aún no de una manera muy conveniente) los tipos dependientes son una característica del lenguaje de programación muy avanzada que es realmente difícil de hacerlo bien, y puede causar una explosión exponencial en la complejidad en la práctica. Siguen siendo un tema de investigación en ciencias de la computación.

Creo que los tipos dependientes de la ruta de Scala solo pueden representar tipos Σ, pero no tipos Π. 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 en sí 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 parámetro implícito, se reduce a una función de tipo ordinaria, ya que se resuelve por tipo. La codificación del producto dependiente en Scala puede tener el siguiente aspecto:

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 en el tipo T.Junto con nuestros tipos Σ, utilizados para expresar la existencia de un objeto con una propiedad dada, el Se forma la lógica, en la que nuestra ecuación es un teorema a probar.

En una nota al margen, en el caso real, el teorema puede ser muy 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 realmente, repitiendo para siempre o lanzando una excepción.

La pregunta era sobre el uso de la función de escritura dependiente de manera más directa y, en mi opinión, sería beneficioso tener un enfoque de escritura dependiente más directo que el que ofrece Scala.
Las respuestas actuales intentan argumentar la pregunta a nivel teórico de tipo. Quiero darle un giro más pragmático. Esto puede explicar por qué las personas están divididas en el nivel de soporte de los tipos dependientes en el lenguaje Scala. Es posible que tengamos en mente definiciones algo diferentes. (por no decir que uno tiene razón y el otro está equivocado).

Este no es un intento de responder a la pregunta de qué tan fácil sería convertir Scala en algo como Idris (me imagino muy difícil) o escribir una biblioteca que ofrezca soporte más directo para capacidades similares a Idris (como singletonsintenta estar en Haskell).

En cambio, quiero enfatizar la diferencia pragmática entre Scala y un lenguaje como Idris.
¿Qué son los bits de código para expresiones de nivel de valor y tipo? Idris usa el mismo código, Scala usa un código muy diferente.

Scala (al igual que Haskell) puede codificar muchos cálculos de nivel de tipo. Esto se muestra en bibliotecas como shapeless. Estas bibliotecas lo hacen utilizando algunos trucos realmente impresionantes e inteligentes. Sin embargo, su código de nivel de tipo es (actualmente) bastante diferente de las expresiones de nivel de valor (encuentro que esa brecha es algo más cercana en Haskell). Idris permite utilizar la expresión de nivel de valor en el nivel de tipo TAL CUAL.

El beneficio obvio es la reutilización del código (no es necesario codificar las expresiones de nivel de tipo por separado del nivel de valor si las necesita en ambos lugares). Debería ser mucho más fácil escribir código a nivel de valor. Debería ser más fácil no tener que lidiar con hacks como singletons (sin mencionar el costo de rendimiento). No necesitas aprender dos cosas, aprendes una sola. A nivel pragmático, terminamos necesitando menos conceptos. Escriba sinónimos, familias de tipos, funciones, ... ¿qué tal solo funciones? En mi opinión, estos beneficios unificadores son mucho más profundos y son más que conveniencia sintáctica.

Considere el código verificado. Ver:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
El verificador de tipo verifica las pruebas de leyes monádicas / functor / aplicativas y las pruebas son reales implementaciones de mónada / functor / aplicativo y no algún equivalente de nivel de tipo codificado que pueda ser el mismo o no el mismo. La gran pregunta es ¿qué estamos probando?

Lo mismo puedo hacer usando trucos de codificación inteligentes (vea lo siguiente para la versión de Haskell, no he visto uno para Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https: // github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
excepto que los tipos son tan complicados que es difícil ver las leyes, las expresiones de nivel de valor se convierten (automáticamente pero aún así) para escribir cosas de nivel y necesita confiar en esa conversión también . Hay margen para el error en todo esto, lo que desafía un poco el propósito de que el compilador actúe como asistente de prueba.

(EDITADO 2018.8.10) Hablando de asistencia para pruebas, aquí hay otra gran diferencia entre Idris y Scala. No hay nada en Scala (o Haskell) que pueda evitar escribir pruebas divergentes:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

mientras que Idris tiene una totalpalabra clave que impide que se compile un código como este.

Una biblioteca de Scala que intente unificar el código de nivel de valor y tipo (como Haskell singletons) sería una prueba interesante para el soporte de Scala de tipos dependientes. ¿Se puede hacer mucho mejor dicha biblioteca en Scala debido a los tipos dependientes de la ruta?

Soy demasiado nuevo en Scala para responder a esa pregunta yo mismo.