Recursos de programación de tipo Scala

102

Según esta pregunta , el sistema de tipos de Scala es Turing completo . ¿Qué recursos están disponibles que permiten a un recién llegado aprovechar el poder de la programación a nivel de tipo?

Estos son los recursos que he encontrado hasta ahora:

Estos recursos son geniales, pero siento que me faltan los conceptos básicos y, por lo tanto, no tengo una base sólida sobre la cual construir. Por ejemplo, ¿dónde hay una introducción a las definiciones de tipos? ¿Qué operaciones puedo realizar en tipos?

¿Existen buenos recursos introductorios?

dsg
fuente
Personalmente, creo que la suposición de que alguien que quiera hacer programación a nivel de tipo en Scala ya sabe cómo programar en Scala es bastante razonable. Incluso si eso significa que no entiendo una palabra de esos artículos a los que vinculó :-)
Jörg W Mittag

Respuestas:

140

Visión general

La programación a nivel de tipo tiene muchas similitudes con la programación tradicional a nivel de valor. Sin embargo, a diferencia de la programación a nivel de valor, donde el cálculo ocurre en tiempo de ejecución, en la programación a nivel de tipo, el cálculo ocurre en tiempo de compilación. Trataré de establecer paralelismos entre la programación a nivel de valor y la programación a nivel de tipo.

Paradigmas

Hay dos paradigmas principales en la programación a nivel de tipo: "orientado a objetos" y "funcional". La mayoría de los ejemplos vinculados desde aquí siguen el paradigma orientado a objetos.

Un buen ejemplo bastante simple de programación a nivel de tipo en el paradigma orientado a objetos se puede encontrar en la implementación de apocalisp del cálculo lambda , replicado aquí:

// Abstract trait
trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

Como puede verse en el ejemplo, el paradigma orientado a objetos para la programación a nivel de tipo procede de la siguiente manera:

  • Primero: defina un rasgo abstracto con varios campos de tipo abstracto (vea a continuación qué es un campo abstracto). Esta es una plantilla para garantizar que existen ciertos tipos de campos en todas las implementaciones sin forzar una implementación. En el ejemplo de cálculo lambda, esto corresponde a trait Lambdaque los siguientes tipos que existen garantías: subst, apply, y eval.
  • Siguiente: defina sustratos que amplíen el rasgo abstracto e implementen los diversos campos de tipo abstracto
    • A menudo, estos sustratos se parametrizarán con argumentos. En el ejemplo de cálculo lambda, los subtipos son los trait App extends Lambdaque están parametrizados con dos tipos ( Sy Tambos deben ser subtipos de Lambda), los que están trait Lam extends Lambdaparametrizados con un tipo ( T) y trait X extends Lambda(que no están parametrizados).
    • los campos de tipo a menudo se implementan haciendo referencia a los parámetros de tipo del sustrato y, a veces, haciendo referencia a sus campos de tipo mediante el operador hash: #(que es muy similar al operador punto: .para valores). En rasgo Appdel ejemplo lambda cálculo, el tipo evalse implementa como sigue: type eval = S#eval#apply[T]. Básicamente, se trata de llamar al evaltipo de parámetro del rasgo Sy llamar applycon parámetro Ten el resultado. Tenga en cuenta que Sse garantiza que tiene un evaltipo porque el parámetro especifica que es un subtipo de Lambda. De manera similar, el resultado de evaldebe tener un applytipo, ya que se especifica que es un subtipo de Lambda, como se especifica en el rasgo abstracto Lambda.

El paradigma funcional consiste en definir lotes de constructores de tipos parametrizados que no se agrupan en rasgos.

