Feb 1, 2021

Reasoning with the HERMIT: Tool support for equational reasoning on GHC Core programs

Hurrah! This is my first post… It’s a report on my reading the paper

Andrew Farmer, Neil Sculthorpe, and Andy Gill. 2015. Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ‘15). Association for Computing Machinery, New York, NY, USA, 23–34.

Prelude

Equational Reasoning

Let’s set the stage with some examples from [1]. We can use the algebraic laws

xy          = yx          {commutativity}
x + (y + z) = (x + y) + z {associativity}
x (y + z)   = xy + xz     {left distributivity}
(x + y) z   = xz + yz     {right distributivity}

to prove the equality (x + a) (x + b) = x^2 + (a + b)x + ab in the following manner:

 (x + a) (x + b)
=   {left distributivityi}
 (x + a)x + (x + a)b
=   {right distributivity}
 x^2 + ax + xb + ab
=   {commutativity}
 x^2 + ax + bx + ab (1)
=   {right distributivity}
 x^2 + (a + b)x + ab (2)

From a computational perspective the expression (1) is less efficient than (2). This shows how equational reasoning may be used to improve the efficiency of some computation.

Reasoning about Haskell Programs

Because Haskell programs are similar to mathematical functions, it is possible apply this form of reasoning to Haskell programs. Hakell’s function definitions can then be viewed as laws or properties saying that the left-hand side may be replaced by the right-hand side. For example, from the definition

double :: Int -> Int
double x = x + x

we know that we may substitute x + x for double x and vice-versa in a program containing the definition. As another example, let’s see how we can use the definition

reverse :: [a] -> [a]
reverse []     = []
reverse (x:xs) = reverse xs ++ [x]

to show the (obvious) equivalence reverse [x] = [x]. The proof goes as follow

 reverse [x]
=   {list notation}
 reverse (x:[])
=   {apply reverse}
 reverse [] ++ [x]
=   {apply reverse}
 [] ++ [x]
=   {apply ++}
 [x]

Note that the result is more efficient because it does not require a function application. We can instruct GHC to substitute [x] for reverse [x] during its optimization passes using the rewrite rules pragma as demonstrated in [2].

Let’s apply what we know to prove forall f g. map f . map g = map (f . g). Recall this definition of map

map :: (a -> b) -> [a] -> [b]
map f []     = []
map f (a:as) = f a : map f as

Both sides of the original equality can be eta-expanded to obtain the equivalent goal

map f (map g xs) = map (λ x -> f (g x)) xs

where xs is an arbitrary list of some type. Now that the list argument is explicit, we can use induction on its structure with the last equality as our induction hypothesis.

For the base case, by definition of map

map (λ x -> f (g x)) [] = []

Also

 map f (map g [])
=   {apply map}
 map f []
=   {apply map}
 []

Since both the right-hand-side and the left-hand-side reduce to the empty list, we conclude that the target proposition holds for empty lists.

Now, for xs = (a:as) we have the following transformations

 map f (map g (a:as))
=   {apply map}
map f (g a : map g as)
=   {apply map}
f (g a) : map f (map g as)
=   {induction hypothesis}
(λ x -> f (g x)) a : map (λ x -> f (g x)) as
=   {apply map}
map (λ x -> f (g x)) (a:as)

And this concludes the proof of the inductive step and that of the equality

forall f g. map f . map g = map (f . g)

Now, imagine that we have a program relying on the equivalence we have just proved; and some months later we update our definition of map. Since the proof of the equivalence relies on the definition of map, we would need to do it one more time to make sure that the equivalence still holds. For such small examples, it is easily done. However, consider what the task could look like for the proofs that all type class laws hold for all the instances defined in a real-world project.

The main Idea

I think the main idea in the paper is that we should automate the proofs once we know the steps involved. The suggested approach is to

  1. Prove the properties using the HERMIT repl
  2. Export the commands sequence in HERMIT scripts
  3. Configure the build pipeline to automatically check the proof at compile time

Instead of relying on languages and tools external to Haskell such as Agda or Coq

HERMIT is a Haskell-specific toolkit designed to support equational reasoning and user-guided program transformation and to do so as part of the GHC compilation pipeline.

The paper presents several contributions, notably:

  1. HERMIT can now be used to check preconditions
  2. HERMIT can now be used to reason about auxiliary properties of programs being transformed
  3. HERMIT now provides built-in structural induction over algebraic data types.

As a case study the authors present the use of HERMIT’s shell to prove the proposition

forall f g. map f . map g = map (f . g)

If you want to try for yourself, assuming you have stack installed, clone this repository, move to the created directory, and run

$ stack build
$ stack exec hermit src/Examples.hs

The first command may take at least the time necessary to prepare a cup of tea. For the second command, the expected output is

[starting HERMIT v1.0.0.0 on src/Examples.hs]
% ghc src/Examples.hs -fforce-recomp -O2 -dcore-lint ...
[1 of 1] Compiling Examples         ( src/Examples.hs, src/Examples.o )
.
.
.
======================= Welcome to HERMIT ================================
HERMIT is a toolkit for the interactive transformation of GHC Core language
programs...
.
.
.
=========================================================================

