support for every expression

[Gozala]

We have bunch of threads discussing this and loose consensus that we could leave this out in 1.0 as long as we can validate it can be added in the future.

Similar to #7 I'm leaning towards something along these lines

input

{
  "mail": [
    { "to": ["alice@web.mail", "malory@web.mail"], "content": "hello alice" },
    { "to": ["bob@gmail.com", "alice@web.mail" ], "content": "hi bob" }
  ]
}

policy

Every message in mail must have some recipient matching *.@web.mail.

[
  [".mail", "?", "?mail"],
  ["for", "?message", "?mail"],
  [".to", "?message", "?to"],
  ["in", "?email", "?to"],
  ["like", "?email", "*@web.mail"]
]

[Gozala]

On the other hand if we embrace selector syntax from jq in #7 perhaps we could do the same for every in fact jq does have construction syntax which may be utilized

Perhaps above policy could be rewritten as follows

[
  ["[.mail]", "?", "?message"], // <-- every message under mail
  [".to[]", "?message", "?email"], // <-- some email from every message
  ["like", "?email", "*@web.mail"] // <-- must match the pattern
]

[Gozala]

Inlining some relevant comments from other thread

Just stashing some research here: this paper adds universal quantification to Kanren: https://www.cs.toronto.edu/~lczhang/jin_universal2021.pdf

It adds a form (forall (v) domain goal)

Translated to our format it looks roughly like this:

{ 
 policy: [ 
   ["forall", ["?goal"], [".foo.bar.[]", "$", "?domain"], 
     ["match", "?goal", "*@example.com"]
   ]
 ]
}


// Rearranged
{ 
  policy: [ 
    [".foo.bar.[]", "$", "?domain"],
    ["forall", ["?x"], "?domain", 
      ["match", "?x", "*@example.com"]
    ]
  ]
}

// Flattened

{ 
  policy: [ 
    [".foo.bar.[]", "$", "?domain"],
    ["forall", ["?x"], "?domain"],
    ["match", "?x", "*@example.com"]
  ]
}

...which looks a heck of a lot like my every suggestion from earlier.

What I like about this is we could add this to the version with an implied some without having to rework the version that doesn't have it 👍

[expede]

On the other hand if we embrace selector syntax from jq in #7

I think we've now done that: universal quantification by default ✅

[Gozala]

// data set
{
  foo: [
    {bar: [1, 0, 0]},
    {bar: [0, 1, 0]},
    {bar: [0, 0, 1]},
  ]
}

// Task: every `foo` has a `bar` that contains at least one >0 element.

// Explicit version is very confusing unless you give very descriptive variable
// names.
[
 ["every", ".foo[]", "?every-foo"]
 [".bar[]", "?every-foo", "?bar-of-every-foo"], // <- this is confusing what is the ?bar
 ["some", "?bar-of-every-foo", "?some-bar-of-every-foo"]
 [">", "?some-bar-of-every-foo", "0"]
]

// Implicit version is a lot shorter but not very intuitive at all, especially
// when second clause could contradict the first one yet be correct.
[
  [">", ".foo[].bar[]?", 0],
  ["<", ".foo[].bar[]?", 0]
]


// Attempt to articulate the problem I have with pushing some / every into the
// the selector is that it seems intuitive but it is misleading.

[">", ".foo[].bar[]?", 0]

// This to me reads as

jq(".foo[].bar?[]", args).some((bar) => bar > 0)

// That is because `jq` returns matches as collection and then you do something
// to it. That is incorrect however because what the policy is actually saying
// is

jq(".foo[]").every(foo => foo.some((bar) => bar > 0))

// It is possible to make a case for the ☝️ interpretation, if you do not have
// variables in the system, but if you introduce them things become even more
// confusing because if we assigned query to the variable it now contains a
// collection as opposed to function you can apply predicates to.
[
  [".", ".foo[].bar[]?", "?some-bar-of-foo"],
  [">", "?some-bar-of-foo", 0],
]

// In comparison this is a lot more clear to me.
[
  ["every", ".foo",
    ["some", ".bar[]" [">", ".", 0]]
]

// Datomic way is not intuitive, have to read few times to comprehend, but it
// is not misleading.
[
  // no foo that does not have a bar > 0
  ["not",
    [".", ".foo[]", "?foo"],
    ["not", [".bar[]", "?foo", "?bar"],
            [">", "?bar", 0]]
  ]
]