Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Fri 28 Aug 2020 12:52 - 13:14 at HIW - Session 3

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.

In the recent months, we have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are: First, there is just a single invocation necessary per Haskell source file, so the workflow becomes easier. Second, we can integrate with GHC and Cabal to support libraries and packages properly. 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 talk, we present the Liquid Haskell plugin workflow and why we think it is superior to the old approach. We 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. We explain the final design, and some of the iterations we needed to get there.

Fri 28 Aug

Displayed time zone: Eastern Time (US & Canada) change

12:30 - 13:30
Session 3HIW at HIW
12:30
22m
Talk
Exactprint in GHC
HIW
12:52
22m
Talk
Liquid Haskell as a GHC Plugin
HIW
Alfredo Di Napoli Well-Typed LLP, Ranjit Jhala University of California at San Diego, USA, Andres Löh Well-Typed LLP, Niki Vazou IMDEA Software Institute
13:14
22m
Talk
Stan — Haskell Static Analyser
HIW
Dmitrii Kovanikov Standard Chartered, Veronika Romashkina None