Alef: un cálculo de efectos algebraicos con tipado bidireccional
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 operacion...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | bachelorThesis Tésis de Grado acceptedVersion |
| Lenguaje: | Español |
| Publicado: |
2020
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/2133/19077 http://hdl.handle.net/2133/19077 |
| Aporte de: |
| Sumario: | 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. |
|---|