Sistemas de tipos
Los sistemas de tipos son disciplinas formales que clasifican las expresiones de los programas según los tipos de valores que calculan, descartando amplias clases de errores antes de que se ejecute un programa.
Definition
Un sistema de tipos es un método sintáctico manejable para probar la ausencia de ciertos comportamientos de programa mediante la clasificación de expresiones según los tipos de valores que calculan.
Scope
Esta área abarca la teoría y el diseño de los sistemas de tipos: tipado estático versus dinámico, polimorfismo paramétrico y ad hoc, subtipado, inferencia de tipos y sistemas avanzados como los tipos dependientes y subestructurales. Aborda la solidez de los tipos, la relación entre los tipos y la lógica a través de la correspondencia de Curry-Howard, y cómo las disciplinas de tipado equilibran la expresividad con las garantías y la decidibilidad.
Sub-topics
Core questions
- ¿Qué garantías proporciona un sistema de tipos y qué es la solidez de tipos?
- ¿Cómo aumentan el polimorfismo y el subtipado la expresividad sin sacrificar la seguridad?
- ¿Se pueden inferir los tipos automáticamente y cuándo es decidible la inferencia?
- ¿Hasta qué punto pueden los tipos codificar propiedades de programa ricas, hasta especificaciones completas?
Key theories
- Solidez de tipos mediante progreso y preservación
- El enfoque sintáctico de Wright y Felleisen demuestra que un sistema de tipos es sólido al establecer que los programas bien tipados no se bloquean: los tipos se preservan bajo evaluación y los términos bien tipados siempre pueden progresar.
- Tipología del polimorfismo y la abstracción
- Cardelli y Wegner organizan el espacio de los conceptos de tipado, distinguiendo el polimorfismo paramétrico y ad hoc, la inclusión (subtipado) y la abstracción de datos dentro de un marco unificado.
- La teoría de tipos como fundamento del lenguaje de programación
- Harper desarrolla una metodología uniforme de estática y dinámica en la que las características del lenguaje se definen mediante reglas de tipado y evaluación, tratando la teoría de tipos como el fundamento organizador para el diseño del lenguaje.
Clinical relevance
Los sistemas de tipos se encuentran entre los métodos formales más ampliamente implementados: detectan errores en tiempo de compilación, documentan interfaces, permiten una refactorización segura e impulsan las herramientas del editor. Avances como los genéricos, el tipado gradual y los tipos de propiedad se han incorporado directamente a los lenguajes industriales convencionales.
History
Los lenguajes tipados surgieron con sistemas tempranos como Algol y el cálculo lambda simplemente tipado. La inferencia de tipos polimórfica de Milner (1978) sustentó ML; Girard y Reynolds idearon independientemente el Sistema F para el polimorfismo paramétrico. La encuesta de Cardelli y Wegner de 1985 sistematizó el campo, y el método de progreso y preservación (1994) se convirtió en la técnica de solidez estándar que Pierce y Harper canonizaron más tarde en los libros de texto.
Debates
- Tipado estático versus dinámico
- Un debate de larga data sopesa la detección temprana de errores y la documentación del tipado estático frente a la flexibilidad y la iteración rápida del tipado dinámico, con el tipado gradual como una reconciliación.
Key figures
- Benjamin Pierce
- Robert Harper
- Luca Cardelli
- Robin Milner
- Matthias Felleisen
Related topics
Seminal works
- pierce2002
- harper2016
- cardelli1985
- wright1994
Frequently asked questions
- ¿Qué significa que un sistema de tipos sea sólido?
- La solidez significa que los programas bien tipados no pueden exhibir los errores que el sistema de tipos está diseñado para prevenir, lo que generalmente se prueba mostrando que los tipos se preservan durante la evaluación y que los programas bien tipados nunca se bloquean.
- ¿Los lenguajes de tipado dinámico tienen sistemas de tipos?
- Tienen tipos y realizan comprobaciones de tipos en tiempo de ejecución, pero carecen de un sistema de tipos estático que rechace programas mal tipados antes de la ejecución; los errores de tipo, en cambio, se manifiestan como fallos en tiempo de ejecución.