Tool Support for Equational Reasoning on GHC Core Programs

Andrew Farmer - The University of Kansas

Neil Sculthorpe - Swansea University

Andy Gill - The University of Kansas

June 11, 2015

- A plugin to the Glasgow Haskell Compiler (GHC).
- Targets GHC's intermediate language, GHC Core.
- Supports both interactive and scripted transformation and proof.
- Provides a large dictionary of compositional local transformations.

```
cabal update
cabal install hermit
```

image from http://www.angelfire.com/ks/larrycarter/LC/OldGuardCameron.html

HERMIT has previously been applied to a variety of *transformational* tasks:

- Domain-specific optimization pass for SYB traversals.
- Domain-specific optimization pass for fusing
`concatMap`in Stream Fusion. - Prototype Haskell-to-Hardware compiler.
- Mechanizing Worker/Wrapper transformation for small examples.

Previously, side- and pre-conditions were not captured.

Inductive reasoning was not supported.

- Lemmas
- Primitive: equivalences between GHC Core expressions.
- Composite: conjunction, disjunction, and implication

- Structural Induction (as a rewrite on lemmas)
- Dictionary Creation

Type-class laws are properties expected to hold for class *instances*.

Example:

```
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
```

The following three laws should hold for any instance of `Monad`

:

```
return-left return x >>= k == k x
return-right k >>= return == k
bind-assoc (j >>= k) >>= l == j >>= (\x -> k x >>= l)
```

If proven, these are typically proven by hand.

As an example, prove the `return-left`

law for lists using HERMIT.

Begin by creating a Haskell program containing the law as GHC rewrite rule.

```
module Laws where
main :: IO ()
main = return ()
{-# RULES "return-left" [~] forall k x. return x >>= k = k x #-}
```

Then invoke HERMIT on this file:

`$ hermit Laws.hs`

The GHC rewrite rule can be turned into a HERMIT lemma.

The monad type parameter can be instantiated to lists.

Begin the proof and instantiate the dictionary parameters.

Rewrite `return`

to a singleton list.

Appeal to two auxiliary lemmas to rewrite (`>>=`

).

Appeal to another auxiliary lemma to eliminate (`++`

).

Both sides are Î±-equivalent, so end the proof.

Comparing by-hand reasoning with the HERMIT script.

```
By-hand HERMIT
================================ =====================================================
rule-to-lemma return-left
copy-lemma return-left return-left-list
inst-lemma return-left-list 'm [| [] |]
prove-lemma return-left-list
inst-dictionaries
return x >>= k
{ definition of return } { application-of 'return ; repeat (unfold <+ smash) }
= [x] >>= k
{ definition of >>= } one-td (lemma-forward bind-left-cons)
= k x ++ ([] >>= k)
{ definition of >>= } one-td (lemma-forward bind-left-nil)
= k x ++ []
{ xs ++ [] == xs } one-td (lemma-forward append-right)
= k x
```

Laws proven in the case study:

Length of proof scripts:

- Overall, proofs are heavy on unfolding and simplification, but short, corresponding to the by-hand versions.
- Auxiliary lemmas help manage proof complexity.
- Practical aspects of targeting GHC Core.
- Unfolding information for library functions such as (
`++`

) - Working with coercions.

- Unfolding information for library functions such as (

- A
*calculational programming*exercise taken from Richard Bird's*Pearls of Functional Algorithm Design*. - Involves both proof and program transformation.
- Requires more advanced reasoning techniques than the type-class laws study.

As an example, this property must be proved in the course of the study:

The proof begins by appealing to a more general lemma:

Now unfold composition, and abstract the `value x`

expression:

Unfold both `ok`

and `good`

:

Prove by cases (`smash`

handles the `undefined`

case):

Appeal to a lemma about integers from a library:

Lemmas stated in textbook.