Tipos intersección

¿Qué son?

Supongamos que tenemos una función con el siguiente tipo

[$$ f: A \rightarrow B \rightarrow C $$]

¿Cuál es el tipo de esta nueva función?

[$$ \lambda x. f x x $$]

Esta claro que la x tendrá que ser de tipo A y de tipo B. Si tuviéramos subtipos, y asumiendo que el tipo de x es X, diríamos

[$$ X\le A,\quad X\le B $$]

Sería tarea del motor de inferencia buscar el tipo adecuado. Por otra parte, podríamos introducir una solución tramposa. Inventarnos el tipo

[$$ X=A\cap B $$]

con las  propiedades

[$$ T\cap S \le T $$]
[$$
T\cap S \le S $$]

Ni que decir tiene que esto recuerda mucho al concepto de intersección de conjuntos, de ahí el nombre.

El sistema de Coppo-Dezani

Si introducimos las reglas usuales de una intersección (es decir, las de un ínfimo) obtenemos el sistema de Coppo-Dezani (sistema CD). Este sistema tiene unas cualidades muy interesantes.

• Cumple la reducción de sujeto. Es lo mínimo que se puede pedir a un sistema de tipos para una estrategia de evaluación por nombre: que si evaluamos en un paso nuestra expresión (sea el redex que sea), el tipo siga siendo el mismo.
• Los términos tipables son los términos fuertemente normalizables. O sea, que sólo podremos darle un tipo a los términos cuya evaluación acabe.
• Las formas normales son tipables ya que no tienen más pasos de evaluación.
• Cumple la expansión de sujeto. Esto es interesante. Si damos un paso de evaluación marcha atrás, el tipo también se mantiene.
• Estas propiedades nos llevan a la gran característica definitoria del sistema CD: Un término es tipable si y sólo si su evaluación acaba sea cual sea la estrategia de evaluación (es fuertemente normalizable).

Esta última propiedad no es buena. Y no lo es porque significa que no podemos darle un tipo a expresiones de la forma

[$$ K x y = x $$]
[$$ K\; 3\;((\lambda z. z z)(\lambda z. z z)) $$]

La función K (el combinador K) descarta su segundo parámetro, por lo que el término debería tener tipo entero (el resultado es 3). Sin embargo, no es tipable porque el segundo argumento nunca termina su evaluación. Este término no es fuertemente normalizable, es sólo normalizable de cabeza.

El sistema de Coppo-Dezani-Venneri

La solución es añadir una constante ? que significa "cualquier cosa". Sería vista como la intersección nula o como el elemento neutro de la intersección.

[$$ \omega \cap X = X $$]
[$$ X \cap \omega = X $$]

Al añadir las reglas apropiadas para introducir esta constante, los autores del sistema CDV se vieron forzados a separar los tipos en dos niveles. El nivel de tipo simple y el nivel de intersección (o secuencia) de tipos.

[$$ \tau ::= X\;\mid\;\omega\;\mid\;\sigma \rightarrow \tau $$]
[$$ \sigma ::= \tau_1 \cap \cdots \cap \tau_n\qquad (n>0) $$]

Con este sistema, las propiedad principal es que se puede asignar un tipo a los términos con forma normal de cabeza.

El sistema de Barendregt-Coppo-Dezani

El problema de los tipos restringidos del sistema CDV se soluciona introduciendo una relación de subtipo. Esto es así porque en posición covariante las intersecciones distribuyen.

[$$ A\rightarrow (B\cap C)=(A\rightarrow B)\cap(A\rightarrow C) $$]

Introduciendo una relación de subtipo que sea un preorden se puede derivar una clase de equivalencia y trabajar con el orden parcial generado en el conjunto cociente.

Este sistema es bastante más complejo. La relación de subtipo tiene hasta ocho reglas. La relación de tipado tiene seis reglas.

El sistema BCD tiene la misma potencia que el CDV. Sin embargo tiene un gran fallo: existen varias formas de demostrar que una expresión tiene un tipo. Las reglas no son dirigidas sintácticamente.

A pesar de todo esto, el sistema BCD es el más conocido y usado de los sistemas de tipos intersección.