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
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
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/1written 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 and
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 == .