El siguiente post es técnico y teórico.

Uno que conoce Haskell y que ha visto como funcionan los tipos tiene una intuición de la relación que existen entre las deducciones lógicas y las de los tipos. El soporte teórico que existe para corroborar estas intuiciones está dado por la denominada correspondencia (a veces denominado isomorfismo) Curry-Howard (Curry es el apellido del lógico cuyo nombre era Haskell de donde proviene el nombre del lenguaje de programación). Encontré esta joyita que hace visible la correspondencia entre la deducción lógica y la inferencia de tipos de Haskell. A lo largo del documento se construye una estructura de tipos con los cuales se puede especificar las condiciones lógicas que quieren/deben demostrarse. Por otro se pueden programar expresiones que representan la propiedad lógica que se quiere demostrar. El sistema de tipos infiere la estructura del tipo de la expresión y la contrasta con el tipo dado explícitamente para corroborar la deducción lógica.