Alef: un cálculo de efectos algebraicos con tipado bidireccional

Abstract

El modelado de efectos computacionales mediante teorías matemáticas es un instrumento fundamental para facilitar el razonamiento sobre programas y poder garantizar su correctitud. Uno de estos modelos es el basado en la teoría de efectos algebraicos, que representa los efectos mediante operaciones de una teoría algebraica que captura su comportamiento. Para incorporar este modelo al diseño de lenguajes de programación se introducen los sistemas de efectos, que extienden los sistemas de tipos con información acerca de los efectos que pueden ser causados por un programa. Sin embargo, las implementaciones de estos sistemas suelen ser muy complejas, perdiendo en gran medida la claridad conceptual provista por los fundamentos teóricos. En esta tesina se describe un sistema de efectos implementable para un cálculo básico con efectos algebraicos y handlers, usando una nueva variación del tipado bidireccional para preservar la claridad y la estrecha relación con la teoría matemática subyacente. Este sistema se prueba seguro respecto a la semántica operacional y se lo implementa en Haskell, mostrando tanto la simplicidad de su formulación como su gran poder expresivo.