Toolkit for building proof automation systems.

Please see the README on GitHub at https://github.com/githubuser/refinery#readme

Refinery

refinery provides a series of language-independent building blocks for creating automated, type directed program synthesis tools. It is currently used to power the automatic code synthesis tool Wingman For Haskell.

Introduction

If you are already familiar with the idea of tactics, feel free to skip ahead to the Usage section.

What exactly do we do when we sit down and write a program? Sure, we may have lofty ideas about what it may do in the end, but I'm talking about the actual process of writing a program. For instance, take the following (rather silly) example:

pairing :: (a -> b) -> (a -> c) -> a -> (b,c)
pairing = _

The first thing we might do is look at the type, see that we are writing a function, and introduce the arguments.

pairing :: (a -> b) -> (a -> c) -> a -> (b,c)
pairing f g a = _

Then, we see that we are trying to make a pair type, so we will introduce a pair constructor.

pairing :: (a -> b) -> (a -> c) -> a -> (b,c)
pairing f g a = (_, _)

Then, we will see that we need to produce a b and a c, and we have two functions in scope that do that, so may as well try them!

pairing :: (a -> b) -> (a -> c) -> a -> (b,c)
pairing f g a = (f _, g _)

Now, we need an a, and we have one in scope, so let's use that!

pairing :: (a -> b) -> (a -> c) -> a -> (b,c)
pairing f g a = (f a, g a)

Now, this entire process of writing this function was entirely mechanical. We just looked at the type of the hole, looked at what we had in scope, and applied some simple edits to get some more holes, and repeated. This feels like we could automate this!

Now, a "tactic" is exactly this. We can think of it morally as something like the following type: (Type -> [Type], [Expr -> Expr]). In short, they break the hole down into a bunch of smaller holes, and combine expressions that fit into those holes into one big expression! This library provides the means for creating simple tactics for any language you can cook up, as well as "tactic combinators", which have a similar flavor to parser combinators. Parser combinators let us compose small atomic parsers together to form larger ones, and Tactic combinators let us compose together small tactics to create sophisticated tools for automatic program synthesis.

Usage

Let's walk through the usage of this library with a small example. The full source code of this example can be found in tests/Spec/STLC.hs.

First, let's import the main module, along with some MTL stuff:

import Data.List

import Control.Monad.Identity
import Control.Monad.State

import Refinery.Tactic

Now let's define a teeny tiny simply typed lambda calculus:

-- Expressions in simply typed lambda calculus, along with holes
data Term
  = Var String
  | Hole
  | Lam String Term
  | Pair Term Term
  deriving (Show, Eq)

-- Types in our version of simply typed lambda calculus
data Type
  = TVar String
  | Type :-> Type
  | TPair Type Type
  deriving (Show, Eq)

Now, we are going to need to define the idea of a "type in a context", commonly referred to as a "Judgement".

newtype Judgement = [(String, Type)] :- Type
  deriving (Show)

Now, a bit of boilerplate is required to tell refinery how to generate holes. Most of the time, you will need to have a fresh source of variables for your holes, or you may need to run effects when you generate them. However, in the name of simplicity, let's just use Identity

instance MonadExtract Term String Identity where
    hole = pure Hole
    unsolvableHole _ = pure Hole

Now for our first tactic:

type T a = TacticT Judgement Term String Int Identity a

-- Tactic for solving holes of type (a,b)
pair :: T ()
pair = rule $ \goal ->
    case goal of
      (hys :- TPair a b) -> Pair <$> subgoal (hys :- a) <*> subgoal (hys :- b)
      _                  -> unsolvable "goal mismatch: Pair"

Now, there is a lot going on here, so let's take it apart piece by piece: To start, let's look at TacticT. The first type parameter is the "goal" type. We can think of this as the thing that we are trying to "solve". For us, this is Judgement, as we are going to need to know exactly what is in scope at a given point.

The next type parameter is what the tactic is going to synthesize, commonly referred to as the "extract".

The next three type parameters are decidedly less exciting. They represent the type of errors, the type of the state, and the base monad. We need to have a way of generating unique names, so let's just use Int as our state to accomplish this.

That final type parameter is the type that the tactic during the course of execution. We will discuss this further in the future, so if you are confused, feel free to ignore this type parameter for now.

Next, we call rule to create a "basic" tactic, that lets us inspect the current goal, and create a bunch of subgoals via subgoal. As we are trying to tell refinery how to synthesize pairs, we case on the type of the hole. If it is a pair type, we create two new goals, one for each component of the tuple type, and then combine the solutions to those subgoals together with a pair constructor. If the type does not match, then we throw an error via unsolvable.

Now, finally, we need a way of solving goals of the form a -> b.

lam :: T ()
lam = rule $ \case
    (hys :- (a :-> b)) -> do
        name <- gets show
        modify (+ 1)
        body <- subgoal $ ((name, a) : hys) :- b
        pure $ Lam name body
    _                  -> unsolvable "goal mismatch: Lam"

This is where the state comes in. We look up the current state, show it for use as a name, and then increment it so that our names are unique. We then create a subgoal for b, and add our new fresh name into scope, specifying that it has type a. We then get the result of the subgoal and put it in a Lam constructor along with our fresh name.

Finally, let's define a tactic for solving a goal by using something in scope.

assumption :: T ()
assumption = rule $ \ (hys :- a) ->
  case find (\(_, ty) -> ty == a) hys of
    Just (x, _) -> pure $ Var x
    Nothing     -> unsolvable "goal mismatch: Assumption"

Now, for something really exciting. Let's write a tactic that can synthesize expressions for this language. Now that we have our building blocks, this is very easy!

auto :: T ()
auto = do
    many_ lam
    (pair >> auto) <|> assumption

Before explaining how exactly this works, let's look at what it does!

λ> solutions auto ([] :- (TVar "a" :-> TVar "b" :-> (TPair (TVar "a") (TVar "b")))) 0
> [Lam "0" (Lam "1" (Pair (Var "0") (Var "1")))]

As we can see, it generated the right thing! Let's now step through how exactly it did this. To start, many_ is a "tactic combinator". It takes a tactic as it's first argument, and will run it repeatedly until it fails. This will result in a single subgoal that looks something like

[("0", TVar "a"), ("1", TVar "b")] :- (TPair (TVar "a") (TVar "b"))

Now, for the magic. The bind for TacticT will run the second tactic on every subgoal created by the first. With this crucial piece of information, we can begin to see how auto works. Once many_ lam is executed, we execute both pair >> auto and assumption against the subgoal generated, and collect all of the solutions found by both branches together. pair will generate 2 subgoals, and then >> auto will apply auto recursively to both of those subgoals.

References

refinery is based roughly on Algebraic Foundations of Proof Refinement.