4 ms·

Thank you for your comments! I agree that type-directed synthesis would be very helpful. One of the inspirations for Barliman is the type-and-example-directed

Thank you for your comments! 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 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.

runeks 10y ago
I guess I don't quite understand the root purpose of program synthesis. It's my impression, as a programmer, that the difficult task is defining ones program logic without ambiguity. If this is indeed the case, then program synthesis already exists in the form of Coq, but it doesn't mean we've made programming easier, it means we've created a tool that reveals all possible failure points of a program, forcing us to consider all possible outcomes. It makes for a provably un-crashable program, but we pay for it in the time it takes to create the specification/implementation (which at this point have converged into one). 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).
- will_byrd 10y ago
  Good questions! > 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 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 http://webyrd.net/quines/quines.pdf https://github.com/webyrd/2012-scheme-workshop-quines-paper-code https://github.com/webyrd/2012-scheme-workshop-quines-paper-...
ahazred8ta 10y ago
Links: http://minikanren.org/ http://minikanren.org/ - https://twitter.com/webyrd https://twitter.com/webyrd - https://en.wikipedia.org/wiki/MiniKanren https://en.wikipedia.org/wiki/MiniKanren - http://stackoverflow.com/questions/tagged/minikanren http://stackoverflow.com/questions/tagged/minikanren -
- will_byrd 10y ago
  Thank you for posting the links! 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 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=zHov3fKYqBA https://www.youtube.com/watch?v=nFE2E91VDAk https://www.youtube.com/watch?v=nFE2E91VDAk
deleted 10y ago
[deleted]

runeks 10y ago

I guess I don't quite understand the root purpose of program synthesis. It's my impression, as a programmer, that the difficult task is defining ones program logic without ambiguity. If this is indeed the case, then program synthesis already exists in the form of Coq, but it doesn't mean we've made programming easier, it means we've created a tool that reveals all possible failure points of a program, forcing us to consider all possible outcomes. It makes for a provably un-crashable program, but we pay for it in the time it takes to create the specification/implementation (which at this point have converged into one). 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).

will_byrd 10y ago
Good questions! > 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 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 http://webyrd.net/quines/quines.pdf https://github.com/webyrd/2012-scheme-workshop-quines-paper-code https://github.com/webyrd/2012-scheme-workshop-quines-paper-...

ahazred8ta 10y ago

Links: http://minikanren.org/ http://minikanren.org/ - https://twitter.com/webyrd https://twitter.com/webyrd - https://en.wikipedia.org/wiki/MiniKanren https://en.wikipedia.org/wiki/MiniKanren - http://stackoverflow.com/questions/tagged/minikanren http://stackoverflow.com/questions/tagged/minikanren -

will_byrd 10y ago
Thank you for posting the links! 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 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=zHov3fKYqBA https://www.youtube.com/watch?v=nFE2E91VDAk https://www.youtube.com/watch?v=nFE2E91VDAk

deleted 10y ago

[deleted]