3 ms·

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

by abeppu 6y ago

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.

aphyr 6y ago
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/4d41e7655b10a68e753f729bdc1c5a6d#file-minikanren-pl-L522-L542 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!

by abeppu 6y ago

aphyr 6y ago

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/4d41e7655b10a68e753f729bdc1c5a6d#file-minikanren-pl-L522-L542 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!