6 ms·

For anyone who finds this topic interesting, you might be interested in the following resources: http://minikanren.org/ http://minikanren.org/ The second edit

For anyone who finds this topic interesting, you might be interested in the following resources: http://minikanren.org/ http://minikanren.org/ The second edition of `The Reasoned Schemer` (MIT Press, 2018): https://mitpress.mit.edu/books/reasoned-schemer-second-edition https://mitpress.mit.edu/books/reasoned-schemer-second-editi... The Clojure/conj 2016 talk Greg Rosenblatt and I gave on Barliman: https://www.youtube.com/watch?v=er_lLvkklsk https://www.youtube.com/watch?v=er_lLvkklsk `A Unified Approach to Solving Seven Programming Problems (Functional Pearl)`, William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, Matthew Might (ICFP 2017) (Open Access): https://dl.acm.org/doi/10.1145/3110252 https://dl.acm.org/doi/10.1145/3110252 and the related talk: https://www.youtube.com/watch?v=o3AHnyEf7IE https://www.youtube.com/watch?v=o3AHnyEf7IE and Nada Amin's interactive version of the paper: http://io.livecode.ch/learn/namin/icfp2017-artifact-auas7pp http://io.livecode.ch/learn/namin/icfp2017-artifact-auas7pp Cheers, --Will

Y_Y 5y ago
Did anything ever come out of Barliman or other attempts to make an interactive interface around this stuff? It's such a cool concept, I'm surprised I never saw a mainstream IDE where I can write rough constraints or examples and have it generate code, just like in those really nice examples of minikanren from a few years back.
- will_byrd 5y ago
  This paper and prototype educational system was based on Barliman: `Towards Answering "Am I On the Right Track?" Automatically using Program Synthesis` Molly Q Feldman, Yiting Wang, William E. Byrd, François Guimbretière, & Erik Andersen. SPLASH-E 2019 https://mollyfeldman.github.io/splashe2019.html https://mollyfeldman.github.io/splashe2019.html This paper was at least partly inspired by the relational interpreter approach that is the foundation of Barliman: `From definitional interpreter to symbolic executor` Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. Proceedings of the 4th ACM SIGPLAN International Workshop on Meta-Programming Techniques and Reflection (META 2019) https://dl.acm.org/doi/10.1145/3358502.3361269 https://dl.acm.org/doi/10.1145/3358502.3361269 As for Barliman, we took a step back from imrpoving the interface, and started doing experiments with a bunch of colleagues on various ways to improve synthesis speed and expressiveness. Until COVID-19 got in the way, Kanae Tsushima and I were beginning to put some of the pieces back together in an improved Barliman, named `新-Barliman` (`Shin-Barliman`, `shin` meaning "new" in Japanese): https://github.com/k-tsushima/Shin-Barliman https://github.com/k-tsushima/Shin-Barliman I'm hoping we will make some real progress again soon!
  - Y_Y 5y ago
    I'm really glad to hear that! That's for contributing to produce this really cool work.
YeGoblynQueenne 5y ago
Hi, Will. I noticed this: >> Your program can be more efficient, you can have more expressive control but if you are not careful, your program can be unsound. In other words: there may be an answer to your query that you do not find. So an analogy would be in a database lookup. If you are doing a database query, maybe there is actually information in a table that you should find, but you do not find it. To clarify, that's incompleteness. Unsoundness is when an inference rule returns wrong results. Incompleteness is where it doesn't return all correct results. As you say, unification without an occurs check is unsound and Prolog's depth-first search is incomplete. I wanted to ask, because you brought it up in the interview, how does minikanren (or minikanrens?) handle the occurs check? You said that you are interested in trying to push the relational aspect as far as possible, recognising that this gives up efficiency - can you quantify to what extent minikanren gives up efficiency and generally say a bit more about the trade-off between (if I understand it correctly) efficiency and relational (declarative?) purity?
- will_byrd 5y ago
  Hi YeGoblynQueenne, I always read your logicy comments and posts--thank you! > To clarify, that's incompleteness. Unsoundness is when an inference rule returns wrong results. Incompleteness is where it doesn't return all correct results. As you say, unification without an occurs check is unsound and Prolog's depth-first search is incomplete. Thank you. Yes, I misspoke. For anyone interested, this video gives a nice overview of soundness and completeness, in the context of logic: https://www.youtube.com/watch?v=HeQX2HjkcNo https://www.youtube.com/watch?v=HeQX2HjkcNo > I wanted to ask, because you brought it up in the interview, how does minikanren (or minikanrens?) handle the occurs check? You said that you are interested in trying to push the relational aspect as far as possible, recognising that this gives up efficiency - can you quantify to what extent minikanren gives up efficiency and generally say a bit more about the trade-off between (if I understand it correctly) efficiency and relational (declarative?) purity? miniKanren performs unification with the occurs check. This is one of the tradeoffs miniKanren makes: sound unification, but it can be expensive. The interleaving complete search is another tradeoff: the search uses more time and memory than does depth-first-search, in those cases in which DFS would be sufficient. Another tradeoff is that miniKanren avoids the use of non-logical / extra-logical operators. There are no cuts, projected variables, var tests, etc., in the pure parts of the language (which is the version I always use). If you want to perform arithmetic, you either have to encode arithmetic as a pure relation (as Oleg Kiselyov has done), or add a fully-relational constraint system for arithmetic to miniKanren (as we did in cKanren). Or, you can add a delayed goals mechanism, although this can lose completeness. There are lots of variants of miniKanren at the this point: alphaKanren (nominal logic programming); cKanren (constraints); probKanren (prototype probabilistic Kanren); dbKanren (Greg Rosenblatt's extension to handle graph database operations, used in mediKanren 2); etc. I hope we can integrate all of the features into a single implementation some day. Cheers, --Will
