Josh Munn's Website

Why I'm Rewriting Microkanren

I’m rewriting my Python microkanren implementation. I’ve always wanted to add tabling, have tried a few times, but stopped due to lack of time, and subtle errors. I’m taking a few steps to simplify the core implementation, and get tabling done.

  1. Removing finite domain and disequality constraints. I rarely use the FD constraints — for anything non-trivial the performance is poor, and I think I’d be better off using another tool. I’ll probably add disequality back in once I’ve got the tabling working properly.
  2. Insisting on type annotations and type checking. I’m hoping that’ll help with reasoning about the pointier edges of the tabling implementation.
  3. Splitting the implementation into a core layer written in Python, with a higher-level API written in Hy. Being able to define some of the userland operators and forms as macros really simplifies things. The idea is that you’ll be able to use the Python core without Hy if you want, but you’ll need to add your own interfaces around running queries and reifying the results. Moving some of the meta-programming out of the core should help with keeping it simple, and the layered approach might open up possibilities for rewriting the core in a more efficient language.

Why not write the whole thing in Hy? Emacs support and other related tooling is poor. hy-mode seems unmaintained, and needs some fixes. The linting, type-checking and auto-formatting story for Python is pretty great at the moment with ruff and pyright.

    ┏━━━━━━━━━━━━━━━┓     ┏━━━━━━━━━━━━━━━┓
    ┃    core.py    ┃░    ┃    lang.hy    ┃░
    ┃               ┃░    ┃               ┃░
    ┃  unify        ┃░    ┃  run          ┃░
    ┃  mplus        ┃◄────┃  conj+        ┃░
    ┃  bind         ┃░    ┃  Zzz          ┃░
    ┃  tabled       ┃░    ┃  ...          ┃░
    ┃  ...          ┃░    ┗━━━━━━━━━━━━━━━┛░
    ┗━━━━━━━━━━━━━━━┛░     ░░░░░░░░░░░░░░░░░
     ░░░░░░░░░░░░░░░░░

Other goals

I’ve been reading some of the Clojure core.logic source code. It’s quite readable. I’m keen to get to the bottom of how they handle unification over Clojure’s various collection types. It seems they use an LCons type — Logical Cons?

There’s also some nice pattern-matching macros in core.logic. defne looks like a macro for defining goal constructors with pattern matching, including a shorthand for introducing fresh logic variables. That will be a fun challenge to implement.

I’d like to add an operator for unification over generic data streams. Think (disj* (?X, ?Y) (query "SELECT foo, bar FROM baz")), where each successful unification with a row from the query would contribute a result. That might be the sort of thing they do in mediKanren — something to look into.

Tags: