Nivel 5 · El cubo-λ

λ2: polimorfismo

El cálculo lambda simplemente tipado garantiza que los cálculos terminan, pero paga un precio de expresividad. Para escribir la función identidad hay que dar una versión para $\texttt{nat}$ , $\lambda x{:}\texttt{nat}.\,x$ , otra para $\texttt{bool}$ , $\lambda x{:}\texttt{bool}.\,x$ , y así sucesivamente. Los detalles que se perdieron fueron las funciones genéricas o polimórficas, que operan sobre una familia entera de tipos. Todo el material de este módulo sigue a Nederpelt y Geuvers (2014) .

El Sistema $\lambda 2$ (también conocido como Cálculo Lambda Polimórfico o Sistema $F$ ) garantiza que los términos dependan de los tipos. En resumen, el propósito de $\lambda 2$ es extender los conceptos de abstracción y aplicación: en $\lambda\rightarrow$ operan solamente sobre términos, mientras que ahora operan también sobre tipos, con dos construcciones nuevas.

Abstracción de tipos: se crea un nuevo tipo de función, $\Lambda \alpha{:}*.\, M$ , que toma un tipo $\alpha$ como argumento y devuelve un término $M$ . Se usa la mayúscula $\Lambda$ para distinguirla visualmente de la abstracción de términos $\lambda$ .
Aplicación de tipos: se puede tomar una de estas funciones polimórficas y aplicarla a un tipo concreto $\sigma$ , escribiendo $M\,\sigma$ .

Ejemplo 8.1 (La identidad genérica)

En $\lambda 2$ se puede capturar la identidad en un único término polimórfico:

\mathrm{Id} \equiv \Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x.

Este término $\mathrm{Id}$ es una función que primero espera un tipo ( $\alpha$ ) y, cuando lo recibe, devuelve la función identidad para ese tipo específico.

$\texttt{nat}$ : si se quiere la identidad para números naturales, se aplica $\mathrm{Id}$ al tipo $\texttt{nat}$ . La $\beta$ -reducción de segundo orden da el resultado esperado: $\mathrm{Id}\ \texttt{nat} \equiv (\Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x)\ \texttt{nat} \rightarrow_\beta \lambda x{:}\texttt{nat}.\, x.$ Por lo tanto, se tiene la identidad para naturales a partir del término genérico.
Tipos funcionales: la generalidad de $\mathrm{Id}$ va más allá. Si se necesita una identidad para funciones de tipo $\texttt{nat} \rightarrow \texttt{bool}$ , el proceso es idéntico: $\mathrm{Id}\ (\texttt{nat} \rightarrow \texttt{bool}) \equiv (\Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x)\ (\texttt{nat} \rightarrow \texttt{bool}) \rightarrow_\beta \lambda x{:}(\texttt{nat} \rightarrow \texttt{bool}).\, x.$

En general, eso es lo que busca el polimorfismo: con una sola definición se captura un patrón infinito.

Los tipos Π

Ahora bien, cuando se intenta asignar un tipo a la identidad polimórfica se topa con un problema. Dado que $\lambda x{:}\alpha.\, x$ tiene tipo $\alpha \rightarrow \alpha$ , una primera conjetura para el tipo de $\mathrm{Id} \equiv \Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x$ podría ser:

\text{tipo tentativo: } * \rightarrow (\alpha \rightarrow \alpha),

donde $*$ representa el «tipo de todos los tipos». Pero aplicando la $\alpha$ -equivalencia, donde los nombres de las variables ligadas no importan, se tendría:

\Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x \quad =_\alpha \quad \Lambda \beta{:}*.\, \lambda x{:}\beta.\, x.

Si se usara el tipo tentativo, sus tipos serían:

\Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x : * \rightarrow (\alpha \rightarrow \alpha), \qquad \Lambda \beta{:}*.\, \lambda x{:}\beta.\, x : * \rightarrow (\beta \rightarrow \beta).

Dos términos idénticos tendrían tipos diferentes; por definición de la $\alpha$ -equivalencia, esto no es posible. La variable de tipo ( $\alpha$ o $\beta$ ) debería estar ligada en el término y en el tipo.

Para resolver esta inconsistencia se introduce el conector de tipo producto cuantificado universalmente o tipo $\Pi$ . En lugar de la flecha simple se escribe:

\Pi \alpha{:}*.\, (\alpha \rightarrow \alpha).

