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

January 18, 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

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 -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 a 'Translate' to a value
-- and its context.
apply :: c -> a -> m b }
-- | The primitive way of building a 'Translate'.
translate :: (c -> a -> m b) -> Translate c m a b
translate = Translate
-- | A 'Translate' that shares the same source
-- and target type.
type Rewrite c m a = Translate c m a a
-- | The primitive way of building a 'Rewrite'.
rewrite :: (c -> a -> m a) -> Rewrite c m a
rewrite = translate
```

```
-- | Core is the sum type of all nodes in the AST that
-- we wish to be able to traverse. All â€™Nodeâ€™ instances
-- in HERMIT define their â€™Genericâ€™ type to be â€™Coreâ€™.
data Core = ModGutsCore ModGuts -- ^ The module.
| ProgramCore CoreProgram -- ^ A program
| BindCore CoreBind -- ^ A binding group.
| DefCore CoreDef -- ^ A recursive definition.
| ExprCore CoreExpr -- ^ An expression.
| AltCore CoreAlt -- ^ A case alternative.
```

```
-- | A 'Lens' is a way to focus on a sub-structure
-- of type @b@ from a structure of type @a@.
newtype Lens c m a b = Lens (Translate c m a ((c,b), b -> m a))
-- | Apply a 'Rewrite' at a point specified by a 'Lens'.
focusR :: Monad m => Lens c m a b
-> Rewrite c m b -> Rewrite c m a
-- | Apply a 'Translate' at a point specified by a 'Lens'.
focusT :: Monad m => Lens c m a b
-> Translate c m b d -> Translate c m a d
-- | Check if the focusing succeeds, and additionally
-- whether unfocusing from an unchanged value would succeed.
testLensT :: MonadCatch m => Lens c m a b -> Translate c m a Bool
instance Monad m => Category (Lens c m)
instance MonadCatch m => CategoryCatch (Lens c m)
```

```
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
type LensH a b = Lens Context HermitM a b
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
- Still early in development
- Single module only (can run different scripts for different modules)
- Next step: an equational reasoning framework that only allows correctness preserving transformations
- Publications:
- The HERMIT in the Machine (Haskell â€™12) â€” describes the HERMIT implementation
- The HERMIT in the Tree (submitted to IFL â€™12) â€“ describes our experiences mechanising existing program transformations

Â