Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Possible syntaxes for flexible unifier w/ multi-lvar constraints
;;Support for simple constraints on lvars during unification was added in 76fd4d7c:
;;but these constraints apply to a single lvar only.
;;The unifier could support more general constraints if it accepted an explicit predicate function.
;;For instance, given this `data-numeric?` predicate and `spec` data:
(defn data-numeric? [data dimension]
(number? (-> data first dimension)))
(def spec {:data (repeatedly 10 #(hash-map :val (rand) :cat (rand-nth [:a :b :c])))
:mapping {:y :val}})
;;I'd like a unifier call that has the same semantics as:
(run* [q]
(fresh [data dim]
(== spec {:data data :mapping {:y dim}})
(project [data dim]
(== true (data-numeric? data dim)))
(== q :success)))
;;A concise syntax is
(unifier1 spec
'{:data ?data :mapping {:y ?dim}}
'(data-numeric? ?data ?dim))
;;but that would require `unifier1` to
;; + prep all of its arguments together
;; + treat its third argument (or last, if more than 3 args) specially
;; + prep, project, and eval the predicate form, which feels gross.
;;We can avoid the last-argument issue via a dynamic var:
(binding [*unifier-constraints* '(data-numeric? ?data ?dim)]
(unifier2 spec))
;;This maintains backwards compatibilty at the expense of being klunky (and suffers from the same prep+project+eval issue).
;;A more programmatically flexible syntax:
(unifier3 '[spec {:data ?data :mapping {:y ?dim}}
[data-numeric? ?data ?dim]])
;;where everything before the `:where` is something to unify and everything after is a tuple of the form [predicate & lvar-arguments].
;;This syntax could be used with the existing unifier since the single-arity implementation is currently undefined.
;;Another option is to pass a map of constraints as the unifier's third arg:
(unifier4 spec '{:data ?data :mapping {:y ?dim}}
{data-numeric? '[?data ?dim]
'?dim keyword?})
;;the map can have entries (constraint-fn -> vector of args) for complex constraints of multiple lvars or (lvar symbol -> constraint-fn) for simple constraints on a single argument.
;;Since the constraint function is given grounded vals, this form could support "or" constraints via set literals.
(unifier4 m '{:a 1 :b ?b}
'{?b #{1 5}})
;;succeeds for m equal to {:a 1 :b 1} OR {:a 1 :b 5}
;;In any of these syntaxes, I'm not sure if we can/want to support anonymous functions, or if in that case the user should just ball up and write a full run* form.

This comment has been minimized.

Copy link
Owner Author

commented Nov 20, 2012

Ping: @swannodette.


This comment has been minimized.

Copy link
Owner Author

commented Nov 21, 2012

@swannodette, here's the scaffold implementation you requested on IRC for the variable-arity unifier to accept an optional :where clause and constraint map in the last position.

(defn unify-with-constraint-map [terms m]
  (prn [terms m]))

(defn unifier
  [u w & ts]
  (let [[where constraint-map] (take-last 2 ts)]
    (if (= where :where)
        (concat [u w] (drop-last 2 ts))
      (unify-with-constraint-map (concat [u w] ts) {}))))

(unifier :u :w 1 2 3 :where {:c :m})
;; => [(:u :w 1 2 3) {:c :m}]
(unifier :u :w :where {:c :m})
;; => [(:u :w) {:c :m}]
(unifier :u :w :z)
;; => [(:u :w :z) {}]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.