Operator-based Equational Reasoning

The support for equational reasoning in Isabelle, Lean and Dafny is built into their syntax, while in Liquid Haskell, the operators for equational reasoning can be provided by a library. This is highly inspired by Agda.

Agda is a general theorem prover based on dependent type theory. Its type system and syntax is flexible enough to allow the library-defined operator

  _≡⟨_⟩_ :∀ (x {y z} : A) -> x ≡ y -> y ≡ z -> x ≡ z

which expresses an equality together with its proof. Observe the similarity between Liquid Haskell's (==.) operator.

  a ≡⟨explanation⟩ b     -- Agda
  a ==. b ? explanation  -- Liquid Haskell

One disadvantages of the operator-based equational reasoning in Liquid Haskell over built-in support like in, say, Dafny is that there each equation is checked independently, whereas Liquid Haskell checks all equalities in one function at once, which can be slower.

While the above tools allow equational reasoning, Liquid Haskell is unique in extending an existing, general-purpose programming language to support theorem proving. This makes Liquid Haskell a more natural choice for verifying Haskell code, both because it is familiar to Haskell programmers, and because it does not require porting code to a separate verification language.

Verification in Haskell

Liquid Haskell is far from the first attempt to bring theorem proving to Haskell. Zeno generates proofs by term rewriting and Halo uses an axiomatic encoding to verify contracts. Both these tools are automatic, but unpredictable and not programmer-extensible, which has limited them to verifying much simpler properties than the ones checked here. Another tool, HERMIT, proves equalities by rewriting the GHC core language, guided by user specified scripts. Compared to these tools, in Liquid Haskell the proofs are Haskell programs while SMT solvers are used to automate reasoning.

Haskell itself is dependently typed, where inductive proofs can be encoded as type class constraints. However, proofs in dependent Haskell do not have the straightforward equational-reasoning style that Liquid Haskell allows and are not SMT-aided.