Introducing the HERMIT Equational Reasoning Framework

Imagine you are sitting at your terminal wishing your Haskell program would go faster. The optimization flag has been turned on, and you know of an unimplemented transformation that could help. What do you do? You could add a new optimization pass to GHC, taking part in the dark art of tuning heuristics to allow it to play well with others. Or you could experiment, using HERMIT.

First Example of HERMIT

As an example we use the Fibonacci function, not because it is interesting, but because it is so well known.

module Main where

fib :: Int -> Int
fib n = if n < 2 then 1 else fib(n-1) + fib(n-2)

Compiling with -O2, and using Criterion to average over 100 tests, we observe that fib 35 runs in 124.0ms±2.6ms on our development laptop.

To enable further optimization of fib, we want to try unrolling the recursive calls. Like the GHC optimizer, we want to do this without changing the source, which is clear and concise.

To do so, we fire up HERMIT, choosing to use the command-line interface (because the GUI version is not written yet). HERMIT uses the GHC plugin mechanism, to insert itself into the optimization pipeline as a rather non-traditional compiler pass, capturing programs mid-compilation and allowing the user to manipulate them.

ghc -fplugin=Language.HERMIT.Plugin
    -fplugin-opt=Language.HERMIT.Plugin:main:Main:mode=i
    -fforce-recomp -O2 -dcore-lint Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
...
module main:Main where
  fib ∷ Int -> Int
  ...
hermit> _

GHC has compiled our program into its intermediate form, called GHC Core, and HERMIT is asking for input. At this point we can start exploring our captured program. There are several bindings, but let us consider just fib.

hermit> consider 'fib
rec fib = λ n →
      case (<) ▲ $fOrdInt n (I# 2) of wild
        False →
          (+) ▲ $fNumInt
            (fib ((-) ▲ $fNumInt n (I# 1)))
            (fib ((-) ▲ $fNumInt n (I# 2)))
        True → I# 1

The consider command moves the focus onto the specified function, and the REPL displays the function's abstract syntax. This is HERMIT's ``compact'' pretty printer for GHC Core. Core programs necessarily contain a substantial amount of information, and in this render engine HERMIT uses ▲ as a placeholder for type arguments. Notice that we refer to a Haskell syntactical name using the Template Haskell convention of prefixing with a tick.

Next we want to unroll fib, to see if this improves performance. Specifically, we want to inline all calls to fib (but nothing else) in a bottom-up manner. HERMIT uses strategic programming as its basis, so we build a strategy using two HERMIT functions.

hermit> any-bu (inline 'fib)
rec fib = λ n →
      case (<) ▲ $fOrdInt n (I# 2) of wild
        False →
          (+) ▲ $fNumInt
            ((λ n →
                case (<) ▲ $fOrdInt n (I# 2) of wild
                  False →
                    (+) ▲ $fNumInt
                      (fib ((-) ▲ $fNumInt n (I# 1)))
                      (fib ((-) ▲ $fNumInt n (I# 2)))
                  True → I# 1)
               ((-) ▲ $fNumInt n (I# 1)))
            ((λ n →
                case (<) ▲ $fOrdInt n (I# 2) of wild
                  False →
                    (+) ▲ $fNumInt
                      (fib ((-) ▲ $fNumInt n (I# 1)))
                      (fib ((-) ▲ $fNumInt n (I# 2)))
                  True → I# 1)
               ((-) ▲ $fNumInt n (I# 2)))
        True → I# 1

Each inner instance of fib has been replaced with its definition, effectively unrolling fib. There are many more simplifications that can be done, such as β-reduction, but GHC is good at this. For now, we just want to test this version; so we type exit and GHC resumes compiling our program.

Now we time this new version. Again, taking the average over 100 tests using Criterion, we observe that the post-HERMIT fib 35 runs in about 76.7ms±3.6ms. We have modified GHC's internal representation of our program mid-compilation, improving it such that the resulting program runs measurably faster. Furthermore, we did not need to alter the original program to do so.

More Information

If you are interested in learning more about HERMIT, we've just submitted a paper to the Haskell Symposium, called Introducing the HERMIT Equational Reasoning Framework, written by Andrew Farmer, Ed Komp, Neil Sculthorpe, and myself. A first release of HERMIT will be available via hackage in the near future.

Andy Gill