bachelorThesis
Alef: un cálculo de efectos algebraicos con tipado bidireccional
Autor
Locascio, Antonio
Institución
Resumen
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. Locascio, Antonio. Universidad Nacional de Rosario. Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Departamento de Ciencias de la Computación, Argentina