1. 13
  1. 3

    Eli Bendersky has an excellent article on unification, (and also talks about a bug in many implementations, I wonder if this implementation has it…): https://eli.thegreenplace.net/2018/unification/

    1. 2

      I’m going to need to re-read this more carefully, but on first blush I don’t see how this implementation supports backtracking. It seems like so long as unification is possible, it will be done permanently, & so it can’t be performed in a speculative way (i.e., it’s not possible for unification performed deep in some call chain to be invalidated later by its sibling). That said, it seems like it ought to be straightforward to tag particular elements of the environment as speculative & give a reference to the choice point for each, or supply some expression that indicates how to calculate the next possibility in case one has been invalidated…

      1. 0

        I am reminded of unification in µKanren.

        1. 4

          You should be! Third paragraph in the intro:

          Cut to last week, I happened to read the MicroKanren paper (which is very readable) and discovered that unification could be very simple! Let me show you how!

          1. 1

            Thank you for humbling me. Somehow I missed that paragraph and only pattern-matched on the code in the body of the post.