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

- There is often a trade-off between the clarity and efficiency of a program.

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code?

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code? Haskell 98?

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code? Haskell 98? Haskell 2010?

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code? Haskell 98? Haskell 2010? GHC-extended Haskell?

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code? Haskell 98? Haskell 2010? GHC-extended Haskell? Which extensions?

- There is often a trade-off between the clarity and efficiency of a program.
- Useful to transform a clear program (specification) into an efficient program (implementation).
- We want to mechanise such transformations on Haskell programs:
- less time-consuming and error prone than pen-and-paper reasoning
- no need to modify the source file

- Several existing transformation systems for Haskell programs, e.g. HaRe, HERA, PATH, Ultra
- But they all operate on Haskell source code (or some variant).
- Haskell source code? Haskell 98? Haskell 2010? GHC-extended Haskell? Which extensions?
- Alternative: GHC Core, GHCâ€™s intermediate language

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

- Haskell Equational Reasoning Model-to-Implementation Tunnel

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

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

HERMIT requires GHC 7.6

- cabal update
- cabal install hermit
- 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:
```

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

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

- Core-specific rewrites, e.g.
- beta-reduce
- eta-expand 'x
- case-split 'x
- inline

- Strategic traversal combinators (from KURE), e.g.
- any-td r
- repeat r
- innermost r

- Navigation, e.g.
- up, down, left, right, top
- consider 'foo
- 0, 1, 2, . . .

- Version control, e.g.
- log
- back, step
- save "myscript.hss"

Two main ways:

- Using KURE
- very expressive
- currently requires recompiling HERMIT

- Using GHC Rules
- lightweight (can be included in the source code of the object program)
- no need to recompile HERMIT
- limited by the expressiveness of RULES

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

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.

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

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

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

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

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

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

- A GHC plugin for interactive transformation of GHC Core programs
- The HERMIT in the Machine (Haskell â€™12) â€” describes the HERMIT implementation
- The HERMIT in the Tree (IFL â€™12) â€“ describes our experiences mechanising existing program transformations

- Current Work
- Worker/wrapper splitter
- Extensibility

- Next step(s)
- Larger worker/wrapper examples
- An equational reasoning framework
- Domain-specific optimization framework
- Android interface