stringtranslate.com

Escritura gradual

La tipificación gradual es un sistema de tipos que se encuentra entre la tipificación estática y la tipificación dinámica . A algunas variables y expresiones se les pueden asignar tipos y la corrección de la tipificación se verifica en tiempo de compilación (que es tipificación estática ) y algunas expresiones pueden dejarse sin tipificar y los posibles errores de tipificación se informan en tiempo de ejecución (que es tipificación dinámica ).

La tipificación gradual permite a los desarrolladores de software elegir uno de los paradigmas de tipificación según sea apropiado, dentro de un único lenguaje. [1] En muchos casos, la tipificación gradual se agrega a un lenguaje dinámico existente, [2] creando un lenguaje derivado que permite, pero no requiere, el uso de tipificación estática. En algunos casos, un lenguaje utiliza tipificación gradual desde el principio.

Historia

El término fue acuñado por Jeremy Siek, quien desarrolló la mecanografía gradual en 2006 junto con Walid Taha. [1] [ se necesita una fuente no primaria ]

Implementación

En la tipificación gradual, se utiliza un tipo especial llamado dinámico para representar tipos estáticamente desconocidos. La noción de igualdad de tipos se reemplaza por una nueva relación llamada consistencia que relaciona el tipo dinámico con todos los demás tipos. La relación de consistencia es reflexiva y simétrica, pero no transitiva. [3]

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, como la subtipificación es transitiva, eso da como resultado que cada tipo se relacione con todos los demás tipos, por lo que la subtipificación 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. [4] [5]

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 conversiones implícitas con respecto a la subtipificación. La idea principal es que la consistencia y la subtipificación son ideas ortogonales que se combinan perfectamente. Para añadir la subtipificación a un lenguaje de tipificación gradual, simplemente hay que añadir la regla de subsunción y una regla de subtipificación que haga que el tipo dinámico sea un subtipo de sí mismo, porque se supone que la subtipificación es reflexiva. (¡Pero no hay que hacer que la parte superior del orden de subtipificación sea dinámica!) [6]

Ejemplos

Ejemplos de lenguajes de tipado gradual derivados de lenguajes de tipado dinámico existentes incluyen Closure Compiler , TypeScript (ambos para JavaScript [7] ), [8] Hack (para PHP), PHP (desde 7.0 [9] ), Typed Racket (para Racket [10] [11] ), Typed Clojure (para Clojure ), [12] Cython (un compilador de Python ), mypy (un verificador de tipos estáticos para Python ), [13] pyre (verificador de tipos estáticos alternativo para Python), [14] o cperl (un Perl 5 tipado ). ActionScript es un lenguaje de tipado gradual [15] que ahora es una implementación de ECMAScript , aunque originalmente surgió por separado como un hermano, ambos influenciados por HyperTalk de Apple .

Se ha desarrollado un sistema para el lenguaje de programación J , [16] añadiendo coerción, propagación de errores y filtrado a las propiedades de validación normales del sistema de tipos, además de aplicar funciones de tipos fuera de las definiciones de funciones, aumentando así la flexibilidad de las definiciones de tipos.

Por el contrario, C# comenzó como un lenguaje de tipado estático, pero a partir de la versión 4.0 se tipifica gradualmente, lo que permite marcar las variables explícitamente como dinámicas mediante el dynamictipo. [17] Los lenguajes de tipado gradual que no se derivan de un lenguaje de tipado dinámico incluyen Dart , Dylan y Raku .

Raku (anteriormente Perl6) tiene implementado el tipado gradual desde el principio. Las comprobaciones de tipo se producen en todas las ubicaciones donde se asignan o vinculan valores. Una variable o parámetro "sin tipo" se tipifica como Any, que coincidirá con (casi) todos los valores. El compilador señala los conflictos de comprobación de tipo en tiempo de compilación si puede determinar en tiempo de compilación que nunca tendrán éxito.

Objective-C tiene tipado gradual para punteros de objetos con respecto a llamadas de métodos. El tipado estático se utiliza cuando una variable se tipifica como puntero a una determinada clase de objeto: cuando se realiza una llamada de método a la variable, el compilador comprueba estáticamente que la clase esté declarada para admitir dicho método, o bien genera una advertencia o un error. Sin embargo, si idse utiliza una variable de ese tipo, el compilador permitirá que se llame a cualquier método en ella.

