Constraints

The previous chapter, Logic Programming, ended on a problem. The STLC type checker, asked about a term that still has a hole in it, has nothing sensible to do: because its first argument is an input, no rule head matches a bare variable and the goal simply fails. With unification in place of matching it does worse, inventing an app (then a lam inside that, and so on) for the hole and looping forever. Neither is any use to an elaborator, which works with such incomplete terms, full of holes still to be filled in, all the time. The fix is to let the checker suspend on a hole rather than guess.

Controlling instantiation

When a rule’s search meets a hole, one of two things should happen instead of guessing: suspend the computation, recording it as a constraint to be retried later, or synthesize a value for the hole through some dedicated routine richer than plain unification (out of scope for this chapter). A suspended computation can also carry data along, anything from a single flag to a whole typing sequent, and the data that several suspended computations have attached to one hole can later be combined. Suspending and resuming are what follow; combining what several constraints know about the same hole is covered in The constraint store.

Matching, not unifying

A signature (Type declarations) splits a predicate’s arguments into input, before the ->, and output, after it. When a rule is selected the two are treated differently: the goal’s input arguments are matched against the rule head’s patterns, its output arguments are unified with them (Formal semantics’s select). The difference shows as soon as an argument is an unassigned variable. Matching it against a constant pattern would have to assign it, so it simply fails to match, no rule fires, and the variable is left untouched. Unifying it succeeds and assigns it:

../code/input-output.elpi:

% An input argument is matched: passing an unassigned variable matches no
% rule, since matching a variable against a rule's pattern would have to
% assign it. An output argument is unified: it does get assigned.

data tm.
symb z tm.
symb s tm -> tm.

pred as-input tm.
as-input z :- print "matched z".
as-input (s _) :- print "matched s _".

pred as-output -> tm.
as-output z.

main :-
  ( as-input _ ; print "as-input: an unassigned variable matched no rule" ),
  as-output Y, print "as-output assigned Y to" Y.

as-input: an unassigned variable matched no rule
as-output assigned Y to z

An input argument is therefore safe to leave partly unknown: a call with a hole in an input position does not force a guess, it finds no matching rule. And that is what lets a rule detect a hole and act on it. The uvar keyword is a head pattern that matches only an unassigned variable, and uvar as E binds E to it. The two rules below are equivalent, the second spelling out what the first means:

of (uvar as E) T :- declare_constraint (of E T) [E].
% equivalent to:
of E T :- var E, declare_constraint (of E T) [E].

The full set of uvar head patterns is in Unification and variables. The standalone mode directive, the older and separate way of marking arguments input or output, is described in Compatibility with Teyjus, Prolog and legacy Elpi.

declare_constraint (Constraint handling rules) is what turns a goal into a constraint. Its goal argument must itself be a function, needing a func signature, because a constraint that could be resumed in more than one way would make the search unpredictable once constraint handling rules start combining constraints.

Suspending and resuming

The list passed to declare_constraint is the constraint’s trigger: the variables whose assignment wakes it up. A constraint honours backtracking just as a plain unification assignment does: undoing the assignment that resumed a constraint suspends it again, as though nothing had happened.

../code/backtracking-constraints.elpi:

% The constraint store honours backtracking: an assignment made and then
% undone leaves a resumed-and-reverted constraint exactly as it was.

func even int.
even (uvar as X) :- !, declare_constraint (even X) [X].
even 0 :- !.
even N :- N > 0, M is N - 2, even M.

main :-
  even Y,
  print "before:", print_constraints,
  (Y = 3, fail ; true),        % assign, resume, fail (3 is not even), backtrack
  print "after backtracking:", print_constraints.

before:
 even X0  /* suspended on X0 */
after backtracking:
 even X0  /* suspended on X0 */

The STLC checker from Logic Programming, with one rule added, closes the problem that chapter ended on: a hole in argument position now suspends instead of looping, and resumes when the hole is filled.

../code/holes.elpi:

% The STLC type checker from "The logic programming model", now handling
% incomplete terms: a hole in argument position suspends instead of looping.

data tm.
symb app tm -> tm -> tm.
symb lam (tm -> tm) -> tm.

data ty.
symb arr ty -> ty -> ty.

func of tm -> ty.
of (app H A) T :- of H (arr S T), of A S.
of (lam F) (arr S T) :- pi c\ of c S ==> of (F c) T.
of (uvar as E) T :- declare_constraint (of E T) [E].

main :-
  of (app H _A) _T,      % H and A are holes: two constraints appear
  print "before:", print_constraints,
  H = (lam x\ x),        % filling one hole resumes its constraint
  print "after:", print_constraints.

before:
 of X0 X1  /* suspended on X0 */ of X2 (arr X1 X3)  /* suspended on X2 */
after:
 of X0 X1  /* suspended on X0 */

Incompatible constraints

Suspending and resuming on their own are not quite enough. Asked about an unknown N, both even N and odd N suspend without complaint. Yet no number is both, so a goal that suspended the two of them should have failed.

../code/incompatible.elpi:

func even int.
even (uvar as X) :- !, declare_constraint (even X) [X].
even 0 :- !.
even N :- N > 0, !, M is N - 2, even M.

func odd int.
odd (uvar as X) :- !, declare_constraint (odd X) [X].
odd 1 :- !.
odd N :- N > 1, !, M is N - 2, odd M.

main :- even N, odd N, print_constraints.

odd X0  /* suspended on X0 */ even X0  /* suspended on X0 */

Both constraints are accepted, quietly, side by side. The remedy is given in the next chapter (The constraint store).