Este artículo de Justin Le inaugura una serie en tres partes dedicada a explorar el extremo más sofisticado del sistema de tipos de Haskell. El objetivo es construir un lenguaje de expresiones tipado embebido (un EDSL) que permita especificar un programa una sola vez y reutilizarlo de varias formas: interpretarlo dentro de Haskell con seguridad de tipos, visualizar su flujo de control y compilarlo a múltiples backends como C o JavaScript, manteniendo la garantía de que la misma función se ejecuta de forma idéntica en cada implementación.
La motivación práctica es directa: el autor ha necesitado en proyectos reales definir un único grafo de programa en Haskell que sea a la vez compilable en C y JavaScript, representable como diagrama y explorable de manera interactiva. Como ejemplo conductor, plantea una máquina de estados con transiciones disparadas, especificada mediante un cálculo lambda tipado.
La primera parte se centra en sentar las bases. Comienza con una representación sin tipos del cálculo lambda como tipo de dato algebraico (ADT) y constata sus limitaciones: expresiones inválidas solo se detectan en tiempo de ejecución mediante el tipo Maybe o Either. Para superar esta restricción, Le introduce expresiones indexadas por tipos (phantom types) usando -XTypeData, -XDataKinds y un parámetro de tipo que etiqueta cada expresión con su tipo de resultado. Esto obliga al compilador GHC a rechazar combinaciones inválidas, como 1 && 2, sin necesidad de comprobaciones manuales. A continuación incorpora singletons (STy) y tipos existenciales (SomeValue) para gestionar variables ligadas y valores heterogéneos en un contenedor homogéneo. Las partes 2 y 3 abordarán, respectivamente, máquinas de estados con predicados embebidos y la compilación a distintos lenguajes con verificación de equivalencia.