library(clpz) activate monotonic mode only in current module

[bakaq]

An use case that I thought about recently is to use library(clpz) in monotonic mode internally in a library. The problem is that if you assertz(clpz:monotonic) in a library, this also activates monotonic mode in the module using the library. Example:

%% Contents of clpz_lib_example.pl
:- module(clpz_lib_example, [
    example/2
]).

:- use_module(library(clpz)).

:- initialization(activate_monotonic_mode).

activate_monotonic_mode :-
    assertz(clpz:monotonic).

example(A, B) :-
    A #= B.
%% End of contents of clpz_lib_example.pl

?- X #= 1 + 2.
   X = 3.
?- use_module(clpz_lib_example).
   true.
?- example(X, Y).
   error(instantiation_error,instantiation_error(unknown(_585274),1)). % Expected
?- example(#X, #Y).
   X = Y, clpz:(X in inf..sup). % Expected
?- X #= 1 + 2.
   error(instantiation_error,instantiation_error(unknown(_585274),1)).  % Unexpected
   X = 3. % Expected, but not found

A workarround is doing assert(clpz:monotonic) before and retractall(clpz:monotonic) after if the monotonic mode wasn't already set. This makes the above example work, but if one of the variables has attributes, the attribute handling could be activated, and if the handling expects clpz to not be in monotonic mode (maybe because when the attribute was put in the variable the mode was deactivated) this could cause a huge mess.

I'm not sure if there is a way to do this properly. One thing I thought about was to assertz(clpz:monotonic(Module)) instead, so that library(clpz) knows that that specific module is in monotonic mode. But I don't know if there is a way to know when a clpz constraint was called in that specific module so it can decide to use or not the monotonic mode.

[triska]

To me, this requirement seems eminently sensible, and it may be a way to gradually increase the use of the monotonic execution mode in different libraries.

@UWN: Do you maybe have any suggestions about how to best implement this or something similar? Thank you a lot!

[bakaq]

it may be a way to gradually increase the use of the monotonic execution mode in different libraries.

Yes! The biggest problem with the monotonic mode is that it currently "infects" the whole program. It would be very nice to have this so you can make a library with the monotonic mode but not have to force your users to also use it, because non-monotonic mode is way more convenient and sufficient for most applications.

[UWN]

The question is really when this is needed. At runtime or at compile time?

One solution for compile time might be to change the non-monotonic mode to SICStus-style mode. SICStus converts prior (or better immediately prior) to term-to-body conversion the loose variables into integer variables. Thus in SICStus:

| ?- call((X=1+1, Y#=X)).
! Type error in argument 2 of user:'t=u+c'/3
! expected an integer, but found 1+1
! goal:  't=u+c'(_423,1+1,0)
| ?- call((X=1+1, call(Y#=X))).                                                         
X = 1+1,                                                                                
Y = 2 ? ;                                                                               
no                                                                                      

(The first call/1 is here not really needed, but it makes clear when term-to-body conversions happen.)

This reduces differences somewhat and increases compatibility to SICStus.

The alternative would be to invent some module-sensitive mechanism which makes all these module issues only worse. In particular when switching dynamically between those.

The very same argument can be put forward for the occurs_check modes. And think of operators.

it currently "infects" the whole program.

To use the metaphor of infection, the very same would happen in the other direction too. Except that it not only affects clpz, but much more than that.

[UWN]

Or to put it the other way round: monotonic programs do run also with that flag disabled. And those who use it in that looser mode still get the benefit of type checking. So the analogy is quite similar to set_prolog_flag(occurs_check, error) where this mode can be used for development and testing and finally it can also be used without it (provided one does not catch those errors, indeed).

In both (is)/2 and default-clpz expressions, one has so often some irregularities like:

?- n_factorial(1+0,F).
   F = 1
;  ... .
?- n_factorial(0+0,F).
   false.  % heu?
?- n_factorial(0,F).
   F = 1
;  false.

By adding (#)/1 this can be solved cleanly.