Extending core.logic (Datomic example)

Unifying Custom Data Structures

core.logic was designed with extensibility in mind. You may want to unify your own custom data structures - not only the ones provided by Clojure. To see how this can be done we'll use Datomic datums as an example.

For the following examples we assume you have created a Datomic test db and the following ns declaration:

(ns example
  (:use [datomic.api :only [db q] :as d])
  (:require [clojure.core.logic :as l]))

(def uri "datomic:dev://localhost:4334/test")
(def conn (d/connect uri))

In order for your custom data structure to participate in unification it must implement IUnifyTerms. But before that you should go ahead and define a protocol for unification with your data structure. It should look something like this:

(defprotocol IUnifyWithDatum
  (unify-with-datum [u v s]))

Now we can implement IUnifyTerms For Datomic datums like so:

(extend-type datomic.db.Datum
  l/IUnifyTerms
  (l/unify-terms [u v s]
    (unify-with-datum v u s)))

u is of course the datum, v is other data structure being unified with and s is the substitutions map. This code simply calls the new protocol function defined by your custom unification protocol. Note that we flipped the order of the arguments - this is critical - unification works via double dispatch in order to resolve the types of the terms being unified. We know u is a datum, we must now see if the unknown v has implemented unify-with-datum such that this operation will succeed.

There are now some base cases we must handle - unification with nil as well as the default unification behavior. Generally these should just return false (Note in the near future failed unification will probably be required to return nil).

(extend-protocol IUnifyWithDatum
  nil
  (unify-with-datum [v u s] false))

(extend-type Object
  IUnifyWithDatum
  (unify-with-datum [v u s] false))

In the case of datums we would like unification to possibly succeed with instances of clojure.lang.Sequential. This is because datums are 4 element tuples. We now implement a simple function that does this. Again returning false for failed unification.

(defn unify-with-datum* [v u s]
  (loop [i 0 v v s s]
    (if (== i 4)
      (if (seq v) false s)
      (if-let [s (l/unify s (first v) (nth u i))]
        (recur (inc i) (next v) s)
        false))))

v will be an instance of clojure.lang.Sequential, u will be the datum and s will be the current substitutions map. It should be clear here that datums may only unify with instances of clojure.lang.Sequential containing only 4 elements. This code simply unifies each element in the current substition - creating a new substitution which must be used for the next unification attempt. If all the elements of v and u unify, we return the new (possibly changed) substitutions map.

Unification is a binary operation - we must handle the possibility of a datum appearing as the left or right operand.

(extend-type clojure.lang.Sequential
  IUnifyWithDatum
  (unify-with-datum [v u s]
    (unify-with-datum* v u s)))

(extend-type datomic.db.Datum
  l/IUnifyWithSequential
  (l/unify-with-seq [v u s]
    (unify-with-datum* u v s)))

There is nothing more to do. Datums can now participate in unification.

Custom Data Sources

In order to write any interesting relational programs against Datomic we need to be able to unify with external data sources. This can be accomplished with to-stream.

(defn datomic-rel [q]
  (fn [a]
    (l/to-stream
      (map #(l/unify a % q) (d/datoms (db conn) :eavt)))))

to-stream creates a stream of choices suitable for core.logic's operation. It can take any seqable data structure. In this case we simply read out raw index data from Datomic. We unify each datum with the closed over argument q. This is important - core.logic relations are just closures. They must return a function that takes a single argument (in this case a) which is the current substitution.

You can now run core.logic queries against Datomic:

(l/run* [q]
  (l/fresh [e a v t]
    (l/== v true)
    (datomic-rel [e a v t])
    (l/== q [e a v t])))