Setting types of unbound variables in Prolog

Question

I'm trying to find a way to set the type of a variable before it has been bound to a value. Unfortunately, the integer/1 predicate cannot be used for this purpose:

%This goal fails if Int is an unbound variable.
get_first_int(Int,List) :-
    integer(Int),member(Int,List),writeln(Int).

I wrote a predicate called is_int that attempts to check the type in advance, but it does not work as I expected. It allows the variable to be bound to an atom instead of an integer:

:- initialization(main).
%This prints 'a' instead of 1.
main :- get_first_int(Int,[a,b,c,1]),writeln(Int).

get_first_int(Int,List) :-
    is_integer(Int),member(Int,List).

is_integer(A) :- integer(A);var(A).

Is it still possible to set the type of a variable that is not yet bound to a value?

Answer 1

In SWI-Prolog I have used when/2 for similar situations. I really don't know if it is a good idea, it definitely feels like a hack, but I guess it is good enough if you just want to say "this variable can only become X" where X is integer, or number, or atom and so on.

So:

will_be_integer(X) :- when(nonvar(X), integer(X)).

and then:

?- will_be_integer(X), member(X, [a,b,c,1]).
X = 1.

But I have the feeling that almost always you can figure out a less hacky way to achieve the same. For example, why not just write:

?- member(X, [a,b,c,1]), integer(X).

???

Answer 2

Specific constraints for integers

In addition to what Boris said, I have a recommendation for the particular case of integers: Consider using CLP(FD) constraints to express that a variable must be of type integer. To express only this quite general requirement, you can post a CLP(FD) constraint that necessarily holds for all integers.

For example:

?- X in inf..sup.
X in inf..sup.

From this point onwards, X can only be instantiated to an integer. Everything else will yield a type error.

For example:

?- X in inf..sup, X = 3.
X = 3.

?- X in inf..sup, X = a.
ERROR: Type error: `integer' expected, found `a' (an atom)

Declaratively, you can always replace a type error with silent failure, since no possible additional instantiation can make the program succeed if this error arises.

Thus, in case you prefer silent failure over this type error, you can obtain it with catch/3:

?- X in inf..sup, catch(X = a, error(type_error(integer,_),_), false).
false.

CLP(FD) constraints are tailor-made for integers, and let you express also further requirements for this specific domain in a convenient way.

Case-specific advice

Let us consider your specific example of get_first_int/2. First, let us rename it to list_first_integer/3 so that it is clear what each argument is, and also to indicate that we fully intend to use it in several directions, not just to "get", but also to test and ideally to generate lists and integers that are in this relation.

Second, note that this predicate is rather messy, since it impurely depends on the instantiation of the list and integer, a property which cannot be expressed in first-order logic but rather depends on something outside of this logic. If we accept this, then one quite straight-forward way to do what you primarily want is to write it as:

list_first_integer(Ls, I) :-
        once((member(I0, Ls), integer(I0))),
        I = I0.

This works as long as the list is sufficiently instantiated, which implicitly seems to be the case in your examples, but definitely need not be the case in general. For example, with fully instantiated lists, we get:

?- list_first_integer([a,b,c], I).
false.

?- list_first_integer([a,b,c,4], I).
I = 4.

?- list_first_integer([a,b,c,4], 3).
false.

In contrast, if the list is not sufficiently instantiated, then we have the following major problems:

?- list_first_integer(Ls, I).
nontermination

and further:

?- list_first_integer([X,Y,Z], I).
false.

even though a more specific instantiation succeeds:

?- X = 0, list_first_integer([X,Y,Z], I).
X = I, I = 0.

Core problem: Defaulty representation

The core problem is that you are reasoning here about defaulty terms: A list element that is still a variable may either be instantiated to an integer or to any other term in the future. A clean way out is to design your data representation to symbolically distinguish the possible cases. For example, let us use the wrapper i/1 to denote an integer, and o/1 to denote any other kind of term. With this representation, we can write:

list_first_integer([i(I)|_], I).
list_first_integer([o(_)|Ls], I) :-
        list_first_integer(Ls, I).

Now, we get correct results:

?- list_first_integer([X,Y,Z], I).
X = i(I) ;
X = o(_12702),
Y = i(I) ;
X = o(_12702),
Y = o(_12706),
Z = i(I) ;
false.

?- X = i(0), list_first_integer([X,Y,Z], I).
X = i(0),
I = 0 ;
false.

And the other examples also still work, if we only use the clean data representation:

?- list_first_integer([o(a),o(b),o(c)], I).
false.

?- list_first_integer([o(a),o(b),o(c),i(4)], I).
I = 4 ;
false.

?- list_first_integer([o(a),o(b),o(c),i(4)], 3).
false.

The most general query now allows us to generate solutions:

?- list_first_integer(Ls, I).
Ls = [i(I)|_16880] ;
Ls = [o(_16884), i(I)|_16890] ;
Ls = [o(_16884), o(_16894), i(I)|_16900] ;
Ls = [o(_16884), o(_16894), o(_16904), i(I)|_16910] ;
etc.

The price you have to pay for this generality lies in these symbolic wrappers. As you seem to care about correctness and also about generality of your code, I consider this a bargain in comparison to more error prone defaulty approaches.

Synthesis

Note that CLP(FD) constraints can be naturally used together with a clean representation. For example, to benefit from more finely grained type errors as explained above, you can write:

list_first_integer([i(I)|_], I) :- I in inf..sup.
list_first_integer([o(_)|Ls], I) :-
        list_first_integer(Ls, I).

Now, you get:

?- list_first_integer([i(a)], I).
ERROR: Type error: `integer' expected, found `a' (an atom)

Initially, you may be faced with a defaulty representation. In my experience, a good approach is to convert it to a clean representation as soon as you can, for the sake of the remainder of your program in which you can then distinguish all cases symbolically in such a way that no ambiguity remains.