Formalización de mónadas concurrentes en Agda: un análisis del caso de la mónada Delay

En los últimos años, la concurrencia ha cobrado mucha importancia en el mundo de la programación, sobre todo debido a la masificación de los procesadores con múltiples núcleos. Los lenguajes de programación funcional, en general, proveen la capacidad de concurrencia mediante funciones ad-hoc, y no mediante primitivas bien fundadas del lenguaje. En este trabajo se presenta una formalización del concepto de mónada concurrente en el lenguaje y asistente de pruebas Agda, así como también otras formalizaciones de conceptos previos como las mónadas, los funtores monoidales y los monoides concurrentes. Luego se analiza el caso particular de la mónada delay, con el objetivo de probar o refutar que esta puede dotarse de una estructura de mónada concurrente. La principal dificultad que se encontró a la hora de realizar esta prueba es la demostración de la ley de intercambio. Se buscó entonces una simplificación del problema y se demostró que los números conaturales forman un monoide concurrente, obteniendo luego una mónada concurrente alternativa a delay: la mónada writer con los conaturales como monoide.