Verbose invariant

[moea]

Just using GH for communication, this isn't a specific issue.

Working on simple invariant query examples - the one below is intended to ensure that all writes to user/points are >= the preceding value - but written in such a way that a transaction would be rejected if any of its points values are decreasing.

(ns invariant.datahike-scratch
  (:require [invariant.datahike]
            [invariant.test.util
             :refer [read-resource]]
            [datahike.api  :as d]
            [datahike.core :as dc]))

(def schema
  [#:db{:ident       :user/points
        :valueType   :db.type/bigint
        :cardinality :db.cardinality/one}])

(defn query [q db tx]
  (d/q q
       db
       (dc/db-with db tx)
       (dc/db-with (dc/empty-db) (concat schema tx))
       tx))

(let [uri "datahike:mem:///invariant-test-2"]
  (d/delete-database uri)
  (d/create-database uri)
  (let [conn (d/connect uri)]
    (d/transact conn schema)
    (d/transact conn [{:db/id 1 :user/points 1}
                      {:db/id 2 :user/points 1}])

    (let [tx [[:db/add 1 :user/points 2]
              [:db/add 2 :user/points 0]]]

      (query '[:find ?all-valid .
               :in $before $after $empty+tx $tx
               :where
               [(subquery
                 [:find (count ?entity) .
                  :where
                  [?entity :user/points _]]
                 $empty+tx) ?n-total]
               [(subquery
                 [:find (count ?entity) .
                  :in   $before $after $empty+tx
                  :where
                  [$after ?entity :user/points ?points-after]
                  [(get-else $before ?entity :user/points 0) ?points-before]
                  [(<= ?points-before ?points-after)]]
                 $before $after $empty+tx) ?n-valid]
               [(= ?n-total ?n-valid) ?all-valid]]
             @conn tx))))

This works, but it's long. I'm sure I'm doing something dumb here, and that it'd be possible to write a short, single query which returns something falsy if any of the points are invalid (i.e. lifting the second subquery and flipping the :where to contain (> ?points-before ?points-after)) - and then doing something else that isn't clear to me.

[whilo]

It is a general problem that whenever you need to calculate aggregates you have to do it in the head of the Datalog program for Datomic and DataScript. Regarding non-termination of Datalog this is not necessary (at least if there is no intertwining with recursion and negation), I think, but there might be other reasons. One first step to get around it would be to define a shortcut subquery function for each aggregate, but we might need to make the parser syntactically aware and find a syntax in the end.

[moea]

@whilo I think the point I was trying to make was that for many examples I've been able to come up with, the queries would be much more brief if the invariant library expected them to unify only in the negative case - i.e. that for many validation problems, expressing the shape of unacceptable values can be easier than expressing the shape of acceptable ones.

[whilo]

There is seemingly no standard for aggregates: https://courses.cs.washington.edu/courses/cse544/18wi/lectures/lecture05-datalog.pdf. We need to provide a way to bind from the outside into the queries mainly, i.e. which logic variables are joint (like in or-join) and potentially also which databases are used and then we could do:

:where
...
[(count [$empty+tx] [?entity] [?entity :user/points _])]
...

I think there is probably a good reason why Datomic does not support it though. I need to think about it.

[moea]

A negate expression which DTRT w/ relations and sequences would handle the case I'm talking about, though I do think it's the common case.

(negate
 [:find (count ?entity) .
  :in   $before $after $empty+tx
  :where
  [$after ?entity :user/points ?points-after]
  [(get-else $before ?entity :user/points 0) ?points-before]
  [(> ?points-before ?points-after)]])

[whilo]

I see. Yes, I think we could just allow to specify which direction the query needs to unify separately on the top-level. This is not perfectly compositional, but it would address this issue. I thought about it also on this cycle counting example, which is similar to yours. We could also allow negate in the head of the query.

[whilo]

The problem is that the expressions in the head of the language are not supposed to be nested.

[whilo]

There is seemingly no standard for aggregates: https://courses.cs.washington.edu/courses/cse544/18wi/lectures/lecture05-datalog.pdf. We need to provide a way to bind from the outside into the queries mainly, i.e. which logic variables are joint (like in or-join) and potentially also which databases are used and then we could do:

:where
...
[(count [$empty+tx] [?entity] [?entity :user/points _])]
...

I think there is probably a good reason why Datomic does not support it though. I need to think about it.

I think subqueries are more flexible though and in full generality you want to have them for each aggregate. So maybe the syntactic overhead is actually ok.