Andrew Farmer

Dissertation Defense

Electrical Engineering and Computer Science

The University of Kansas

April 30, 2015

Advisor: Andy Gill

- It is difficult to write programs which are both correct and fast.
- One approach is to refine a correct executable specification to a fast implementation via program transformation.
- Establishing this connection formally is time-consuming and requires considerable expertise.
- In the functional languages community, this connection is often established via
*semi-formal reasoning*.

- Functional languages facilitate reasoning by hand.
- Program transformation accomplished by modifying program source.
- Program properties proven alongside code.

Typically performed equationally:

Reasoning sample from The Worker/Wrapper Transformation

Semi-formal reasoning is popular because it is relatively simple, but it has limitations:

- Modifying source code obfuscates it, losing intermediate reasoning steps.
- Tedious to perform on real programs.
- No correspondence enforced between recorded reasoning steps and program as program changes over time.

Semi-formal reasoning is popular because it is relatively simple, but it has limitations:

- Modifying source code obfuscates it, losing intermediate reasoning steps.
- Tedious to perform on real programs.
- No correspondence enforced between recorded reasoning steps and program as program changes over time.

**Proposal: Provide tool support!**

Mechanizing semi-formal reasoning, during compilation, lowers the burden of writing programs which are both correct and fast.

Mechanizing semi-formal reasoning, during compilation, lowers the burden of writing programs which are both correct and fast.

- Semi-formal reasoning aids in writing programs which are both correct and fast.

Mechanizing semi-formal reasoning, during compilation, lowers the burden of writing programs which are both correct and fast.

- Semi-formal reasoning aids in writing programs which are both correct and fast.
- Mechanization lowers the burden of semi-formal reasoning.
- Tedious details/reductions are handled by the tool.
- Reasoning steps can be recorded/replayed.

- Semi-formal reasoning aids in writing programs which are both correct and fast.
- Mechanization lowers the burden of semi-formal reasoning.
- Tedious details/reductions are handled by the tool.
- Reasoning steps can be recorded/replayed.

- Operating during compilation has fundamental benefits to mechanization.
- Implicit information (types/instance definitions) in the source is explicit.
- Target language is syntactically smaller/more stable.

- Presents the design and implementation of HERMIT, a compile-time reasoning assistant for the Haskell language.
- Demonstrates that semi-formal reasoning can be mechanized at compile time at a level of abstraction comparable to performing it by hand.
- Provides evidence that an interactive means of exploring optimizations, such as HERMIT's interactive interface, reduces the effort in developing such optimizations.

Along the way:

- Extends TrieMaps to support first-order pattern matching in the map key.
- Solves a long-standing practical limitation of the Stream Fusion shortcut deforestation system.

- Presents the design and implementation of HERMIT, a compile-time reasoning assistant for the Haskell language.

- Demonstrates that semi-formal reasoning can be mechanized at compile time at a level of abstraction comparable to performing it by hand.
- Provides evidence that an interactive means of exploring optimizations, such as HERMIT's interactive interface, reduces the effort in developing such optimizations.

Along the way:

- Extends TrieMaps to support first-order pattern matching in the map key.
- Solves a long-standing practical limitation of the Stream Fusion shortcut deforestation system.

Existing tools do not address needs of semi-formal reasoning.

- Target source language (e.g. HaRe, PATH, HERA, etc)
- Source language is syntactically large.
- Typing information not locally available, must be inferred.
- Difficult to handle language extensions.
- Transformation-oriented

- Target intermediate language (e.g. HALO, Zeno, etc)
- Automatic, non-interactive
- Specialized
- Proof-oriented

- A plugin to the Glasgow Haskell Compiler (GHC).
- Targets GHC's intermediate language, GHC Core.
- Supports both interactive and scripted transformation and proof.
- Provides a large dictionary of compositional local transformations.

```
cabal update
cabal install hermit
```

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

```
class Functor f where
fmap :: (a -> b) -> f a -> f b
instance Functor Maybe where
fmap :: (a -> b) -> Maybe a -> Maybe b
fmap _ Nothing = Nothing
fmap f (Just x) = Just (f x)
fmap :: forall f. Functor f => (forall a b. (a -> b) -> f a -> f b)
digitToInt :: Char -> Int
```

Haskell

`fmap digitToInt (Just '5')`

GHC Core

`fmap Maybe $fFunctorMaybe Char Int digitToInt (Just Char '5')`

- Provides evidence that an interactive means of exploring optimizations, such as HERMIT's interactive interface, reduces the effort in developing such optimizations.

Along the way:

- Extends TrieMaps to support first-order pattern matching in the map key.
- Solves a long-standing practical limitation of the Stream Fusion shortcut deforestation system.

- Case Study: Proving Type-Class Laws
- Case Study: Making a Century
- Mechanized known Worker/Wrapper transformations from literature.

Type-class laws are properties expected to hold for class *instances*.

Example:

```
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
```

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

If proven, these are typically proven by hand.

As an example, prove the `return-left`

law for lists using HERMIT.

Begin by creating a Haskell program containing the law as GHC rewrite rule.

```
module Laws where
main :: IO ()
main = return ()
{-# RULES "return-left" [~] forall k x. return x >>= k = k x #-}
```

Then invoke HERMIT on this file:

`$ hermit Laws.hs`

The GHC rewrite rule can be turned into a HERMIT lemma.

The monad type parameter can be instantiated to lists.

Begin the proof and instantiate the dictionary parameters.