Comparación entre programación a nivel de valor y programación a nivel de tipo

  • clase abstracta
    • nivel de valor: abstract class C { val x }
    • nivel de tipo: trait C { type X }
  • tipos dependientes de la ruta
    • C.x (haciendo referencia al valor del campo / función x en el objeto C)
    • C#x (campo de referencia tipo x en el rasgo C)
  • firma de función (sin implementación)
    • nivel de valor: def f(x:X) : Y
    • nivel de tipo: type f[x <: X] <: Y(esto se llama un "constructor de tipos" y generalmente ocurre en el rasgo abstracto)
  • implementación de funciones
    • nivel de valor: def f(x:X) : Y = x
    • nivel de tipo: type f[x <: X] = x
  • condicionales
  • comprobar la igualdad
    • nivel de valor: a:A == b:B
    • nivel de tipo: implicitly[A =:= B]
    • nivel de valor: ocurre en la JVM a través de una prueba unitaria en tiempo de ejecución (es decir, sin errores de tiempo de ejecución):
      • en esencia es una afirmación: assert(a == b)
    • nivel de tipo: ocurre en el compilador a través de una verificación de tipo (es decir, sin errores del compilador):
      • en esencia es una comparación de tipos: p. ej. implicitly[A =:= B]
      • A <:< B, compila solo si Aes un subtipo deB
      • A =:= B, compila solo si Aes un subtipo de By Bes un subtipo deA
      • A <%< B, ("visible como") se compila solo si Ase puede ver como B(es decir, hay una conversión implícita de Aa un subtipo de B)
      • un ejemplo
      • más operadores de comparación

Conversión entre tipos y valores

  • En muchos de los ejemplos, los tipos definidos a través de rasgos suelen ser tanto abstractos como sellados y, por lo tanto, no se pueden instanciar directamente ni a través de una subclase anónima. Por lo tanto, es común usarlo nullcomo un valor de marcador de posición cuando se realiza un cálculo de nivel de valor usando algún tipo de interés:

    • por ejemplo val x:A = null, ¿dónde Aestá el tipo que le interesa?
  • Debido al borrado de tipo, todos los tipos parametrizados tienen el mismo aspecto. Además, (como se mencionó anteriormente) los valores con los que está trabajando tienden a ser todos null, por lo que condicionar el tipo de objeto (por ejemplo, a través de una declaración de coincidencia) es ineficaz.

El truco consiste en utilizar funciones y valores implícitos. El caso base suele ser un valor implícito y el caso recursivo suele ser una función implícita. De hecho, la programación a nivel de tipo hace un uso intensivo de los implícitos.

Considere este ejemplo ( tomado de metascala y apocalisp ):

sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat

Aquí tienes una codificación peano de los números naturales. Es decir, tiene un tipo para cada entero no negativo: un tipo especial para 0, a saber _0; y cada entero mayor que cero tiene un tipo de la forma Succ[A], donde Aes el tipo que representa un entero más pequeño. Por ejemplo, el tipo que representa 2 sería: Succ[Succ[_0]](sucesor aplicado dos veces al tipo que representa cero).

Podemos alias varios números naturales para una referencia más conveniente. Ejemplo:

type _3 = Succ[Succ[Succ[_0]]]

(Esto es muy parecido a definir vala como el resultado de una función).

Ahora, suponga que queremos definir una función de nivel de valor def toInt[T <: Nat](v : T)que toma un valor de argumento v, que se ajusta Naty devuelve un número entero que representa el número natural codificado en vel tipo de. Por ejemplo, si tenemos el valor val x:_3 = null( nullde tipo Succ[Succ[Succ[_0]]]), querríamos toInt(x)volver 3.

Para implementar toInt, vamos a hacer uso de la siguiente clase:

class TypeToValue[T, VT](value : VT) { def getValue() = value }

Como veremos a continuación, habrá un objeto construido a partir de la clase TypeToValuepara cada uno Natde _0hasta (por ejemplo) _3, y cada uno almacenará la representación del valor del tipo correspondiente (es decir TypeToValue[_0, Int], almacenará el valor 0, TypeToValue[Succ[_0], Int]almacenará el valor 1, etc.). Tenga en cuenta, TypeToValueestá parametrizado por dos tipos: Ty VT. Tcorresponde al tipo al que estamos tratando de asignar valores (en nuestro ejemplo, Nat) y VTcorresponde al tipo de valor que le estamos asignando (en nuestro ejemplo, Int).

