Variable de tipo

Una variable de tipo ( type variable ) en lenguajes de programación y teoría de tipos  es una variable que puede tomar un valor de un conjunto de tipos de datos .

Una variable de tipo se usa en una definición de tipo de datos algebraica de la misma manera que un parámetro se usa en una definición de función , pero se usa para pasar un tipo de datos sin pasar los datos en sí. Los caracteres griegos se utilizan tradicionalmente como identificadores de variables de tipo en la teoría de tipos (aunque muchos lenguajes de programación utilizan el alfabeto latino y permiten nombres más largos).

Ejemplo

En la siguiente definición del tipo polimórfico " lista " en Standard ML , el identificador 'a(pronunciado "alfa") es una variable de tipo [2] :

tipo de datos 'una lista = nil | :: de 'a * 'una lista

Cuando se usa este tipo polimórfico , se sustituye un tipo específico en la variable de tipo, de modo que se pueden formar muchos tipos monomórficos en el programa: string list, int list, int list listetc. Con esta sustitución, cada referencia a una variable de tipo se reemplaza por el mismo tipo. La información de tipo resultante se usa para verificar y optimizar el programa, después de lo cual generalmente se borra, de modo que el mismo código de destino procese objetos de tipos inicialmente diferentes (pero hay excepciones a esta regla, en particular, en MLton ).

Si un tipo polimórfico está parametrizado por varias variables de tipo, entonces los tipos sustituidos en ellas pueden ser diferentes o idénticos, pero se respeta la regla de sustitución. Por ejemplo, si este tipo es:

tipo de datos ( 'a , 'b ) t = Único de 'a | Doble de 'a * 'a | Par de 'a * 'b

instanciar así:

escriba t_ir = ( int , real ) t

entonces Single(4), Double(4,5)y Pair(4,5.0)serán valores válidos de tipo t_ir, e intentar construir un valor Single(5.0)dará como resultado un error de tipeo porque el parámetro 'atiene el valor " int".

Vinculación y cuantificación

El alcance de cualquier variable de tipo está ligado a un contexto específico [3] [4] . En el siguiente ejemplo, el identificador 'ase usa de forma independiente en dos firmas, lo que significa que no requiere la igualdad de tipos en línea entre definiciones:

val foo : 'a -> 'a val bar : 'a -> 'a

Esto queda claro cuando se usa una variable de tipo de enlace explícito (ámbito explícito o límite explícito ):

val foo : [ 'a ] 'a -> 'a val bar : [ 'a ] 'a -> 'a

Un enlace limita el alcance de una variable de tipo dada.

En los dialectos clásicos de ML, el enlace explícito de las variables de tipo es una característica opcional y la mayoría de las implementaciones no se admiten porque son innecesarias; el enlace en ellas está implícito en la deducción de tipos , lo que es posible debido a las limitaciones de las primeras versiones del sistema Hindley-Milner . En el sistema completo F , esta declaración se escribe como . Tal notación se llama forma normal prenex . La letra mayúscula en esta entrada significa la función de la capa de tipo (función de nivel de tipo ), cuyo parámetro es la variable de tipo. Después de sustituir un tipo específico en esta variable, esta función devuelve una función monomórfica de nivel de valor (función de nivel de valor ). Un prenexo es un enlace explícito de una variable de tipo con el prefijo de una firma de tipo. Las primeras versiones del sistema Hindley-Milner solo permitían la forma prenex, es decir, requerían que se creara una instancia de una variable de tipo con un valor específico antes de que se necesitara una llamada de función. Esta restricción se denomina polimorfismo prenex  : no solo simplifica en gran medida el mecanismo de coincidencia de tipos , sino que también permite inferir todos o casi todos (según el dialecto) los tipos en el programa.