kamaal 5y ago
Hi Will, Do you any plans for writing a book on MiniKanren for Enterprise programmers? - Kamaal.
- will_byrd 5y ago
  Hi Kamaal! I know Cisco is using core.logic, which is David Nolen's Clojure variant of miniKanren, in their ThreatGrid product. I think the Enterprisey uses of mediKanren are a bit different than the purely relational programming that I find most interesting, though. Having said that, we are now on our second generation of mediKanren, which is software that performs reasoning over large biomedical knowledge graphs: https://github.com/webyrd/mediKanren/tree/master/medikanren2 https://github.com/webyrd/mediKanren/tree/master/medikanren2 mediKanren is being developed by the Hugh Kaul Precision Medicine Institute at the University of Alabama at Birmingham (HKPMI). HKPMI is run by Matt Might, who you may know from his work on abstract interpretation and parsing with derivatives, or from his more recent work on precision medicine. mediKanren is part of the NIH NCATS Biomedical Data Translator Project, and is funded by NCATS: https://ncats.nih.gov/translator https://ncats.nih.gov/translator Greg Rosenblatt, who sped up Barliman's relational interpreter many order of magnitude, has been hacking on dbKanren, which augments miniKanren with automatic goal reordering, stratified queries/aggregation, a graph database engine, and many other goodies. dbKanren is the heart of mediKanren 2. I can imagine co-writing a book on mediKanren 2, and its uses for precision medicine... Cheers, --Will
  - rscho 5y ago
    As an MD, I would be extremely interested in such a book! I'm a big fan of yours :-) I'm still working on my adaptation of MiniKanren for unification over multidimensional array terms, BTW. I hope to get it really working, someday. Cheers!
agumonkey 5y ago
Hi, thanks for spreading ideas and doing videos. What's new in the relational field ?
siddboots 5y ago
Hi Will! Your talks really left a mark on me and I’ve been playing around with relational programming stuffs ever since. Thank you! While you’re here... Has there been any progress on support for rational numbers (or other number systems) in pure minikanren? I’ve always wanted to have a crack at it, but have no idea if it has already been done.

Y_Y 5y ago

Did anything ever come out of Barliman or other attempts to make an interactive interface around this stuff? It's such a cool concept, I'm surprised I never saw a mainstream IDE where I can write rough constraints or examples and have it generate code, just like in those really nice examples of minikanren from a few years back.

will_byrd 5y ago
This paper and prototype educational system was based on Barliman: `Towards Answering "Am I On the Right Track?" Automatically using Program Synthesis` Molly Q Feldman, Yiting Wang, William E. Byrd, François Guimbretière, & Erik Andersen. SPLASH-E 2019 https://mollyfeldman.github.io/splashe2019.html https://mollyfeldman.github.io/splashe2019.html This paper was at least partly inspired by the relational interpreter approach that is the foundation of Barliman: `From definitional interpreter to symbolic executor` Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. Proceedings of the 4th ACM SIGPLAN International Workshop on Meta-Programming Techniques and Reflection (META 2019) https://dl.acm.org/doi/10.1145/3358502.3361269 https://dl.acm.org/doi/10.1145/3358502.3361269 As for Barliman, we took a step back from imrpoving the interface, and started doing experiments with a bunch of colleagues on various ways to improve synthesis speed and expressiveness. Until COVID-19 got in the way, Kanae Tsushima and I were beginning to put some of the pieces back together in an improved Barliman, named `新-Barliman` (`Shin-Barliman`, `shin` meaning "new" in Japanese): https://github.com/k-tsushima/Shin-Barliman https://github.com/k-tsushima/Shin-Barliman I'm hoping we will make some real progress again soon!
- Y_Y 5y ago
  I'm really glad to hear that! That's for contributing to produce this really cool work.

YeGoblynQueenne 5y ago

