is there a rationale for why lvars as map keys do not unify?

(run* [q]
  (fresh [a b]
    (== {a b} {:a 2})
    (== q (list a b))))
;; => ()

in my spare time i’ve been working on a term rewriting engine and was also confronted with the problem of unifying maps. i was able to find a solution that achieves this. i was surprised to find that core.logic doesn’t support this, however, i wouldn’t be surprised if i may have overlooked something in my own algorithm.

there is no one way to do it

@hiredman explain.

(== {a b c d} {:a 1 😛 2})

(== {a b c d} {:a 1 :b 2})

the algorithm i wrote unifies ground entries, then entries with ground values, then entries with ground keys, then entries where both the key and value are variable.

there is no single unification for that

your example can be unified in multiple ways, the values can be streamed to a, b, c, and d in those cases.

actually, that’s not true.

the fact there exists a solution refutes that argument.

so maybe my understanding here is misguided.

can you explain your emphasis on “single”?

lists are defined inductively via cons, so there is a one order they can be walked for unification, and that orders arises from the definition

maps are not inductively defined, so there is no single iteration order, so there is no fixed thing to wire in to the unifier

you can do it, but you will have to make some choices to do it that preclude being general, which is what a library like core.logic is trying to do

i see. can you elaborate more on why the inductive property is important?

wrt core.logic?

i’m guessing the solution here would be to use another goal in favor of == which does stream the substitutions.

because unification has to traverse datastructures, if a datastructure is defined inductively, that is an order the structure can be traversed

I bet you could make it work if you either only used one concrete map type, or sorted it before unifying

the strategy i mentioned above works pretty well. although, again, my setting is term rewriting which expects the left-hand side of the equation to be ground.

sure, if your model is less general then you can do more

so, in the context of core logic, would the solution then be two stream the solutions via a custom goal?

i understand the rationale above now.