I agree that type-directed synthesis would be very helpful. One of the inspirations for Barliman is the type-and-example-directed program synthesis by Peter-Michael Osera and Steve Zdancewic:
http://www.cis.upenn.edu/~stevez/papers/OZ15.pdf
I want to experiment with a typed version of Scheme (a mini-ML with s-expressions) to see how much types would improve synthesis. In previous work with Michael Ballantyne, Michael showed that adding types could significantly improve the synthesis capability of the relational interpreter used by Barliman.
The miniKanren constraint logic system used by Barliman can be use to write type checkers and type inferencers that can perform type habitation, similar in spirit to the Djinn system mentioned by Cybiote. This is a topic Oleg Kiselyov and Dan Friedman have explored, for example. I'm very interested in improving our ability to write more sophisticated type inferencers in miniKanren, and in using the inferencer to guide synthesis.
Part of the motivation for Barliman is to explore what can be done for dynamically typed languages. Perhaps something like soft typing or gradual typing would be useful in this context.
Another idea I want to explore is using high-level properties, as in property-based testing, or even software contracts, to help guide synthesis.
I should mention that Greg Rosenblatt has improved Barliman's synthesis abilities recently, by specializing the underlying relational interpreter, using techniques similar to those in the Mercury compiler. I need to update the documentation to show the improved synthesis, which still needs work in order to be useful.
I'm also working with Rob Zinkov and Evan Donahue on using stochastic search to improve miniKanren's synthesis ability.
I'm very much open to collaboration on Barliman, synthesis, relational interpreters/type inferencers, constraint logic programming, etc.
> It's my impression, as a programmer, that the difficult task is defining ones program logic without ambiguity.
Certainly the unambiguous specification of a program's behavior is a difficult task! Barliman's approach is to allow for the behavior of a function to be partially specified. That is, the specification of behavior is ambiguous, since the examples can only specify the intended behavior over a small number of inputs/expected outputs. Many other synthesis tools allow for ambiguous specification of behavior, and use heuristics such as parsimony (smallest program is assumed to be the correct choice) to pick one of infinitely many programs consistent with the partial specification.
The idea for Barliman is to make the writing/editing of the code interact with synthesis-by-example, in order to give the programmer continuous feedback on whether the current code is consistent with the tests, and hopefully to make a reasonable guess at any missing code. As the programmer fills in the code for a function, the search space shrinks. Still, there may be infinitely many definitions that satisfy the partial specification, so Barliman sometimes guesses a goofy definition!
I want to explore adding high-level properties, contracts, optional types, etc., to Barliman, to make it possible to specify the desired behavior in more detail. However, I want to make all of these specifications optional, to maintain the flexibility of a language like Scheme. I think this is still an under-explored area in program synthesis, especially given how much code is written in JavaScript, Python, Ruby, etc.
> If I can write a specification in a language that some tool can transform into a source code implementation (which can then be compiled and executed), then I wouldn't call that tool a "program synthesizer" but rather a "compiler" (and the specification language would then be a programming language).
It is true that if you completely specify/prove correct your program in Coq (for example), you can extract a running programming from that specification. This is an interesting and powerful technique, and is in many ways similar to a compiler, as you point out.
However, I don't think of this approach as program synthesis. In program synthesis I might give a non-constructive specification of a program's behavior, and ask the computer to find such a program. For example, I could completely specify what it means for a number `n` to be the square root of another number `m` without giving an algorithm to find `n`. If I know of such an algorithm, I may be able to prove it correct in Coq, and extract running code from Coq. However, I can't expect that Coq will find the algorithm for me. To me this is the difference between proving code correct and performing synthesis.
However, the division is somewhat murky--for example, some forms of synthesis can be used to prove correctness of the program. For example, a well-known example in miniKanren (the system Barliman uses for synthesis) is to generate a quine directly from the mathematical definition of a quine. A quine in Scheme is some expression `q` that evaluates to itself. In a relational Scheme interpreter implemented in miniKanren, we can generate quines by running the query:
(run n (q) (evalo q q))
Where `n` is the number of quines you would like to generate, `evalo` is the name of the relational Scheme interpreter, and `run` is miniKanren's interface operator. One of the quines generated is:
((lambda (_.0) (list _.0 (list 'quote _.0))) '(lambda (_.0) (list _.0 (list 'quote _.0))))
where `_.0` is a legal Scheme identifier. This expression is alpha-equivalent to the most famous Scheme quine (https://www.nyx.net/~gthompso/quine.htm).
In the case of quine generation, we are proving that the generated program is a quine by synthesizing it from its definition. (Assuming that both miniKanren and the relational Scheme interpreter are correct, of course!) We have also synthesized fixpoint combinators from their definitions in a similar fashion. Note that this approach is different from, but complimentary to, the synthesis-from-example approach used by Barliman.
If the quines example interests you, you might look at our paper and code from the 2012 Scheme Workshop:
William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012.
http://webyrd.net/quines/quines.pdf
https://github.com/webyrd/2012-scheme-workshop-quines-paper-...
For anyone interested in how the relational interpreter powering Barliman works, here is a short talk I gave at PolyConf last year:
https://www.youtube.com/watch?v=eQL48qYDwp4
And here is a much more in-depth two-part talk I gave at Lambda Lounge Utah:
https://www.youtube.com/watch?v=zHov3fKYqBA https://www.youtube.com/watch?v=nFE2E91VDAk
From skimming the page, it looks to me like an example of inductive programming.
So for Haskell, it would be closer to something like Djinn, where code is generated/proved from a type specification.
> So for Haskell, it would be closer to something like Djinn,
> where code is generated/proved from a type specification.
The high-level idea is that if you are going to take the trouble to specify the type of a function (as in Haskell), and tests that use the function (as in unit testing), and high-level properties of the function (as in Quickcheck), you may as well try to get the computer to actually generate the function for you, rather than writing it yourself.
You mentioned Coq above. Coq users rely on the `crush` tactic to try to fill in the boring details of a proof obligation. This is similar in spirit to search used in synthesis systems. If you can give the high-level specification, let the computer do the "boring" work. Of course, the boring work may be difficult or computationally expensive, and the high-level specification may be ambiguous...
So it's possible that this idea makes more sense for languages without a strong type system. In any case, trying to complete a partial function definition without looking at the native types of the language means you miss a lot of information, especially in the case of Haskell, where the types tell you so much, if not everything, you need to know about a function.