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.

It's like pedagogical fantasy, or like, narrative programming instead of literate programming.

In Neal Stephenson's Anathem there are monks that turn mathematical proofs into songs and other art, and it reminds me of that.

Someone had a go at creating music in the style of the mathic world from Anathem - I rather like it:

https://synthesist.net/music/anathem/

it's something like... magical realism + hard sci-fi? not gonna attempt a portmanteau but ideas welcome

> The Church. The lambda calculus. The gay agenda.

I just about lost it with that one. Started laughing so hard I woke up my wife...

> ... balancing a binary tree was an interview question which I personally bombed in 2010 ...

Thank you, Kyle. That first snippet gave me joy. That second snippet, though... that gave me _hope_.

I lost it at:

“One more thing,” you request. “Some kind of product type.”

“Ma'am, this is a Wendy’s.”

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]

[0] https://github.com/webyrd/mediKanren [1] https://www.uab.edu/news/health/item/10703-diagnosis-in-2-12...

There's this talk as well: https://www.youtube.com/watch?v=Yval98eOyZc

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.

If you take a look at the "full" version of this program, which uses more struct types, it involves a good deal more explicit recursion: https://gist.github.com/aphyr/4d41e7655b10a68e753f729bdc1c5a...

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.

Seriously. This is the first entry in the x-ing the interview series where I understood literally 0% of the code

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, [lambda, [tree, balanced],
    [conde, [[rotso, tree, balanced],
             [balancedo, balanced]]]]

`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.

If you’ve never implemented a Lisp, here’s a relevant thing to give a read: https://sep.yimg.com/ty/cdn/paulgraham/jmc.ps

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++.

the two (Prolog and SQL) even have something of a middle ground - Datalog (https://en.wikipedia.org/wiki/Datalog)

" You couldn’t remember how to balance a binary tree, so you thought you’d define the transformational invariants and have Prolog solve them for you."

Well, yes, that's one good reason to know Prolog.

This is a work of high art.

Now make everything run backwards! :)

Wait--it does run backwards!?

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!

I love it!

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 0: PROLOG

Level 1: (non-relational implementation of) LISP

Level 2: (purely functional? implementation of) microKanren

Level 3: (purely relational implementation of) tree balancing

In [0] we invert this approach, also arriving at code that behaves relationally:

Level 0: LISP

Level 1: (purely functional implementation of) miniKanren

Level 2: (purely relational implementation of) LISP

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 last example in [0] goes further:

Level 0: LISP

Level 1: (purely functional implementation of) miniKanren

Level 2: (purely relational implementation of) LISP

Level 3: (purely functional implementation of) LISP

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.

[0] https://dl.acm.org/doi/10.1145/3110252 and http://io.livecode.ch/learn/gregr/icfp2017-artifact-auas7pp

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.

https://gist.github.com/aphyr/4d41e7655b10a68e753f729bdc1c5a... is titled 'Minikanren in Lisp in Prolog'.

there's also a 'Report abuse' link nearby...

For better or worse, they only care about abuse of github, not the poor code that they house...

When I grow up, I want to be Kyle.

I like how the forest of trees collapses back into a single tree. That was neat.

I've been waiting for another one of these!

How is it the best butt in tech also gets to be the best writer in tech?

How is this even remotely fair?

This is a wholly inappropriate comment

I can't speak for anyone else, but it's my favorite comment so far. :-)

Isn't that a conflict of interest?

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

somewhere the ghost of Cyrano De Bergerac smiles upon you.

What did I just read? Not that I read all of it, I made it to the 1921 paragraph and slowly clicked the back arrow.

This one is pretty technical, it might be easier to start with some of the older ones: https://aphyr.com/posts/341-hexing-the-technical-interview

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.

Not to mention the fantasy mythology stuff.

Yeah, not all of us are into the fantasy mythology stuff.

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.

You know how some sorts of programming are described as black magic? It’s like taking that literally and writing a silly short story.