[HN Gopher] What Is miniKanren?
___________________________________________________________________
What Is miniKanren?
Author : Bluestein
Score : 168 points
Date : 2025-01-02 13:15 UTC (9 hours ago)
(HTM) web link (minikanren.org)
(TXT) w3m dump (minikanren.org)
| mentalgear wrote:
| anyone else clicked because they read "miniKaren" ? :P
| laidoffamazon wrote:
| Minikanren was the subject of a phenomenal talk by Matt Might for
| it's applications in medicine
|
| [0] https://www.janestreet.com/tech-talks/algorithm-for-
| precisio...
| Bluestein wrote:
| ... wherein:
|
| "It will demonstrate progress to date, including the now-
| routine use of relational programming in miniKanren to identify
| personalized treatments for patients with some of the rarest
| and most challenging diseases in the world."
|
| ... wherefrom I cannot help but be amazed at how
| personalization through data optimization apparently actually
| helps solve such things and _can_ be an approach.-
| smeej wrote:
| A couple years ago, I tried to wrap my poor little non-
| developer head around how to use this, because I have a handful
| of things going on medically that seem (to me) to be connected,
| but I can't manage to get any doctors to care enough to help me
| figure out, but I was hopelessly out of my depth.
|
| Normally I can at least figure out how to _use_ something, even
| if I don 't understand how it works under the hood, but with
| this, I couldn't even figure out the next step.
| worldsayshi wrote:
| You might have better luck if you try today using Claude as
| support?
| will_byrd wrote:
| Alas, you'd still need the knowledge graphs. I hope the
| licensing issues for at least some of the KGs will be
| resolved soon. It's a tricky issue. Even some of the
| ontologies and controlled vocabularies in biomedicine can't
| be released publicly due to copyright restrictions (for
| example, full SemMedDB uses UMLS which uses SNOMED).
| will_byrd wrote:
| Sorry about that.
|
| mediKanren's source code is under MIT license, and is on
| GitHub. Alas, the knowledge graphs we use for mediKanren
| aren't produced by us, and often have very complex licenses
| (one KG might include knowledge from 80 or 100 databases,
| each with a different license). As a result, we can't just
| release the KGs that are needed to actually use mediKanren.
| Also, creating high-quality queries that take into account
| all the nuances and quirks of the KGs is tricky, and changes
| as the KGs and the Biolink standard evolve. As a result,
| mediKanren requires some expertise to use effectively, along
| with access to the KGs.
|
| An application that uses mediKanren as a back-end (along with
| other reasoners) is the NIH NCATS Biomedical Data Translator:
|
| https://ui.transltr.io/
|
| Please keep in mind that both Translator and mediKanren are
| designed for researchers and for biomedical research, not for
| patient care or treatment recommendations.
| smeej wrote:
| It's surprisingly reassuring to realize it wasn't actually
| my fault that I couldn't figure it out. Thanks for
| explaining! I'll look into Translator and see if I can get
| anywhere that way.
| isoprophlex wrote:
| That was an incredible read, a real-life Dr. House episode. And
| very exciting technology, too. Thanks for sharing.
| riffraff wrote:
| fantastic talk, thanks for sharing.
| z5h wrote:
| Implementing and using a miniKanren was fun and enlightening. And
| it helped me appreciate how incredibly optimized and fast SWI-
| Prolog is for relational/logical programming. If someone knows of
| a miniKanren/language combination that outperforms SWI-Prolog and
| has good developer ergonomics for relational/logical programming,
| I'd love to hear about it.
| cess11 wrote:
| IIRC SWI-Prolog can be embedded in Python if that's your thing.
| Interfacing with Scryer Prolog might be require a bit more but
| ought to be doable, and if they haven't surpassed SWI in some
| performance metrics yet I'd be surprised.
|
| I'm kind of a lisper but I find it easier to get things done in
| a proper Prolog than the kanrens.
| upghost wrote:
| It hasn't been merged into the main branch yet, but you can
| embed Scryer in Python now[1], and it's quite enjoyable. I've
| also embedded in Java, Clojure, and elisp[2] :)
|
| The Clojure one is bundled up into a library called
| libscryer-clj, which I haven't released yet, but it operates
| the same way as libpython-clj[3], libjulia-clj[4], and
| libapl-clj[5].
|
| As an aside, Scryer is hella ergonomic. clpz+reif is an
| amazing and amazingly powerful combination, and Scryer's DCG
| philsophy over double quoted strings is _chefs kiss_ -- it
| really delivers on the original mission of Prolog.
| Ediprolog[6] is a fantastic REPL for Emacs.
|
| And honestly if you haven't seen Marcus Triska's work[7], by
| God you are missing out on one of the true joys of life.
|
| [1]: https://github.com/jjtolton/scryer-
| prolog/blob/ISSUE-2464/sc...
|
| [2]: https://github.com/mthom/scryer-prolog/discussions/2687
|
| [3]: https://github.com/clj-python/libpython-clj
|
| [4]: https://github.com/cnuernber/libjulia-clj
|
| [5]: https://github.com/jjtolton/libapl-clj
|
| [6]: https://www.metalevel.at/ediprolog/
|
| [7]: https://www.youtube.com/@ThePowerOfProlog
| jasonhemann wrote:
| I was going to mention how cool JJs work is. Upvote to all
| those links.
| will_byrd wrote:
| Hi! I'm one of the miniKanren peeps. Happy to talk miniKanren and
| relational programming!
| eihli wrote:
| Hey! Thanks for all of the work you do. I love reading your
| stuff.
|
| Lately, I've been playing a lot with the code from Neural
| Guided Constraint Logic Programming for Program Synthesis [1].
| I want to apply it to searching for neural network
| architectures. Something like: (define-
| relation (layero layer in out) ;; [2] (conde
| ((== layer `(Linear ,in ,out))) ((== layer `(Relu ,in
| ,out)) (== in out)) ((fresh (percent)
| (== layer `(Dropout ,in ,out ,percent)) (== in
| out) (countero percent) (<o '(1)
| percent) (<o percent '(0 0 1 0 0 1 1))))))
|
| And a `layerso` that is just a sequence of `layers`. And then
| use some metric that captures how effective the training run
| was and use that metric for teaching the search network.
|
| I'm sure there's better ways to do it than the way I'm going
| about it. But it's a fun way to learn a bunch of cool new
| stuff.
|
| Thanks for getting me started down this path!
|
| [1] https://arxiv.org/abs/1809.02840
|
| [2]
| https://github.com/eihli/reason/blob/523920773b7040325c8098a...
| anotherhue wrote:
| Love your talks! The enthusiasm is infectious.
| simonw wrote:
| I have a feature request for the https://minikanren.org/
| website: just one prominent block of example code on that
| homepage (as early as possible) would be REALLY useful for
| helping understand at a glance what kind of language this is.
|
| I even clicked through quite a few of those prominent early
| links and didn't find a code example!
| ffsm8 wrote:
| Is that even possible for something like this? You've got a
| pretty long list of implementations, each having its own
| language specific syntax, e.g.
| https://github.com/pythological/kanren for one python version
| - and there are several Python versions linked on the
| homepage.
| simonw wrote:
| In that case an example box with tabs at the top -
| "miniKanren in Python / Go / Ruby" or whatever - would
| really help illustrate that point.
| will_byrd wrote:
| Thank you for the feedback!
|
| We are working on a new version of the website, with
| HTTPS, and with better examples and a better layout.
|
| I love your blog posts on LLMs, BTW! We've been
| experimenting with combining LLMs and miniKanren in
| various ways.
| kazinator wrote:
| I'm interested in a miniKanren port, or something like it, to
| TXR Lisp. I would possibly make it a part of the standard
| library of the language, so programs could rely on it just
| being there.
| selimthegrim wrote:
| I wonder if this might be able to help make LLM output
| compliant to a schema you can reverse engineer from an API
| endpoint like NEMSIS.
| BoingBoomTschak wrote:
| Personally, I wasn't a fan of The Reasoned Schemer's format,
| https://io.livecode.ch/learn/webyrd/webmk worked better as my
| introduction.
|
| See also: uKanren
| (http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf) and
| various ports like CL (https://github.com/rgc69/si-kanren) or
| Clojure (https://github.com/clojure/core.logic)
| will_byrd wrote:
| Here's another miniKanren-related livecode you might enjoy
| (both are thanks to Nada Amin's cool livecode.io tech!):
|
| https://io.livecode.ch/learn/gregr/icfp2017-artifact-auas7pp
| BoingBoomTschak wrote:
| Thanks. Personally, I'd love to see more like https://alex-
| hhh.github.io/2021/08/fish-puzzle.html
|
| When I was in university, the usual Prolog example was
| solving a game of Cluedo.
| noisy_boy wrote:
| Is using miniKanren the only way to solve the fish-puzzle?
| If no, which language will be most ergonomic and accessible
| to solve it?
| shakna wrote:
| Pascal and Common Lisp were employed in the old benchmark
| assessment [0]. So just about anything should be able to.
|
| But I'd expect many solver languages to be able to make
| it easier, like Prolog, datalog, mercury.
|
| [0] http://cse.unl.edu/~choueiry/Documents/Hybrid-
| Prosser.pdf
| jasonhemann wrote:
| I think there'll be all manner of constraint and
| constraint-logic programming approaches that'd be
| amenable. I wish I had a great answer for you as "the
| best".
|
| IMO, these "zebra puzzle"/"einstein puzzle" style
| problems are like a "hello world" for many related
| techniques. What's more, there are many languages that
| combine several of these techniques together so that you
| can easily pick and choose where appropriate.
|
| If you were just wanting to compare against _another_
| related style, answer-set programming is one thing that
| comes to mind.
| Jtsummers wrote:
| Like most things in programming, there is no "only way"
| to solve something, and certainly no one language (or
| DSL) to solve anything. You could solve it
| programmatically in C writing your own backtracker or
| state enumerator and a validation function for the rules
| (or block of code if you are like an old coworker that
| liked 10k SLOC C functions).
|
| miniKanren, Prolog, and others let you write the rules
| more concisely (almost always) and clearly (most of the
| time, not everyone will write clear code and clarity is
| subjective) than that, though.
| fud101 wrote:
| I wish I was smart enough to understand this. I printed out the
| paper and tried real hard to understand but felt hopelessly out
| of my depth.
| will_byrd wrote:
| Hi! Which paper were you trying to read?
|
| I'd be happy to try to explain anything you found confusing.
|
| Perhaps this online tutorial would be a helpful start:
|
| https://io.livecode.ch/learn/webyrd/webmk
| layer8 wrote:
| The main problem is likely that many programmers aren't
| familiar with Scheme, or any kind of Lisp. So the material is
| presented in the context of a host language that itself
| requires substantial effort to really get used to.
|
| Personally, while I did some Lisp back in university and was
| reasonably conversant in it at the time, nowadays whenever
| something nontrivial is presented in Lisp, it's just too much
| mental overhead to get back into it, in addition to trying to
| understand the thing that is being presented.
|
| Terminology like "logic variable" also needs to be explained,
| if you want to address an audience that isn't already
| familiar with logic programming.
| marcosdumay wrote:
| If you are struggling to learn the language, you may have
| better luck learning Prolog first. So you don't deal with the
| added complexity of it being embedded in a completely unrelated
| language.
|
| And remember this language for when, after you know Prolog, you
| start to see how it applies nicely to parts of everything you
| write, but it completely unsuitable for solving the entirety of
| almost any problem.
| jasonhemann wrote:
| You totally absolutely are smart enough to understand this.
| Possibly overly so! Happy to jump on a call and answer
| questions, if useful!
| adz5a wrote:
| The paper on microKanren [1] is imho the most approachable
| piece outside the "reasoned schemer" [2]. The thesis on which
| it is based is also interesting but is a thicker beast. Looking
| at stuff from the clojure world (clojure.core.logic and this
| talk [3]) is also interesting imho, especially from a dev
| perspective. From this point of view I found this talk [4] to
| be especially enlightening in how to build a database / query
| engine and concrete applications of MiniKanren / datalog.
|
| [1] https://github.com/jasonhemann/microKanren
|
| [2] https://mitpress.mit.edu/books/reasoned-schemer-second-
| editi...
|
| [3]
| https://www.youtube.com/watch?v=irjP8BO1B8Y&ab_channel=Cloju...
|
| [4]
| https://www.youtube.com/watch?v=y1bVJOAfhKY&t=10s&ab_channel...
| emmelaich wrote:
| I looked at the tutorial and choked at the first step.
|
| First it says "== unifies two terms". Then the first example
| says "(== x z) (== 3 y)" _associates_ x with z and y with 3.
| Are "unify" and "associate" the same thing? Why use different
| words? Why does the association reverse for x and z vs 3 and y?
| Is it commutative?
| tmtvl wrote:
| They are commutative. As to whether unification and
| association are the same thing... yes, kinda. Unifying two
| terms kinda means associating them with each other in a
| database. Though I will say that it would have been better to
| say 'unifies x and z, as well as y and 3'.
| Arnavion wrote:
| Unification in the context of logic programming is basically
| like "use these questions and solve for all the unknowns" in
| algebra, except it's done with logical statements instead of
| algebraic equations. Searching for something like
| "unification prolog" (Prolog being the most well-known logic
| programming language) will probably give helpful material.
|
| For example you could start with two facts like "Fedora is
| red." and "Cat is green." Then if you ask the system "X is
| red." it'll tell you "X = fedora". If you ask it to list all
| the solutions of "X and Y are not the same color." it'll list
| "X = fedora, Y = cat" and "X = cat, Y = fedora". This process
| of binding variables to values (or other variables during
| simplification) is unification.
| chriswarbo wrote:
| Unification is reflexive: (== x x) = x for
| all x
|
| It is commutative: (== x y) = (== y x) for
| all x and y
|
| It is idempotent: (== x (== x y)) = (== x
| y) for all x and y
|
| And it is associative: (== x (== y z)) =
| (== (== x y) z)
|
| It's _not_ transitive, e.g. if we unify pairs (using made up
| syntax [a, b]) then (== [x, 1] [2, y]) =
| [2, 1] (== [2, y] [z, 3]) = [2, 3] (== [x, 1]
| [z, 3]) does not unify (since 1 does not unify with 3)
| ergeysay wrote:
| I found sokuza-kanren [0] to be a wonderful introduction. It
| starts with the absolute basics and builds into a minimal logic
| system through a series of well-documented steps.
|
| [0] https://github.com/miniKanren/sokuza-kanren
| riku_iki wrote:
| but one need to learn lisp to read it?..
| jasonhemann wrote:
| What's your preferred PL? I suspect we could do a similar
| build-it-up in that lang too.
| riku_iki wrote:
| I personally code in c++, java and python.
|
| I think python is the most common and simple language
| with majority of devs would understand for concepts
| learning, but it is likely too slow for practical
| applications.
| jasonhemann wrote:
| One of the things miniKanren has going for it is that
| tons of folk have built little embedded implementations
| in the whatever your favorite host language is. For
| instance, here's https://web.archive.org/web/202112051755
| 13id_/https://erik-j... a walkthrough of how you'd
| implement the basics in Python. Comes with an
| explanation.
| coliveira wrote:
| The important thing is to realize how much programming has been
| wasted solving problems that can be easily expressed as logic
| programming and/or integer programming. If you need to solve
| logic and combinatorial based problems, learning these techniques
| will save you hundreds of hours.
| thih9 wrote:
| Sounds interesting. Could you give a specific example?
|
| Say, in a SaaS web app that provides a comments widget (a
| Disqus clone), what behavior (user facing or behind the scenes)
| would be a good candidate to implement with logic/integer
| programming?
| pkal wrote:
| I have a hunch this might be about the difference between
| "programming" and "coding". Web stuff, Hardware, and other
| things that don't get to just communicate with other
| programmers or programmers have a tendency of piling layers
| upon layers with custom glue and pipes everywhere.
| riku_iki wrote:
| There could be library of UI primitives and backend in
| logical language, then you would write declaration of what
| you want exactly:
|
| - I want window of these size, with such controls
|
| - when this button is clicked, text from this control appears
| in that DB column
|
| and system figures out all details making it cross platform,
| fault tollerant, etc if all infra is coded on that platform
| ashton314 wrote:
| AWS uses a SAT solver (Z3) to resolve permissions.
|
| I can see miniKanren (or some other logic programming
| language) being helpful in the realm of authorization.
| perching_aix wrote:
| i don't know, but their website doesn't support https at least
| mcmcmc wrote:
| Why does it need to?
| jessekv wrote:
| To protect the users of the site from receiving pages that
| have been tampered with?
| scotty79 wrote:
| What was the last time that you got served tampered webpage
| over http?
| simonw wrote:
| Happened to my startup back in ~2012.
|
| We had built an iPhone app that retrieved HTML pages from
| a server, but then scanned for extra metadata that was
| embedded in HTML comments for things like what navigation
| options should be displayed to accompany that page.
|
| We got a bug report from a user that the app broke when
| they used it on the free WiFi on the London Underground.
|
| It turned out there was some weird proxy running on that
| WiFi network that stripped HTML comments and injected
| extra tracking code into pages!
|
| Switching to https fixed the bug. I haven't shipped
| anything that uses plaintext HTTP since then.
| will_byrd wrote:
| Thank you all for your comments! We are working on a new
| version of the website, with a new layout, better
| examples up front, and HTTPS.
| kazinator wrote:
| I believe I'm being served tampered content every single
| time I access HTTP, so the last time that happened
| coincides with the last time I used a HTTP URL.
|
| Here are two hurdles:
|
| 1. Can you prove me wrong?
|
| 2. Next, given 1, can you rationally justify not rolling
| out HTTPS everywhere.
|
| In other words, is it actually a valid argument that
| "often, nothing bad happens when you use HTTP, so it is
| okay".
|
| Tampering of content has nothing to do with your privacy;
| it's a security matter. A nefarious man-in-the-middle
| could insert content which attacks your browser or
| redirects it to a malicious site, etc.
|
| That attacker could be on a network close to you, or a
| network close to the site. It's not a matter of trusting
| or not trusting the original site that serves the HTTP.
|
| Therefore it doesn't matter that you're just accessing
| the site as an anonymous visitor without an authenticated
| account, just viewing public content.
| stalfosknight wrote:
| I read this as "miniKaren" at first.
| t00 wrote:
| Sadly you're not alone
| sesm wrote:
| The name pre-dates the Karen stereotype, but IMO the naming
| clash is beneficial. I won't be surprised if miniKanren
| implementation for some new language is actually called Karen.
| Bluestein wrote:
| "Kraken" here, at first. But just me I acknowledge ...
| agumonkey wrote:
| the 'n' is where the logic comes from
| adamgordonbell wrote:
| Request: I'd love to learn more logic programming, SAT solvers,
| and equation solvers, but in a language I'm familiar with. Maybe
| python? But where to start?
|
| I played with some Scala mini Karen implementations before, but
| the ones I tried were all half-baked or non-working.
| will_byrd wrote:
| You might find Chris Mungall's py-typedlogic interesting:
|
| https://py-typedlogic.github.io/
| adamgordonbell wrote:
| Thanks! And thanks for miniKanren and reasoned schemer!
| debugnik wrote:
| If you're interested in SMT solvers, the Z3 bindings for Python
| are very easy to use.
| jasonhemann wrote:
| For folks that want to engage / learn more, there's been an
| annual miniKanren workshop and also a monthly miniKanren hangout
| online. Interested folk should totally come to either both!
| lambertsimnel wrote:
| The website describes the online hangouts as weekly and doesn't
| list any future dates:
|
| http://minikanren.org/#hangouts
|
| Is there more information somewhere?
| will_byrd wrote:
| I haven't held any hangouts online for years, although I'd
| consider restarting them if there is interest.
|
| We do have a monthly call of miniKanren/OCanren researchers
| from around the world, where someone presents on their
| research. If you are interested, please send me an email!
| xyzzy4747 wrote:
| Imagine it being 2024 and you don't know how to make your website
| HTTPS.
| imglorp wrote:
| Does it matter for an informational site? HTTP is quicker and
| doesn't expire certs etc.
|
| Of course, agree, it's totally needed for anything with a login
| or downloads etc, but serious question, what's the risk/benefit
| tradeoff here?
| xyzzy4747 wrote:
| If you use HTTP you can have middlemen hijacking your content
| or inserting malicious things and nobody would know. There's
| all kinds of weird actors out there.
| will_byrd wrote:
| Yes, that's enough reason to upgrade.
|
| We're working on it! Should have a new version of the site
| up within a few days.
|
| Thanks!
| Arnavion wrote:
| The risk is that HTTPS is something you have to manage.
| Either your hosting provider auto-renews certs for you (which
| might cost) or you set up your own automation (which can
| fail, and I've seen enough properties with expired LE-issued
| certs to know that email reminders can be missed and certbot
| is not a silver bullet). That said, usually an expired cert
| fails open, ie users can still visit your website if they
| accept the scary "this is unsafe" warning. This is not an
| option if your website uses HSTS or is on a TLD with implicit
| HSTS (eg .dev), but in that case you're opting in to the
| responsibility of renewing your certs reliably.
|
| The benefit is that you can be sure that nothing modifies the
| traffic between your server and the client, so the client
| sees your content without any modification.
|
| The counter-points to the benefit are that a) the traffic can
| still be *blocked* by any party in the middle (eg a state-
| level firewall), b) that traffic can absolutely be modified
| if the client has accepted an alternative CA for whatever
| reason (legal, corporate, etc) and that CA is used to MITM
| the connection to your server, and c) you as a website
| operator don't necessarily care about the MITM situation of
| every client's network (ie them having a MITM is their
| problem, not yours).
|
| There's another benefit that browsers restrict some JS API to
| only run on https pages, which matters if you wanted to use
| those API. https://developer.mozilla.org/en-
| US/docs/Web/Security/Secure...
| Isamu wrote:
| Shoutout to the illustrator of the Reasoned Schemer, Duane Bibby!
| Familiar to TeX fans and detractors alike.
|
| https://www.tug.org/interviews/bibby.html
| will_byrd wrote:
| Yes! Great artwork.
| hartator wrote:
| SerpApi | https://serpapi.com | Junior to Senior Fullstack
| Engineer positions | Customer Success Engineer | Talent
| Acquisition Specialist | Based in Austin, TX but remote-first
| structure | Full-time | ONSITE or FULLY REMOTE | $150K - 180K a
| year 1099 for US or local avg + 20% for outside the US
|
| SerpApi is the leading API to scrape and parse search engine
| results. We deeply support Google, Google Maps, Google Images,
| Bing, Baidu, and a lot more.
|
| Our current stack is Ruby, Rails, MongoDB, and React.JS. We are
| looking for more Junior and Senior FullStack Engineers.
|
| We have an awesome work environment: We are a remote first
| company (before Covid!). We do continuous integration, continuous
| deployments, code reviews, code pairings, profit sharing, and
| most of communication is async via GitHub.
|
| We value super strongly transparency, do open books, have a
| public roadmap, and contribute to the EFF.
|
| Apply at: https://serpapi.com/careers
| samatman wrote:
| You've posted in the wrong thread.
| hartator wrote:
| Thanks!
| notum wrote:
| Mini Karen, on the other hand...
| bobsacamano19 wrote:
| Haha my dyslexic ass read the title as "MiniKaren"... I was
| half-expecting to see some miniaturized version of someone
| complaining at a grocery store or something
| ashton314 wrote:
| A while back I was trying to understand the guts of miniKanren. I
| Did a careful reading of the paper and wrote up my notes along
| with the code here: https://codeberg.org/ashton314/microKanren
|
| Hope that helps someone. :) It's a fantastic little gem of a
| program.
|
| Don't forget: https://aphyr.com/posts/354-unifying-the-technical-
| interview
| coldtea wrote:
| It's a small computer language that wants to "talk to the
| manager"
___________________________________________________________________
(page generated 2025-01-02 23:01 UTC)