A Tutorial on Liquid Haskell
Liquid Haskell is a preprocessor for GHC (the primary Haskell compiler) that allows the programmer to equip a program with more sophisticated type annotations. An automatic external theorem prover such as Z3 is then used to prove the program type-correct with respect to these extra annotations.
The language of types supported by Liquid Haskell is based on refinement types, and allows types to be restricted to certain values or properties of their values. For example, we can define the type of integers between 0 and 10, or the type of lists that have a particular length. We can establish pre- and postconditions of functions using refinement types, potentially proving rather sophisticated properties.
In this tutorial, I will introduce Liquid Haskell, explain how it works, and what can (and cannot) be expected of it. We will look at a number of examples and see how they can be equipped with more precise types than Haskell would normally allow.
This session is held on