Research Results
The researchers Alfredo Di Napoli, Andres Löh (both from Well-Typed LLP), Ranjit Jhala (University of California at San Diego) and Niki Vazou, from the IMDEA Software Institute have presented: “Liquid Haskell as a GHC Plugin” at the Haskell Implementors’ Workshop (HIW 2020) in ICFP 2020.
Liquid Haskell is a system that extends GHC with refinement types. Constraints arising from the refinement types are sent to an external automatic theorem prover such as z3. By employing such additional checks, one can express more interesting properties about Haskell programs statically.
Up until now, Liquid Haskell has been a separate executable that uses the GHC API, but would run on Haskell files individually and just say “SAFE” or “UNSAFE”. If “SAFE”, one could then proceed to compile a program normally.
Recently, the researchers have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are:
When checking source files, Liquid Haskell requires information about the constraints already established for dependent libraries. Previously, these had to be hand-distributed for selected modules with Liquid Haskell itself. Now, they become part of normal GHC interface files and can be distributed for arbitrary user packages via Hackage.
In this work, the researchers present the Liquid Haskell plugin workflow and why they think it is superior to the old approach. They also discuss the implementation of the plugin: it is interesting because it does not neatly fit into the plugin categories currently provided. Morally, Liquid Haskell typechecks the code, but in order to generate constraints to feed to the prover, it must access (unoptimised!) core code. They explain the final design, and some of the iterations they needed to get there.
For more details, check out the relevant blogs on (liquidhaskell)1 and (well-typed)2 and join (Liquid Haskell’s slack)3 for feedback and questions!
