Haskell en cinco puntos: elección incondicional mediante parametricidad

Fuentes: "Five-Point Haskell": Unconditional Election (via Parametricity)

Justin Le publica la segunda entrega de su serie «Five-Point Haskell», centrada en el principio que bautiza como «elección incondicional». La idea aprovecha la parametricidad de Haskell: cuando una función tiene un tipo polimórfico como forall a. a -> a, el compilador deduce propiedades que toda implementación respetará, sin necesidad de anotaciones, pruebas ni restricciones explícitas. Por ejemplo, una función forall a. a -> a solo puede devolver el mismo valor que recibe, y una forall a. a -> String debe devolver una cadena constante, pues no puede inspeccionar su argumento.

El artículo contrasta este comportamiento con el de lenguajes como Java o TypeScript, donde una función (A) -> A podría devolver cualquier cosa —incluido negar un entero— porque no existe parametricidad. Le explica que añadir restricciones mediante typeclasses (como Show a => a -> String) no rompe el principio: acota qué información del valor se puede usar, pero las propiedades que quedan fuera del typeclass siguen siendo inaccesibles para la función.

A partir de ahí, el autor propone un juego mental: dada una signatura polimórfica, deducir qué puede y qué no puede hacer una función. Plantea ejercicios con listas y continuaciones, mostrando cómo se obtienen los llamados «teoremas libres», relaciones que toda implementación debe cumplir —por ejemplo, que mapear una función antes o después de ciertas operaciones polimórficas produce el mismo resultado. Estos teoremas funcionan como una demostración gratis de correctitud estructural.

Le cierra la entrega recordando que Haskell puede usarse como probador de teoremas: la signatura actúa como proposición y la implementación como prueba. Aunque no profundiza ahí, sienta las bases para futuras entregas donde explorará usos prácticos más allá de la verificación formal.