Este tipo representa a las funciones que, para todo tipo $\alpha$ , devuelven un término de tipo $\alpha \rightarrow \alpha$ . La variable $\alpha$ está ahora ligada por el cuantificador $\Pi$ , resolviendo el problema. Ahora se puede asignar un tipo único a la identidad polimórfica:

(\Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x) : (\Pi \alpha{:}*.\, \alpha \rightarrow \alpha).

Por la ligadura de $\Pi$ , la $\alpha$ -equivalencia se preserva como se debe:

\Pi \alpha{:}*.\, (\alpha \rightarrow \alpha) \quad =_\alpha \quad \Pi \beta{:}*.\, (\beta \rightarrow \beta).

El sistema formal λ2

Con la intuición y la maquinaria de los tipos $\Pi$ establecidas, se puede definir formalmente el Sistema $\lambda 2$ .

Definición 8.2 (Sintaxis de tipos y términos en λ2)

Usando notación gramatical, como en el módulo del cálculo lambda, se tiene:

El conjunto de tipos, $\mathbb{T}2$ , se extiende para incluir los tipos $\Pi$ : $\mathbb{T}2 = \mathbb{V} \mid (\mathbb{T}2 \rightarrow \mathbb{T}2) \mid (\Pi\, \mathbb{V}{:}*.\, \mathbb{T}2),$ donde $\mathbb{V}$ es el conjunto de las variables de tipo: $\alpha, \beta, \gamma$ , etc.
El conjunto de términos pre-tipados, $\Lambda_{\mathbb{T}2}$ , se extiende para incluir abstracción y aplicación de tipos: $\Lambda_{\mathbb{T}2} = V \mid (\Lambda_{\mathbb{T}2}\, \Lambda_{\mathbb{T}2}) \mid (\Lambda_{\mathbb{T}2}\, \mathbb{T}2) \mid (\lambda V{:}\mathbb{T}2.\, \Lambda_{\mathbb{T}2}) \mid (\Lambda\, \mathbb{V}{:}*.\, \Lambda_{\mathbb{T}2}).$

Nota 8.3 (Contextos de λ2)

Las reglas de derivación de $\lambda 2$ son las mismas de $\lambda\rightarrow$ más tres nuevas reglas: una de formación de tipos y dos para manejar la abstracción y aplicación de tipos, que se detallan a continuación. Los contextos de $\lambda 2$ se amplían en consecuencia: además de declaraciones de variables de término $x : A$ con $A \in \mathbb{T}2$ , admiten declaraciones de variables de tipo $\alpha : *$ , y toda variable de tipo debe declararse antes de su primer uso.

Definición 8.4 (Reglas de derivación clave de λ2)

(abstracción $_2$ ) Si, asumiendo que $\alpha$ es un tipo, se puede demostrar que el término $M$ tiene tipo $A$ , entonces se concluye que $\Lambda \alpha{:}*.\, M$ tiene tipo $\Pi \alpha{:}*.\, A$ :

\frac{\Gamma,\ \alpha : * \vdash M : A}{\Gamma \vdash \Lambda \alpha{:}*.\, M : \Pi \alpha{:}*.\, A}.

(aplicación $_2$ ) Si se tiene un término polimórfico $M$ de tipo $\Pi \alpha{:}*.\, A$ y un tipo bien formado $B$ , se puede aplicar $M$ a $B$ . El tipo resultante es $A$ , pero con todas las ocurrencias de $\alpha$ reemplazadas por $B$ :

\frac{\Gamma \vdash M : (\Pi \alpha{:}*.\, A) \qquad \Gamma \vdash B : *}{\Gamma \vdash M\, B : A[\alpha := B]}.

(formación) $\Gamma \vdash B : *$ si $B \in \mathbb{T}2$ y todas las variables de tipo libres de $B$ están declaradas en $\Gamma$ . Esta regla es la que deriva la segunda premisa de (aplicación $_2$ ) para tipos compuestos como $\alpha \to \alpha$ o $\texttt{nat} \to \texttt{bool}$ .

Las reglas (variable), (aplicación) y (abstracción) de $\lambda\rightarrow$ se mantienen sin cambios.

Ejemplo 8.5 (Derivación formal de la identidad polimórfica)

Demostrar el juicio:

\vdash (\Lambda \alpha.\, \lambda x{:}\alpha.\, x) : (\Pi \alpha{:}*.\, \alpha \rightarrow \alpha).

Demostración.

A probar:

