Preámbulo · Lean desde cero

fun: la función anónima

En el cuaderno, definir una función lleva dos actos: se le da un nombre y se da su regla. «Sea $f \colon \mathbb{N} \to \mathbb{N}$ definida por $f(x) = x + 1$ ». Lean separa los dos actos, y el segundo puede existir sin el primero. Esta es la expresión más importante de todo el lenguaje:

fun (x : Nat) => x + 1

Se lee: «la función que a cada natural $x$ le asigna $x + 1$ ». Es exactamente el objeto $x \mapsto x + 1$ de la notación matemática moderna: la regla, sin bautizo. La palabra fun abre la definición, el paréntesis (x : Nat) introduce la variable con su tipo (los dos puntos de la página anterior), y la flecha => separa la variable del cuerpo.

¿Y su tipo? Toda expresión tiene uno, así que preguntemos:

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

El tipo es Nat → Nat. La flecha que el matemático escribe en « $f \colon \mathbb{N} \to \mathbb{N}$ » no es decoración: es un tipo en sí misma, el tipo de las funciones de Nat en Nat. Igual que 2 + 2 habita en Nat, la función anónima habita en Nat → Nat. Guarda esta flecha: reaparecerá en un lugar inesperado en la página 5.

Aplicar: yuxtaposición, sin paréntesis

Para aplicar la función a un argumento basta escribirlos juntos:

#eval (fun (x : Nat) => x + 1) 41   -- 42

Obsérvese lo que no hay: paréntesis alrededor del argumento. Donde el cuaderno escribe $f(41)$ , Lean escribe f 41. La aplicación es por yuxtaposición: función, espacio, argumento. Los paréntesis que sí aparecen agrupan la función anónima completa, para que Lean no lea 41 como parte del cuerpo. Al evaluar, Lean sustituye x por 41 en el cuerpo y calcula 41 + 1. Esa sustitución es el único motor de cómputo del cálculo lambda , el sistema de los años treinta del que fun desciende en línea directa.

Por qué hace falta la anotación

¿Qué pasa si se omite el tipo de la variable? Considérese la función identidad, la más inocente de todas:

fun x => x

¿La identidad de qué? ¿De Nat? ¿De Bool? ¿De Nat → Nat? Nada en la expresión lo determina, y Lean no adivina: responde el error failed to infer binder type («no pude inferir el tipo de la variable»). Hay dos remedios. El primero, anotar la variable, como se ha hecho hasta ahora. El segundo es la ascripción de la página 1, declarando el tipo de la expresión completa:

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

Con el tipo Nat → Nat declarado por fuera, Lean deduce que x tiene que ser Nat y ya no pide la anotación. Es la promesa cumplida de la página anterior: «sea $f \colon \mathbb{N} \to \mathbb{N}$ » primero, la fórmula después.

Nota (Cuándo adivina Lean)

El Lean completo tiene convenciones que a veces le permiten inferir el tipo sin ayuda: los literales numéricos, por ejemplo, se leen como Nat por defecto, así que fun x => x + 1 a secas puede pasar. Pero son convenciones, no magia: con fun x => x no hay literal que oriente y el error aparece igual. El laboratorio de esta página es más estricto y pide siempre la anotación o la ascripción; es el hábito correcto para leer la tesis.

Ponerle nombre: def

Cuando la función merece nombre, la orden def se lo da. Hay dos estilos, y conviene reconocer ambos porque la tesis usa los dos:

def sucesor := fun (x : Nat) => x + 1

def sucesor (x : Nat) : Nat := x + 1

El primero dice: «sucesor es un nombre para esta expresión fun». El segundo mueve la variable a la izquierda y anota el tipo del resultado; es azúcar sintáctico para exactamente la misma función anónima. Tras cualquiera de los dos, sucesor 41 evalúa a 42. El nombre es pura conveniencia: el objeto matemático es la expresión fun.

Pruébalo

Los tres presets recorren la página: la función anónima, su aplicación a 41, y un intento de aplicarla a true. Este último falla, y vale la pena leer el error con calma: Lean juzga el tipo antes de calcular, así que rechaza true donde esperaba un Nat sin ejecutar nada. Es la misma disciplina de la resta truncada, ahora protegiendo funciones.

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) => x + 1 es la función $x \mapsto x + 1$ : una regla sin nombre, y una expresión como cualquier otra.
Su tipo es Nat → Nat: la flecha de « $f \colon \mathbb{N} \to \mathbb{N}$ » es un tipo.
Se aplica por yuxtaposición: f 41, no $f(41)$ .
Si Lean no puede inferir el tipo de la variable, se anota (x : Nat) o se usa la ascripción (fun x => x + 1 : Nat → Nat).
def da nombre a una expresión; los dos estilos de def definen el mismo objeto.

Queda una pregunta natural: esta fun toma una variable. ¿Y las funciones de dos variables, como la suma? La respuesta de Lean es más elegante que añadir sintaxis nueva, y tiene nombre propio: currificación. Es la página siguiente.