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 forminstantiation_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?
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 andnn_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 == [].