La correspondencia Curry-Howard: cuando los tipos se convierten en demostraciones

En la serie Hacer los estados invalidos irrepresentables 1. Por que los flags booleanos son bugs disfrazados, vimos que los tipos suma (enums) codifican los estados del dominio con precisión, mientras que los flags booleanos crean explosiones exponenciales de valores sin sentido. Pero hay una razón más profunda por la que esto funciona, y viene de un teorema descubierto décadas antes de que existieran Rust, TypeScript o incluso Java.

Los tipos son proposiciones. Los programas son demostraciones.

#

La correspondencia Curry-Howard, descubierta por Haskell Curry (1934) y William Alvin Howard (1969), establece un mapeo directo entre la lógica y la teoría de tipos:

No es una analogía vaga. Es un isomorfismo: cada enunciado a la izquierda tiene una contraparte precisa a la derecha, y viceversa.

Qué significa esto en la práctica

#

Cuando escribes una definición de tipo, estás enunciando una proposición. Cuando construyes un valor de ese tipo, estás proporcionando una demostración.

Considera este enum:

enum Light {
    Red,
    Green,
    Yellow,
}

La proposición: “Un semáforo está en exactamente uno de tres estados: Red, Green o Yellow.”

Cada vez que creas un Light::Red, estás construyendo una demostración de que la proposición se cumple. El compilador verifica esta demostración en cada lugar de uso mediante pattern matching exhaustivo: si haces match sobre un Light y olvidas Yellow, la demostración está incompleta, y el compilador la rechaza.

Ahora compara con booleanos:

struct Light {
    is_red: bool,
    is_green: bool,
    is_yellow: bool,
}

La proposición: “Un semáforo tiene alguna combinación de flags rojo, verde y amarillo.” Es una afirmación mucho más débil. No dice nada sobre exclusividad. La “demostración” (cualquier valor de este tipo) incluye Light { is_red: true, is_green: true, is_yellow: false }, que demuestra una proposición que es verdadera en el sistema de tipos pero falsa en la realidad.

El tipo función como implicación

#

Una función A -> B corresponde a la implicación lógica “si A entonces B”. Una función que transforma un tipo en otro es una demostración de que la primera proposición implica la segunda.

fn ship_order(order: PaidOrder) -> ShippedOrder {
    // ...
}

Esta función es una demostración de la proposición: “Si un pedido está pagado, entonces puede ser enviado.” El sistema de tipos garantiza que no puedes llamar a esta función con un CancelledOrder. La implicación se cumple por construcción.

Si la función tomara un struct con flags booleanos, la proposición sería: “Dada alguna combinación de flags booleanos, obtienes alguna otra combinación.” Eso no demuestra casi nada sobre tu dominio.

Por qué importa ! (Never)

#

El tipo vacío ! en Rust (o Void en Haskell) tiene cero valores. Bajo Curry-Howard, corresponde a Falso: una proposición sin demostración. No puedes construir un valor de tipo ! porque no hay demostración de Falso.

Por eso las expresiones match con ! no requieren brazos: si un valor no puede existir, no hay nada que manejar. El compilador de Rust lo entiende:

fn absurd(x: !) -> String {
    match x {
        // Sin brazos necesarios -- x no puede existir
    }
}

Una función de ! a cualquier cosa es siempre válida (vacuamente verdadera: “si Falso entonces cualquier cosa” es un teorema en lógica). Esto se conoce como el principio ex falso quodlibet.

Correcto por construcción

#

En métodos formales, correcto por construcción significa construir un sistema de tal forma que los comportamientos inválidos sean estructuralmente imposibles, en vez de construirlo y verificarlo después.

Hacer los estados inválidos irrepresentables es la manifestación a nivel de tipos de este principio. En vez de escribir el código y después testear que los estados imposibles nunca ocurren, diseñas los tipos de modo que los estados imposibles no puedan expresarse desde el principio.

Hay una jerarquía de cuánta garantía obtienes:

La mayoría del software en producción opera en los niveles 3 y 4. Pasar del nivel 4 al nivel 3, de comprobaciones en runtime a particionado de tipos en compilación, es la mejora con mayor palanca que puedes hacer en seguridad de tipos. Es gratis en runtime, no requiere herramientas externas, y funciona en todo lenguaje con tipos suma.

Tipos refinamiento: el siguiente paso hacia arriba

#

Los tipos refinamiento llevan predicados: {x: Int | x > 0} describe un entero positivo. Lenguajes como Liquid Haskell y F* los soportan directamente. El compilador no solo comprueba que tienes un Int, sino que verifica que el predicado se cumple.

Los tipos suma aproximan los tipos refinamiento a una granularidad más gruesa. En vez de predicados arbitrarios, particionan el dominio en casos finitos con nombre. Un enum con cinco variantes no es tan preciso como un tipo refinamiento con un predicado arbitrario, pero es infinitamente más preciso que un producto de booleanos.

La idea práctica: no necesitas tipos dependientes ni demostradores de teoremas formales para obtener la mayor parte del beneficio. El salto de “bolsa de booleanos” a “enum bien elegido” elimina clases enteras de bugs, y todo lenguaje mainstream lo soporta hoy.

La conclusión

#

La correspondencia Curry-Howard nos dice que la relación entre tipos y corrección no es una metáfora vaga. Los tipos son proposiciones. Los programas son demostraciones. Cuando eliges un tipo suma sobre un producto de booleanos, estás haciendo una afirmación lógica más fuerte sobre tu dominio, y el compilador demuestra esa afirmación en cada build.

Correcto por construcción no es solo un eslogan. Es una práctica de diseño: elige tipos que hagan lo imposible inexpresable, y deja que el compilador haga la verificación gratis.