This tutorial introduces the features of a basic program synthesis tool of Granule for automatically generating programs from linear and graded modal types. Please refer to our LOPSTR 2020 paper Resourceful program synthesis from graded linear types (pre-proceedings version) for more details if you are interested in the theory and implementation of the synthesis tool.
First, you'll need to install Granule. You can find the guide to installing the latest realease of Granule here.
We recommend using VS Code along with the Granule VS Code extension. This tool has several useful shortcuts for Granule, including synthesis.
See the documentation on how to use the interpreter. If you are new to Granule, then we recommend going through the Granule tutorial.
The synthesis functionality covered in this tutorial is still very much a work in progress so please do raise an issue if something doesn't behave as expected.
Now let's see how we can synthesise programs from linear and graded modal types!
Let's begin with a simple example, which shows how linearity and graded modalities affect our ability to synthesise programs.
Say we want to write a function which takes some input of type a
and simply duplicates it, producing a
pair of values of type a
. We can start writing this function in Granule by giving the type, like so:
copy : ∀ a . a → (a × a)
copy = ?
Here, the ?
represents a "hole" in place of an implementation. The synthesis tool can be invoked on this hole and will
attempt to fill it based on the type
we've given for copy
. Place the cursor over and use the keyboard shortcut Ctrl-e Ctrl-e
(from the Granule
VS Code extension) to synthesise. For the type we've given for copy
, what should we expect the result to be?
... there isn't one! This is because the type we gave for copy
is uninhabited. Remember, Granule uses a linear type system, where
values must be used exactly once. In copy
, we use a
twice, violating linearity. This means that we cannot synthesise an implementation
for this version of copy
. Here we see an example of where synthesis can help guide the design of our programs: the failure to synthesise a
program suggests that there may be something wrong with out type!
We can fix the type of copy
through the use of a graded modal type. Consider the type of copy'
below:
copy' : ∀ a . a [2] → (a × a)
copy' = ?
Our input a
is now graded by 2, drawing from the natural numbers semiring for tracking
exact usage of values inside a program. We still don't have an implementation, so we've put
another hole ?
. We can now synthesise an implenetation for copy'
by pressing Ctrl-e Ctrl-e
, giving us:
copy' : ∀ a . a [2] → (a × a)
copy' [y] = (y, y)
Success! The hole has been replaced by a program which adheres to the type of copy'
. By pattern matching on
the input value (of type a [2]
), we obtain a value y
which we have the capability to use exactly twice, which we use up by
using them to construct a pair. Here we have seen a really simple example of synthesis with linear and graded modal types. In the next section,
we'll build on this to synthesise more complex programs using different semirings available in Granule.
At the moment, synthesis is still in a proof-of-concept state in Granule. Consequently, the synthesis tool can only be used on a subset of the full Granule language. This will change very soon, however, so stay tuned!
So what types can we use in synthesis? We have already seen that we can use linear function types (→
), product types (×
), and graded modal types. In addition
to these we can also synthesise from unit types (()
) and sum types. To synthesise with sum types, we either have to import the Either
data type from the Granule standard library by import Either
at the start of our Granule file, or re-implement the data type in the file itself:
data Either a b where Left a | Right b
Note that currently the synthesis tool is hardcoded to use the above type and constructor names for sum types!
Now that we know what types we can synthesise from, let's take a look at some of the other graded modalities that we can use.
We've already seen the natural numbers semirings for tracking exact usage of values in our example for copy'
. But sometimes, we need more
flexibility and the ability to approximate usages of values inside a program. This is where the intervals semiring is useful. Interval graded modalities
have the form [x..y]
. where x
represents a lower bound on usage and y
an upper bound. For example, if we had a value graded by the interval [2..4]
, then we have to use it at least twice, and anywhere up to four times. Let's incorporate what we've learned about the types we can use in synthesis with this new semiring to synthesise a function that eliminates a sum type. In this semiring, our graded modalities will be drawn from intervals over the natural numbers:
import Either
sumElim : ∀ a, b, c . Either a b → (a → c) [0..1] → (b → c) [0..1] → c
sumElim = ?
Here, we have an input type Either a b
and we want to end up with something of type c
.
We have two additional functions as inputs with types (a → c) [0..1]
and (b → c) [0..1]
, both of
which are graded by [0..1]
. This means we can use each of these functions either once or not at all.
Using the synthesis tool, we get an implementation for this function:
import Either
sumElim : ∀ a, b, c . Either a b → (a → c) [0..1] → (b → c) [0..1] → c
sumElim (Left x) [u] [v] = u x
sumElim (Right y) [u] [v] = v x
Pattern mathing on the cases of the Either
, we simultaneously unbox the two auxilliary functions, allowing us to use them as their interval grades permit.
For the two sum type constructors, Left
and Right
, we then apply the relevant function to get something of type c
as our result. The interval grades are
required here because we only use one of the functions in each branch, so we need to have the capability to discard them for the branch where they are not used.
Up until now we have been synthesising programs from types using graded modalities which draw from one of Granule's built-in semirings. However, we can go further that this! As well as being able to synthesise programs from types which have multiple semirings in the same type, we can also synthesise programs from types which are polymorphic in their semiring. Let's take a look at an example:
push : ∀ a, b : Type, s : Semiring, c : S . (a × b) [c] → (a [c] × b [c])
push = ?
From the type of push
, we can see that it is a function which takes a pair of values graded by grade c
, drawing from an arbitrary semiring, and returns a pair where the constituent elements of the pair have the same types as the input, except both are now graded by c
, rather than the whole pair. Synthesing an implentation for push
, we get the following program:
push : ∀ a : Type, s : Semiring, c : S . (a × b) [c] → (a [c] × b [c])
push [(x, y)] = ([x], [y])
Such a function comes in useful when we are composing functions together, whose grades might not match up, requiring us to do some manipulation to make things fit together. For example, imagine we had a function which projects the first element of a pair:
fst : ∀ a, b : Type . (a × b [0]) → a
fst (x, [y]) = x
The second element of the pair must be graded by 0
, allowing us to discard it and return only the first element. But say we had a pair of values which is graded by an interval grade (a × b) [0..1]
, and we wanted to project the first element. We can't use our already defined fst
function as the types don't match. We could write another version of fst
specialised to this scenario, but we'd rather not. However, what we can do is distribute the grade of our pair over the pair's constituent elements using the push
, giving us a pair of type (a [0..1] × b [0..1])
. We can then simply apply fst
to this resulting pair as the types now align. Essentially, we have gone from having a pair where we have the capability to use the entire pair 0
to 1
times, to a pair where we can use each constituent element between 0
to 1
times.
This program we synthesised above is an example of a distributive law for product types. We find that such an operation is not uncommon when programming with graded modal types, and that we can actually derive these distributive combinators automatically for most data types. For more information on this, we recommend reading the TLLA-Linearity 2020 paper Deriving distributive laws for graded linear types.
So far we have used the Ctrl-e Ctrl-e
command from the Granule VS Code extension to synthesise
programs from holes. Alternatively, we can invoke the synthesis tool from the command line via the
--synthesise
and --rewrite-holes
flags when compiling a Granule file using gr
. For example:
gr myFile.gr --synthesise --rewrite-holes
Running the tool this way will attempt to synthesise a program for each hole in the Granule file. The additional flags
--hole-line
and --hole-column
can be used to specifiy a specific hole to synthesise a program for, leaving the other holes untouched. For example:
gr myFile.gr --synthesise --rewrite-holes --hole-line 3 --hole-column 8
will attempt to synthesise a program for a hole at line 3 and column 8 in myFile.gr
. If no such hole exists here then the synthesis tool will not be invoked.
The program synthesis tool presented here is actually paramterised by a resource management scheme, which alters the approach that the synthesis algorithm takes
towards managing the available resources it can synthesise programs from. The resource management scheme can have a considerable affect on the efficiency of the synthesis tool. By default, the additive approach is used. The subtractive approach can be used instead by including the --substractive
flag when synthesising via the command line. Additionally, there is an alternative additive approach called additive pruning, which can be used by including the --alternate
flag. For further information on resource management, how these schemes work, and the implications they have for performance, we recommend reading the LOPSTR 2020 paper.
That's it for now! Currently, the synthesis tool is being updated to allow synthesis from arbitrary user defined ADTs/GADTs and to include synthesis of recursive function definitions. We are also working on making the integration of synthesis into Granule more user-friendly.