Welcome! Please see the About page for a little more info on how this works.

Ask a Question

core.unify doesn't handle maps correctly

+4 votes
in core.unify by
edited by

core.unify does a classic approach to unification: in garner-unifiers, it has a branch for sequential things, whereby it unifies the first elements of each sequence and then uses those bindings to unify the remaining bits:

https://github.com/clojure/core.unify/blob/master/src/main/clojure/clojure/core/unify.clj#L120

(every? composite? [x y]) (garner-unifiers uv-fn
                                           variable?
                                           (rest x) 
                                           (rest y)
                                           (garner-unifiers uv-fn
                                                            variable?
                                                            (first x)
                                                            (first y) 
                                                            binds))

Maps also take this path. 

unify=> (composite? {})
true

The code then expects first and rest to get the sequence of the same keys (and unifiable values) from both maps. This is not necessarily true. It's broken when keys have the same hash in a hashmap and it's broken when keys are in a different order when in an arraymap

unify=> (let [kws #{:a :b :c :d :e :f :g :h :i :dCv :wxW}]
          (assert (= (hash :dCv) (hash :wxW)))
          [(garner-unifiers (zipmap kws (repeat '?a))
                            (zipmap kws (repeat 1)))
           (garner-unifiers (zipmap kws (repeat '?a))
                            (zipmap (reverse kws) (repeat 1)))])
[{?a 1} nil]
unify=> [(garner-unifiers {:a '?a :b '?b} {:a 1 :b 2})
         (garner-unifiers {:a '?a :b '?b} {:b 2 :a 1})]
[{?a 1, ?b 2} nil]

Fun thread in #clojure : https://clojurians.slack.com/archives/C03S1KBA2/p1727544444884499
And hat tip to p-himik who identified the minimal reproduction here.

1 Answer

+1 vote
by

I've got the following patch for consideration. it works in two phases:
1. It identifies any keys which are "not complex". Complex here meaning a variable, or some kind of collection. These are keys that presumably can be matched on equality and not need unification. Probably the most common type.
2. Complex keys that need unification and backtracking.

I think there might be one weakness in the patch in that it considers x to be a template and y to be the concrete values and this is not true.

diff --git a/src/main/clojure/clojure/core/unify.clj b/src/main/clojure/clojure/core/unify.clj
index a89db73..c53a0c7 100644
--- a/src/main/clojure/clojure/core/unify.clj
+++ b/src/main/clojure/clojure/core/unify.clj
@@ -101,6 +101,36 @@
   (and (composite? form)
        (#{'&} (first form))))
 
+(defn- garner-unifiers-map
+  [uv-fn variable? x y binds]
+  (let [complex-key? (some-fn variable? composite?)
+        concrete-ks  (->> x keys (filter (complement complex-key?)))
+        simple-binds (reduce (fn [binds k]
+                               (garner-unifiers uv-fn variable?
+                                                (find x k)
+                                                (find y k)
+                                                binds))
+                             binds
+                             concrete-ks)]
+    (if (or (nil? simple-binds) (every? (complement complex-key?) (keys x)))
+      simple-binds
+      (letfn [(solve [x y binds]
+                (let [x' (first x)]
+                  (when-let [sol (reduce (fn [_ kv]
+                                           (when-let [binds (garner-unifiers uv-fn variable? x' kv binds)]
+                                             (when-let [binds (garner-unifiers-map
+                                                                uv-fn variable?
+                                                                (dissoc x (key x'))
+                                                                (dissoc y (key kv))
+                                                                binds)]
+                                               (reduced binds))))
+                                         nil
+                                         y)]
+                    sol)))]
+        (solve (apply dissoc x concrete-ks)
+               (apply dissoc y concrete-ks)
+               simple-binds)))))
+
 (defn- garner-unifiers
   "Attempt to unify x and y with the given bindings (if any). Potentially returns a map of the 
    unifiers (bindings) found.  Will throw an `IllegalStateException` if the expressions
@@ -117,6 +147,8 @@
       (variable? y)             (uv-fn variable? y x binds)
       (wildcard? x)             (uv-fn variable? (second x) (seq y) binds)
       (wildcard? y)             (uv-fn variable? (second y) (seq x) binds)
+      (and (map? x) (map? y))   (when (= (count x) (count y))
+                                 (garner-unifiers-map uv-fn variable? x y binds))
       (every? composite? [x y]) (garner-unifiers uv-fn
                                                  variable?
                                                  (rest x) 
diff --git a/src/test/clojure/clojure/core/unify_test.clj b/src/test/clojure/clojure/core/unify_test.clj
index a96d476..57a27da 100644
--- a/src/test/clojure/clojure/core/unify_test.clj
+++ b/src/test/clojure/clojure/core/unify_test.clj
@@ -100,3 +100,28 @@
     (is (= {} (unify '[1 ?x] '[1])))
     (is (= {} (unify '[1 ?x ?y ?z] '[1])))))
 
+
+(deftest map-order
+  (testing "Map unification is not sensitive to array map order"
+    (is (= '{?a 1, ?b 2} (unify '{:a ?a :b ?b} {:a 1 :b 2})))
+    (is (= '{?a 1, ?b 2} (unify '{:a ?a :b ?b} {:b 2 :a 1})))
+    (testing "including when keys are unified"
+      (is (= '{?a 1, ?b :b} (unify '{:a ?a ?b :b} {:a 1 :b :b})))
+      (is (= '{?a 1, ?b :b} (unify '{:a ?a ?b :b} {:b :b :a 1})))))
+  (testing "handles collisions in keys"
+    (let [kws #{:a :b :c :d :e :f :g :h :i :dCv :wxW}]
+      (is (= '{?a 1} (unify (zipmap kws (repeat '?a))
+                            (zipmap kws (repeat 1)))))
+      (is (= '{?a 1} (unify (zipmap (reverse kws) (repeat '?a))
+                            (zipmap kws (repeat 1)))))))
+  (testing "Backtracks on complex keys"
+    (is (= '{?a 1, ?b 2, ?c 3, ?d 3, ?e 4}
+           (unify '{?a [?b ?c]
+                    ?d [?e ?e]}
+                  {1 [2 3]
+                   3 [4 4]})))
+    (is (= '{?a 1, ?b 2, ?c 3, ?d 3, ?e 4}
+           (unify '{?a [?b ?c]
+                    ?d [?e ?e]}
+                  {3 [4 4]
+                   1 [2 3]})))))
Maintained by Cognitect on behalf of the Clojure community
...