Temporary "exists" variables in suchthat

[julianhyde]

In suchthat expressions you often need to declare a variable in an "exists". But it can be a little verbose. Suppose you have a list of edges and a function:

val edges = [(1, 2), (2, 3), (1, 4), (4, 2), (4, 3)];

fun isEdge (x, y) = (x, y) elem edges;

To compute a list of nodes that are two steps apart, you could write:

from (x, y) suchthat exists (
  from z suchthat isEdge(x, z) andalso isEdge(z, y));

Using the in paradigm you generate two temporary variables z and z2 that need to be eliminated using group x, y:

from (x, z) in edges,
    (z2, y) in edges
  where z = z2
  group x, y;

Leveraging #184 this becomes slightly more concise but you still need a group to eliminate z:

from (x, z) in edges,
    (same z, y) in edges
  group x, y;

We propose a variant of exists:

from (x, y) exists z suchthat isEdge(x, z) andalso isEdge(z, y);

In Datalog, any variable that does not appear on the left-side of the rule becomes an "exists variable", for example Z in the following:

is_step2 (X, Y) :- is_edge(X, Z), is_edge(Z, Y).

Morel cannot compete with Datalog's terseness. Morel is a typed language, and that means that its variables need to be declared, in a pattern, at exactly one point, so that their type can be specified. (Usually the type is inferred, but that point needs to exist.) The exists variable suchthat sugar seems to be about as terse as we can get.

[julianhyde]

The follow is more concise. Is it better?

from (x, y, exists z) suchthat isEdge(x, z) andalso isEdge(z, y);

[julianhyde]

Following #202, the syntax would be

from x, y, z
  where isEdge (x, y) andalso isEdge (z, y)

That seems better. No exists keyword necessary.