general
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 de nivel de valor, donde el cálculo se produce en tiempo de ejecución, en la programación de nivel de tipo, el cálculo se produce en tiempo de compilación. Trataré de establecer paralelismos entre la programación en el nivel de valor y la programación en el 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 a partir de aquí siguen el paradigma orientado a objetos.
Una buena bastante simple ejemplo de programación a nivel de tipo en el paradigma orientado a objetos, se pueden encontrar en apocalisp de implementation of the lambda calculus, reproducido 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 se puede ver en el ejemplo, el orientado a objetos paradigma para los ingresos de programación a nivel de tipo de la siguiente manera:
- primero: definir un rasgo abstracto con diversos campos de tipo abstracto (ver más abajo para lo que es un campo de resumen). Esta es una plantilla para garantizar que ciertos campos de tipos existen en todas las implementaciones sin forzar una implementación.En el ejemplo de cálculo lambda, esto corresponde a
trait Lambda que garantiza que existen los siguientes tipos: subst, apply y eval.
- siguiente: definir subtraits que extienden el rasgo abstracto y poner en práctica los diversos campos de tipo abstracto
- A menudo, estos subtraits se pueden parametrizar con argumentos. En el ejemplo de cálculo lambda, los subtipos son
trait App extends Lambda que se parametriza con dos tipos (S y T, ambos deben ser subtipos de Lambda), trait Lam extends Lambda parametrizadas con un tipo (T), y trait X extends Lambda (que no es parametrizada).
- los campos de tipo se implementan a menudo consultando los parámetros de tipo del subtrama y algunas veces haciendo referencia a sus campos de tipo mediante el operador hash:
# (que es muy similar al operador de punto: . para valores). En el rasgo App del ejemplo de cálculo lambda, el tipo eval se implementa de la siguiente manera: type eval = S#eval#apply[T]. Esto es esencialmente llamar al tipo eval del parámetro del rasgo S, y llamar al apply con el parámetro T en el resultado. Tenga en cuenta que se garantiza que S tiene un tipo eval porque el parámetro lo especifica como un subtipo de Lambda. Del mismo modo, el resultado de eval debe tener un tipo apply, ya que se especifica que es un subtipo de Lambda, como se especifica en el rasgo abstracto Lambda.
El paradigma funcional consiste en definir un montón de constructores de tipos parametrizados que no están agrupados en rasgos.
Comparación entre programación a nivel de valor y la programación a nivel de tipo
- abstract class
- valor de nivel:
abstract class C { val x }
- tipo de nivel:
trait C { type X }
- ruta dependiente tipos
C.x (referencia valor de campo/función de x en el objeto C)C#x (referencia de tipo de campo x en rasgo C)
- función de firma (sin aplicación)
- valor de nivel :
def f(x:X) : Y
- tipo-nivel:
type f[x <: X] <: Y (esto se llama un "constructor de tipo" y generalmente ocurre en el rasgo abstracto)
- implementación de la función
- valor de nivel:
def f(x:X) : Y = x
- tipo de nivel:
type f[x <: X] = x
- condicionales
- comprobar la igualdad
- valor de nivel:
a:A == b:B
- tipo de nivel:
implicitly[A =:= B]
- valor de nivel: sucede en la JVM a través de una prueba de unidad en tiempo de ejecución (es decir, no hay errores de tiempo de ejecución):
- en esencia es una aserción:
assert(a == b)
- tipo de nivel: sucede en el compilador a través de un typecheck (es decir, no hay errores de compilador):
- , en esencia, es una tipo de comparación: por ejemplo
implicitly[A =:= B]
A <:< B, compila solamente si A es un subtipo de BA =:= B, compila solamente si A es un subtipo de B y B es un subtipo de AA <%< B, ("visibles como") compila sólo si A es visible como B (es decir,hay una conversión implícita de A a un subtipo de B)- an example
- more comparison operators
La conversión entre tipos y valores
En muchos de la ex Los ejemplos, los tipos definidos a través de los rasgos a menudo son abstractos y sellados, y por lo tanto no pueden ser instanciados directamente ni a través de una subclase anónima. Por lo tanto, es común el uso de null como un valor de marcador de posición cuando se hace un cálculo de nivel de valor utilizando algún tipo de interés:
- por ejemplo,
val x:A = null, donde A es el tipo que se preocupan por
Debido al tipo-borrado, tipos parametrizados todos tienen el mismo aspecto. Además, (como se mencionó anteriormente), los valores con los que está trabajando tienden a ser null, por lo que condicionar el tipo de objeto (por ejemplo, a través de una declaración de coincidencia) no es efectivo.
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 implícitos.
Considere este ejemplo (taken from metascala y apocalisp):
sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat
Aquí tienen una codificación de Peano de los números naturales. Es decir, tiene un tipo para cada entero no negativo: un tipo especial para 0, es decir, _0; y cada entero mayor que cero tiene un tipo del formulario Succ[A], donde A es 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 se parece mucho a la definición de un val ser el resultado de una función)
Ahora, supongamos que queremos definir una función de nivel de valor def toInt[T <: Nat](v : T) que tiene en un valor de argumento , v, que cumple con Nat y devuelve un número entero que representa el número natural codificado en el tipo v. Por ejemplo, si tenemos el valor val x:_3 = null (null de tipo Succ[Succ[Succ[_0]]]), querríamos que toInt(x) devolviera 3.
Para implementar toInt, vamos a hacer uso de la clase siguiente:
class TypeToValue[T, VT](value : VT) { def getValue() = value }
Como veremos a continuación, habrá un objeto construido a partir de la clase TypeToValue para cada Nat de _0 hasta (ej.) _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 que TypeToValue se parametriza en dos tipos: T y VT. T corresponde al tipo al que intentamos asignar valores (en nuestro ejemplo, Nat) y VT corresponde al tipo de valor que le asignamos (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 ponemos en práctica toInt de la siguiente manera:
def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()
Para entender cómo toInt obras, consideremos lo que 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 ttv del tipo TypeToValue[_0, Int] (ya que z es del tipo _0). Encuentra el objeto _0ToInt, llama al método getValue de este objeto y recupera 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 ttv del tipo TypeToValue[Succ[_0], Int] (ya que y es del 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 toma un argumento implícito (v) del tipo TypeToValue[_0, Int] (es decir, un TypeToValue donde el primer parámetro de tipo tiene uno menos Succ[_]). El compilador suministra _0ToInt (como se hizo en la evaluación de toInt(z) anterior) y succToInt construye un nuevo objeto TypeToValue con el valor 1. De nuevo, es importante tener en cuenta que el compilador proporciona todos estos valores implícitamente, ya que no tenemos acceso a ellos explícitamente.
verificación del trabajo
Hay varias maneras de verificar que sus cálculos de nivel tipo están haciendo lo que se espera. Aquí hay algunos enfoques. Haga dos tipos A y B, que desea verificar son iguales.A continuación, comprobar que la siguiente compilación:
Equal[A, B]
implicitly[A =:= B]
Alternativamente, se puede convertir el tipo a un valor (como se muestra arriba) y hacer una verificación en tiempo de ejecución de los valores. P.ej. assert(toInt(a) == toInt(b)), donde a es del tipo A y b es del tipo B.
Recursos adicionales
El conjunto completo de construcciones disponibles pueden encontrarse en la sección Tipos de the scala reference manual (pdf).
Adriaan Moors tiene varios trabajos académicos sobre constructores de tipos y temas relacionados con ejemplos de Scala:
Apocalisp es un blog con muchos ejemplos de pro tipo-pro Gramática en scala.
- Type-Level Programming in Scala es una visita guiada fantástica de algunos programación a nivel de tipo que incluye booleanos, números naturales (como anteriormente), los números binarios, listas heterogéneos, y más.
- More Scala Typehackery es la implementación de cálculo lambda anterior.
ScalaZ es un proyecto muy activo que está proporcionando la funcionalidad que se extiende la API Scala usando varias características de programación de nivel de tipo. Es un proyecto muy interesante que tiene muchos seguidores.
MetaScala es una biblioteca de nivel de tipo para Scala, incluidos metaetipos para números naturales, booleanos, unidades, HList, etc. Es un proyecto por Jesper Nordenberg (his blog).
El Michid (blog) tiene algunos ejemplos impresionantes de programación a nivel de tipo de Scala (de otra respuesta):
Debasish Ghosh (blog) tiene algunos mensajes pertinentes, así:
(He estado investigando sobre este tema y esto es lo que he aprendido. Todavía estoy nuevo a ella, así que por favor señale cualquier inexactitud en esta respuesta.)
wiki de la comunidad? –
Personalmente, creo que la suposición de que alguien que quiera hacer programación a nivel de tipo en Scala ya sabe cómo hacer programación en Scala es bastante razonable. Incluso si eso significa que no entiendo una palabra de esos artículos a los que vinculó :-) –