HERMIT: Mechanized Reasoning during Compilation in the Glasgow Haskell Compiler


Andrew Farmer
Dissertation Defense
Electrical Engineering and Computer Science
The University of Kansas
April 30, 2015


Advisor: Andy Gill

Introduction

Semi-formal Reasoning

pearls of functional algorithm design

Typically performed equationally:

reasoning fragment
Reasoning sample from The Worker/Wrapper Transformation

Semi-formal Reasoning

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

Semi-formal Reasoning

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

Proposal: Provide tool support!

Thesis

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

Thesis

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

Thesis

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

Thesis

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

Contributions

Along the way:

Contributions

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

Along the way:

Haskell Reasoning Tools

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

HERMIT

cabal update
cabal install hermit
image from http://www.angelfire.com/ks/larrycarter/LC/OldGuardCameron.html

GHC Core

GHC Core

Haskell vs GHC Core

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

GHC - Architecture

GHC architecture

HERMIT - Plugin

HERMIT Plugin

HERMIT - Architecture

HERMIT Architecture

Contributions

  • Demonstrates that semi-formal reasoning can be mechanized at compile time at a level of abstraction comparable to performing it by hand.

Along the way:

Evidence

Case Study: Proving Type-Class Laws

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.

Case Study: Proving Type-Class Laws

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

Case Study: Proving Type-Class Laws

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

Example Step 1

The monad type parameter can be instantiated to lists.

Example Step 2

Case Study: Proving Type-Class Laws

Begin the proof and instantiate the dictionary parameters.