El lenguaje de programación JS++ , lanzado en 2011, es un superconjunto de JavaScript (tipificado dinámicamente) con un sistema de tipos gradual que es adecuado para casos especiales de ECMAScript y API DOM . [18]

Referencias

  1. ^ ab Siek, Jeremy (24 de marzo de 2014). "¿Qué es la tipificación gradual?".
  2. ^ Bracha, Gilad (2004). "Sistemas de tipos conectables". Taller OOPSLA'04 sobre el resurgimiento de los lenguajes dinámicos .
  3. ^ Siek, Jeremy; Taha, Walid (septiembre de 2006). Tipado gradual para lenguajes funcionales (PDF) . Scheme and Functional Programming 2006. Universidad de Chicago . Págs. 81–92.
  4. ^ Thatte, Satish (1990). "Tipificación cuasiestática". Actas del 17.º simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '90 . ACM . pp. 367–381. doi :10.1145/96709.96747. ISBN. 978-0897913430.S2CID8725290  .​
  5. ^ Oliart, Alberto (1994). Un algoritmo para inferir tipos cuasiestáticos (informe técnico). Universidad de Boston. 1994-013.
  6. ^ Siek, Jeremy; Taha, Walid (agosto de 2007). "Gradual Typing for Objects" (Tipado gradual para objetos). ECOOP 2007 – Programación orientada a objetos . Apuntes de clase en informática. Vol. 4609. Springer . págs. 2–27. doi :10.1007/978-3-540-73589-2_2. ISBN . 978-3-540-73588-5.
  7. ^ Feldthaus, Asger; Møller, Anders (2014). "Comprobación de la corrección de las interfaces TypeScript para bibliotecas de JavaScript". Actas de la Conferencia internacional ACM de 2014 sobre lenguajes y aplicaciones de sistemas de programación orientados a objetos. Portland, Oregón, EE. UU.: ACM Press. pp. 1–16. doi :10.1145/2660193.2660215. ISBN . 978-1-4503-2585-1.
  8. ^ Swamy, N.; Fournet, C.; Rastogi, A.; Bhargavan, K.; Chen, J.; Strub, PY; Bierman, G. (2014). "Tipado gradual integrado de forma segura en JavaScript" (PDF) . Actas del 41.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '14 . págs. 425–437. doi :10.1145/2535838.2535889. ISBN 9781450325448.
  9. ^ "PHP: Argumentos de función - Manual » Tipificación estricta".
  10. ^ Tobin-Hochstadt, Sam; Felleisen, Matthias. "Migración entre lenguajes: de scripts a programas". Actas del Simposio sobre sistemas de programación orientada a objetos, volumen complementario . Portland, OR. Tobin-Hochstadt06 . Consultado el 6 de noviembre de 2020 .
  11. ^ Tobin-Hochstadt, Sam; Felleisen, Matthias. "El diseño y la implementación de un esquema tipificado". Actas de la revista Principles of Programming Languages . San Diego, CA. Tobin-Hochstadt08 . Consultado el 6 de noviembre de 2020 .
  12. ^ Chas Emerick. "Guía del usuario de Clojure tipificado". GitHub .
  13. ^ Jukka Lehtosalo. "mypy: escritura estática opcional para Python".
  14. ^ "Pyre - Un verificador de tipos de alto rendimiento para Python 3".
  15. ^ Aseem Rastogi; Avik Chaudhuri; Basil Hosmer (enero de 2012). "Los entresijos de la inferencia de tipos gradual" (PDF) . Association for Computing Machinery (ACM) . Consultado el 23 de septiembre de 2014 .
  16. ^ "sistema de tipos-j". GitHub .
  17. ^ "dynamic (C# Reference)". Biblioteca MSDN . Microsoft . Consultado el 14 de enero de 2014 .
  18. ^ "El sistema de tipos de JS++, Apéndice B: Problemas (¿Por qué fue difícil resolverlo?)" . Consultado el 10 de febrero de 2020 .

Lectura adicional