Sistema de tipos

Un lenguaje de programación consta de un sistema de secuencias permitidas de símbolos ( constructos ) junto con reglas que definen cómo se interpreta cada constructo. Por ejemplo, un lenguaje podría permitir expresiones que representen diversos tipos de datos, expresiones que proporcionen reglas de estructuración para los datos, expresiones que representen diversas operaciones sobre los datos y constructos que proporcionen reglas de secuenciación para el orden en que se deben realizar las operaciones.

Un sistema de tipos simple para un lenguaje de programación es un conjunto de reglas que asocia un tipo de dato (por ejemplo, entero , coma flotante , cadena ) con cada término (expresión con valor de datos) en un programa informático . En sistemas de tipos más complejos, se pueden asignar tipos a diversas construcciones, como variables , expresiones , funciones y módulos . ^{[ 1 ]}

Los sistemas de tipos formalizan y refuerzan las categorías, de otro modo implícitas, que el programador utiliza para los tipos de datos algebraicos , las estructuras de datos u otros tipos de datos , como "cadena", "matriz de números flotantes" o "función que devuelve un valor booleano".

El propósito principal de un sistema de tipos en un lenguaje de programación es reducir las posibilidades de errores en los programas informáticos debido a discrepancias en la interpretación de valores en diferentes partes del programa. El objetivo es evitar que las operaciones que esperan un tipo de valor determinado se apliquen a valores para los que dicha operación no tiene sentido (errores de validez). ^{[ 2 ]} Un sistema de tipos puede detectar y prevenir algunas de estas discrepancias. Cuando se detecta una discrepancia de tipos, se denomina error de tipo .

El tipo de un término limita los contextos en los que puede utilizarse. Para una variable, el sistema de tipos determina los valores permitidos. Para que dicha variable pueda presentarse como parámetro en una operación, esta debe poder aceptar cualquier valor que permita el tipo de la variable.

Los sistemas de tipos se especifican normalmente como parte del diseño del lenguaje de programación . Están integrados en los intérpretes y compiladores del lenguaje. En algunos lenguajes, el sistema de tipos puede ampliarse mediante herramientas opcionales que realizan comprobaciones adicionales utilizando la sintaxis y la gramática de tipos originales del lenguaje .

Los sistemas de tipos permiten definir interfaces entre las distintas partes de un programa informático y, posteriormente, comprobar que dichas partes se han conectado de forma coherente. Esta comprobación puede realizarse de forma estática (en tiempo de compilación ), dinámica (en tiempo de ejecución ) o mediante una combinación de ambas.

Los sistemas de tipos también tienen otros propósitos, como expresar reglas de negocio, permitir ciertas optimizaciones del compilador , posibilitar el despacho múltiple y proporcionar una forma de documentación .

Descripción general del uso

Un ejemplo de sistema de tipos simple es el del lenguaje C. Las partes de un programa en C son las definiciones de funciones . Una función es invocada por otra.

La interfaz de una función indica el nombre de la función y una lista de parámetros que se pasan a su código. El código de la función que la invoca indica el nombre de la función invocada, junto con los nombres de las variables que almacenan los valores que se le pasan.

Durante la ejecución de un programa informático , los valores se almacenan temporalmente y, a continuación, la ejecución salta al código de la función invocada. El código de la función invocada accede a los valores y los utiliza.

Si las instrucciones dentro de la función están escritas bajo el supuesto de recibir un valor entero , pero el código que la llama pasa un valor de punto flotante , entonces la función invocada calculará un resultado incorrecto.

El compilador de C comprueba que los tipos de los argumentos pasados a una función al llamarla coincidan con los tipos de los parámetros declarados en la definición de la función. Si los tipos no coinciden, el compilador genera un error o una advertencia en tiempo de compilación.

Un compilador también puede usar el tipo estático de un valor para optimizar el almacenamiento necesario y la elección de algoritmos para las operaciones con dicho valor. En muchos compiladores de C, el tipo de dato float , por ejemplo, se representa en 32 bits , de acuerdo con la especificación IEEE para números de punto flotante de precisión simple . Por lo tanto, utilizarán operaciones de microprocesador específicas para punto flotante en esos valores (suma, multiplicación, etc.).

La profundidad de las restricciones de tipo y la forma en que se evalúan afectan la tipificación del lenguaje. Un lenguaje de programación puede, además, asociar una operación con diversas resoluciones para cada tipo, en el caso del polimorfismo de tipos . La teoría de tipos es el estudio de los sistemas de tipos. Los tipos concretos de algunos lenguajes de programación, como los enteros y las cadenas, dependen de aspectos prácticos de la arquitectura de la computadora , la implementación del compilador y el diseño del lenguaje .

Fundamentos

Formalmente, la teoría de tipos estudia los sistemas de tipos. Un lenguaje de programación debe tener la oportunidad de verificar los tipos utilizando el sistema de tipos, ya sea en tiempo de compilación o en tiempo de ejecución, anotado manualmente o inferido automáticamente. Como Mark Manasse lo expresó concisamente: ^{[ 3 ]}

El problema fundamental que aborda una teoría de tipos es asegurar que los programas tengan significado. El problema fundamental que plantea una teoría de tipos es que los programas con significado pueden carecer de significados predefinidos. La búsqueda de sistemas de tipos más complejos surge de esta tensión.

Asignar un tipo de dato, denominado tipado , da significado a una secuencia de bits , como un valor en la memoria o un objeto , como una variable . El hardware de un ordenador de propósito general no puede distinguir, por ejemplo, entre una dirección de memoria y un código de instrucción , ni entre un carácter , un entero o un número de coma flotante , porque no hace ninguna distinción intrínseca entre ninguno de los posibles valores que podría representar una secuencia de bits . ^{[ nota 1 ]} Asociar una secuencia de bits con un tipo transmite ese significado al hardware programable para formar un sistema simbólico compuesto por dicho hardware y un programa.

Un programa asocia cada valor con al menos un tipo específico, pero también puede ocurrir que un valor se asocie con muchos subtipos . Otras entidades, como objetos , módulos , canales de comunicación y dependencias , pueden asociarse a un tipo. Incluso un tipo puede asociarse a otro tipo. En teoría, una implementación de un sistema de tipos podría asociar identificaciones denominadas tipo de dato (un tipo de valor), clase (un tipo de objeto) y clase (un tipo de tipo o metatipo). Estas son las abstracciones que puede experimentar la tipificación, en una jerarquía de niveles contenida en un sistema.

Cuando un lenguaje de programación desarrolla un sistema de tipos más elaborado, obtiene un conjunto de reglas más preciso que la verificación de tipos básica. Sin embargo, esto tiene un costo: las inferencias de tipo (y otras propiedades) se vuelven indecidibles , y el programador debe prestar mayor atención a la anotación del código o a las operaciones y el funcionamiento del sistema. Resulta complejo encontrar un sistema de tipos suficientemente expresivo que satisfaga todas las prácticas de programación de forma segura .

Un compilador de lenguaje de programación también puede implementar un sistema de tipos dependientes o de efectos , lo que permite que un verificador de tipos verifique aún más especificaciones del programa. Más allá de simples pares valor-tipo, una "región" virtual de código se asocia con un componente de "efecto" que describe qué se hace con qué y permite, por ejemplo, generar un informe de error. De este modo, el sistema simbólico puede ser un sistema de tipos y efectos , lo que le confiere mayor seguridad que la simple verificación de tipos.

