Nivel 5 · El cubo-λ

λω̲: constructores de tipos

Con $\lambda 2$ se tiene la capacidad de que los términos dependan de los tipos, dando el mecanismo del polimorfismo. Ahora bien, no se tiene forma de crear constructores de tipos genéricos, como un tipo lista List que pueda ser aplicado a nat para crear la lista de los naturales List nat. Para lograr esto se necesita que los tipos puedan depender de otros tipos. Esta es la siguiente abstracción que será necesario deducir.

Este es el sentido del Sistema $\lambda\underline{\omega}$: introduce una nueva jerarquía que permite definir operadores que transforman tipos en otros tipos. La presentación sigue a Nederpelt y Geuvers (2014) .

La jerarquía de kinds: los tipos de los tipos

Si los términos tienen tipos, ¿qué tienen los tipos? La respuesta en $\lambda\underline{\omega}$ es que los tipos tienen kinds. Los kinds son los «tipos de los tipos», que permiten clasificar los tipos y los constructores de tipos. La jerarquía es la siguiente:

1. El kind $*$: es el kind de todos los tipos que pueden ser habitados por términos. Por ejemplo, $\texttt{nat}$, $\texttt{bool}$ y $\texttt{nat} \rightarrow \texttt{nat}$ son todos de kind $*$: $$\texttt{nat} : *, \qquad (\texttt{nat} \rightarrow \texttt{nat}) : *.$$
2. Kinds funcionales (por ejemplo $* \to *$): es el kind de los constructores de tipos que toman un tipo (de kind $*$) y devuelven otro tipo (de kind $*$). Un constructor que toma un tipo $\alpha$ y devuelve el tipo de las funciones de $\alpha$ a $\alpha$ sería $T := \lambda \alpha{:}*.\, (\alpha \rightarrow \alpha)$: $$(\lambda \alpha{:}*.\, \alpha \rightarrow \alpha) : (* \rightarrow *).$$ De igual manera, un constructor como $\texttt{Pair}$ (el constructor de tipo producto, que toma dos tipos $A$ y $B$ y genera el tipo producto $A \times B$, cuyos términos son pares ordenados $(a, b)$ con $a : A$ y $b : B$) tendría el kind $* \rightarrow * \rightarrow *$.
3. El sort $\square$: así como los términos tienen tipos y los tipos tienen kinds, los kinds también deben tener un súper tipo que los clasifique. Este nivel superior es el súper tipo $\square$: $$* : \square, \qquad (* \rightarrow *) : \square.$$

En general, la jerarquía (términos : tipos : kinds : $\square$) es la que da a $\lambda\underline{\omega}$ su estructura. Esta jerarquía tiene una conexión directa con Lean: usando #check, Lean revela el tipo de cualquier construcción, permitiendo verla en acción.

1. Tipos de kind $*$. En la teoría, $\texttt{nat}$ y $\texttt{bool}$ son tipos habitados por términos y por lo tanto tienen kind $*$. En Lean, el kind $*$ se representa como Type:

   -- Se pide a Lean el "tipo" del tipo Nat
   #check Nat  -- Lean responde: Nat : Type
   
   -- Lo mismo para tipos funcionales
   #check Nat -> Bool  -- Lean responde: Nat -> Bool : Type

   Esto confirma que Nat y Nat -> Bool son, en el lenguaje de Lean, de tipo Type (el análogo a $*$).

2. Constructores de tipos de kind $* \to *$. En la teoría, List tendría el kind $* \to *$. Para que Lean muestre esta versión simplificada (ignorando niveles superiores), se le pide que verifique a List como si fuera un Type -> Type:

   -- Se le pide a Lean que considere a List como un constructor de Nivel 0.
   #check (List : Type -> Type)
   -- Lean responde: List : Type -> Type

   La respuesta Type -> Type es la notación de Lean para el kind $* \to *$. Cuando se le da un argumento (como Nat), produce un nuevo tipo habitable:

   -- Aplicamos el constructor List al tipo Nat
   #check List Nat  -- Lean responde: List Nat : Type

   De esta forma, List : Type -> Type toma Nat : Type y devuelve List Nat : Type.

3. El súper tipo $\square$ y los universos de Lean. Finalmente, si los tipos tienen Type como su «tipo», ¿cuál es el «tipo» de Type? Aquí es donde Lean implementa el concepto de $\square$ a través de una jerarquía de universos, para evitar paradojas lógicas:

   -- ¿Cuál es el "tipo" de "Type"?
   #check Type    -- Lean responde: Type : Type 1
   #check Type 1  -- Lean responde: Type 1 : Type 2
   -- y así sucesivamente...

   Type 1 es el análogo en Lean del súper tipo $\square$ para Type (que en este contexto es $*$). Esta jerarquía (Type : Type 1 : Type 2 ...) es la manera en que los asistentes de pruebas implementan los niveles de los «tipos de tipos».

Constructores y niveles

Reglas fundamentales de derivación

La regla de variable, por sí sola, no permite derivar juicios como

Este juicio es intuitivamente válido: si se sabe que $\alpha$ es un tipo en un contexto, debería seguir siéndolo si se añaden más suposiciones.

Una derivación trabajada

Las derivaciones en $\lambda\underline{\omega}$ suelen incluir pasos que, aunque necesarios para la formalidad, son obvios o repetitivos, como aplicaciones de (sort), (variable) y (debilitamiento). Se adoptan derivaciones abreviadas para omitir estos pasos y destacar las aplicaciones esenciales de reglas como (abstracción), (aplicación) y (conversión).

Regla de conversión

Ahora bien, en Lean se pueden definir constructores de tipos propios, como el ejemplo teórico $T := \lambda \alpha{:}*.\, (\alpha \rightarrow \alpha)$, y verificar su tipo:

-- Definimos un constructor que toma un tipo T y devuelve el tipo T -> T
def mapeo_interno (T : Type) : Type := T -> T

-- Verificamos su "kind"
#check mapeo_interno  -- Lean responde: mapeo_interno : Type -> Type

La regla de (conversión) dice que tipos equivalentes son intercambiables. Con #reduce, que en Lean sirve para hacer todas las reducciones posibles a un término, se ve que mapeo_interno Nat es equivalente a Nat -> Nat:

-- ¿A qué es equivalente mapeo_interno Nat?
#reduce mapeo_interno Nat  -- Lean muestra el resultado: Nat -> Nat

Resumen del sistema de reglas de λω̲

Las reglas de derivación en $\lambda\underline{\omega}$ generalizan las de sistemas anteriores para operar en todos los niveles de la jerarquía.

Esta tabla resume el sistema $\lambda\underline{\omega}$. Como se puede observar, las reglas de abstracción y formación utilizan exclusivamente el conector no dependiente $\rightarrow$, lo que distingue a $\lambda\underline{\omega}$ de otros sistemas más expresivos del cubo lambda.

Con el Sistema $\lambda\underline{\omega}$ se añade la posibilidad de crear operadores que manipulan y construyen tipos. Combinado con $\lambda 2$, da un sistema, $\lambda\omega$ (sin subrayado), con polimorfismo y constructores de tipos. Es la base de muchos lenguajes de programación funcional avanzados: por ejemplo, el lenguaje Haskell se apoya en una extensión de este sistema para su sistema de tipos (Hudak et al., 2007) .

Quedan cubiertas dos de las tres dependencias nuevas. La página siguiente introduce la tercera y más importante para la matemática: tipos que dependen de términos.