prologiso-prolog

Safer type tests in Prolog


ISO-Prolog (ISO/IEC 13211-1:1995 including Cor.1:2007, Cor.2:2012) offers the following built-in predicates for testing the type of a term:

8.3 Type testing

1 var/1. 2 atom/1. 3 integer/1. 4 float/1. 5 atomic/1. 6 compound/1. 7 nonvar/1. 8 number/1. 9 callable/1. 10 ground/1. 11 acyclic_term/1.

Within this group there are those whose purpose is solely to test for a certain instantiation, that is 8.3.1 var/1, 8.3.7 nonvar/1, 8.3.10 ground/1, and those that assume that a term is sufficiently instantiated such that the type test is safe. Unfortunately, they are combined with testing for a concrete instantiation.

Consider the goal integer(X) which fails if X is a nonvar term that is not an integer and when X is a variable. This destroys many desirable declarative properties:

?- X = 1, integer(X).
   true.
?- integer(X), X = 1.
   false.

Ideally the second query would either succeed using some form of coroutining ; or it would issue an instantiation error1 according to the error classification. After all:

7.12.2 Error classification

Errors are classified according to the form of Error_term:

a) There shall be an Instantiation Error when an
argument or one of its components is a variable, and an
instantiated argument or component is required. It has
the form instantiation_error.

...

Note that this implicit combination of instantiation testing and type testing leads to many errors in Prolog programs and also here on SO.

A quick fix to this situation would be to add an explicit test in front of every test built-in, either verbosely as

   ( nonvar(T) -> true ; throw(error(instantiation_error,_)) ),
   integer(T), ....

or more compactly as

functor(T, _,_),
integer(T), ....

it could be even

T =.. _,
integer(T), ...

My question is twofold:

How to provide this functionality on the user level?

and, to make this also a bit challenging:

What is the most compact implementation of a safer atomic/1 written in ISO-Prolog?


1 Other less desirable options would be to loop or to produce a resource error. Still preferable to an incorrect result.

Solution

  • The testing for types needs to distinguish itself from the traditional "type testing" built-ins that implicitly also test for a sufficient instantiation. So we effectively test only for sufficiently instantiated terms (si). And if they are not sufficiently instantiated, an appropriate error is issued.

    For a type nn, there is thus a type testing predicate nn_si/1 with the only error condition

    a) If there is a θ and σ such that nn_si(Xθ) is true and nn_si(Xσ) is false
    instantiation_error.

    atom_si(A) :-
       functor(A, _, 0),    % for the instantiation error
       atom(A).
    
    integer_si(I) :-
       functor(I, _, 0),
       integer(I).
    
    atomic_si(AC) :-
       functor(AC,_,0).
    
    list_si(L) :-
       \+ \+ length(L, _),  % for silent failure
       sort(L, _).          % for the instantiation error
    
    character_si(Ch) :-
       functor(Ch,Ch,0),
       atom(Ch),
       atom_length(Ch,1).
    
    chars_si(Chs) :-
       \+ \+ length(Chs,_),
       \+ ( once(length(Chs,_)), member(Ch,Chs), nonvar(Ch), \+ character_si(Ch) ),
       \+ ( member(Ch,Chs), \+ character_si(Ch) ). % for the instantiation error
    

    This is available as library(si) in Scryer.

    In SWI, due to its differing behavior in length/2, use rather:

    list_si(L) :-
        '$skip_list'(_, L, T),
        functor(T,_,_),
        T == [].