Ya sea automatizado por el compilador o especificado por un programador, un sistema de tipos hace que el comportamiento del programa sea ilegal si se sale de las reglas del sistema de tipos. Las ventajas que ofrecen los sistemas de tipos especificados por el programador incluyen:

Abstracción (o modularidad ): Los tipos permiten a los programadores pensar a un nivel superior al bit o byte, sin preocuparse por la implementación de bajo nivel . Por ejemplo, pueden concebir una cadena como un conjunto de caracteres en lugar de una matriz de bytes. Además, los tipos permiten a los programadores pensar y expresar interfaces entre dos subsistemas de cualquier tamaño. Esto posibilita una mayor localización, de modo que las definiciones necesarias para la interoperabilidad de los subsistemas se mantengan coherentes cuando estos se comunican.
Documentación : En sistemas de tipos más expresivos, los tipos pueden servir como una forma de documentación que aclara la intención del programador. Por ejemplo, si un programador declara que una función devuelve un tipo de marca de tiempo, esto documenta la función cuando dicho tipo se puede declarar explícitamente más adelante en el código como un tipo entero.

Las ventajas que ofrecen los sistemas de tipos especificados por el compilador incluyen:

Optimización : la comprobación estática de tipos puede proporcionar información útil en tiempo de compilación . Por ejemplo, si un tipo requiere que un valor se alinee en memoria a un múltiplo de cuatro bytes, el compilador puede utilizar instrucciones de máquina más eficientes.
Seguridad : Un sistema de tipos permite al compilador detectar código sin sentido o inválido. Por ejemplo, podemos identificar una expresión como inválida cuando las reglas no especifican cómo dividir un número entero entre una cadena . El tipado fuerte ofrece mayor seguridad, pero no puede garantizar una seguridad de tipos completa .3 / "Hello, World"

Errores de tipo

Se produce un error de tipo cuando una operación recibe un tipo de datos diferente al esperado. ^{[ 4 ]} Por ejemplo, un error de tipo ocurriría si una línea de código divide dos enteros y recibe una cadena de letras en lugar de un entero. ^{[ 4 ]} Es una condición no deseada ^{[ nota 2 ]} que puede manifestarse en varias etapas del desarrollo de un programa. Por lo tanto, se necesita una herramienta para la detección de errores en el sistema de tipos. En algunos lenguajes, como Haskell , para los que la inferencia de tipos es automática, el compilador puede disponer de lint para ayudar en la detección de errores.

La seguridad de tipos contribuye a la corrección de los programas , pero puede garantizarla a costa de convertir la propia verificación de tipos en un problema indecidible (como en el problema de la parada ). En un sistema de tipos con verificación automática, un programa puede ejecutarse incorrectamente sin generar errores de compilación. La división por cero es una operación insegura e incorrecta, pero un verificador de tipos que solo se ejecuta en tiempo de compilación no la detecta en la mayoría de los lenguajes; esta división se manifestaría como un error en tiempo de ejecución . Para demostrar la ausencia de estos defectos, se utilizan comúnmente otros métodos formales , conocidos colectivamente como análisis de programas . Alternativamente, un sistema de tipos suficientemente expresivo, como en los lenguajes con tipado dependiente, puede prevenir este tipo de errores (por ejemplo, al expresar el tipo de los números distintos de cero ). Además, las pruebas de software son un método empírico para encontrar errores que un verificador de tipos no detectaría.

comprobación de tipos

El proceso de verificar y hacer cumplir las restricciones de los tipos, la comprobación de tipos , puede ocurrir en tiempo de compilación (una comprobación estática) o en tiempo de ejecución (una comprobación dinámica).

Si una especificación de lenguaje exige que sus reglas de tipado sean estrictas, permitiendo más o menos solo aquellas conversiones de tipo automáticas que no pierden información, se puede decir que el proceso es fuertemente tipado ; de lo contrario, es débilmente tipado .

Estos términos no suelen utilizarse en sentido estricto.

Verificación de tipos estática

La verificación estática de tipos es el proceso de comprobar la seguridad de tipos de un programa mediante el análisis de su código fuente . Si un programa supera la verificación estática, se garantiza que cumple con un conjunto de propiedades de seguridad de tipos para todas las entradas posibles.

La comprobación estática de tipos puede considerarse una forma limitada de verificación de programas (véase seguridad de tipos ) y, en un lenguaje con tipado seguro, también puede considerarse una optimización. Si un compilador puede demostrar que un programa está bien tipado, no necesita realizar comprobaciones de seguridad dinámicas, lo que permite que el binario compilado resultante se ejecute más rápido y ocupe menos espacio.

La verificación de tipos estática para lenguajes Turing-completos es inherentemente conservadora. Es decir, si un sistema de tipos es a la vez correcto (lo que significa que rechaza todos los programas incorrectos) y decidible (lo que significa que es posible escribir un algoritmo que determine si un programa está bien tipado), entonces debe ser incompleto (lo que significa que hay programas correctos que también son rechazados, aunque no presenten errores en tiempo de ejecución). ^{[ 7 ]} Por ejemplo, considérese un programa que contiene el siguiente código:

if <complex test> then <do something> else <signal that there is a type error>

Aunque la expresión <complex test>siempre se evalúe trueen tiempo de ejecución, la mayoría de los verificadores de tipos rechazarán el programa por ser mal tipado, ya que es difícil (si no imposible) para un analizador estático determinar que la elserama no se tomará. ^{[ 8 ]} En consecuencia, un verificador de tipos estático detectará rápidamente errores de tipo en rutas de código poco utilizadas. Sin verificación de tipos estática, incluso las pruebas de cobertura de código con una cobertura del 100 % pueden ser incapaces de encontrar tales errores de tipo. Las pruebas pueden fallar en detectar tales errores de tipo porque se debe tener en cuenta la combinación de todos los lugares donde se crean valores y todos los lugares donde se utiliza un valor determinado.

Varias características útiles y comunes de los lenguajes de programación no se pueden comprobar de forma estática, como la conversión descendente de tipos . Por lo tanto, muchos lenguajes cuentan con comprobación de tipos tanto estática como dinámica; el verificador de tipos estático comprueba lo que puede, y las comprobaciones dinámicas comprueban el resto.

Muchos lenguajes con comprobación de tipos estática proporcionan una forma de eludir el verificador de tipos. Algunos lenguajes permiten a los programadores elegir entre seguridad de tipos estática y dinámica. Por ejemplo, históricamente C# declara variables estáticamente, ^{[ 9 ]}^{: 77, Sección 3.2} pero C# 4.0 introduce la dynamicpalabra clave, que se utiliza para declarar variables que se comprobarán dinámicamente en tiempo de ejecución. ^{[ 9 ]}^{: 117, Sección 4.1} Otros lenguajes permiten escribir código que no es seguro en cuanto a tipos; por ejemplo, en C , los programadores pueden convertir libremente un valor entre dos tipos cualesquiera que tengan el mismo tamaño, subvirtiendo efectivamente el concepto de tipo.

Verificación de tipos dinámica e información de tipos en tiempo de ejecución

