Lennart Augustsson (Standard Chartered Bank):
Putting Curry-Howard to work
It is a well known fact that there is a correspondence between propositions and type, and similarly a correspondence between a the proof of a proposition and a program of a type; this is the Curry-Howard correspondence. In this talk I will describe a program, Djinn, which takes a Haskell type and produces a program of that type, using the Curry-Howard correspondence. For the subset of Haskell types that Djinn can handle (no recursive types) it does quite well. For instance, it can derive the code for all the standard monads in Haskell, including continuations and call/cc.
Synthesis of Functions Using Generic Programming
Inductive programming aims to synthesize functions or programs from a small number of input-output pairs. In general there will by many functions that have the desired behaviour. From this family of solutions we are interested in the smallest or simplest function. In some situations there are (often well known) algorithms to construct such functions, for instance for fitting a linear function through a set of points in the R2. In general it is very hard to construct functions for arbitrary data types in this way. Instead of constructing a function that has the desired behaviour we use a generate-and-test based approach. Our system generates a sequence of more and more complex candidate functions, the system verifies if these candidates have the desired behaviour and yields the first candidate that passes this test. Since there are enormous many candidate functions one has to guide this search procedure in one way or another to synthesize the desired function in reasonable time.
In this paper we show how we can control the synthesis of candidate functions effectively by defining a tailor made data type for the grammar of the candidate functions. Instances of this data type are the abstract syntax trees of the candidate functions. The instances of these data types representing the candidate functions are generated by a generic algorithm. Instances of this synthesis algorithm for specific data types can be derived automatically by the compiler of the host language (the functional programming language Clean). It appears that the generic algorithm for generating instances of a data type that is used to generate test suites in the model-based test tool Gast is very effective to synthesize candidate functions in inductive programming.
In order to verify if a synthesized abstract syntax tree represents the correct function, the system needs to be able to execute it as a function. This is done by a user defined instance of a type class that transforms the abstract syntax tree to the corresponding function. These instances are always very simple. For a new application domain the user has to define the grammar of candidate functions as a data type and how instances of this data type are transformed to functions. The system synthesizes the instances and tests the candidates until one (or more) functions with the desired behaviour are found. This approach has been proven to be effective in generating small functional programs and lambda expressions.
Neil Mitchell (Standard Chartered Bank):
Deriving a DSL from One Example
Given an appropriate domain specific language (DSL), it is possible to describe the relationship between Haskell data types and many generic functions, typically type class instances. While describing the relationship is possible, it is not always an easy task. There is an alternative -- simply give one example output for a carefully chosen input, and have the relationship derived.