En los lenguajes de programación , un sistema de tipos es un sistema lógico que comprende un conjunto de reglas que asigna una propiedad llamada tipo a las diversas construcciones de un programa informático , como variables , expresiones , funciones o módulos . [1] Estos tipos formalizan y refuerzan las categorías implícitas que el programador usa para tipos de datos algebraicos , estructuras de datos u otros componentes (por ejemplo, "cadena", "matriz de flotante", "función que devuelve booleanos"). El objetivo principal de un sistema de tipos es reducir las posibilidades de errores.en programas de computadora [2] definiendo interfaces entre diferentes partes de un programa de computadora, y luego verificando que las partes se hayan conectado de manera consistente. Esta verificación puede ocurrir de forma estática (en tiempo de compilación ), dinámicamente (en tiempo de ejecución ) o como una combinación de ambos. Los sistemas de tipos también tienen otros propósitos, como expresar reglas comerciales, habilitar ciertas optimizaciones del compilador , permitir el envío múltiple , proporcionar una forma de documentación, etc.
Un sistema de tipos asocia un tipo con cada valor calculado y, al examinar el flujo de estos valores, intenta asegurar o probar que no pueden ocurrir errores de tipo . El sistema de tipos dado en cuestión determina qué constituye un error de tipo, pero en general, el objetivo es evitar que las operaciones que esperan cierto tipo de valor se utilicen con valores para los que esa operación no tiene sentido (errores de validez). Los sistemas de tipos a menudo se especifican como parte de los lenguajes de programación y se incorporan a los intérpretes y compiladores, aunque el sistema de tipos de un lenguaje se puede ampliar mediante herramientas opcionales que realizan comprobaciones adicionales utilizando la sintaxis y la gramática de tipos originales del lenguaje.
Un ejemplo de un sistema de tipo simple es la de la lengua C . Las partes de un programa en C son las definiciones de funciones . Una función es invocada por otra función. La interfaz de una función indica el nombre de la función y una lista de parámetros que se pasan al código de la función. El código de una función de invocación establece el nombre de la invocación, junto con los nombres de las variables que contienen valores para pasarle. Durante la ejecución, los valores se colocan en un almacenamiento temporal, luego 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 con el supuesto de recibir un valor entero , pero el código de llamada pasó unvalor de punto flotante , la función invocada calculará el resultado incorrecto. El compilador de C verifica los tipos de argumentos pasados a una función cuando se llama con los tipos de parámetros declarados en la definición de la función. Si los tipos no coinciden, el compilador arroja un error en tiempo de compilación.
Un compilador también puede usar el tipo estático de un valor para optimizar el almacenamiento que necesita y la elección de algoritmos para las operaciones sobre el valor. En muchos compiladores de C, el tipo de datos flotantes , por ejemplo, se representa en 32 bits , de acuerdo con la especificación IEEE para números de coma flotante de precisión simple . Por lo tanto, utilizarán operaciones de microprocesador específicas de punto flotante en esos valores (suma, multiplicación, etc. de punto flotante).
La profundidad de las restricciones de tipo y la forma de su evaluación afectan la mecanografía del idioma. Un lenguaje de programación puede asociar además una operación con varias resoluciones para cada tipo, en el caso de polimorfismo de tipo . La teoría de tipos es el estudio de sistemas de tipos. Los tipos concretos de algunos lenguajes de programación, como los números enteros y las cadenas, dependen de cuestiones prácticas de la arquitectura de la computadora, la implementación del compilador y el diseño del lenguaje.
Formalmente, la teoría de tipos estudia los sistemas de tipos. Un lenguaje de programación debe tener la oportunidad de verificar el tipo 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]