El tipado gradual es un sistema de tipos en el que se pueden dar tipos a algunas variables y expresiones y la corrección del tipado se verifica en tiempo de compilación (que es tipado estático ) y algunas expresiones pueden dejarse sin tipear y los eventuales errores de tipo se informan en tiempo de ejecución (lo que es escritura dinámica ). La escritura gradual permite a los desarrolladores de software elegir cualquier tipo de paradigma según corresponda, desde un solo idioma. [1]En muchos casos, la escritura gradual se agrega a un lenguaje dinámico existente, creando un lenguaje derivado que permite, pero no requiere, el uso de la escritura estática. En algunos casos, un idioma utiliza la escritura gradual desde el principio.
Historia
El término fue acuñado por Jeremy Siek. Jeremy Siek y Walid Taha comenzaron a investigar la mecanografía gradual en 2006. [1]
Implementación
En particular, la tipificación gradual usa un tipo especial llamado dynamic para representar tipos desconocidos estáticamente, y la tipificación gradual reemplaza la noción de igualdad de tipos con una nueva relación llamada consistencia que relaciona el tipo dinámico con cualquier otro tipo. La relación de consistencia es simétrica pero no transitiva. [2]
Los intentos anteriores de integrar la tipificación estática y dinámica intentaron hacer que el tipo dinámico fuera tanto el superior como el inferior de la jerarquía de subtipos. Sin embargo, debido a que el subtipo es transitivo, eso da como resultado que cada tipo se relacione con cualquier otro tipo, por lo que el subtipo ya no descartaría ningún error de tipo estático. La adición de una segunda fase de verificación de plausibilidad al sistema de tipos no resolvió completamente este problema. [3] [4]
La tipificación gradual se puede integrar fácilmente en el sistema de tipos de un lenguaje orientado a objetos que ya utiliza la regla de subsunción para permitir upcasts implícitos con respecto a la subtipificación. La idea principal es que la consistencia y el subtipo son ideas ortogonales que se componen muy bien. Para agregar subtipos a un lenguaje escrito gradualmente, simplemente agregue la regla de subsunción y agregue una regla de subtipo que haga que el tipo dinámico sea un subtipo de sí mismo, porque se supone que el subtipo es reflexivo. (¡Pero no haga que la parte superior del orden de subtipo sea dinámica!) [5]
Ejemplos de
Ejemplos de lenguajes de escritura gradual derivados de lenguajes de escritura dinámica existentes incluyen Closure Compiler , TypeScript (ambos para JavaScript [6] ), [7] Hack (para PHP), PHP (desde 7.0 [8] ), Typed Racket (para Racket ), Clojure con tipo (para Clojure ), [9] Cython (un compilador de Python ), mypy (un verificador de tipo estático para Python ), [10] pyre (verificador de tipo estático alternativo para Python), [11] o cperl (un Perl 5 con tipo ). ActionScript es un lenguaje escrito gradualmente [12] que ahora es una implementación de ECMAScript , aunque originalmente surgió por separado como hermano, ambos influenciados por HyperTalk de Apple .
Se ha desarrollado un sistema para el lenguaje de programación J , [13] agregando coerción, propagación de errores y filtrado a las propiedades de validación normales del sistema de tipos, así como también aplicando funciones de tipo fuera de las definiciones de función, por lo que aumenta la flexibilidad de las definiciones de tipo.
Por el contrario, C # comenzó como un lenguaje de tipado estático, pero a partir de la versión 4.0 se teclea gradualmente, lo que permite que las variables se marquen explícitamente como dinámicas mediante el uso del dynamic
tipo. [14] Los lenguajes escritos gradualmente que no se derivan de un lenguaje escrito dinámicamente incluyen Dart , Dylan y Raku .
Raku (anteriormente Perl6) tiene la escritura gradual implementada desde el principio. Las verificaciones de tipo se realizan en todas las ubicaciones donde se asignan o enlazan valores. Una variable o parámetro "sin tipo" se escribe como Any
, que coincidirá con (casi) todos los valores. El compilador marca los conflictos de verificación de tipos en el momento de la compilación si puede determinar en el momento de la compilación que nunca tendrán éxito.
Objective-C tiene escritura gradual para punteros a objetos con respecto a las llamadas a métodos. La escritura estática se usa cuando una variable se escribe como puntero a una determinada clase de objeto: cuando se realiza una llamada a un método a la variable, el compilador verifica estáticamente que la clase está declarada para admitir dicho método, o genera una advertencia o error . Sin embargo, si id
se utiliza una variable del tipo , el compilador permitirá que se invoque cualquier método en ella.
El lenguaje de programación JS ++ , lanzado en 2011, es un superconjunto de JavaScript (tipado dinámicamente) con un sistema de tipo gradual que es sólido para los casos de esquina de ECMAScript y DOM API. [15]
Referencias
- ^ a b Siek, Jeremy. "¿Qué es la mecanografía gradual?" .
- ^ Siek, Jeremy; Taha, Walid (septiembre de 2006). Mecanografía gradual para lenguajes funcionales (PDF) . Esquema y programación funcional 2006 . Universidad de Chicago . págs. 81–92.
- ^ Thatte, Satish (1990). Escritura casi estática . POPL 1990: Principios ACM de lenguajes de programación . ACM . págs. 367–381. doi : 10.1145 / 96709.96747 . ISBN 978-0897913430.
- ^ Oliart, Alberto (1994). Un algoritmo para inferir tipos cuasi-estáticos (informe técnico). Universidad de Boston. 1994-013.
- ^ Siek, Jeremy; Taha, Walid (agosto de 2007). Escritura gradual de objetos . ECOOP 2007: Congreso Europeo de Programación Orientada a Objetos . Apuntes de conferencias en Ciencias de la Computación. 4609 . Springer . págs. 2-27. doi : 10.1007 / 978-3-540-73589-2_2 . ISBN 978-3-540-73588-5.
- ^ Feldthaus, Asger; Møller, Anders (2014). "Comprobación de la corrección de las interfaces de TypeScript para las bibliotecas de JavaScript" . Actas de la Conferencia Internacional ACM 2014 sobre lenguajes y aplicaciones de sistemas de programación orientados a objetos - OOPSLA '14 . Portland, Oregon, EE.UU .: ACM Press: 1–16. doi : 10.1145 / 2660193.2660215 . ISBN 978-1-4503-2585-1.
- ^ Swamy, N .; Fournet, C .; Rastogi, A .; Bhargavan, K .; Chen, J .; Strub, PY; Bierman, G. (2014). "Escritura gradual incrustada de forma segura en JavaScript". Actas del 41º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '14 (PDF) . págs. 425–437. doi : 10.1145 / 2535838.2535889 . ISBN 9781450325448.
- ^ "PHP: Argumentos de función - Manual» Escritura estricta " .
- ^ Chas Emerick. "Guía del usuario de Clojure mecanografiada" .
- ^ Jukka Lehtosalo. "mypy - Escritura estática opcional para Python" .
- ^ "Pyre: un verificador de tipo eficaz para Python 3" .
- ^ Aseem Rastogi; Avik Chaudhuri; Basil Hosmer (enero de 2012). "Los entresijos de la inferencia de tipo gradual" (PDF) . Asociación de Maquinaria de Computación (ACM) . Consultado el 23 de septiembre de 2014 .
- ^ "tipo-sistema-j" .
- ^ "dinámico (referencia de C #)" . Biblioteca de MSDN . Microsoft . Consultado el 14 de enero de 2014 .
- ^ "El sistema de tipos JS ++, Apéndice B: Problemas (¿Por qué fue tan difícil de resolver?)" . Consultado el 10 de febrero de 2020 .
Otras lecturas
- Siek, Jeremy G .; Vitousek, Michael M .; Cimini, Matteo; Boyland, John Tang (2015). Ball, Thomas; Bodik, Rastislav; Krishnamurthi, Shriram; Lerner, Benjamin S .; Morrisett, Greg (eds.). Criterios refinados para la escritura gradual . I Cumbre de Avances en Lenguajes de Programación (SNAPL 2015) . Leibniz International Proceedings in Informatics (LIPIcs). 32 . Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik. págs. 274-293. doi : 10.4230 / lipics.snapl.2015.274 . ISBN 9783939897804.