Ahora hacemos las siguientes dos definiciones implícitas:

implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = 
     new TypeToValue[Succ[P], Int](1 + v.getValue())

Y lo implementamos de la toIntsiguiente manera:

def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()

Para entender cómo toIntfunciona, consideremos qué hace en un par de entradas:

val z:_0 = null
val y:Succ[_0] = null

Cuando llamamos toInt(z), el compilador busca un argumento implícito ttvde tipo TypeToValue[_0, Int](ya que zes de tipo _0). Encuentra el objeto _0ToInt, llama al getValuemétodo de este objeto y vuelve 0. El punto importante a tener en cuenta es que no especificamos al programa qué objeto usar, el compilador lo encontró implícitamente.

Ahora consideremos toInt(y). Esta vez, el compilador busca un argumento implícito ttvde tipo TypeToValue[Succ[_0], Int](ya que yes de tipo Succ[_0]). Encuentra la función succToInt, que puede devolver un objeto del tipo apropiado ( TypeToValue[Succ[_0], Int]) y lo evalúa. Esta función en sí misma toma un argumento implícito ( v) de tipo TypeToValue[_0, Int](es decir, a TypeToValuedonde el primer parámetro de tipo tiene uno menos Succ[_]). El compilador suministra _0ToInt(como se hizo en la evaluación toInt(z)anterior) y succToIntconstruye un nuevo TypeToValueobjeto con valor 1. Nuevamente, es importante tener en cuenta que el compilador proporciona todos estos valores implícitamente, ya que no tenemos acceso a ellos explícitamente.

Comprobando tu trabajo

Hay varias formas de verificar que sus cálculos a nivel de tipo estén haciendo lo que espera. Aquí hay algunos enfoques. Haz dos tipos Ay B, que quieras verificar, son iguales. Luego verifique que se compile lo siguiente:

Alternativamente, puede convertir el tipo en un valor (como se muestra arriba) y hacer una verificación en tiempo de ejecución de los valores. Por ejemplo assert(toInt(a) == toInt(b)), donde aes de tipo Ay bes de tipo B.

Recursos adicionales

El conjunto completo de construcciones disponibles se puede encontrar en la sección de tipos del manual de referencia de scala (pdf) .

Adriaan Moors tiene varios artículos académicos sobre constructores de tipos y temas relacionados con ejemplos de scala:

Apocalisp es un blog con muchos ejemplos de programación a nivel de tipo en scala.

ScalaZ es un proyecto muy activo que proporciona una funcionalidad que extiende la API de Scala utilizando varias funciones de programación a nivel de tipo. Es un proyecto muy interesante que tiene muchos seguidores.

MetaScala es una biblioteca a nivel de tipo para Scala, que incluye metatipos para números naturales, booleanos, unidades, HList, etc. Es un proyecto de Jesper Nordenberg (su blog) .

El Michid (blog) tiene algunos ejemplos asombrosos de programación a nivel de tipo en Scala (de otra respuesta):

Debasish Ghosh (blog) también tiene algunas publicaciones relevantes:

(He estado investigando un poco sobre este tema y esto es lo que he aprendido. Todavía soy nuevo en él, así que indique cualquier inexactitud en esta respuesta).

dsg
fuente
12

Además de los otros enlaces aquí, también están las publicaciones de mi blog sobre metaprogramación de nivel de tipo en Scala:

michid
fuente
Solo quería agradecer el interesante blog; Lo he estado siguiendo por un tiempo y especialmente la última publicación mencionada anteriormente ha agudizado mi comprensión de las propiedades importantes que debe tener un sistema de tipos para un lenguaje orientado a objetos. ¡Así que gracias!
Zach Snow
4

Scalaz tiene código fuente, wiki y ejemplos.

Vasil Remeniuk
fuente