El significado matemático del concepto de tipo en lenguajes de programación

Ponente(s): Favio Ezequiel Miranda Perea

En lenguajes de programación los tipos se usan para predecir el comportamiento de las expresiones de manera estática, es decir antes de ser evaluadas. Por ejemplo 2+x será un entero si x lo es; y también para filtrar programas o expresiones que causan errores de ejecución, como 5 + true, pues no están bien tipadas. En este ámbito se define un tipo como una colección de valores que sirve para clasificar y aproximar el valor de una expresión de manera estática, es decir, sin evaluar. De acuerdo a esta definición podría pensarse que un tipo es simplemente un conjunto. Por ejemplo, el tipo Integer corresponde al conjunto $\mathbb{Z}$ de números enteros; el tipo Bool, al conjunto de dos valores $\{true,false\}$ y el tipo $A\to B$ , al conjunto de funciones de $A$ en $B$. El propósito de esta charla es discutir por qué esta intuición es incorrecta, así como definir a los tipos como órdenes parciales con ciertas características que permiten fundamentar otros conceptos naturales en programación como la no terminación de un programa y la definición recursiva de funciones y tipos. Este trabajo se desarrolla con apoyo del proyecto UNAM-DGAPA-PAPIIT IN101723.