This is like an entirely new genre within fantasy. I don't even know what you would call it, but it is both entertaining and a beautiful showing of skill all at the same time.
Maybe you can't even call it fantasy since it is real code & logic with no magic involved.
I love aphyr's posts so much. Aside from just being super entertaining, they have a significant degree of pedagogical value. If one sets out to fathom these incantations, they will end up studying a large swath of under-appreciated languages and theory.
It was fun to read this because I happened to study at Indiana University where most of the work on *Kanren happened.
If anyone is interested in practical applications, Will Byrd (mentioned in the story) went on to work with Matt Might (HN's favorite CS-prof-turned-doctor). One of the products of that was mediKanren[0] which operates over medical research. There was some publicity around mediKanren last year.[1]
I've enjoyed all the posts in this series, but this is first time it's I've "empathized" with some aspect of the problem solving.
I've taken a couple of stabs at writing a mini/micro-kanren in a language which _isn't_ a lisp, often following along closely with some paper from Hemann, Friedman and/or Byrd -- and if the language _doesn't_ have macros it really does get awkward. As mentioned at the PS, for a good long stretch, this post is pretty directly transcribing the 'microkanren' paper, and without macros at some point Vidrun would have had to invent some of her own idioms.
The other trick to having the embedded kanren really work with the host language, which is swept a bit under the rug, is that `walk*` / `walkr` in this post implicitly assumes that everything in your universe is a variable, an atomic value, or a cons. In that sense, it's a little funny that (I think) her kanren can't really solve "inside" of the structs that she asked to be provided.
This is an excellent observation--and indeed, one of the things about implementing (so, so many versions of) microKanren is that I've learned the paper version relies heavily on magic. It is very easy to get a microKanren that works sometimes, but explodes in some conditions, because of the subtle ways that the paper relies on the behavior of improper lists (raw cons pairs) vs proper lists, and because many recursive cases which would normally be explicitly enumerated (or handled via polymorphic dispatch) just happen to work correctly thanks to the way they encode bindings, substitutions, etc as lists. In particular, there are many places where it looks like a `map` might make things simpler, but will subtly break things, thanks to the need to recurse into improper lists. The mplus/bind control flow graph is also... extremely tricky if you aren't precise about null/empty/car/cdr.
her kanren can't really solve "inside" of the structs that she asked to be provided.
Ahhhh, so this is true, and actually a feature: uKanren exploits scheme vectors as lvars, and initially my language was just lists. I wound up adding structs precisely so that I'd have an analogous non-list compound type!
I wish there was an explainAphyr site or a wiki or subreddit or something where there's a step by step explanation of both the mythology and the code involved.
There's a link at the very bottom to a fully annotated, commented copy of the full source code, and a fairly good summary of what was going on in the footnote.
Prolog is... different, it's going to take some getting used to. The Art of Prolog is a great resource, reading the first few chapters should get you far enough that you can then roughly understand what the code is doing and Google (or skim forward though the rest of the book) to look up the unfamiliar syntax for things like arithmetic. You should probably ignore the cut (the ! Aisha adds) for a while and come back to it once you've written some Prolog and gotten a feel for how it works. cuts are simple, but only once you've wrapped your head around Prolog's execution strategy. A good way to know that you get it is that you no longer accidentally write infinite loops.
Of course, once you understand logic programming you still have most of this essay left to go through. Even if you've used lisp you've probably never had to implement one! And of course, after you've gotten through all that, now you need to read code written in this strange lisp. A microKanren. almost Prolog, but different in some key ways; it uses a different execution strategy which prevents those infinite loops. The Reasoned Schemer is the second half of this essay but expanded out to book form, it would make a great explanation if you're down for a nice read and you have a free Saturday.
Once you've gotten through all that the syntax has become completely unrecognizable but the final solution is fun, and makes all the ceremony worth it:
`balanceo` is a relation which is only satisfied if `tree` is a tree and `balanced` is the balanced form. If you pass in `tree` it returns the correct `balanced`. I'm not sure, but it looks like it probably also works if you only pass in `balanced`, in which case it will return the unbalanced `trees` which correspond to that balanced tree. You might even be able to pass in nothing, in which case it will return a bunch of pairs of unbalanced trees and their balanced forms.
The definition of `balanceo`, essentially, says that "[balanceo tree balanced] is only true if balanced can be formed by performing rotations on tree, and balanced is balanced." MicroKanren figures out the rest. That's declarative programming! Pretty great! Though, it only works for small trees, which does tarnish the magic a little.
I don't know if I should feel embarrassed or not too - I'm a lead C++ programmer and I don't understand any of the code or what they are trying to do. It's like learning a language, only to discover people speaking such a dialect of it that you don't understand a word.
I don't see any reason why you should be embarrassed - if you haven't seen Prolog (or anything similar) it is very different to more conventional languages. It's arguable that Prolog is closer to SQL than C++.
I had thought that the non-logical features at the Prolog-implementation-of-Lisp level would lose relationality. And it does, at the level of the Lisp implementation. But you gain relationality at the microKanren level!
One thing I love about this wonderful story is that it shows you can use constraint logic programming to solve a problem (in a hilariously roundabout way), by using a tower of languages:
Level 3: (purely functional implementation of) tree balancing (or whatever)
At first glance it may seem goofy to implement LISP-within-miniKanren-within-LISP. After all, we started with LISP! However, the LISP we end up with inherits the relationality of its miniKanren implementation, which means we can encode our problem in LISP, but have miniKanren apply the search and constraint solving under the hood.
The extra level of LISP interpretation allows us to put logic variables representing unknown values in new positions, giving us increased expressivity, at a significant performance cost.
If we can figure out how to apply staged evaluation/partial evaluation/supercompilation/etc. effectively to these towers of interpreters to reduce the interpretive overhead, these "jokes" may turn out to be surprisingly useful.
I wanna say that I really appreciate that the one of the deities to whom Vidrun prays participates in (enlightening) discussion around fanfic about his work.
Is it? A quick look at the Mastodon / Twitter links at the bottom of the article should make it clear the author is (rightfully) proud of his butt. I suppose that won't prevent the rest of HN from getting offended, so maybe it's somewhat inappropriate. But not wholly.
I do think it’s wholly inappropriate to comment on another person’s body parts in a public forum, when it is not the topic of discussion, even if that person appears to be proud of said body part. But I can see your take on it
He takes what should be a simple problem and solves it with the entirely the wrong tools. There's some comedy, the tools are comically wrong and overpowered for the task at hand. There's also the sheer thrill of seeing such tools used at all, we don't generally write this kind of stuff at work.
Then… don't read it? You are perfectly within your rights to start reading a thing, go "this is not for me", and stop reading it, without announcing this fact.
Maybe you can't even call it fantasy since it is real code & logic with no magic involved.