Hi, Will. I noticed this: >> Your program can be more efficient, you can have more expressive control but if you are not careful, your program can be unsound. In other words: there may be an answer to your query that you do not find. So an analogy would be in a database lookup. If you are doing a database query, maybe there is actually information in a table that you should find, but you do not find it. To clarify, that's incompleteness. Unsoundness is when an inference rule returns wrong results. Incompleteness is where it doesn't return all correct results. As you say, unification without an occurs check is unsound and Prolog's depth-first search is incomplete. I wanted to ask, because you brought it up in the interview, how does minikanren (or minikanrens?) handle the occurs check? You said that you are interested in trying to push the relational aspect as far as possible, recognising that this gives up efficiency - can you quantify to what extent minikanren gives up efficiency and generally say a bit more about the trade-off between (if I understand it correctly) efficiency and relational (declarative?) purity?

will_byrd 5y ago
Hi YeGoblynQueenne, I always read your logicy comments and posts--thank you! > To clarify, that's incompleteness. Unsoundness is when an inference rule returns wrong results. Incompleteness is where it doesn't return all correct results. As you say, unification without an occurs check is unsound and Prolog's depth-first search is incomplete. Thank you. Yes, I misspoke. For anyone interested, this video gives a nice overview of soundness and completeness, in the context of logic: https://www.youtube.com/watch?v=HeQX2HjkcNo https://www.youtube.com/watch?v=HeQX2HjkcNo > I wanted to ask, because you brought it up in the interview, how does minikanren (or minikanrens?) handle the occurs check? You said that you are interested in trying to push the relational aspect as far as possible, recognising that this gives up efficiency - can you quantify to what extent minikanren gives up efficiency and generally say a bit more about the trade-off between (if I understand it correctly) efficiency and relational (declarative?) purity? miniKanren performs unification with the occurs check. This is one of the tradeoffs miniKanren makes: sound unification, but it can be expensive. The interleaving complete search is another tradeoff: the search uses more time and memory than does depth-first-search, in those cases in which DFS would be sufficient. Another tradeoff is that miniKanren avoids the use of non-logical / extra-logical operators. There are no cuts, projected variables, var tests, etc., in the pure parts of the language (which is the version I always use). If you want to perform arithmetic, you either have to encode arithmetic as a pure relation (as Oleg Kiselyov has done), or add a fully-relational constraint system for arithmetic to miniKanren (as we did in cKanren). Or, you can add a delayed goals mechanism, although this can lose completeness. There are lots of variants of miniKanren at the this point: alphaKanren (nominal logic programming); cKanren (constraints); probKanren (prototype probabilistic Kanren); dbKanren (Greg Rosenblatt's extension to handle graph database operations, used in mediKanren 2); etc. I hope we can integrate all of the features into a single implementation some day. Cheers, --Will

kamaal 5y ago

Hi Will, Do you any plans for writing a book on MiniKanren for Enterprise programmers? - Kamaal.

will_byrd 5y ago
Hi Kamaal! I know Cisco is using core.logic, which is David Nolen's Clojure variant of miniKanren, in their ThreatGrid product. I think the Enterprisey uses of mediKanren are a bit different than the purely relational programming that I find most interesting, though. Having said that, we are now on our second generation of mediKanren, which is software that performs reasoning over large biomedical knowledge graphs: https://github.com/webyrd/mediKanren/tree/master/medikanren2 https://github.com/webyrd/mediKanren/tree/master/medikanren2 mediKanren is being developed by the Hugh Kaul Precision Medicine Institute at the University of Alabama at Birmingham (HKPMI). HKPMI is run by Matt Might, who you may know from his work on abstract interpretation and parsing with derivatives, or from his more recent work on precision medicine. mediKanren is part of the NIH NCATS Biomedical Data Translator Project, and is funded by NCATS: https://ncats.nih.gov/translator https://ncats.nih.gov/translator Greg Rosenblatt, who sped up Barliman's relational interpreter many order of magnitude, has been hacking on dbKanren, which augments miniKanren with automatic goal reordering, stratified queries/aggregation, a graph database engine, and many other goodies. dbKanren is the heart of mediKanren 2. I can imagine co-writing a book on mediKanren 2, and its uses for precision medicine... Cheers, --Will
- rscho 5y ago
  As an MD, I would be extremely interested in such a book! I'm a big fan of yours :-) I'm still working on my adaptation of MiniKanren for unification over multidimensional array terms, BTW. I hope to get it really working, someday. Cheers!

agumonkey 5y ago

Hi, thanks for spreading ideas and doing videos. What's new in the relational field ?

siddboots 5y ago

Hi Will! Your talks really left a mark on me and I’ve been playing around with relational programming stuffs ever since. Thank you! While you’re here... Has there been any progress on support for rational numbers (or other number systems) in pure minikanren? I’ve always wanted to have a crack at it, but have no idea if it has already been done.