La comprobación dinámica de tipos es el proceso de verificar la seguridad de tipos de un programa en tiempo de ejecución. Las implementaciones de lenguajes con comprobación dinámica de tipos suelen asociar cada objeto en tiempo de ejecución con una etiqueta de tipo (es decir, una referencia a un tipo) que contiene su información de tipo. Esta información de tipo en tiempo de ejecución (RTTI) también se puede utilizar para implementar despacho dinámico , enlace tardío , conversión descendente , programación reflexiva (reflexión) y características similares.

La mayoría de los lenguajes con tipado seguro incluyen algún tipo de verificación dinámica de tipos, incluso si también cuentan con un verificador de tipos estático. ^{[ 10 ]} Esto se debe a que muchas características o propiedades útiles son difíciles o imposibles de verificar estáticamente. Por ejemplo, supongamos que un programa define dos tipos, A y B, donde B es un subtipo de A. Si el programa intenta convertir un valor de tipo A a tipo B, lo que se conoce como conversión descendente , la operación solo es válida si el valor que se está convirtiendo es realmente de tipo B. Por lo tanto, se necesita una verificación dinámica para comprobar que la operación es segura. Este requisito es una de las críticas a la conversión descendente.

Por definición, la comprobación dinámica de tipos puede provocar que un programa falle en tiempo de ejecución. En algunos lenguajes de programación, es posible anticipar y recuperarse de estos fallos. En otros, los errores de comprobación de tipos se consideran fatales.

Los lenguajes de programación que incluyen comprobación de tipos dinámica pero no comprobación de tipos estática suelen denominarse "lenguajes de programación de tipado dinámico".

Combinando la comprobación de tipos estática y dinámica

Algunos lenguajes permiten tanto el tipado estático como el dinámico. Por ejemplo, Java y otros lenguajes aparentemente de tipado estático admiten la conversión descendente de tipos a sus subtipos , la consulta de un objeto para descubrir su tipo dinámico y otras operaciones de tipo que dependen de la información de tipo en tiempo de ejecución. Otro ejemplo es C++ RTTI . En general, la mayoría de los lenguajes de programación incluyen mecanismos para gestionar diferentes tipos de datos, como uniones disjuntas , polimorfismo en tiempo de ejecución y tipos variantes . Incluso sin interactuar con anotaciones de tipo o comprobación de tipos, estos mecanismos son sustancialmente similares a las implementaciones de tipado dinámico.

En los lenguajes orientados a objetos, generalmente se accede a los objetos mediante una referencia cuyo tipo de destino estático (o tipo manifiesto) es igual al tipo de tiempo de ejecución del objeto (su tipo latente) o a un supertipo del mismo. Esto se ajusta al principio de sustitución de Liskov , que establece que todas las operaciones realizadas sobre una instancia de un tipo dado también pueden realizarse sobre una instancia de un subtipo. Este concepto también se conoce como subsunción o polimorfismo de subtipos . En algunos lenguajes, los subtipos pueden tener tipos de retorno y tipos de argumento covariantes o contravariantes, respectivamente.

Algunos lenguajes, como Clojure , Common Lisp o Cython, realizan comprobación de tipos dinámica por defecto, pero permiten que los programas opten por la comprobación de tipos estática mediante anotaciones opcionales. Una razón para usar estas sugerencias sería optimizar el rendimiento de secciones críticas de un programa. Esto se formaliza mediante la tipificación gradual . El entorno de programación DrRacket , un entorno pedagógico basado en Lisp y precursor del lenguaje Racket, también utiliza tipado flexible. ^{[ 11 ]}

Por el contrario, a partir de la versión 4.0, el lenguaje C# proporciona una forma de indicar que una variable no debe someterse a una comprobación de tipo estática. Una variable cuyo tipo sea dynamicno estará sujeta a dicha comprobación. En su lugar, el programa se basa en la información de tipo en tiempo de ejecución para determinar cómo se puede utilizar la variable. ^{[ 12 ]}^{[ 9 ]}^{: 113–119}

En Rust , el objeto trait proporciona tipado dinámico de tipos que no contienen tiempos de vida o que solo los contienen. ^[¹³^]dynstd::any::Any'static

Verificación de tipos estática y dinámica en la práctica

La elección entre tipado estático y dinámico implica ciertas concesiones .

El tipado estático puede encontrar errores de tipo de forma fiable en tiempo de compilación, lo que aumenta la fiabilidad del programa entregado. Sin embargo, los programadores discrepan sobre la frecuencia con la que ocurren los errores de tipo, lo que genera más discrepancias sobre la proporción de esos errores codificados que se detectarían al representar adecuadamente los tipos diseñados en el código. ^{[ 14 ]}^{[ 15 ]} Los defensores del tipado estático creen que los programas son más fiables cuando se han comprobado bien sus tipos, mientras que los defensores del tipado dinámico señalan el código distribuido que ha demostrado ser fiable y las bases de datos de errores pequeñas. El valor del tipado estático aumenta a medida que aumenta la robustez del sistema de tipos. Los defensores del tipado dependiente , implementado en lenguajes como Dependent ML y Epigram , han sugerido que casi todos los errores pueden considerarse errores de tipo, si los tipos utilizados en un programa están correctamente declarados por el programador o inferidos correctamente por el compilador. ^[¹⁶^]

El tipado estático suele dar como resultado un código compilado que se ejecuta más rápido. Cuando el compilador conoce los tipos de datos exactos que se utilizan (lo cual es necesario para la verificación estática, ya sea mediante declaración o inferencia), puede generar código máquina optimizado. Algunos lenguajes de tipado dinámico, como Common Lisp, permiten declaraciones de tipo opcionales para la optimización por este motivo.

Por el contrario, el tipado dinámico puede permitir que los compiladores se ejecuten más rápido y que los intérpretes carguen código nuevo de forma dinámica, ya que los cambios en el código fuente en lenguajes de tipado dinámico pueden resultar en menos comprobaciones y menos código que revisar. Esto también puede reducir el ciclo de edición, compilación, prueba y depuración.