module Example where
    map :: ∀ a b . (a → b) → [a] → [b]
hermit<0>

The last line is an invitation to enter HERMIT commands. Entering the uncommented lines to the prompt will lead to the verification of the proof. Here is an example of interactive proof checking from the paper.

set-pp-type Omit

-- module main:MapFusion where map :: forall a b . (a -> b) -> [a] -> [b]

binding-of 'map

-- map = \ f ds ->
--   case ds of wild
--     [] -> []
--     (:) a as -> (:) (f a) (map f as)

top

-- module main:MapFusion where map :: forall a b . (a -> b) -> [a] -> [b]

rule-to-lemma map-fusion
prove-lemma map-fusion

-- Goal:
-- forall f g. (.) (map f) (map g) = map ((.) f g)

extensionality 'xs

-- Goal:
-- forall f g xs. (.) (map f) (map g) xs = map ((.) f g) xs

lhs (unfold '.)

-- Goal:
-- forall f g xs. map f (map g xs) = map ((.) f g) xs

induction 'xs

-- Goal:
-- forall f g.
-- (map f (map g undefined) = map ((.) f g) undefined)
-- ^
-- ((map f (map g []) = map ((.) f g) [])
--  ^
--  (forall a b. (map f (map g b) = map ((.) f g) b) => (map f (map g ((:) a b)) = map ((.) f g) ((:) a b))))

any-bu ((unfold 'map) >>> (undefined-case <+ case-reduce))

-- Goal:
-- forall f g.
-- (undefined = undefined)
-- ^
-- (([] = [])
--  ^
--  (forall a b.
--   (map f (map g b) = map ((.) f g) b)
--   =>
--   ((:) (f (g a)) (map f (map g b)) = (:) ((.) f g a) (map ((.) f g) b))))

simplify-lemma

-- Goal:
-- forall f g a b.
-- (map f (map g b) = map ((.) f g) b)
-- =>
-- ((:) (f (g a)) (map f (map g b)) = (:) ((.) f g a) (map ((.) f g) b))

forall-body

-- Goal:
-- (map f (map g b) = map ((.) f g) b)
-- =>
-- ((:) (f (g a)) (map f (map g b)) = (:) ((.) f g a) (map ((.) f g) b))

consequent

-- Notice when we move past the antecedent, it comes into scope!

-- Assumed lemmas:
-- ind-hyp-0 (Built In)
--   map f (map g b) = map ((.) f g) b
-- Goal:
-- (:) (f (g a)) (map f (map g b)) = (:) ((.) f g a) (map ((.) f g) b)

one-td (lemma-forward ind-hyp-0)

-- Assumed lemmas:
-- ind-hyp-0 (Built In)
--   map f (map g b) = map ((.) f g) b
-- Goal:
-- (:) (f (g a)) (map ((.) f g) b) = (:) ((.) f g a) (map ((.) f g) b)

simplify

-- Assumed lemmas:
-- ind-hyp-0 (Built In)
--   map f (map g b) = map ((.) f g) b
-- Goal:
-- (:) (f (g a)) (map ((.) f g) b) = (:) (f (g a)) (map ((.) f g) b)

end-case -- proven map-fusion

-- module main:MapFusion where map :: forall a b . (a -> b) -> [a] -> [b]

Possible Improvement

[…] Some of the transformations provided by HERMIT only offer partial correctness. […] In the next version we intend to allow the user the option of disabling the set of partially correct transformations, and of enforcing that any preconditions are satisfied before a transformation can be used.

Also, there is a useful technique in equational reasoning that is not supported by HERMIT at the time of the publication. To illustrate, consider this other example again from [1]: the computation of an efficient version of reverse. To avoid the quadratic time induced by the use of ++ in the previous definition the authors specify a new function reverse' such that

reverse' xs ys = reverse xs ++ ys

And instead of giving a definition of reverse' and proving that it satisfies the specification above, they derive the definition from the specification by induction on xs.

Base case:

 reverse' [] ys
=   {specification of reverse'}
 reverse [] ++ ys
=   {apply revere}
 [] ++ ys
=   {apply ++}
 ys

Inductive case:

 reverse' (x:xs) ys
=   {specification of reverse'}
 reverse (x:xs) ++ ys
=   {apply reverse}
 (reverse xs ++ [x]) ++ ys
=   {associativity of ++}
 reverse xs ++ ([x] ++ ys)
=   {induction hypothesis}
 reverse' xs ([x] ++ ys)
=   {apply ++}
 reverse' xs (x : ys)

The conclusion is

reverse' :: [a] -> [a] -> [a]
reverse' [] ys     = ys
reverse' (x:xs) ys = reverse' xs (x : ys)

Finally a nicer version of reverse is defined

reverse :: [a] -> [a]
reverse xs = reverse' xs []

The derivations of programs in such a backward manner although not supported can still be verified by using the resulting definition as a goal in a verification of the specification.

References

  1. Programming in Haskell, 2nd Ed, Graham Hutton
  2. Playing by the Rules: Rewriting as a practical optimisation technique in GHC, Simon Peyton Jones, Andrew Tolmach, Tony Hoare