Resultados de investigación
Los investigadores Alfredo Di Napoli, Andres Löh (ambos de Well-Typed LLP), Ranjit Jhala (Universidad de California en San Diego) y Niki Vazou, del Instituto IMDEA Software han presentado: “Liquid Haskell as a GHC Plugin” en el Haskell Implementors’ Workshop (HIW 2020) en ICFP 2020.
Liquid Haskell es un sistema que amplía el GHC con tipos de refinamiento. Las restricciones que surgen de los tipos de refinamiento se envían a un provertidor de teorema automático externo como el z3. Empleando tales comprobaciones adicionales, uno puede expresar más propiedades interesantes sobre los programas de Haskell de forma estática.
Hasta ahora, Liquid Haskell ha sido un ejecutable separado que utiliza la API del GHC, pero se ejecutaría en los archivos de Haskell individualmente y sólo diría “SAFE” o “UNSAFE”. En el caso de que el resultado fuera “SAFE”, se podría entonces proceder a compilar un programa normalmente.
Recientemente, los investigadores han reescrito Liquid Haskell para que ahora sea un plugin del GHC. Las principales ventajas de este enfoque son:
Al comprobar los archivos fuente, Liquid Haskell requiere información sobre las restricciones ya establecidas para las bibliotecas dependientes. Anteriormente, éstas tenían que ser distribuidas manualmente para los módulos seleccionados con el propio Liquid Haskell. Ahora, pasan a formar parte de los archivos normales de la interfaz GHC y pueden distribuirse para paquetes de usuario arbitrarios a través de Hackage.
En este trabajo, los investigadores presentan el flujo de trabajo de los plugins de Liquid Haskell y por qué creen que es superior al antiguo enfoque. También discuten la implementación del plugin: es interesante porque no encaja perfectamente en las categorías de plugin que se proporcionan actualmente. Moralmente, Liquid Haskell comprueba el código, pero para generar restricciones para alimentar al demostrador, debe acceder al código central (¡no optimizado!). Además, explican el diseño final, y algunas de las iteraciones que necesitaban para llegar allí.
Para conocer más detalles, puede echar un vistazo a blogs relevantes en (liquidhaskell)1 y (well-typed)2 así como unirse a (Liquid Haskell’s slack)3 para realizar preguntas y obtener ‘feedback’.
