Liquid Haskell is an extension to Haskell that adds refinement types to the language, which are then checked via an external theorem prover such as z3. With refinement types, one can express many interesting properties of programs that are normally out of reach of Haskell’s type system or only achievable via quite substantial encoding efforts and advanced type system constructs. On the other hand, the overhead for checking refinement types is often rather small, because the external solver is quite powerful.
Liquid Haskell used to be an external, standalone executable, but is now available as a GHC plugin, making it much more convenient to use.
In this tutorial, we’ll discuss how refinement types work, give many examples of their use and learn how to work with Liquid Haskell productively.
Prerequisites Good familiarity with Haskell basics is useful. However, no knowledge of type system language extensions or type-level programming is required.
