Desarrollo de records extensibles en lenguajes con tipos dependientes

Abstract

Los records extensibles son estructuras de datos que permiten asociar valores de distintos tipos a etiquetas para poder ser accedidos mediante ellas, al igual que permiten extender esa estructura con nuevos campos de forma dinámica. Existen varias soluciones de records extensibles en varios lenguajes, sean como primitivas de lenguaje o como bibliotecas de usuario, cada una con sus ventajas y desventajas. Una de ellas es la biblioteca HList de Haskell, que utiliza listas heterogéneas para definir tales records. En este trabajo se presentará una solución de records extensibles en un lenguaje fuertemente tipado con tipos dependientes llamado Idris, basándose en la biblioteca HList. Este trabajo explorará las propiedades de los tipos dependientes y el desarrollo en Idris, y demostrará que es posible realizar una implementación de records extensibles en base a ellos, con resultados interesantes. Se presentarán los beneficios de esta solución en el contexto de un lenguaje de expresiones aritméticas definido como un embedded Domain Specific Language en Idris.