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.
El término fue acuñado por Jeremy Siek, quien desarrolló la mecanografía gradual en 2006 con Walid Taha. [1] [ se necesita una fuente no primaria ]
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 ascendentes 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 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 explícitamente las variables 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]