Nivel 2 · Tipos simples (λ→)

Tipado à la Church y à la Curry

El tipado de $\lambda$-términos comienza asignando tipos a las variables. Existen dos enfoques principales, y la diferencia entre ellos organiza buena parte de la teoría de tipos :

1. Tipado à la Church (explícito): se prescribe un tipo único para cada variable al momento de su introducción. Los tipos de los términos más complejos se deducen considerando las restricciones de tipado.
2. Tipado à la Curry (implícito): no se asignan tipos explícitos a las variables; en su lugar, se busca inferir los tipos mediante un proceso de deducción y conjeturas.

Para comparar ambos estilos, la tesis tipa dos veces el mismo término,

una función constante de dos argumentos aplicada al resultado de $y\,x$. El contraste entre los dos resultados finales es el contenido real de esta página.

À la Church: tipos escritos a mano

El propósito es derivar, paso a paso, el tipo del término $M$ utilizando las reglas de tipado à la Church.

1. Declaraciones iniciales. Se indican los tipos conocidos de las variables libres: $$x : \alpha \rightarrow \alpha, \qquad y : (\alpha \rightarrow \alpha) \rightarrow \beta .$$
2. Aplicación parcial $y\, x$. La variable $y$ espera un argumento de tipo $\alpha \rightarrow \alpha$ y $x$ posee exactamente ese tipo, por lo que la aplicación es válida: $$y\, x : \beta .$$
3. Construcción de una función constante de dos argumentos. Se introducen dos nuevas variables para ilustrar una función que ignora su segundo argumento: $$z : \beta, \qquad u : \gamma ,$$ y se define el término $$\lambda z\, u .\, z \;:\; \beta \rightarrow \gamma \rightarrow \beta \;=\; \beta \rightarrow (\gamma \rightarrow \beta).$$
4. Aplicación total. Al aplicar la función constante al resultado del paso 2 se obtiene: $$(\lambda z\, u .\, z)\,(y\, x) : \gamma \rightarrow \beta .$$

Es decir, el término $(\lambda z\, u .\, z)(y\, x)$ recibe un valor de tipo $\gamma$ y devuelve uno de tipo $\beta$.

El formato explícito

En el tipado explícito, cada variable y expresión tiene un tipo declarado abiertamente. Retomando el cálculo anterior, con $z$ de tipo $\beta$ y $u$ de tipo $\gamma$, el resultado completo se escribe como un juicio (Definición 7.51):

Esta expresión se lee así: «asumiendo que la variable $x$ tiene tipo $\alpha \rightarrow \alpha$ y la variable $y$ tiene tipo $(\alpha \rightarrow \alpha) \rightarrow \beta$ (el contexto), se demuestra que el término $(\lambda z : \beta .\, \lambda u : \gamma .\, z)(y\, x)$ resulta en una función de tipo $\gamma \rightarrow \beta$». El símbolo $\vdash$ separa el contexto de la afirmación principal. Nótese también que $(\lambda z : \beta .\, \lambda u : \gamma .\, z)$ es una forma abreviada de expresar $\lambda z : \beta .\, (\lambda u : \gamma .\, (z))$; si se excluyen los tipos, sería equivalente a $\lambda z .\, \lambda u .\, z$.

À la Curry: tipos inferidos

Ahora se infieren los tipos del mismo término $M \equiv (\lambda z\, u .\, z)\,(y\, x)$ sin suponer tipos de antemano, generando y resolviendo ecuaciones.

1. Asignar tipos de variable. Se introduce un símbolo de tipo para cada variable del término (libres: $y, x$; ligadas: $z, u$), asegurando la consistencia de la aplicación $y\, x$: $$z : A, \quad u : C, \quad y : E \rightarrow F, \quad x : E .$$
2. Analizar las partes. Se analizan los dos componentes de la aplicación principal:
   • La función: el término $\lambda z\, u .\, z$ toma un argumento $z$ de tipo $A$ y devuelve una función que toma un argumento $u$ de tipo $C$ para finalmente devolver $z$. Por lo tanto, su tipo es $A \rightarrow (C \rightarrow A)$.
   • El argumento: la aplicación $y\, x$ toma la función $y : E \rightarrow F$ y el argumento $x : E$. El resultado es un término de tipo $F$.
3. Unir las partes y resolver. Al aplicar la función al argumento, $(\lambda z\, u .\, z)(y\, x)$, se genera una restricción: el tipo que la función espera como entrada ($A$) debe coincidir con el tipo del argumento que se le pasa ($F$): $$\text{Restricción: } \boxed{A = F}$$ Sabiendo esto, la aplicación de una función de tipo $A \rightarrow (C \rightarrow A)$ a un argumento de tipo $A$ produce un resultado de tipo $C \rightarrow A$. Por lo tanto: $$M : C \rightarrow A .$$
4. Instanciación concreta. Si se elige, por ejemplo, $$x : \beta, \quad y : \beta \rightarrow \alpha, \quad u : \delta$$ (donde la declaración para $z$ es implícita por la restricción), las asignaciones corresponden a $E = \beta$, $F = \alpha$ y $C = \delta$. Dado que $A = F$, se tiene $A = \alpha$. Sustituyendo en el resultado final: $$M : \delta \rightarrow \alpha .$$

El enfoque à la Curry evidencia que un mismo término puede admitir distintos tipos según las asignaciones iniciales: el mismo $M$ recibió arriba el tipo $\gamma \rightarrow \beta$ y aquí el tipo $\delta \rightarrow \alpha$.

Unicidad de tipos à la Church

Queda una pregunta de fondo: los cálculos de esta página fueron hechos a mano, pero ¿existe un algoritmo que los haga siempre, para cualquier término? La respuesta, sorprendentemente generosa, es el tema de la página siguiente.