Liquid Haskell:
If Liquid Haskell succeeds, the program is compiled normally.
The primary goal of Liquid Haskell is to add more precise types to a Haskell program, so that you can e.g.:
If a program is erroneous in Haskell, it is wrong in Liquid Haskell as well:
We can use set comprehension notation to refine a Haskell type signature for Liquid Haskell:
Remember, Haskell will still see the program without the extra annotations, so in general you need two type signatures.
We can define abbreviations in for Liquid Haskell in much the same way that we can do in Haskell:
The type parameter must be a capital letter here! (Lower-case letters for "Haskell" type variables, upper-case letters for Liquid Haskell expressions.)
The Liquid Haskell Prelude defines (among other things) a convenient synonym for natural numbers.
All of these work (but we have to choose one).
What is the type of (+)?
The type of plus is a dependent function type.
Note: We can only use what we have established in the types. If we remove the Liquid type signature for plus, then i9 will no longer typecheck.
A precondition restricts how or when we can call a function.
A postcondition establishes knowledge that can be used by the system.
If we compose function calls, Liquid Haskell will check if the knowledge established by the postconditions implies the necessary preconditions (by asking an SMT solver).
Once again, we can only work with what we have established via the types. E.g., changing the type of combine to Nat -> Nat does not work without adapting the type of pre as well.
SMT solvers are relatively good at dealing with integers. Because Liquid Haskell relies on an SMT solver to do all the hard work, we get to benefit from that:
abs?sub so that it implements subtraction restricted to (suitable) natural numbers?halve that captures that the sum of the two components of the resulting tuple is the equal to the function argument? (Hint: you can use fst and snd in the refinement to access the components of the pair.)