LiquidHaskell (LH) refines Haskell's types with logical predicates that let you enforce important properties at compile time.
Guarantee Functions are Total¶
LH warns you that head is not total as it is missing the case for []
and checks that it is total on NonEmpty
lists.
(more...)
The input contract propagates to uses of head
which are verified by ensuring the arguments are NonEmpty
.
Keep Pointers Within Bounds¶
LH lets you avoid off-by-one errors that can lead to crashes or buffer overflows. (more...)
Dependent contracts let you specify, e.g. that dotProduct
requires equal-sized vectors.
Avoid Infinite Loops¶
LH checks that functions terminate and so warns about the infinite recursion due to the missing case in fib
.
(more...)
Metrics let you check that recursive functions over complex data types terminate.
Enforce Correctness Properties¶
Write correctness requirements, for example a list is ordered, as refinements. LH makes illegal values be unrepresentable. (more...)
LH automatically points out logic bugs, and proves that functions return correct outputs for all inputs.
Prove Laws by Writing Code¶
Specify laws, e.g. that the append function ++
is associative, as Haskell functions.
Verify laws via equational proofs that are plain Haskell functions. Induction is simply recursion, and case-splitting is just pattern-matching.
Get Started¶
The easiest way to try LiquidHaskell is online, in your browser. This environment is ideal for quick experiments or following one of the tutorials:
- The Official Tutorial (long but complete) (has interactive exercises)
- Andres Loeh's Tutorial (concise but incomplete)
For links to more documentation, see the nav-bar at the top of this page.
Get Involved¶
If you are interested in contributing to LH and its ecosystem, that's great! We have more information on our GitHub repository.