Tool Support for Equational Reasoning on GHC Core Programs

Andrew Farmer - Facebook

Neil Sculthorpe - Swansea University

Andy Gill - The University of Kansas

Haskell Symposium

September 3, 2015

Functional programming languages encourage equational reasoning.

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

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)
```

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

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)
```

Rewrite rules are used to guide optimization:

`{-# RULES "stream/unstream" forall s. stream (unstream s) = s #-}`

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

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)
```

Rewrite rules are used to guide optimization:

`{-# RULES "stream/unstream" forall s. stream (unstream s) = s #-}`

GHC does not verify the laws hold or that rewrite rules are correct.

If proven, the proof is typically performed by hand, using equational reasoning.

By Hand

- Slow
- Error prone
- Difficult to keep in sync

Via Another Language

- Transliteration into Coq/Agda/etc
- Requires considerable expertise
- Semantic mismatch

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

```
cabal update
cabal install hermit
```

(Stick to GHC 7.8 for now.)

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

HERMIT has previously focused on *transformational* tasks:

- Domain-specific optimization passes (SYB traversals, Stream Fusion's
`concatMap`). - Prototype Haskell-to-Hardware compiler.
- Mechanizing Worker/Wrapper transformations for small examples.

Reasoning capabilities were limited:

- Abstraction only via re-running transformation scripts.
- Non-transformational reasoning (e.g. induction) impossible.
- Pre- and side-conditions unchecked or 'in the way'.

Add 'lemmas' to HERMIT:

- Primitive: equivalences between GHC Core expressions
- Conjunction, disjunction, implication, and universal quantification

Add 'lemmas' to HERMIT:

- Primitive: equivalences between GHC Core expressions
- Conjunction, disjunction, implication, and universal quantification

When all you have is KURE, everything looks like a transformation...

- Lemmas can be used as bi-directional transformations.
- Reasoning is performed by transforming
*lemmas*.- 'Proof' by transforming a lemma into the primitive truth value.
- Structural induction is a lemma transformation.
- Lemmas can transform other lemmas.

- Interactive and scriptable reasoning, just like program transformations.

- HERMIT's new equational-reasoning infrastructure
- Demonstration of interactive reasoning
- Case study: Verifying type-class laws
- Case study: textbook equational reasoning (from
*Pearls of Functional Algorithm Design*) - Cabal integration

A *calculational programming* exercise taken from Richard Bird's *Pearls of Functional Algorithm Design*.

Involves both equational reasoning and program transformation.

This property must be proved in the course of the study:

`filter (good . value) = filter (good . value) . filter (ok . value)`

As a HERMIT lemma:

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:

Type Class Laws

- Proofs are heavy on unfolding and simplification, but brief, corresponding to the by-hand versions.
- Practical aspects of targeting GHC Core.
- Unfolding information for library functions such as (
`++`

) - Working with coercions.

- Unfolding information for library functions such as (

Making a Century

- Mechanizing proofs in textbook was straightforward.
- Proved many properties the textbook only assumed.
- Awkward: Associativity
- One error was discovered in textbook.

Equational reasoning can be mechanized during compilation at a level of abstraction comparable to performing it by hand.

HERMIT can enforce a connection between the program, the reasoning steps, and the compiled program.

Upcoming:

- New GHCi-based interactive read-eval-print loop.
- Parser for GHC Core expressions.
- Connect to other proof tools which target GHC Core.
- Return to Worker/Wrapper, target larger example programs.