Prolog Best Practice: checking if a variable is already bound.

Question

I posted this solution to an question but ony left me a comment saying:

Predicates to check if "variable" is free or already bound should change strategy for deriving right unifications for other "variables" (i.e. speed up, or make possible to derive them). The same for dynamic predicates - they can be used to speed-up something, but they shouldn't be used as trigger of changing behaviour of something.

I am wondering why this is. Why is it bad practice to check if something is already defined to something else? Do you think it is bad practice? Are there other options that would be 'better practice'.

Here was my solution:

% ================================
% Ensures that all variables are unique.  
% ================================

% Base case: Assigned variables unique values
used([], Nin, Nin).

% Have already assigned a value to this variable
used([A|B], Nin, Nout) :-
        integer(A), % <----------------- THIS IS THE LINE IN QUESTION
        helper(B,Nin,Nout).

% Have not assigned a value to this variable yet
% Assign it and remove it from the list.  
used( [A|B] , Nin, Nout) :-
        member(A,Nin),
        delete(Nin,A,Temp),
        helper(B,Temp,Nout).

Answer 1

The fundamental problem of predicates like integer/1, atom/1 etc. is that they are not monotonic.

Take for example ?- integer(5)., which succeeds. But a more general goal, ?- integer(X)., fails!

For declarative debugging and automatically generated explanations, we expect that if a goal succeeds, every generalization of that goal must not fail.

The "proper" (i.e., if you want nice monotonic predicates that make declarative sense) thing to do would be for integer/1 to raise an instantiation error on queries like ?- integer(X). on the grounds that it does not have enough information to answer the question at this time. Instead of integer/1, you should use must_be/2 from library(error) to obtain this sound behaviour:

?- must_be(integer, X).
ERROR: Arguments are not sufficiently instantiated

must_be/2 behaves monotonically, which is in general a nice property.

Extending ony's comment: The problem is that (at least if the sample results above are correct) your predicate is no longer a true relation because goals are now not commutative: ?- X = 0, X = Y, addUnique([X,Y,3],3). succeeds, but simply exchanging the order of goals does not yield the same result because ?- X = Y, addUnique([X,Y,3], 3), X = 0. fails.

Such phenomena are common consequence of using meta-logical predicates. The declarative solution to such problems are constraints, see for example dif/2. They are monotonic, commutative and generally much easier to understand.