El enlace más simple de las variables de tipo se llama su cuantificación . Destacan dos casos:

  • la acción de una variable de tipo se extiende a toda la definición de tipo: ['a, 'b] 'a -> 'b -> 'amatemáticamente, dicho tipo se escribe a través del cuantificador universal ; por lo tanto, dicha variable de tipo se denomina "cuantificada universalmente", y el tipo completo se denomina "polimórfico universal";
  • el efecto de una variable de tipo se extiende solo a una parte de la definición de tipo: ['a] 'a -> (['b] 'b -> 'a)matemáticamente, dicho tipo se escribe a través del cuantificador existencial ; por lo tanto, dicha variable se llama "cuantificada existencialmente", y el tipo completo se llama "existencial".

No en todos los casos, "convertir" un tipo polimórfico universal en un tipo existencial da un tipo práctico o diferencias notables del polimorfismo universal, pero en ciertos casos, el uso de tipos existenciales eleva el polimorfismo paramétrico a un nivel de primera clase , es decir permite pasar funciones polimórficas sin vincularlas como parámetros a otras funciones (ver polimorfismo de primera clase ). Un ejemplo clásico es la implementación de listas heterogéneas (ver wikibook). La anotación explícita de tipos en este caso se vuelve obligatoria, porque la inferencia de tipos para el polimorfismo por encima del rango 2 es algorítmicamente indecidible [5] .

En la práctica, los tipos universalmente polimórficos dan una generalización del tipo de datos y los tipos existenciales, la abstracción del tipo de datos [6] .

Haskell distingue varios modos (disponibles como extensiones de lenguaje): el modo Rank2Types permite solo algunas formas de tipos existenciales que abren polimorfismos no más altos que el rango 2, para los cuales la inferencia de tipo aún es decidible; el modo RankNTypes permite mover el cuantificador universal ( forall a) dentro de tipos funcionales que forman parte de firmas más complejas [7] , el modo ImpredicativeTypes permite tipos existenciales arbitrarios [8] .

OCaml implementa el soporte para la cuantificación existencial a través de una solución llamada "tipos abstractos localmente" [ 9 ] .

La especificación de ML estándar define una cuantificación especial para algunas operaciones integradas. Su sintaxis no está regulada y difiere en las implementaciones del lenguaje (la mayoría de las veces simplemente está oculta). Por ejemplo, la firma de la operación de suma incorporada podría simplificarse de la siguiente manera:

val + : [ int , palabra , real ] 'a * 'a -> 'a

Esta semántica implementa una forma primitiva de polimorfismo ad-hoc  , combinando varias operaciones de suma físicamente diferentes bajo un único identificador " +". Los desarrolladores de OCaml abandonaron esta solución eliminando por completo el polimorfismo ad-hoc del lenguaje ( los tipos de datos algebraicos generalizados aparecieron en versiones posteriores ).

A fines de la década de 1980, apareció la extensión Hindley-Milner , que brinda la capacidad de limitar, si es necesario, el rango de valores para cualquier variable de tipo en tipos recién definidos: clases de tipos . Una clase de tipo restringe los contextos de escritura permitidos de manera más estricta , lo que permite que una variable de tipo sea instanciada solo por tipos que pertenecen a una clase especificada explícitamente.

Esta extensión se implementó por primera vez en el núcleo del lenguaje Haskell , por ejemplo, el operador de comparación de igualdad tiene la siguiente firma :

( == ) :: ( Eq a ) => a -> a -> Bool

El proyecto del lenguaje de próxima generación, sucesor ML [1]  , rechaza la necesidad de la inferencia de tipos , confiando en la anotación de tipo explícita (manifiesta) (incluida la vinculación explícita de variables de tipo), que proporciona soporte directo para el sistema completo F con primer polimorfismo de clase y una serie de extensiones, incluidas jerarquías de subtipos y tipos existenciales [1] .

Variables de tipo especial

La clase principal de variables de tipo utilizadas en todos los lenguajes de la familia ML son variables de tipo aplicativo que pueden tomar valores del conjunto de todos los tipos permitidos en un idioma en particular. En los dialectos clásicos, se denotan sintácticamente como " 'a" (un identificador alfanumérico, que siempre comienza con un solo apóstrofo ); en Haskell como " a" (un identificador alfanumérico, que siempre comienza con una letra minúscula).

Además, a lo largo de la historia de ML , se han distinguido subclases especiales de variables de tipo.

Variables de un tipo cuya igualdad puede verificarse (o variables de un tipo comparable, variables de tipo de igualdad ): pueden tomar valores del conjunto de todos los tipos cuya igualdad puede verificarse ( tipos de igualdad en inglés  ). Su uso permite aplicar la operación de comparación de igualdad a objetos de tipos polimórficos. Se denotan como " " (identificador alfanumérico, siempre comenzando con dos apóstrofes ). Curiosamente, uno de los objetivos originales para los que se desarrollaron las clases de tipo fue precisamente la generalización de tales variables de tipo de Standard ML [10] . Han sido criticados repetidamente debido a la complicación significativa (y posiblemente justificada) de la definición del lenguaje y la implementación de compiladores (la mitad de las páginas de la Definición contienen una u otra enmienda a ellos) [11] . En principio, no es aconsejable verificar la igualdad de tipos de datos abstractos complejos, ya que tales verificaciones pueden requerir una cantidad significativa de tiempo. Por lo tanto, a partir de lenguajes posteriores de la familia ML , se eliminó el soporte para variables de un tipo que permitiera realizar pruebas de igualdad. Haskell usa la clase de tipo en su lugar . ''a Eq a

Las variables de tipo imperativo proporcionaron una solución ad hoc al problema de seguridad de tipo asociado con los efectos secundarios en un lenguaje con polimorfismo paramétrico . Este problema no surge en lenguajes puros ( Haskell , Clean ), pero para lenguajes impuros ( Standard ML , OCaml ) el polimorfismo de referencia plantea una amenaza de errores de tipeo [3] [4] . Las variables de tipo imperativo formaban parte de la Definición de SML'90, pero dejaron de tener significado propio después de que se acuñara la " restricción de valor " , que pasó a formar parte de la definición revisada de SML'97. El soporte sintáctico para las variables de tipo imperativo en SML'97 se mantuvo por compatibilidad con el código escrito anteriormente, pero las implementaciones modernas las tratan de manera idéntica a las aplicativas. Denotado por " '_a" (un identificador alfanumérico, que siempre comienza con un apóstrofe y un guión bajo) [3] .

Las variables de tipo débil se utilizaron en el compilador SML/NJ como una alternativa a las variables de tipo imperativo, proporcionando mucha más potencia (más precisamente, menos restricciones). Denotado por " '1a", " '2a" y así sucesivamente (un identificador alfanumérico, que siempre comienza con un apóstrofe y un número). El número que sigue inmediatamente al apóstrofe indica la gradación de "debilidad" de la variable de tipo. Al igual que las variables de tipo imperativo, ahora se tratan de forma idéntica a las de aplicación. [3]

Notas

  1. ↑ 1 2 3 ML2000, 1999 .
  2. ↑ Aquí, para el enlace explícito ( enlace explícito ) una variable de tipo, se usa la sintaxis actual adoptada en el proyecto sucesor de ML [1] : ['a]. Debido a que Haskell designó esta sintaxis como azúcar sintáctica sobre tipo , la palabra claveList se introdujo para declarar variables de tipo . forall
  3. ↑ 1 2 3 4 MacQueen-TypeChecking .
  4. ↑ 12 MLton : alcance .
  5. ↑ haskell_existenciales .
  6. ↑ Cardelli, Wegner, 1985 .
  7. ↑ haskell_rankNtypes .
  8. ↑ haskell_impredicative_types .
  9. ↑ Extensiones OCaml. 7.13 Tipos localmente abstractos
  10. ↑ Philip Wadler, Stephen Blott. Cómo hacer que el polimorfismo ad-hoc sea menos ad hoc . — 1988.
  11. ↑ Andrew W. Appel. Una crítica del ML estándar . — Universidad de Princeton, versión revisada de CS-TR-364-92, 1992.

Literatura

Enlaces

 Tipos de datos
Ininterpretable
Numérico
Texto
Referencia
Compuesto
resumen
Otro
Temas relacionados