El objetivo es derivar el cuerpo más interno de la expresión, que es la variable $x$ . Para esto se asume un contexto $\Gamma_1$ donde tanto el tipo $\alpha$ como la variable $x$ con dicho tipo están declarados. Sea $\Gamma_1 = \{\alpha{:}*,\ x{:}\alpha\}$ . Se aplica la regla (variable), ya que la condición $(x{:}\alpha)$ es un miembro del contexto $\Gamma_1$ : $\alpha{:}*,\ x{:}\alpha \vdash x : \alpha \quad (1)$
El objetivo es demostrar $\alpha{:}* \vdash \lambda x{:}\alpha.\, x : \alpha \to \alpha$ . Usando el juicio (1) como premisa, se aplica la regla de (abstracción). La regla abstrae la variable de término $x$ , elimina $x{:}\alpha$ del contexto y construye un tipo flecha ( $\to$ ): $\frac{ \overbrace{\alpha{:}*,\ x{:}\alpha \vdash x : \alpha}^{\text{premisa, del juicio (1)}} }{ \underbrace{\alpha{:}*}_{\text{contexto resultante}} \vdash \underbrace{\lambda x{:}\alpha}_{\text{abstracción}} .\, \underbrace{x}_{\text{cuerpo}} : \underbrace{\alpha \to \alpha}_{\text{tipo construido}} } \quad (2)$
Para demostrar el juicio original se usa el juicio (2) como premisa y se aplica la regla de abstracción de tipo, denotada (abst $_2$ ). Esta regla abstrae la variable de tipo $\alpha$ , elimina $\alpha{:}*$ del contexto y construye un tipo universal (cuantificado) $\Pi$ : $\frac{ \overbrace{\alpha{:}* \vdash \lambda x{:}\alpha.\, x : \alpha \to \alpha}^{\text{premisa, del juicio (2)}} }{ \underbrace{\varnothing}_{\text{contexto final}} \vdash \underbrace{\Lambda \alpha{:}*}_{\text{abstracción}} .\, \underbrace{(\lambda x{:}\alpha.\, x)}_{\text{cuerpo}} : \underbrace{\Pi \alpha{:}*.\,(\alpha \to \alpha)}_{\text{tipo final}} }$

En resumen, se tiene el siguiente árbol de derivación:

(x{:}\alpha) \in \{\alpha{:}*,\ x{:}\alpha\}

(variable)

\alpha{:}*,\ x{:}\alpha \vdash x : \alpha

(abstracción)

\alpha{:}* \vdash \lambda x{:}\alpha.\, x \;:\; \alpha \to \alpha

(abst₂)

\vdash \Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x \;:\; \Pi \alpha{:}*.\,(\alpha \to \alpha)

Ejemplo en Lean: la identidad polimórfica

La parte teórica de la identidad polimórfica, $\mathrm{Id} \equiv \Lambda \alpha{:}*.\, \lambda x{:}\alpha.\, x$ , puede ser bastante abstracta. Sin embargo, usando Lean la implementación es directa y permite manipular las expresiones como en un lenguaje de programación. La sintaxis {α : Type} introduce una variable de tipo implícita, equivalente a la abstracción de tipo $\Lambda \alpha$ .

def identidad_polimorfica {α : Type} (x : α) : α := x

Se comprueba el tipo que Lean le asigna:

#check identidad_polimorfica
-- identidad_polimorfica {α : Type} (x : α) : α

Unos ejemplos rápidos de uso; se utilizan los -- para mostrar los resultados:

#eval identidad_polimorfica 42      -- 42
#eval identidad_polimorfica true    -- true
#eval identidad_polimorfica "hola"  -- "hola"

En resumen, Lean permite el polimorfismo porque la función se adapta al argumento. Esto muestra cómo se puede reutilizar código, usando definiciones anteriores y exhibiendo la utilidad del polimorfismo. El Sistema $\lambda 2$ hereda las mismas propiedades de $\lambda\rightarrow$ , incluyendo la confluencia (Church–Rosser) y la normalización fuerte para términos bien tipados, lo que garantiza que cualquier cómputo polimórfico bien formado terminará. La $\beta$ -reducción se extiende incluyendo la aplicación de tipos: $(\Lambda \alpha{:}*.\, M)\, T \rightarrow_\beta M[\alpha := T]$ . La propiedad de la reducción del sujeto también se mantiene: si un término tiene un cierto tipo, cualquier término al que se reduzca también tendrá ese mismo tipo. Los detalles y demostraciones se pueden encontrar en Nederpelt y Geuvers (2014) .

Con $\lambda 2$ los términos dependen de los tipos. La página siguiente añade la dependencia opuesta dentro del mundo de los tipos: operadores que construyen tipos a partir de otros tipos.