Reasoning with the HERMIT

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

Equational Reasoning

Functional programming languages encourage equational reasoning.

Type Class Laws and RULES

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 and RULES

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 and RULES

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.

Reasoning in Haskell

By Hand

Via Another Language

HERMIT

cabal update
cabal install hermit
(Stick to GHC 7.8 for now.)
image from http://www.angelfire.com/ks/larrycarter/LC/OldGuardCameron.html

HERMIT

HERMIT has previously focused on transformational tasks:

Reasoning capabilities were limited:

In This Paper

Add 'lemmas' to HERMIT:

map fusion lemma

In This Paper

Add 'lemmas' to HERMIT:

return left lemma

Leveraging KURE

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

In The Paper

Case Study: Making a Century

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

Involves both equational reasoning and program transformation.

Making a Century Example:

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

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

As a HERMIT lemma:

Lemma 6.2 Example Step 1

The proof begins by appealing to a more general lemma:

Filter Split Lemma

Lemma 6.2 Example Step 2

Making a Century Example:

Now unfold composition, and abstract the value x expression:

Lemma 6.2 Example Step 3

Lemma 6.2 Example Step 4

Making a Century Example:

Unfold both ok and good:

Lemma 6.2 Example Step 5

Making a Century Example:

Prove by cases (smash handles the undefined case):

Lemma 6.2 Example Step 6

Appeal to a lemma about integers from a library:

integer lemma

Lemma 6.2 Example Step 7

Case Study Takeaways

Type Class Laws

Making a Century

Conclusion

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: