Attributed variables: Interface convergence

[triska]

There are two major deficits of the current attributed variable interface predicate attr_unify_hook/2:

1. It is called only after the unification has already taken place.
2. In the case of simultaneous unifications like [X,Y] = [a,b], it is called with all bindings already in place.

However, there are cases where we need to reason about variables before the unification takes place or, equivalently, any pre-existing triggering unifications are undone before the hook is called. See below for the justification.

I recommend convergence with the interface used by SICStus Prolog, also to increase portability across different Prolog systems, or the design of an interface that is at least as general.

Specifically, it would help tremendously if verify_attributes/3 were called upon unifications with the same semantics as in SICStus Prolog:

1. first, the unifications are undone
2. verify_attributes(+Variable, +Value, -Goals) is called
3. the unifications are redone
4. Goals are executed

---

Real-world examples

I give two examples to explain why attr_unify_hook/2 is insufficient. The first example is shown in git commit 988ea20b7. It shows that the current interface is extremely error prone to use, because it can unexpectedly bind several variables at once and then trigger the hook with an arbitrary number of bindings suddenly in place. Realistically, nobody can exhaustively think of all cases that can simultaneously happen and cover them. The author of dif/2 also ran into this exact problem, as evidenced by a filed issue about dif/2.

The second example arises in a CLP(B) implementation that uses Zero-suppressed Binary Decision Diagrams (ZDDs). A ZDD is interpreted like any decision diagram, but with the following twist: Variables that do not occur in a branch must be 0. Here is an example showing the ZDD for X=\=Y, with the dotted lines indicating 0:

When working with ZDDs, we must keep track of all CLP(B) variables that appear in constraints, because we need to figure out "all variables that do not occur in the ZDD".

If unifications are performed step by step, i.e., just as with individual unifications, no problems arise, even with attr_unify_hook/2. For example, suppose we have X = 1, Y = 1. The first unification leads us into the right branch of the ZDD. We arrive at true, which means that this is true if all variables that do not occur in the ZDD (i.e., Y), are 0. Therefore, we post Y=0 from within attr_unify_hook/2. The second unification will therefore automatically fail.

But suppose the unifications are performed simultaneously, as in [X,Y] = [1,1]. The first unification again leads us into the right branch of the ZDD, but now we cannot find out which variables do not occur in the ZDD, because Y is no longer a variable at the time the hook is called!

More information about this issue: Minato task.

There may be ways to work around this, but they involve essentially duplicating the Prolog view of variables within the program, using IDs of variables to distinguish them. Also, this is not at all how we expect to reason about our datastructures.

For these reasons, it is very desirable that the unification hooks are called before the bindings are in place, and for each binding individually.

[TeamSPoon]

Secretly my mental picture of attribute variables had always been that they are not bound before calls to hooks. When I saw that so many people (yourself @triska included) seeming to be fine with them being bound at the time of the hooks I was really really impressed how you could still do CLP(??) . But, when I started ported to port a version of Description Logic, which amounts to porting CHR, (another todo list convergence LOL). I was stuck doing a mind numbing workaround of linearizing args: That means I was cloning attributed variables just to send them off to their impending "death by unification" in which attrib_unify_hook would send the original copy a gold star (a practice perhaps started in the Great War) .. But i needed to know where to send it and that meant every original variable needed to gensym a module for attrib_unify_hook) .

So let's discuss this issue, I have been working on a branch of SWI-Prolog capable of your needs this but will need help to make it lean towards convergence as well.

moved unrelated content/comments to logicmoo/swipl-devel#1

[JanWielemaker]

FYI, I don't have a strong opinion on the attvar interface. I'm happy with everything as long as the old interface remains supported or can be supported using an emulation layer that doesn't make it much slower. Please do look at existing interfaces, probably notably SICStus and ECLiPSe and design things to be as compatible as possible.

If you delay binding, be careful about cyclic terms and the occur check. See e.g., unifiable/3 in pl-prims.c, which performs the normal unification and then unbinds by examining the trail.

[triska]

Douglas, it is awesome that you are looking into this! Using the current interface (for clarity, please note the exact spelling: attr_unify_hook/2) to implement actual constraint solvers is an uphill battle: I managed to do it for CLP(FD), but for CLP(B) it is definitely not general enough. In addition, it is extremely error prone to use, because all variables may already be aliased when the hook is called. So, it is not at all like I'm happily using the interface and everything is fine; in fact, it's more of the opposite: When implementing constraint solvers, I'm continuously struggling with the current SWI interface and always wish for a cleaner one. Thank you for helping to finally solve this issue, I am looking forward to working with you on this and will help in every way I can to port all constraint libraries to the new interface once it becomes available!

To (massively!) improve the situation, having verify_attributes/3 exactly as in SICStus Prolog would be my personal preference: It is very declarative, and most importantly is called with the bindings undone. Please check out the SICStus documentation. Note that the other predicates are all either already available in SWI, or can be easily mapped for compatibility, but verify_attributes/3 can not, because in SWI, the hook (attr_unify_hook/2) is called with the binding already in place.

I therefore suggest you do the following: In your branch, provide verify_attributes/3 with the same semantics as in SICStus Prolog. In that branch, I will rewrite CLP(FD) and CLP(B) to use this new interface. (This will bring both of these systems closer to running in SICStus Prolog too, as a nice side-effect.) I will have some suggestions on how to support libraries that still use the attr_unify_hook/2 interface for the time being.

Most importantly, please first focus on getting the semantics right. This will allow us to run test cases and port actual solvers to the interface. Please let us postpone the discussion about performance: It is also important, but let us discuss it after having the SICStus-compatible semantics in place. If it is any reassurance, recall that SICStus is much faster than SWI-Prolog in many constraint benchmarks even though its interface for attributed variables is much more general than that of SWI, so this is a good indication that the SICStus interface can also be implemented efficiently.

[TeamSPoon]

Markus,

Nice, that get_attr/2 put_attr/2 are named differently than get_attrs/2 or put_attrs/2. Yes, we can for now (or later) map them.

Looks like I can very easily make verify_attributes/3 work as documented though it will be called only on Module:verify_attributes/3 that has either put_attr/3 or put_attrs/2 in the identical manner and call order that we do with attr_unify_hook/2
Like Sicstus says: "Var might have no attributes present in Module; the unification extension mechanism is not sophisticated enough to filter out exactly the variables that are relevant for Module."

Interesting.. So for our mainstream inclusion into SWI we could leave attr_unify_hook/2 as-is and only called if verify_attributes/3 did not veto the unification?

I see that verify_attributes/3is documented with the ability to create new choice points.. that won't be a problem (we will see if @JanWielemaker will need to answer a few questions.. But at least on one branch of this, I extended the pl-vmi.c )

I'll get a little bit ahead of myself: In fact, I am glad to create new choice points, this will make labeling/2 magically easier in the future.

[triska]

Yes, for backward compatibility, we could simply either just call attr_unify_hook/2 after the unification (as is currently the case), or, more elegantly, simply remove special provisions for attr_unify_hook/2 entirely from the core, and automatically add a definition of verify_attributes/3 that yields [attr_unify_hook(Attr,Value)] to modules that define attr_unify_hook/2. This expresses attr_unify_hook/2 in terms of verify_attributes/3, and requires only support for this predicate in the core.

Please expand on where verify_attributes/3 will be called: Note that the SICStus documentation says that verify_attributes/3 may even be called in modules where there are no attributes defined for that variable. It would be OK if that goes down to what you are saying, i.e., only where attributes are actually put on the variable, but it would still be interesting why the unification mechanism of SICStus does not do it as precisely. It may help you to improve the mechanism's performance in some cases if you know that it is OK to call verify_attributes/3 even in modules where the variable has no attribute attached.

[TeamSPoon]

Yes that can be a good with with core..

foo:attr_unify_hook(Attrib,Value):- ...CODE...

can be be replaced by

foo:verify_attributes(Var,Value,[]):-get_attr(Var,foo,Attrib), ...CODE...

Expanding on where verify_attributes/3 can be called is very easy to do in fact.
But first off our present situation:

At present in core as you know attr_unify_hook/2 must be present for all modules that wish to add attributes. Why? Optimization, because it is cheaper to assume a predicate exists and call it rather than doing something slow like current_predicate/N. (I was thinking about this before I read your comments) Wondering if this should also be a requirement of verify_attributes/3 to be defined as well. Personally I don't like either being a requirement.. (so I made it iterated thru the Modules to call verify_attributes/3 I first have it check current_predicate/1) And it did slow things down a little. Then I argued to myself, "Any module willing to put_attr/3 should be willing to step up and define hooks."

So right now this is how I have verify_attributes/3 implemented

%%  '$wakeup'(+List)
%
%   Called from the kernel *before* assignments have been made to
%   attributed variables.

'$wakeup'(L):- 
  wno_hooks('$wakeup_attrs'(L)).

% 4096 disables the unification hooks presently running
% don't worry, hook code still be able to use wakeups on other variables.
% This wrapper is only for safe debugging 
wno_hooks(G):-  '$sinkmode'(W,W),T is W  \/ 4096, '$sinkmode'(_,T),                 call_cleanup(G,'$sinkmode'(_,W)).


% version only calling it where modules have defined an attribute
'$wakeup_attrs'([]).
'$wakeup_attrs'(wakeup(Var, Attrs3, Value, Rest)) :-           
        call_all_attr_verify_hooks(Var, Attrs3, Value),
        (nonvar(Var)->true;Var=Value),
        call_all_attr_uhooks(Var, Attrs3, Value),
    '$wakeup'(Rest).

% Allow someone who binds this Var to move us onto the next stage 
% In fact, they do not even need to use the original value .. for example ...
% ==
%   verify_attributes(Var, "between one and three", _Goals) :- member(Var,[1,2,3]).
% ==
% (this is for later labeling ..  this does not conflict with Sicstus)
call_all_attr_verify_hooks(Var, _, _) :- nonvar(Var),!.  
call_all_attr_verify_hooks(Var, [], Value).
call_all_attr_verify_hooks(Var, att(Module, AttVal, Rest), Value) :-        
   (current_predicate(Module:verify_attributes/3)->
     (attvar_residuals(att(Module,AttVal,[]), Var, Goals, [])-> Module:verify_attributes(Var, Value, Goals)) ;true),
    call_all_attr_verify_hooks(Var,  Rest, Value).


call_all_attr_uhooks([], _).
call_all_attr_uhooks(att(Module, AttVal, Rest), Value) :-
    uhook(Module, AttVal, Value),
    call_all_attr_uhooks(Rest, Value).

The alternative that gives that flexibility

% Searches for modules defining verify_attributes/3.
% unused pseudocode :)
call_all_attr_verify_hooks(Var, Attr3, Value) :-  
  Template= Module:verify_attributes(Var,Value,Goals),
 ((  current_predicate(_,Template) ,
   \+ predicate_property(Template,imported_from(_)),
    attrs_to_residual_goals(Attr3,Goals),
   (Template -> true ; (!,fail)) )
          *-> true ; fail)). 

Which I would be happy with if we didn't have to use current_predicate/2

[JanWielemaker]

current_predicate/2 and predicate_property/2 are out of the question. For one thing, ISO
current_predicate/2 is not supposed to work for static code (works in SWI). Second, these
are just too slow operations. A simple option is to define

system:verify_attributes(_Var, _Attr3, _Value) :- fail.

I think I'm more in favour of having an undefined predicate trap, as that is far easier to debug
instead of a failing unification because somebody adds an attribute without defining a hook.

Can you help clarifying what will happen if we do put_attr(V, test, a) and call V = v. This is my picture with holes:

• Unify V=v, this pushes the wakeup goals.
  • Does the actual binding happen?
    • if yes, when and how is it undone? Immediately after unification? Just before
      wakeup?
    • if no, how to we protect against the occur check? This would be problematic
      if the answer above is Immediately after unification because there may be
      multiple unifications before wakeup is called.
• If wakeup is called
  • We call verify_attributes(Var, AttrList, Value) in every module where we now call
    attr_unify_hook/2. The difference is that the binding is not yet made and you
    have access to all other attributes on this variable.
  • We can easily provide all attributes to all hooks without changing anything to the C
    code. Why do we need access to the variable bound (also next question)?
• When is the binding actually done? Do the hooks to that? That would mean
  X = Y, X == Y is no longer necessarily true. That would worry me.

[TeamSPoon]

Agreed about current_predicate/2 and predicate_property/2.

I am sure you thought of (and maybe this is what you meant) as well

:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).

And modules could do.

:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).
prolog:verify_attributes(Var,Value,Goals):-  \+ mymodule:verify_attributes(Var,Value,Goals) ->  (!,fail);true.

mymodule:verify_attributes(Var,Value,Goals):- ...MODULE_CODE...

Answers to the next questions (filling in outline).

But in preview I did test this...

 ?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X.
   Call: (8) [$syspreds] leash(-all)
   Unify: (8) [$syspreds] leash(-all)
   Exit: (8) [$syspreds] leash(-all)
   Call: (8) [system] _G307319{}=_G306598
   Exit: (8) [system] _G307319{}=_G307319{}
   Call: (8) [system] _G307319{}==_G307319{}
   Exit: (8) [system] _G307319{}==_G307319{}
X = Y.

[trace]  ?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X,X==Z.
   Call: (8) [$syspreds] leash(-all)
   Unify: (8) [$syspreds] leash(-all)
   Exit: (8) [$syspreds] leash(-all)
   Call: (8) [system] _G307384{}=_G306598
   Exit: (8) [system] _G307384{}=_G307384{}
   Call: (8) [system] _G307384{}==_G307384{}
   Exit: (8) [system] _G307384{}==_G307384{}
   Call: (8) [system] _G307384{}==_G306604
   Fail: (8) [system] _G307384{}==_G306604
false.

[JanWielemaker]

Not sure what to think about the trace. In a hurry ...

For the modules, I meant system. The trick is that whenever you have a module that has
no verify_attributes/3 definition, it will default (first to user) to the system module definition.
I definitely do not want to use the prolog module.

[TeamSPoon]

Ahah, i get it.. great idea!

the small change of ...

system:verify_attributes(_Var, _Attr3, _Value). 

(At least i think)

[triska]

There are several misconceptions here, so I would like to first clear up a few important high-level aspects by using the SICStus documentation to walk through the example that Jan posted: Suppose we have put_attr(V, test, a), and then post V = v.

1. Engine: First, the binding is undone. The precise timing when this happens is still to be defined, let us discuss it separately. I think we can undo it any time we like, as long as it is before verify_attributes/3 is called. In fact, if you can implement that, I think the binding need not even take place at all before (5), see below.
2. Engine: test:verify_attributes(V, v, Gs) is called. Note that the second argument is the value that the variable is about to be bound to, not a list of all attributes.
3. User: test:verify_attributes/3 is the user-defined predicate. If it is not defined, failure is definitely not an option because that would silently break existing user code. It is also a misconception that the current "attr_unify_hook/2 must be present for all modules that wish to add attributes": This is not the case, as you can easily test, and the current state is desirable for the important reason that we often attach attributes to variables just for efficient lookup in certain datastructures, and these variables are never even unified with anything, so users should not have to define attr_unify_hook/2 for them. In my view, if test:verify_attributes/3 is undefined, it should be equivalent to test:verify_attributes(_, _, []).
4. User: test:verify_attributes/3 must not bind the variable itself. Instead, it communicates via the third argument all goals that are to be invoked after the unification. For instance, the obvious emulation of the current test:attr_unify_hook/2 would be:

   test:verify_attributes(Var, Value, [test:attr_unify_hook(Attr,Value)]) :-
       get_attr(Var, test, Attr).

5. Engine: The original variable binding is redone. V = v.
6. Engine: The goals computed by the third argument of test:verify_attributes/3 are called.

Note specifically that, due to (5), if X = Y succeeds, then X == Y will also succeed.

I would also like to state the most important high-level goal: The current interface falls extremely short in the case of simultaneous unifications like [X,Y] = [a,b]. This is because at the time attr_unify_hook/2 is called for X, Y is no longer a variable and its attributes cannot be directly accessed. Therefore, both unifications must be undone in such cases to truly benefit from verify_attributes/3. As I understand it, the occurs check may as well take place after (5): Semantically, a unification that is STO is false, so the only downside I see is that an STO unification may fail instead of yielding an error when occurs_check is set to error.

[TeamSPoon]

if we do put_attr(V, test, a) and call V = v.

• Unify V=v, this pushes the wakeup goals.
  • No actual binding happens. Instead, binding is scheduled to happen outside of C via $wakeup/1
  • With the occurs_check code there might be some difficulties yet.
  • Since there may be multiple unifications before wakeup is called. Each successive unification schedules more wakeup. The attributed variable continues to delay. And remains a variable so it can continue to claim it is free.
• If wakeup is called
  • We disable the delay system temporarily for the V so unification treats it like a common variable.
  • We call verify_attributes(Var, AttrList, Value) in every module where we now call attr_unify_hook/2. The difference is that the binding is not yet made and we have access to all other attributes on this variable.
  • We can easily provide all attributes to all hooks without changing anything to the C code.
  • Why do we need access to the variable bound? We really do not need to access it bound since most hooks can see the Value.
    • Though I did design a usecase where it is partially bound and the hooks further bind it (like as a workspace) .. (Though a sane person would do that in attributes)
  • attr_unify_hook/2 is agnostic to whether it was bound or not.
  • Once I had left it unbound, and was able to implement a common prolog variable!

plvar(X):- mvar_set(X,+remainVar),put_attr(X,plvar,binding(X,_)).
plvar:attr_unify_hook(binding(Var,Prev),Value):-  Value=Prev,put_attr(Var,plvar,binding(Var,Value)).

• When is the binding actually done it is by the hooks.
  • The hooks if poorly written (or brilliantly written) could even make X = Y, X == Y fail. For example they could decide whenever X is bound to a variable to make X = 1 instead. (thus 1==Y fails) ..
  • Some case that could be worrisome but other cases useful.
  • I did leave in one barrier to hooks when unifying with a plain old prolog variable. Most likely the X=Y will have put X into Y (instead of the other way around) thus never calling wakeups on X. so X==Y.. will effectively be seen as X==X
  • I gave us the ability to remove that barrier, that is the more experimental part
    Marked with "eager" is where most C code that would call Trail(Y,makeRef(X)). will instead call unifyAttVar(X,Y) which will add a $wakeup/1

test:attr_unify_hook(nonvar,Value):-nonvar(Value).
test:attr_unify_hook(var,Value):- var(Value).

?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y. 
false.

?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign),X=Y,X==Y. 
X=Y.  /*this is why *I* like eager  it prevents ignoring the hooks  */

?- put_attr(X, test, var), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y. 
X=Y.

(BTW: I typed this before reading @triska's post above this one)

[TeamSPoon]

@triska Point 4, Perhaps I'll should throw an exception when I get the Var back and it's been bound?