Lógica con Contenido Computacional

Durante la sesión de hoy vimos un poco sobre cómo podemos agregar contenido computacional a las pruebas en el nivel de tipos.

Para esto utilizamos la correspondencia Curry-Howard, desarrollando funciones y haciendo uso de algunos tipos de datos básicos en Haskell.

Material

Durante la sesión utilicé un Notebook de Jupyter para escribir y compilar el contenido de Haskell.

Puedes descargar el notebook para ejecutarlo en tu propia instancia de iHaskell en el siguiente enlace: Sesion4.ipynb.

O puedes visualizar el material con los resultados ya ejecutados en: Notebook en Línea

Referencias

Utilicé este contenido como referencia para preparar el material.

• Propositions as Types por Philip Wadler
• Type Logic in Haskell
• Propositions as Types for Beginners in Haskell por Stephen Pimentel en LambdaConf 2018.