Preámbulo · Lean desde cero

Varias variables: currificación

La suma toma dos números. En el cuaderno se escribe $f \colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ , $f(x, y) = x + y$ : una función cuyo dominio es un producto cartesiano. Lean no necesita el producto. Escribe la suma con dos binders seguidos:

#check fun (x : Nat) (y : Nat) => x + y
-- fun x y => x + y : Nat → Nat → Nat

El tipo es Nat → Nat → Nat, y la clave está en cómo se lee. La flecha asocia a la derecha: Nat → Nat → Nat significa Nat → (Nat → Nat). Es decir: una función que recibe un Nat y devuelve… otra función, de tipo Nat → Nat. La «función de dos variables» es en realidad una función de una variable cuyo valor es una función de una variable.

La observación matemática detrás es una biyección: dar una función $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ es exactamente lo mismo que dar una función $\mathbb{N} \to (\mathbb{N} \to \mathbb{N})$ . A cada $f(x, y)$ le corresponde la función que a cada $x$ le asigna la función $y \mapsto f(x, y)$ , y viceversa. El paso de la primera forma a la segunda se llama currificación, por el lógico Haskell Curry, y Lean vive permanentemente del lado currificado: no hay funciones de dos argumentos, solo funciones que devuelven funciones.

Aplicación parcial

Si la suma es Nat → (Nat → Nat), entonces dársela a un solo argumento es perfectamente legal:

#check (fun (x : Nat) (y : Nat) => x + y) 2   -- : Nat → Nat

El resultado es la función $y \mapsto 2 + y$ , «sumar dos». Es un valor legítimo, pero al pedirle #eval el laboratorio responde con un mensaje que conviene entender: el resultado es una función, y una función no tiene representación imprimible. El Lean real da el mismo aviso (could not synthesize a Repr instance): puede tener la función, pero no sabe mostrarla como muestra un 4. No es un error de tipos; el #check funciona sin queja. Aplíquese a un segundo argumento y vuelve a haber un número.

Nombres locales y decisiones

Dos piezas más de sintaxis, ambas expresiones con valor. La primera, let, da un nombre local dentro de una expresión:

#eval let doble := fun (x : Nat) => x * 2; doble (doble 3)   -- 12

Se lee «sea doble la función que duplica; calcúlese doble (doble 3)». Es el «sea» del cuaderno, con alcance limitado a la expresión que sigue.

La segunda, if … then … else, decide entre dos valores:

#eval if 2 ≤ 3 then 10 else 20   -- 10

En Lean el if no es una instrucción sino una expresión: tiene tipo y valor, como todo. Y eso impone una condición que un lenguaje sin tipos no pediría: las dos ramas deben tener el mismo tipo, porque la expresión completa necesita un tipo antes de saberse qué rama gana. Un if que devuelve 10 o true según el caso no tiene tipo posible, y Lean lo rechaza.

Ejemplo (Funciones que reciben funciones)

Si las funciones son valores, nada impide que sean argumentos. Esta expresión recibe una función f y la aplica dos veces al cero:

#check fun (f : Nat → Nat) => f (f 0)   -- : (Nat → Nat) → Nat

Nótese el tipo: (Nat → Nat) → Nat, con paréntesis obligatorios a la izquierda, porque no es lo mismo que Nat → Nat → Nat (la asociación por defecto va a la derecha). Para el matemático esto no es exótico: los operadores, como $\frac{d}{dx}$ o la integral definida, son exactamente esto, funciones cuyos argumentos son funciones. En Lean son ciudadanos de primera clase desde la primera página.

Pruébalo

Los presets: la aplicación parcial (léase el mensaje de #eval con calma), el let con doble, y el if como expresión.

Laboratorio Lean

Un Lean en miniatura: cada expresión pasa por el mismo ciclo que en el asistente real, primero el tipo (#check), después el valor (#eval).

#checkNat → Nat

#evalEl resultado es una función y no tiene representación imprimible. Lean da el mismo error: «could not synthesize a Repr instance». Aplícala a un argumento para obtener un valor.

Lo que ya sabes

fun (x : Nat) (y : Nat) => x + y tiene tipo Nat → Nat → Nat, que se lee Nat → (Nat → Nat): la flecha asocia a la derecha.
Currificar es usar la biyección entre $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ y $\mathbb{N} \to (\mathbb{N} \to \mathbb{N})$ ; Lean vive del lado currificado.
Aplicar a un solo argumento produce una función (aplicación parcial); #eval no puede imprimirla, pero #check la acepta.
let nombra localmente; if … then … else es una expresión y sus dos ramas comparten tipo.
Las funciones pueden ser argumentos: (Nat → Nat) → Nat es el tipo de un operador.

Hasta aquí, todos los tipos vienen dados de fábrica: Nat, Bool y las flechas entre ellos. La página siguiente muestra de dónde salen: en Lean los tipos se declaran, constructor por constructor, y los axiomas de Peano caben en tres líneas.