Un sistema de tipos es un conjunto de reglas en lenguajes de programación que asignan propiedades, llamadas tipos , a las diversas construcciones que componen un programa , como variables , expresiones , funciones o módulos . La función principal del sistema de tipos es reducir el número de errores en los programas [1] definiendo interfaces entre diferentes partes del programa y luego verificando la consistencia de la interacción de estas partes. Esta verificación puede ocurrir estáticamente ( en tiempo de compilación ) o dinámicamente ( en tiempo de ejecución) y también ser una combinación de ambos.
Según Pierce , el sistema de tipos es un método sintáctico decidible para probar la ausencia de ciertos comportamientos del programa mediante la clasificación de construcciones según los tipos de valores calculados [2] .
Un ejemplo de un sistema de tipo simple se puede ver en el lenguaje C. Las partes de un programa en C se escriben como definiciones de función . Las funciones se llaman entre sí. La interfaz de una función especifica el nombre de la función y una lista de valores que se pasan a su cuerpo. La función que llama postula el nombre de la función que quiere llamar y los nombres de las variables que contienen los valores que quiere pasar. Durante la ejecución del programa, los valores se colocan en el almacenamiento temporal y luego la ejecución se pasa al cuerpo de la función llamada. El código de función llamado accede y utiliza los valores. Si las instrucciones en el cuerpo de una función se escriben asumiendo que se les debe pasar un valor entero para su procesamiento, pero el código de llamada pasó un número de coma flotante, entonces la función llamada evaluará el resultado incorrecto. El compilador de C compara los tipos definidos para cada variable pasada con los tipos definidos para cada variable en la interfaz de la función llamada. Si los tipos no coinciden, el compilador genera un error en tiempo de compilación.
Técnicamente, el sistema de tipos asigna un tipo a cada valor calculado y luego, al realizar un seguimiento de la secuencia de esos cálculos, intenta verificar o demostrar que no hay errores de coincidencia de tipos . El sistema de tipo específico puede determinar qué causa un error, pero generalmente el objetivo es evitar que las operaciones que asumen ciertas propiedades de sus parámetros reciban parámetros para los que esas operaciones no tienen sentido, lo que evita errores lógicos . Además, también previene errores de dirección de memoria .
Los sistemas de tipos generalmente se definen como parte de los lenguajes de programación y se integran en sus intérpretes y compiladores. Sin embargo, el sistema de tipos del idioma se puede ampliar con herramientas especiales que realizan comprobaciones adicionales basadas en la sintaxis de escritura original en el idioma.
El compilador también puede usar un tipo de valor estático para optimizar el almacenamiento y elegir una implementación algorítmica de operaciones en ese valor. Por ejemplo, en muchos compiladores de C , un tipo float está representado por 32 bits, de acuerdo con la especificación IEEE para operaciones de punto flotante de precisión simple . En base a esto, se utilizará un conjunto especial de instrucciones de microprocesador para valores de este tipo (suma, multiplicación y otras operaciones).
El número de restricciones impuestas a los tipos y cómo se calculan determinan la tipificación del idioma. Además, en el caso del polimorfismo de tipo , el lenguaje también puede especificar para cada tipo el funcionamiento de diversos algoritmos específicos. El estudio de los sistemas de tipos es la teoría de los tipos , aunque en la práctica un sistema de tipos particular de un lenguaje de programación se basa en las características de la arquitectura de la computadora, la implementación del compilador y la imagen general del lenguaje.
La justificación formal de los sistemas de tipos es la teoría de tipos . Un lenguaje de programación incluye un sistema de tipos para realizar la verificación de tipos en tiempo de compilación o en tiempo de ejecución , lo que requiere declaraciones de tipo explícitas o inferirlas por sí mismo. Mark Manasse formuló el problema de la siguiente manera [3] :
El principal problema que resuelve la teoría de tipos es asegurarse de que los programas tengan sentido. El principal problema con la teoría de tipos es que los programas significativos pueden no comportarse según lo previsto. La consecuencia de esta tensión es la búsqueda de sistemas tipográficos más potentes.
Texto original (inglés)[ mostrarocultar] El problema fundamental que aborda una teoría de tipos es garantizar que los programas tengan significado. La causa fundamental de una teoría de tipos es que los programas significativos pueden no tener significados problemáticos atribuidos a ellos. La búsqueda de sistemas de tipos más ricos resulta de esta tensión. —Mark Massey [3]La operación de asignación de tipo, llamada tipeo, otorga significado a cadenas de bits , como un valor en la memoria de la computadora , u objetos , como una variable . La computadora no tiene forma de distinguir, por ejemplo, una dirección en la memoria de una instrucción de código , o un carácter de un número entero o de punto flotante , ya que las cadenas de bits que representan estos diferentes significados no tienen características obvias que permitan hacer suposiciones sobre su significado. La asignación de bits de tipo a cadenas proporciona esta inteligibilidad, convirtiendo así el hardware programable en un sistema de caracteres que consiste en ese hardware y software.
El proceso de verificación y restricción de tipos (verificación de tipos o verificación de tipos) se puede realizar en tiempo de compilación tipado estático) o en tiempo de ejecución (tipado dinámico). También son posibles soluciones intermedias (cf. tipificación secuencial ).
Si la especificación del idioma requiere que las reglas de tipeo se implementen estrictamente (es decir, permitir en un grado u otro solo aquellas conversiones automáticas de tipo que no pierdan información), dicho lenguaje se denomina fuertemente tipado ; ), de lo contrario, débilmente tipado . Estos términos son condicionales y no se utilizan en justificaciones formales.
Un lenguaje se denomina tipificado si la especificación de cada operación define los tipos de datos a los que se puede aplicar esta operación, lo que implica su inaplicabilidad a otros tipos [4] . Por ejemplo, el dato que representa " este texto entrecomillado " es del tipo " строка". En la mayoría de los lenguajes de programación, dividir un número por una cadena no tiene sentido, y la mayoría de los lenguajes modernos rechazarán un programa que intente realizar tal operación. En algunos lenguajes, una operación sin sentido será detectada durante la compilación ( tipado estático ), y el compilador la rechazará. En otros, se detectará en tiempo de ejecución ( tipado dinámico ), lanzando una excepción .
Un caso especial de los lenguajes tipificados son los lenguajes de un solo tipo ( ing. single-type language ), es decir, los lenguajes con un solo tipo. Suelen ser lenguajes de scripting o marcado , como REXX y SGML , cuyo único tipo de datos es la cadena de caracteres, que se utiliza para representar datos numéricos y de caracteres.
Los lenguajes no tipificados, a diferencia de los tipificados, le permiten realizar cualquier operación sobre cualquier dato, que en ellos están representados por cadenas de bits de longitud arbitraria [4] . La mayoría de los lenguajes ensambladores no están tipificados . Ejemplos de lenguajes sin tipo de alto nivel son BCPL , BLISS , Forth , Refal .
En la práctica, pocos lenguajes pueden considerarse tipificados en términos de teoría de tipos (permitiendo o rechazando todas las operaciones), la mayoría de los lenguajes modernos ofrecen solo cierto grado de tipificación [4] . Muchos lenguajes industriales brindan la capacidad de eludir o romper el sistema de tipos, intercambiando la seguridad de tipos por un control más preciso sobre la ejecución del programa ( juego de palabras ).
El término "polimorfismo" se refiere a la capacidad del código para ejecutarse en valores de muchos tipos diferentes, o la capacidad de diferentes instancias de la misma estructura de datos para contener elementos de diferentes tipos. Algunos sistemas de tipos permiten el polimorfismo para mejorar potencialmente la reutilización del código : en lenguajes con polimorfismo, los programadores solo necesitan implementar estructuras de datos como una lista o una matriz asociativa una vez, y no necesitan desarrollar una implementación para cada tipo de elemento que planean almacenar estructuras. Por esta razón, algunos informáticos a veces se refieren al uso de ciertas formas de polimorfismo como " programación genérica ". Las justificaciones del polimorfismo desde el punto de vista de la teoría de tipos son prácticamente las mismas que para la abstracción , la modularidad y, en algunos casos , la subtipificación de datos .
Se han desarrollado varios tipos de sistemas especiales para usar bajo ciertas condiciones con ciertos datos, así como para el análisis estático de programas. En su mayor parte, se basan en las ideas de la teoría de tipo formal y se usan solo como parte de los sistemas de investigación.
Los tipos existenciales, es decir, los tipos definidos por un cuantificador existencial (existence quantifier) , son un mecanismo de encapsulación a nivel de tipo : es un tipo compuesto que oculta la implementación de algún tipo en su composición.
El concepto de tipo existencial se usa a menudo junto con el concepto de tipo de registro para representar módulos y tipos de datos abstractos , debido a su propósito de separar la implementación de la interfaz. Por ejemplo, un tipo T = ∃X { a: X; f: (X → int); }describe una interfaz de módulo (familias de módulos con la misma firma) que tiene un valor de datos del tipo Xy una función que toma un parámetro exactamente del mismo tipo Xy devuelve un número entero. La implementación puede ser diferente:
Ambos tipos son subtipos del tipo existencial más general Ty corresponden a tipos implementados concretamente, por lo que cualquier valor que pertenezca a cualquiera de ellos también pertenece al tipo T. Si t es un valor de tipo T, t.f(t.a)pasa la verificación de tipos, independientemente del tipo abstracto al que pertenezca X. Esto da flexibilidad para elegir los tipos que son apropiados para una implementación particular, ya que los usuarios externos solo acceden a los valores del tipo interfaz (existencial) y están aislados de estas variaciones.
En general, el verificador de consistencia de tipos no puede determinar a qué tipo existencial pertenece un módulo determinado. En el ejemplo anterior intT { a: int; f: (int → int); }, también podría tener tipo ∃X { a: X; f: (int → int); }. La solución más simple es especificar explícitamente para cada módulo el tipo implícito en él, por ejemplo:
Aunque los tipos y módulos de datos abstractos se han utilizado en los lenguajes de programación durante mucho tiempo, no se construyó un modelo formal de tipos existenciales hasta 1988 [5] . La teoría es un cálculo lambda tipado de segundo orden similar al Sistema F , pero con cuantificación existencial en lugar de cuantificación universal .
Los tipos existenciales están explícitamente disponibles como una extensión experimental del lenguaje Haskell , donde son una sintaxis especial que le permite usar una variable de tipo en una definición de tipo algebraica sin moverla a la firma de un constructor de tipos , es decir, sin aumentar su aridad [ 6] . El lenguaje Java proporciona una forma limitada de tipos existenciales a través del comodín . En los lenguajes que implementan el polimorfismo let clásico al estilo ML , los tipos existenciales se pueden simular por medio de los llamados " valores indexados por tipo " [7] .
Muchos sistemas de tipo estático, como los de C y Java, requieren una declaración de tipo : el programador debe asignar explícitamente un tipo específico a cada variable. Otros, como el sistema de tipos Hindley-Milner utilizado en ML y Haskell , hacen inferencia de tipos : el compilador infiere los tipos de variables en función de cómo el programador usa esas variables.
Por ejemplo, para una función f(x,y)que realiza sumas xy y, el compilador podría inferir que xy ydeben ser números, ya que la operación de suma se define solo para números. Por lo tanto, llamar a una función en algún lugar del programa fpara parámetros que no sean numéricos (por ejemplo, para una cadena o una lista) indica un error.
Las constantes y expresiones numéricas y de cadena suelen expresar un tipo en un contexto particular. Por ejemplo, una expresión 3.14puede significar un número real , mientras que [1,2,3]puede ser una lista de números enteros, generalmente una matriz .
En términos generales, la inferencia de tipos es posible si es fundamentalmente decidible en la teoría de tipos. Además, incluso si la inferencia es indecidible para una teoría de tipo dada, la inferencia es a menudo posible para muchos programas reales. El sistema de tipos de Haskell , que es una variación del sistema de tipos de Hindley-Milner , es una restricción del sistema Fω a los llamados tipos polimórficos de primer rango en los que se puede decidir la inferencia. Muchos compiladores de Haskell proporcionan polimorfismo de rango arbitrario como una extensión, pero esto hace que la inferencia de tipo sea indecidible, por lo que se requiere una declaración de tipo explícita. Sin embargo, la comprobación de la coherencia de tipos sigue siendo decidible, y para los programas con polimorfismo de primer orden, los tipos siguen siendo derivables.
Algunos lenguajes, como C# , tienen un sistema de tipos unificado [8] . Esto significa que todos los tipos del lenguaje, hasta los primitivos , se heredan de un único objeto raíz (en el caso de C#, de la clase Object). Java tiene varios tipos primitivos que no son objetos. Junto con estos, Java también proporciona tipos de objetos de contenedor para que el desarrollador pueda usar los tipos primitivos o de objetos como mejor le parezca.
El mecanismo de verificación de consistencia de tipo en un lenguaje tipificado estáticamente verifica que cualquier expresión se ajuste al tipo esperado por el contexto en el que ocurre. Por ejemplo, en una instrucción de asignación de tipo, el tipo deducido de la expresión debe coincidir con el tipo declarado o deducido de la variable . La notación de conformidad, llamada compatibilidad , es específica de cada idioma. x := eex
Si ey xson del mismo tipo, y se permite la asignación para ese tipo, entonces la expresión es legal. Por lo tanto, en los sistemas de tipos más simples, la cuestión de la compatibilidad de dos tipos se simplifica a la cuestión de su igualdad ( equivalencia ). Sin embargo, diferentes idiomas tienen diferentes criterios para determinar la compatibilidad de tipos de dos expresiones. Estas teorías de la equivalencia varían entre dos extremos: los sistemas de tipo estructural , en los que dos tipos son equivalentes si describen la misma estructura interna de un valor; y sistemas de tipos nominativos , en los que tipos sintácticamente diferentes nunca son equivalentes ( es decir, dos tipos son iguales solo si sus identificadores son iguales) .
En idiomas con subtipos , las reglas de compatibilidad son más complejas. Por ejemplo, si Aes un subtipo de B, entonces Ase puede usar un valor de tipo en un contexto que espera un valor de tipo B, incluso si lo contrario no es cierto. Al igual que con la equivalencia, las relaciones de subtipos varían según los idiomas y son posibles muchas variaciones de las reglas. La presencia de polimorfismo paramétrico o situacional en un lenguaje también puede afectar la compatibilidad de tipos.
Algunos programadores prefieren los sistemas de tipo estático , otros prefieren los dinámicos . Los lenguajes tipificados estáticamente señalan errores de consistencia de tipo en tiempo de compilación , pueden generar código ejecutable de manera más eficiente y, para tales lenguajes, es factible una finalización más relevante en IDE . Los defensores de la tipificación dinámica argumentan que son más adecuados para la creación rápida de prototipos y que los errores de coincidencia de tipos son solo una pequeña fracción de los errores potenciales en los programas [9] [10] . Por otro lado, en los lenguajes tipificados estáticamente, la declaración de tipo explícita generalmente no se requiere si el lenguaje admite la inferencia de tipos , y algunos lenguajes tipificados dinámicamente realizan optimizaciones en tiempo de ejecución [11] [12] , a menudo mediante el uso de tipo parcial inferencia [13] .
| Tipos de datos | |
|---|---|
| Ininterpretable | |
| Numérico | |
| Texto | |
| Referencia | |
| Compuesto | |
| resumen |
|
| Otro | |
| Temas relacionados | |