Introducing HERMIT
A Plugin for Transforming GHC Core Language Programs


Andrew Farmer
afarmer@ittc.ku.edu

(joint work with Andy Gill, Ed Komp, Neil Sculthorpe, Robert Blair, Jan Bracker, Patrick Flor, Nick Frisby, Adam Howell, Ryan Scott, and Michael Tabone)

Functional Programming Group
Information and Telecommunication Technology Center
University of Kansas

April 9, 2013

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Motivation

Core

data ModGuts  = ModGuts {_ :: [CoreBind], ...}
data CoreBind = NonRec Id CoreExpr
              | Rec [(Id, CoreExpr)]
data CoreExpr = Var Id
              | Lit Literal
              | App CoreExpr CoreExpr
              | Lam Id CoreExpr
              | Let CoreBind CoreExpr
              | Case CoreExpr Id Type [CoreAlt]
              | Cast CoreExpr Coercion
              | Tick (Tickish Id) CoreExpr
              | Type Type
              | Coercion Coercion
type CoreAlt  = (AltCon, [Id], CoreExpr)
data AltCon   = DataAlt DataCon | LitAlt Literal | DEFAULT

What is HERMIT?

What is HERMIT?

What is HERMIT?

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

What is HERMIT?

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

Downloading and Running HERMIT

HERMIT requires GHC 7.6

  1. cabal update
  2. cabal install hermit
  3. hermit Main.hs

The hermit command just invokes GHC with some default flags:

% hermit Main.hs
ghc Main.hs -fforce-recomp -O2 -dcore-lint
    -fsimple-list-literals -fexpose-all-unfoldings
    -fplugin=HERMIT
    -fplugin-opt=HERMIT:main:Main:

Demonstration: Unrolling Fibonacci

As a first demonstration, let's transform the fib function by unrolling the recursive calls once.

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

Demonstration: Unrolling Fibonacci

As a first demonstration, let's transform the fib function by unrolling the recursive calls once.

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

HERMIT

HERMIT Architecture

HERMIT Commands

Developing Transformations

Transformation Development Cycle

Adding Transformations to HERMIT

Two main ways:

{-# RULES "map/map"
    forall f g xs. map f (map g xs) = map (f . g) xs
#-}

KURE

Consider the first case rewriting rule from the Haskell 98 Report.

case e of { alts } = (\v -> case v of { alts }) e
where v is a new variable

Writing a rule that expresses this syntactical rewrite is straightforward.

rule_a :: ExpE -> Q ExpE
rule_a (CaseE e alts) = do
    v <- newName "v"
    return $ AppE (mkLamE [VarP v] $ CaseE (VarE v) alts) e
rule_a _              = fail "rule_a not applicable"

KURE is a DSL that allows the structured promotion of locally acting rules into globally acting rules.

Strategic Rewriting

Strategic Traversals

Try a rewrite, and if it fails, do nothing.

try(s) = s <+ id

Repeatedly apply a rewrite, until it fails.

repeat(s) = try(s ; repeat(s))

Apply a rewrite in a topdown manner.

topdown(s) = s ; all(topdown(s))

Principal KURE Types

data Translate c m a b = Translate { apply :: c -> a -> m b }

-- | A 'Translate' that shares the same source and target type.
type Rewrite c m a = Translate c m a a

The Category Zoo:

instance Functor m           => Functor (Translate c m a)
instance Applicative m       => Applicative (Translate c m a)
instance Alternative m       => Alternative (Translate c m a)
instance Monad m             => Monad (Translate c m a)
instance MonadCatch m        => MonadCatch (Translate c m a)
instance MonadPlus m         => MonadPlus (Translate c m a)
instance Monad m             => Category (Translate c m)
instance MonadCatch m        => CategoryCatch (Translate c m)
instance Monad m             => Arrow (Translate c m)
instance MonadPlus m         => ArrowZero (Translate c m)
instance MonadPlus m         => ArrowPlus (Translate c m)
instance Monad m             => ArrowApply (Translate c m)
instance (Monad m, Monoid b) => Monoid (Translate c m a b)

KURE in HERMIT

-- HERMIT translations all operate over the same context and monad.
type TranslateH a b = Translate Context HermitM a b
type RewriteH   a   = Rewrite Context HermitM a

-- Context: bindings in scope, current ModGuts information
-- HermitM: fresh name supply, expression stash

betaReduce :: RewriteH CoreExpr
betaReduce = do App (Lam v e1) e2 <- idR
                return $ Let (NonRec v e2) e1

Congruence Combinators

-- | Translate an expression of the form: @Lam@ ’Id’ ’CoreExpr’
lamT :: TranslateH CoreExpr a
     -> (Id -> a -> b)
     -> TranslateH CoreExpr b
lamT t f =
    translate $ \ c e -> case e of
        Lam b e1 -> f b <$> apply t (addLambdaBinding b c @@ 0) e1
        _        -> fail "no match for Lam"

Congruence Combinators in Action

-- | (let v = ev in e) x ==> let v = ev in e x
letFloatApp :: RewriteH CoreExpr
letFloatApp =
  do vs <- appT letVarsT freeVarsT intersect
     let letAction = if null vs then idR else alphaLet
     appT letAction idR $ \ (Let bnds e) x -> Let bnds $ App e x

Current Status

Next: Worker/Wrapper