Verify_attributes in SICStus Prolog

Attribute variables permit to extend unification. The following is about arcane details of the interface. Let's cut right to the chase!

In sicstus-prolog library(atts) provides predicates for using attributed variables. I think I get what the SICStus Prolog User's Manual page for library(atts) says, except for one detail about verify_attributes(-Var, +Value, -Goals):

[...] verify_attributes/3 is called before Var has actually been bound to Value. If it fails, the unification is deemed to have failed. It may succeed nondeterminately, in which case the unification might backtrack to give another answer. It is expected to return, in Goals, a list of goals to be called after Var has been bound to Value. Finally, after calling Goals, any goals blocked on Var are called.

The above sentence (highlighted by me) confused me—and a lot, too:)

I have always thought that unification is a procedure that could either:

succeed with the most general unifier (modulo variable renaming)
or fail.

But succeed nondeterminately?!

When is that "feature" ever of use to implementors of constraint solvers?

I can't think of a single use case... help please!

EDIT

Actually, I regard non-determinacy in (my) solver code a bug—not a feature. For any non-determinacy can easily be emulated by returning some disjunction in Goals.

Solution

You find the same behaviour in XSB:

verify_attributes(-Var, +Value)
This predicate is called whenever an attributed variable Var (which has at least one attribute) is about to be bound to Value (a non-variable term or another attributed variable). When Var is to be bound to Value, a special interrupt called attributed variable interrupt is triggered, and then XSB's interrupt handler (written in Prolog) calls verify_attributes/2. If it fails, the unification is deemed to have failed. It may succeed non-deterministically, in which case the unification might backtrack to give another answer.
http://xsb.sourceforge.net/shadow_site/manual2/node4.html

It has nothing to do with the third parameter that returns a goal, to be executed later. This third parameter is even missing in XSB, there is no such third parameter in this call back. I guess the riddles solution is such, that the verify_attributes/2 hook might leave a choice point, and that the subsequent unification is in the continuation of this choice point.

So that during backtracking, the choice point is tried again. And this means that the subsequent unifications are undone, and then tried again as well in case the choice point provides a further solution. With a clever organization of how the call back is called, I guess every Prolog system could implement that, since Prolog systems should champion choice points.

But because of lack of use cases might also do without it. Neither freeze/2 nor when/2 require it, since they work with the instantiated variable. Nor do the typical CLP(X) require it, since choice points are unwanted. But it might exist in XSB, since the third argument is missing. If you disallow non-determinism in the verify hook, you need to provide alternatives.

To sum up the alternatives to compensate for barring non-determinism:

verify_attributes/3:
The third argument in SICStus variant of verify_attributes/2, which is verify_attributes/3. The goals there can be non-deterministic. The goals will see the variable instantiated.
attr_unify_hook/2:
This is the SWI-Prolog hook. It will see the variable instantiated as well. But a small test shows that it allows non-determinism:

    Welcome to SWI-Prolog (threaded, 64 bits, version 8.1.4)
    
    ?- [user].
    |: foo:attr_unify_hook(_,_) :- write('a'), nl.
    |: foo:attr_unify_hook(_,_) :- write('b'), nl.
    |: 
    % user://1 compiled 0.01 sec, 2 clauses
    true.
    
    ?- put_attr(X, foo, 1), X=2.
    a
    X = 2 ;
    b
    X = 2.