Los lenguajes de tipado estático que carecen de inferencia de tipos (como C y Java antes de la versión 10 ) requieren que los programadores declaren los tipos que debe usar un método o función. Esto puede servir como documentación adicional del programa, activa y dinámica, en lugar de estática. Esto permite que el compilador evite que se desincronicen y que los programadores la ignoren. Sin embargo, un lenguaje puede ser de tipado estático sin requerir declaraciones de tipos (ejemplos incluyen Haskell , Scala , OCaml , F# , Swift y, en menor medida, C# y C++ ), por lo que la declaración explícita de tipos no es necesaria para el tipado estático en todos los lenguajes.

El tipado dinámico permite construcciones que algunas comprobaciones de tipos estáticas (simples) rechazarían por ilegales. Por ejemplo, las funciones `eval` , que ejecutan datos arbitrarios como código, se vuelven posibles. Una función `eval` es posible con el tipado estático, pero requiere un uso avanzado de tipos de datos algebraicos . Además, el tipado dinámico facilita el desarrollo de código transitorio y prototipos, permitiendo, por ejemplo, el uso transparente de una estructura de datos de marcador de posición ( objeto simulado ) en lugar de una estructura de datos completa (generalmente con fines de experimentación y prueba).

El tipado dinámico suele permitir el tipado dinámico (que facilita la reutilización del código ). Muchos lenguajes con tipado estático también incluyen el tipado dinámico u otros mecanismos como la programación genérica , que también facilitan la reutilización del código.

El tipado dinámico suele facilitar el uso de la metaprogramación . Por ejemplo, las plantillas de C++ suelen ser más engorrosas de escribir que el código equivalente en Ruby o Python , ya que C++ tiene reglas más estrictas en cuanto a las definiciones de tipos (tanto para funciones como para variables). Esto obliga al desarrollador a escribir más código repetitivo para una plantilla que el que necesitaría un desarrollador de Python. Las construcciones de tiempo de ejecución más avanzadas, como las metaclases y la introspección, suelen ser más difíciles de usar en lenguajes de tipado estático. En algunos lenguajes, estas características también pueden utilizarse, por ejemplo, para generar nuevos tipos y comportamientos sobre la marcha, basándose en datos de tiempo de ejecución. Estas construcciones avanzadas suelen estar disponibles en lenguajes de programación dinámica ; muchos de ellos son de tipado dinámico, aunque el tipado dinámico no tiene por qué estar relacionado con los lenguajes de programación dinámica .

Sistemas de tipo fuerte y débil

Los lenguajes suelen denominarse coloquialmente de tipado fuerte o de tipado débil . De hecho, no existe una definición universalmente aceptada de estos términos. En general, existen términos más precisos para representar las diferencias entre los sistemas de tipado que llevan a denominarlos "fuertes" o "débiles".

Seguridad de tipos y seguridad de memoria

Una tercera forma de clasificar el sistema de tipos de un lenguaje de programación es mediante la seguridad de las operaciones y conversiones tipadas. Los informáticos utilizan el término lenguaje seguro en cuanto a tipos para describir lenguajes que no permiten operaciones ni conversiones que infrinjan las reglas del sistema de tipos.

Los informáticos utilizan el término lenguaje seguro para la memoria (o simplemente lenguaje seguro ) para describir aquellos lenguajes que impiden que los programas accedan a memoria que no ha sido asignada para su uso. Por ejemplo, un lenguaje seguro para la memoria comprueba los límites de los arrays o, en su defecto, garantiza estáticamente (es decir, en tiempo de compilación, antes de la ejecución) que los accesos a arrays fuera de sus límites provocarán errores de compilación y, posiblemente, errores en tiempo de ejecución.

Considere el siguiente programa de un lenguaje que es seguro en cuanto a tipos y memoria: ^{[ 17 ]}

var x := 5; var y := "37"; var z := x + y;

En este ejemplo, la variable ztendrá el valor 42. Aunque esto no sea lo que el programador anticipó, es un resultado bien definido. Si yfuera una cadena diferente, una que no pudiera convertirse en un número (por ejemplo, " Hola, Mundo "), el resultado también estaría bien definido. Un programa puede ser seguro en cuanto a tipos o memoria y aun así fallar ante una operación no válida. Esto se aplica a lenguajes donde el sistema de tipos no es lo suficientemente avanzado como para especificar con precisión la validez de las operaciones en todos los operandos posibles. Pero si un programa encuentra una operación que no es segura en cuanto a tipos, terminar el programa suele ser la única opción.

Consideremos ahora un ejemplo similar en C:

int x = 5 ; char y [] = "37" ; char * z = x + y ; printf ( "%c \n " , * z );

En este ejemplo, zapuntará a una dirección de memoria cinco caracteres más allá de y, equivalente a tres caracteres después del carácter cero de terminación de la cadena a la que apunta y. Esta es una memoria a la que no se espera que el programa acceda. En términos de C, esto es simplemente un comportamiento indefinido y el programa puede hacer cualquier cosa; con un compilador simple, podría imprimir cualquier byte almacenado después de la cadena "37". Como muestra este ejemplo, C no es seguro en cuanto a la memoria. Dado que se asumió que los datos arbitrarios eran caracteres, tampoco es un lenguaje seguro en cuanto a tipos.

En general, la seguridad de tipos y la seguridad de memoria van de la mano. Por ejemplo, un lenguaje que admite aritmética de punteros y conversiones de números a punteros (como C) no es seguro ni en cuanto a memoria ni en cuanto a tipos, porque permite acceder a memoria arbitraria como si fuera memoria válida de cualquier tipo.

Niveles variables de verificación de tipos

Algunos lenguajes permiten aplicar diferentes niveles de verificación a diferentes regiones del código. Algunos ejemplos son:

La use strictdirectiva en JavaScript ^{[ 18 ]}^{[ 19 ]}^{[ 20 ]} y Perl aplica una verificación más estricta.
En PHP ^[²¹^] , por archivo, solo se permite una variable del tipo exacto de la declaración de tipo; de lo contrario, se lanzará una declare(strict_types=1)excepción .TypeError
Option Strict OnEn VB.NET, esto permite que el compilador requiera una conversión entre objetos.

También se pueden utilizar herramientas adicionales como lint e IBM Rational Purify para lograr un mayor nivel de rigor.

Sistemas de tipos opcionales

Se ha propuesto, principalmente por Gilad Bracha , que la elección del sistema de tipos sea independiente de la elección del lenguaje; que un sistema de tipos sea un módulo que pueda integrarse en un lenguaje según sea necesario. Él cree que esto es ventajoso, porque lo que él llama sistemas de tipos obligatorios hacen que los lenguajes sean menos expresivos y el código más frágil. ^{[ 22 ]} El requisito de que el sistema de tipos no afecte la semántica del lenguaje es difícil de cumplir.

La tipificación opcional está relacionada con la tipificación gradual , pero es distinta de ella . Si bien ambas disciplinas de tipificación pueden utilizarse para realizar análisis estáticos del código ( tipificación estática ), los sistemas de tipificación opcionales no imponen seguridad de tipos en tiempo de ejecución ( tipificación dinámica ). ^{[ 22 ]}^{[ 23 ]}

Polimorfismo y tipos

El término polimorfismo se refiere a la capacidad del código (especialmente, funciones o clases) para operar con valores de múltiples tipos, o a la capacidad de diferentes instancias de la misma estructura de datos para contener elementos de distintos tipos. Los sistemas de tipos que permiten el polimorfismo generalmente lo hacen para mejorar el potencial de reutilización del código: en un lenguaje con polimorfismo, los programadores solo necesitan implementar una estructura de datos, como una lista o un array asociativo , una sola vez, en lugar de una vez para cada tipo de elemento con el que planean usarla. Por esta razón, los informáticos a veces llaman programación genérica al uso de ciertas formas de polimorfismo . Los fundamentos teóricos de tipos del polimorfismo están estrechamente relacionados con los de la abstracción , la modularidad y (en algunos casos) el subtipado .

Sistemas de tipos especializados

Se han creado numerosos sistemas de tipos especializados para su uso en entornos específicos con determinados tipos de datos, o para el análisis estático de programas fuera de banda . Con frecuencia, estos sistemas se basan en ideas de la teoría formal de tipos y solo están disponibles como parte de prototipos de sistemas de investigación.

La siguiente tabla ofrece una visión general de los conceptos de teoría de tipos que se utilizan en sistemas de tipos especializados. Los nombres $M, N, O$ abarcan términos y los nombres $\sigma ,\tau$ abarca diferentes tipos. Se utilizará la siguiente notación:

$M:\sigma$ significa que $M$ tiene tipo $\sigma$ ;
$M(N)$ es que la aplicación de $M$ en $N$ ;
${\displaystyle \tau [\alpha$ (resp. $\tau [x:=N]$ ) describe el tipo que resulta de reemplazar todas las ocurrencias de la variable de tipo $α$ (respectivamente, la variable de término $x$ ) en $\tau$ por el tipo $σ$ (resp. término $N$ ).

↑ También conocido como tipo de producto dependiente , ya que ${\textstyle (x:\sigma )\to \tau =\prod _{x:\sigma }\tau }$ .
↑ También conocido como tipo de suma dependiente , ya que ${\textstyle (x:\sigma )\times \tau =\sum _{x:\sigma }\tau }$ .

Tipos dependientes

Los tipos dependientes se basan en la idea de usar escalares o valores para describir con mayor precisión el tipo de algún otro valor. Por ejemplo, $\mathrm {matrix} (3,3)$ podría ser el tipo de $3\times 3$ matriz. A continuación, podemos definir reglas de tipado como la siguiente regla para la multiplicación de matrices:

\mathrm {matrix} _{\mathrm {multiply} }:\mathrm {matrix} (k,m)\times \mathrm {matrix} (m,n)\to \mathrm {matrix} (k,n)

donde $k$ , $m$ , $n$ son valores enteros positivos arbitrarios. Se ha creado una variante de ML llamada ML dependiente basada en este sistema de tipos, pero debido a que la verificación de tipos para tipos dependientes convencionales es indecidible , no todos los programas que los utilizan pueden ser verificados sin algún tipo de limitaciones. ML dependiente limita el tipo de igualdad que puede decidir a la aritmética de Presburger .

Otros lenguajes, como Epigram, permiten determinar el valor de todas las expresiones para facilitar la verificación de tipos. Sin embargo, en general, la prueba de decidibilidad es indecidible , por lo que muchos programas requieren anotaciones manuales que pueden ser muy complejas. Dado que esto dificulta el desarrollo, muchas implementaciones de lenguaje ofrecen una solución sencilla: la opción de desactivar esta condición. No obstante, esto conlleva que el verificador de tipos entre en un bucle infinito al procesar programas que no cumplen con la verificación de tipos, lo que provoca un fallo en la compilación.

Tipos lineales

Los tipos lineales , basados en la teoría de la lógica lineal y estrechamente relacionados con los tipos de unicidad , son tipos asignados a valores que poseen la propiedad de tener una única referencia en todo momento. Son valiosos para describir valores inmutables de gran tamaño , como archivos, cadenas de caracteres, etc., ya que cualquier operación que destruya simultáneamente un objeto lineal y cree uno similar (como str = str + "a") puede optimizarse internamente en una mutación in situ. Normalmente, esto no es posible, puesto que tales mutaciones podrían causar efectos secundarios en partes del programa que mantienen otras referencias al objeto, violando la transparencia referencial . También se utilizan en el prototipo del sistema operativo Singularity para la comunicación entre procesos, asegurando estáticamente que los procesos no puedan compartir objetos en la memoria compartida para evitar condiciones de carrera. El lenguaje Clean (un lenguaje similar a Haskell ) utiliza este sistema de tipos para obtener una gran velocidad (en comparación con realizar una copia profunda) sin comprometer la seguridad.

Tipos de intersección

Los tipos de intersección describen valores que pertenecen a dos tipos dados con conjuntos de valores superpuestos. Por ejemplo, en la mayoría de las implementaciones de C, el valor de `signed char` va de -128 a 127 y el de `unsigned char` va de 0 a 255, por lo que el tipo de intersección de estos dos tipos tendría un rango de 0 a 127. Dicho tipo de intersección se puede pasar de forma segura a funciones que esperan valores de `signed char` o `unsigned char`, ya que es compatible con ambos.

Los tipos de intersección son útiles para describir tipos de funciones sobrecargadas: por ejemplo, si " int→ int" es el tipo de función que toma un argumento entero y devuelve un entero, y " float→ float" es el tipo de función que toma un argumento flotante y devuelve un flotante, entonces la intersección de estos dos tipos se puede usar para describir funciones que hacen una u otra, según el tipo de entrada que reciban. Dicha función podría pasarse a otra función que espera una función " int→ int" de forma segura; simplemente no usaría la funcionalidad " float→ ".float

En una jerarquía de subclases, la intersección de un tipo con un tipo antecesor (como su tipo padre) es el tipo más derivado. La intersección de tipos hermanos está vacía.

El lenguaje Forsythe incluye una implementación general de tipos de intersección. Una forma restringida son los tipos de refinamiento .

Tipos de sindicatos

Los tipos de unión son tipos que describen valores que pertenecen a cualquiera de dos tipos. Por ejemplo, en C, el tipo `signed char` tiene un rango de -128 a 127, y el tipo `unsigned char` tiene un rango de 0 a 255, por lo que la unión de estos dos tipos tendría un rango "virtual" general de -128 a 255 que puede usarse parcialmente dependiendo de a qué miembro de la unión se acceda. Cualquier función que maneje este tipo de unión tendría que trabajar con enteros en este rango completo. En general, las únicas operaciones válidas en un tipo de unión son operaciones válidas en ambos tipos que se unen. El concepto de "unión" de C es similar a los tipos de unión, pero no es seguro en cuanto a tipos, ya que permite operaciones que son válidas en cualquiera de los tipos, en lugar de en ambos . Los tipos de unión son importantes en el análisis de programas, donde se utilizan para representar valores simbólicos cuya naturaleza exacta (por ejemplo, valor o tipo) se desconoce.

En una jerarquía de subclases, la unión de un tipo y un tipo antecesor (como su padre) es el tipo antecesor. La unión de tipos hermanos es un subtipo de su antecesor común (es decir, todas las operaciones permitidas en su antecesor común están permitidas en el tipo de unión, pero también pueden tener otras operaciones válidas en común).

Tipos existenciales

Los tipos existenciales se utilizan frecuentemente junto con los tipos de registro para representar módulos y tipos de datos abstractos , debido a su capacidad para separar la implementación de la interfaz. Por ejemplo, el tipo "T = ∃X { a: X; f: (X → int); }" describe una interfaz de módulo que tiene un miembro de datos llamado a de tipo X y una función llamada f que toma un parámetro del mismo tipo X y devuelve un entero. Esto podría implementarse de diferentes maneras; por ejemplo:

intT = { a: int; f: (int → entero); }
floatT = { a: float; f: (float → int); }

Estos tipos son subtipos del tipo existencial más general T y corresponden a tipos de implementación concretos, por lo que cualquier valor de uno de estos tipos es un valor de tipo T. Dado un valor "t" de tipo "T", sabemos que "tf(ta)" está bien tipado, independientemente del tipo abstracto X. Esto proporciona flexibilidad para elegir tipos adecuados a una implementación particular, mientras que los clientes que utilizan únicamente valores del tipo de interfaz —el tipo existencial— quedan al margen de estas opciones.

En general, es imposible que el verificador de tipos infiera a qué tipo existencial pertenece un módulo dado. En el ejemplo anterior, intT { a: int; f: (int → int); } también podría tener el tipo ∃X { a: X; f: (X → int); }. La solución más sencilla es anotar cada módulo con su tipo previsto, por ejemplo:

intT = { a: int; f: (int → entero); } como ∃X { a: X; f: (X → int); }

Aunque los tipos de datos abstractos y los módulos se habían implementado en lenguajes de programación desde hacía bastante tiempo, no fue hasta 1988 que John C. Mitchell y Gordon Plotkin establecieron la teoría formal bajo el lema: "Los tipos [de datos] abstractos tienen tipo existencial". ^{[ 25 ]} La teoría es un cálculo lambda tipado de segundo orden similar al Sistema F , pero con cuantificación existencial en lugar de universal.

Mecanografía gradual

En un sistema de tipos con tipado gradual , a las variables se les puede asignar un tipo tanto en tiempo de compilación (tipado estático) como en tiempo de ejecución (tipado dinámico). ^{[ 26 ]} Esto permite a los desarrolladores de software elegir el paradigma de tipos que mejor les convenga, dentro de un mismo lenguaje. ^{[ 26 ]} El tipado gradual utiliza un tipo especial llamado dinámico para representar tipos estáticamente desconocidos; reemplaza la noción de igualdad de tipos con una nueva relación llamada consistencia que relaciona el tipo dinámico con todos los demás tipos. La relación de consistencia es simétrica pero no transitiva. ^{[ 27 ]}

Declaración e inferencia explícitas o implícitas

Muchos sistemas de tipado estático, como los de C y Java, requieren declaraciones de tipo : el programador debe asociar explícitamente cada variable con un tipo específico. Otros, como el de Haskell, realizan inferencia de tipos : el compilador deduce los tipos de las variables según cómo las utilicen los programadores. Por ejemplo, dada una función que suma y , el compilador puede inferir que y deben ser números, ya que la suma solo está definida para números. Por lo tanto, cualquier llamada a en otra parte del programa que especifique un tipo no numérico (como una cadena o una lista) como argumento generaría un error.f(x,y)xyxyf

Las constantes y expresiones numéricas y de cadena en el código pueden implicar, y a menudo lo hacen, un tipo en un contexto particular. Por ejemplo, una expresión podría implicar un tipo de punto flotante , mientras que podría implicar una lista de enteros, normalmente una matriz .3.14[1,2,3]

La inferencia de tipos es posible en general, si es computable en el sistema de tipos en cuestión. Además, incluso si la inferencia no es computable en general para un sistema de tipos dado, suele ser posible para un gran subconjunto de programas reales. El sistema de tipos de Haskell, una versión de Hindley-Milner , es una restricción del Sistema Fω a los llamados tipos polimórficos de rango 1, en los que la inferencia de tipos es computable. La mayoría de los compiladores de Haskell permiten el polimorfismo de rango arbitrario como extensión, pero esto hace que la inferencia de tipos no sea computable. (Sin embargo, la verificación de tipos es decidible , y los programas de rango 1 aún tienen inferencia de tipos; los programas polimórficos de rango superior se rechazan a menos que se les proporcionen anotaciones de tipo explícitas).

Problemas de decisión

Un sistema de tipos que asigna tipos a términos en entornos de tipos utilizando reglas de tipado está naturalmente asociado con los problemas de decisión de verificación de tipos , tipabilidad y habitabilidad de tipos . ^{[ 28 ]}

Dado un entorno de tipos $\Gamma$ , un término $e$ y un tipo $\tau$ , decidir si el término $e$ Se le puede asignar el tipo $\tau$ en el entorno de tipos.
Dado un término $e$ , decidir si existe un entorno de tipos $\Gamma$ y un tipo $\tau$ de tal manera que el término $e$ Se le puede asignar el tipo $\tau$ en el entorno de tipos $\Gamma$ .
Dado un entorno de tipos $\Gamma$ y un tipo $\tau$ , decidir si existe un término $e$ que se le puede asignar el tipo $\tau$ en el entorno de tipos.

Sistema de tipos unificado

Algunos lenguajes como C# o Scala tienen un sistema de tipos unificado. ^{[ 29 ]} Esto significa que todos los tipos de C#, incluidos los tipos primitivos, heredan de un único objeto raíz. Cada tipo en C# hereda de la clase Object. Algunos lenguajes, como Java y Raku , tienen un tipo raíz, pero también tipos primitivos que no son objetos. ^{[ 30 ]} Java proporciona tipos de objetos envoltorio que coexisten con los tipos primitivos, de modo que los desarrolladores pueden usar tanto los tipos de objetos envoltorio como los tipos primitivos más simples que no son objetos. Raku convierte automáticamente los tipos primitivos a objetos cuando se accede a sus métodos. ^{[ 31 ]}

Compatibilidad: equivalencia y subtipado

Un verificador de tipos para un lenguaje de tipado estático debe comprobar que el tipo de cualquier expresión sea coherente con el tipo esperado por el contexto en el que aparece dicha expresión. Por ejemplo, en una instrucción de asignación de la forma , el tipo inferido de la expresión debe ser coherente con el tipo declarado o inferido de la variable . Esta noción de coherencia, denominada compatibilidad , es específica de cada lenguaje de programación.x := eex

Si el tipo de ey el tipo de xson iguales, y se permite la asignación para ese tipo, entonces esta es una expresión válida. Por lo tanto, en los sistemas de tipos más simples, la cuestión de si dos tipos son compatibles se reduce a si son iguales (o equivalentes ). Sin embargo, los diferentes lenguajes tienen diferentes criterios para determinar cuándo se entiende que dos expresiones de tipo denotan el mismo tipo. Estas diferentes teorías de equivalencia de tipos varían ampliamente, siendo dos casos extremos los sistemas de tipos estructurales , en los que dos tipos cualesquiera que describan valores con la misma estructura son equivalentes, y los sistemas de tipos nominativos , en los que dos expresiones de tipo sintácticamente distintas no denotan el mismo tipo ( es decir , los tipos deben tener el mismo "nombre" para ser iguales).

En lenguajes con subtipos , la relación de compatibilidad es más compleja: si Bes un subtipo de A, entonces un valor de tipo Bpuede usarse en un contexto donde Ase espera uno de tipo ( covariante ), incluso si lo contrario no es cierto. Al igual que la equivalencia, la relación de subtipo se define de manera diferente para cada lenguaje de programación, con muchas variaciones posibles. La presencia de polimorfismo paramétrico o ad hoc en un lenguaje también puede tener implicaciones para la compatibilidad de tipos.

Véase también

Comparación de sistemas de tipos
Variación de tipos : concepto de lenguaje de programación
Polimorfismo (informática) : uso de una interfaz o símbolo con respecto a múltiples tipos diferentes.
Firma de tipo : define las entradas y salidas de una función, subrutina o método.
Teoría de tipos – Teoría matemática de los tipos de datos

Notas

↑ La línea de computadoras ALGOL de Burroughs determinaba el contenido de una ubicación de memoria mediante sus bits de bandera. Los bits de bandera especifican el contenido de una ubicación de memoria. Las instrucciones, el tipo de datos y las funciones se especifican mediante un código de 3 bits, además de su contenido de 48 bits. Solo el MCP (Programa de Control Maestro) podía escribir en los bits del código de bandera.
↑ Por ejemplo, una abstracción con fugas podría surgir durante el desarrollo, lo que podría mostrar que se necesita más desarrollo de tipos. —"La evaluación de un programa bien tipado siempre termina".—B. Nordström, K. Petersson y JM Smith^{[ 5 ]} Un cambio sistemático en las variables para evitar la captura de una variable libre puede introducir un error , en un lenguaje de programación funcional donde las funciones son ciudadanos de primera clase.^{[ 6 ]} —Del artículo sobre cálculo lambda .

Referencias

↑ Pierce 2002 , p. 1: "Un sistema de tipos es un método sintáctico manejable para probar la ausencia de ciertos comportamientos de un programa clasificando las frases según los tipos de valores que calculan."
↑ Cardelli 2004 , p. 1: "El propósito fundamental de un sistema de tipos es prevenir la aparición de errores de ejecución durante la ejecución de un programa."
↑ Pierce 2002 , pág. 208.
1 2 Sethi, R. (1996). Lenguajes de programación: conceptos y construcciones (2.ª ed.). Addison-Wesley. pág. 142. ISBN 978-0-201-59065-4OCLC 604732680
↑ Nordström, B.; Petersson, K.; Smith, JM (2001). "Teoría de tipos de Martin-Löf" . Estructuras algebraicas y lógicas . Manual de lógica en informática. Vol. 5. Oxford University Press. pág. 2. ISBN 978-0-19-154627-3.
↑ Turner, DA (12 de junio de 2012). "Algo de historia de los lenguajes de programación funcional" (PDF) . Conferencia invitada en TFP12, en la Universidad de St Andrews . Véase la sección sobre Algol 60.
↑ "... cualquier sistema de tipos sólido y decidible debe ser incompleto" —D. Remy (2017). pág. 29, Remy, Didier. "Sistemas de tipos para lenguajes de programación" (PDF) . Archivado del original (PDF) el 14 de noviembre de 2017. Recuperado el 26 de mayo de 2013 .
↑ Pierce 2002 .
1 2 3 Skeet, Jon (2019). C# en profundidad (4.ª ed.). Manning. ISBN 978-1617294532.
↑ Miglani, Gaurav (2018). "Despacho dinámico de métodos o polimorfismo en tiempo de ejecución en Java" . Archivado del original el 7 de diciembre de 2020. Consultado el 28 de marzo de 2021 .
↑ Wright, Andrew K. (1995). Practical Soft Typing (PhD). Rice University. hdl : 1911/16900 .
↑ "dinámico (Referencia de C#)" . Biblioteca MSDN . Microsoft . Consultado el 14 de enero de 2014 .
↑ "std::any — Rust" . doc.rust-lang.org . Consultado el 7 de julio de 2021 .
↑ Meijer, Erik; Drayton, Peter. "Tipado estático cuando sea posible, tipado dinámico cuando sea necesario: el fin de la guerra fría entre los lenguajes de programación" (PDF) . Microsoft Corporation.
↑ Laucher, Amanda; Snively, Paul (2012). "Tipos vs. Pruebas" . InfoQ.
↑ Xi, Hongwei (1998). Tipos dependientes en programación práctica (PhD). Departamento de Ciencias Matemáticas, Universidad Carnegie Mellon. CiteSeerX 10.1.1.41.548 . Xi, Hongwei; Pfenning, Frank (1999). «Tipos dependientes en la programación práctica». Actas del 26.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM. págs. 214–227 . CiteSeerX 10.1.1.69.2042 . doi : 10.1145/292540.292560 . ISBN 1581130953. S2CID 245490 .
↑ Visual Basic es un ejemplo de un lenguaje que es seguro tanto en cuanto a tipos como a memoria.
↑ "4.2.2 La variante estricta de ECMAScript" . Especificación del lenguaje ECMAScript® 2020 (11.ª ed.). ECMA. Junio de 2020. ECMA-262.
↑ "Modo estricto – JavaScript" . MDN . Developer.mozilla.org. 3 de julio de 2013. Consultado el 17 de julio de 2013 .
↑ "Modo estricto (JavaScript)" . MSDN . Microsoft . Consultado el 17 de julio de 2013 .
↑ "Tipado estricto" . Manual de PHP: Referencia del lenguaje: Funciones .
1 2 Bracha, G. "Tipos conectables" (PDF) .
↑ "Claro. Se llama "tipado gradual" y yo lo calificaría de moderno..." ¿ Existe algún lenguaje que permita tanto el tipado estático como el dinámico? stackoverflow. 2012.
1 2 3 Kopylov, Alexei (2003). "Intersección dependiente: una nueva forma de definir registros en la teoría de tipos". 18º Simposio IEEE sobre Lógica en Ciencias de la Computación . LICS 2003. IEEE Computer Society. pp. 86– 95. CiteSeerX 10.1.1.89.4223 . doi : 10.1109/LICS.2003.1210048 .
↑ Mitchell, John C.; Plotkin, Gordon D. (julio de 1988). "Los tipos abstractos tienen tipo existencial" (PDF) . ACM Trans. Program. Lang. Syst . 10 (3): 470– 502. doi : 10.1145/44501.45065 . S2CID 1222153 .
1 2 Siek, Jeremy (24 de marzo de 2014). "¿Qué es la mecanografía gradual?" .
↑ Siek, Jeremy; Taha, Walid (septiembre de 2006). Tipado gradual para lenguajes funcionales (PDF) . Scheme y programación funcional 2006. Universidad de Chicago . págs. 81–92 .
^ Barendregt, Henk; Dekkers, Wil; Statman, Richard (20 de junio de 2013). Cálculo Lambda con tipos . Prensa de la Universidad de Cambridge. pag. 66.ISBN 978-0-521-76614-2.
↑ "8.2.4 Unificación del sistema de tipos". Especificación del lenguaje C# (5.ª ed.). ECMA. Diciembre de 2017. ECMA-334.
↑ "Tipos nativos" . Documentación de Perl 6 .
↑ "Numéricos, § Auto-boxing" . Documentación de Perl 6 .

Lecturas adicionales

Cardelli, Luca ; Wegner, Peter (diciembre de 1985). "Sobre la comprensión de los tipos, la abstracción de datos y el polimorfismo" (PDF) . ACM Computing Surveys . 17 (4): 471– 523. CiteSeerX 10.1.1.117.695 . doi : 10.1145/6041.6042 . S2CID 2921816 .
Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press. ISBN 978-0-262-16209-8.
Cardelli, Luca (2004). «Sistemas de tipos» (PDF) . En Allen B. Tucker (ed.). CRC Handbook of Computer Science and Engineering (2.ª ed.). CRC Press. ISBN 978-1584883609.
Tratt, Laurence (julio de 2009). «5. Lenguajes de tipado dinámico» . Advances in Computers . Vol. 77. Elsevier. pp. 149–184 . doi : 10.1016/S0065-2458(09)01205-4 . ISBN 978-0-12-374812-6.

Enlaces externos

Contenido multimedia relacionado con sistemas de tipos en Wikimedia Commons
"Qué debes saber antes de debatir sobre sistemas de tipos"

[26] También conocido como tipo de producto dependiente , ya que ${\textstyle (x:\sigma )\to \tau =\prod _{x:\sigma }\tau }$ .

[27] También conocido como tipo de suma dependiente , ya que ${\textstyle (x:\sigma )\times \tau =\sum _{x:\sigma }\tau }$ .

[Burroughs-4] La línea de computadoras ALGOL de Burroughs determinaba el contenido de una ubicación de memoria mediante sus bits de bandera. Los bits de bandera especifican el contenido de una ubicación de memoria. Las instrucciones, el tipo de datos y las funciones se especifican mediante un código de 3 bits, además de su contenido de 48 bits. Solo el MCP (Programa de Control Maestro) podía escribir en los bits del código de bandera.

[leakyCondition-8] Por ejemplo, una abstracción con fugas podría surgir durante el desarrollo, lo que podría mostrar que se necesita más desarrollo de tipos. —"La evaluación de un programa bien tipado siempre termina".—B. Nordström, K. Petersson y JM Smith^{[ 5 ]} Un cambio sistemático en las variables para evitar la captura de una variable libre puede introducir un error , en un lenguaje de programación funcional donde las funciones son ciudadanos de primera clase.^{[ 6 ]} —Del artículo sobre cálculo lambda .

[FOOTNOTEPierce20021-1] Pierce 2002 , p. 1: "Un sistema de tipos es un método sintáctico manejable para probar la ausencia de ciertos comportamientos de un programa clasificando las frases según los tipos de valores que calculan."

[FOOTNOTECardelli20041-2] Cardelli 2004 , p. 1: "El propósito fundamental de un sistema de tipos es prevenir la aparición de errores de ejecución durante la ejecución de un programa."

[FOOTNOTEPierce2002208-3] Pierce 2002 , pág. 208.

[Sethi1997-5] 1 2 Sethi, R. (1996). Lenguajes de programación: conceptos y construcciones (2.ª ed.). Addison-Wesley. pág. 142. ISBN 978-0-201-59065-4OCLC 604732680

[hlcs-6] Nordström, B.; Petersson, K.; Smith, JM (2001). "Teoría de tipos de Martin-Löf" . Estructuras algebraicas y lógicas . Manual de lógica en informática. Vol. 5. Oxford University Press. pág. 2. ISBN 978-0-19-154627-3.

[tfp12-7] Turner, DA (12 de junio de 2012). "Algo de historia de los lenguajes de programación funcional" (PDF) . Conferencia invitada en TFP12, en la Universidad de St Andrews . Véase la sección sobre Algol 60.

[9] "... cualquier sistema de tipos sólido y decidible debe ser incompleto" —D. Remy (2017). pág. 29, Remy, Didier. "Sistemas de tipos para lenguajes de programación" (PDF) . Archivado del original (PDF) el 14 de noviembre de 2017. Recuperado el 26 de mayo de 2013 .

[FOOTNOTEPierce2002-10] Pierce 2002 .

[Skeet-11] 1 2 3 Skeet, Jon (2019). C# en profundidad (4.ª ed.). Manning. ISBN 978-1617294532.

[12] Miglani, Gaurav (2018). "Despacho dinámico de métodos o polimorfismo en tiempo de ejecución en Java" . Archivado del original el 7 de diciembre de 2020. Consultado el 28 de marzo de 2021 .

[13] Wright, Andrew K. (1995). Practical Soft Typing (PhD). Rice University. hdl : 1911/16900 .

[14] "dinámico (Referencia de C#)" . Biblioteca MSDN . Microsoft . Consultado el 14 de enero de 2014 .

[15] "std::any — Rust" . doc.rust-lang.org . Consultado el 7 de julio de 2021 .

[16] Meijer, Erik; Drayton, Peter. "Tipado estático cuando sea posible, tipado dinámico cuando sea necesario: el fin de la guerra fría entre los lenguajes de programación" (PDF) . Microsoft Corporation.

[17] Laucher, Amanda; Snively, Paul (2012). "Tipos vs. Pruebas" . InfoQ.

[18] Xi, Hongwei (1998). Tipos dependientes en programación práctica (PhD). Departamento de Ciencias Matemáticas, Universidad Carnegie Mellon. CiteSeerX 10.1.1.41.548 . Xi, Hongwei; Pfenning, Frank (1999). «Tipos dependientes en la programación práctica». Actas del 26.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM. págs. 214–227 . CiteSeerX 10.1.1.69.2042 . doi : 10.1145/292540.292560 . ISBN 1581130953. S2CID 245490 .

[19] Visual Basic es un ejemplo de un lenguaje que es seguro tanto en cuanto a tipos como a memoria.

[20] "4.2.2 La variante estricta de ECMAScript" . Especificación del lenguaje ECMAScript® 2020 (11.ª ed.). ECMA. Junio de 2020. ECMA-262.

[21] "Modo estricto – JavaScript" . MDN . Developer.mozilla.org. 3 de julio de 2013. Consultado el 17 de julio de 2013 .

[22] "Modo estricto (JavaScript)" . MSDN . Microsoft . Consultado el 17 de julio de 2013 .

[23] "Tipado estricto" . Manual de PHP: Referencia del lenguaje: Funciones .

[Bracha-24] 1 2 Bracha, G. "Tipos conectables" (PDF) .

[25] "Claro. Se llama "tipado gradual" y yo lo calificaría de moderno..." ¿ Existe algún lenguaje que permita tanto el tipado estático como el dinámico? stackoverflow. 2012.

[K03-28] 1 2 3 Kopylov, Alexei (2003). "Intersección dependiente: una nueva forma de definir registros en la teoría de tipos". 18º Simposio IEEE sobre Lógica en Ciencias de la Computación . LICS 2003. IEEE Computer Society. pp. 86– 95. CiteSeerX 10.1.1.89.4223 . doi : 10.1109/LICS.2003.1210048 .

[29] Mitchell, John C.; Plotkin, Gordon D. (julio de 1988). "Los tipos abstractos tienen tipo existencial" (PDF) . ACM Trans. Program. Lang. Syst . 10 (3): 470– 502. doi : 10.1145/44501.45065 . S2CID 1222153 .

[siek-30] 1 2 Siek, Jeremy (24 de marzo de 2014). "¿Qué es la mecanografía gradual?" .

[siekTaha-31] Siek, Jeremy; Taha, Walid (septiembre de 2006). Tipado gradual para lenguajes funcionales (PDF) . Scheme y programación funcional 2006. Universidad de Chicago . págs. 81–92 .

[32] Barendregt, Henk; Dekkers, Wil; Statman, Richard (20 de junio de 2013). Cálculo Lambda con tipos . Prensa de la Universidad de Cambridge. pag. 66.ISBN 978-0-521-76614-2.

[33] "8.2.4 Unificación del sistema de tipos". Especificación del lenguaje C# (5.ª ed.). ECMA. Diciembre de 2017. ECMA-334.

[34] "Tipos nativos" . Documentación de Perl 6 .

[35] "Numéricos, § Auto-boxing" . Documentación de Perl 6 .

[ 1 ]

[ 2 ]

[ 3 ]

[ nota 1 ]

[ 4 ]

[ nota 2 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[

[ 14 ]

[ 15 ]

[

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[

[ 22 ]

[ 23 ]

[ 25 ]

[ 26 ]

[ 27 ]

[ 28 ]

[ 29 ]

[ 30 ]

[ 31 ]

[ 5 ]

[ 6 ]