In Type tests in Prolog (YouTube presentation of the series “The Power of Prolog”), the type-testing predicates
si standing for “sufficiently instantiated”) are presented.
These predicates throw an instantiation error if their parameter is not “sufficiently instantiated” to make a decision, and otherwise succeed or fail depending on whether the test passes or not. Let’s say they behave in a succeed/fail/throw manner.
The standard type tests like
integer/1 fail without further ado if they receive a fresh variable, there is no “unknown for now” for them. They behave in a succeed/fail/fail manner. Not nice.
Markus Triska writes on quora
First, the type-testing predicates like
compound/1would (and should) throw instantiation errors if their arguments are not sufficiently instantiated.
This is also what the original versions of Prolog did. However, DEC 10 Prolog chose to replace instantiation errors by silent failures, and this has been perpetuated in the Edinburgh tradition for type tests including the ISO standard.
The fact that the original behaviour was not kept is very unfortunate and easily leads to programs that are incomplete.
There is a related discussion on Stack Overflow: Safer type tests in Prolog. Quote:
integer(X)means that there is no integer. The reason
integer(X)fails is that DEC10 did not have errors, whereas its predecessor (Marseille) Prolog I did have errors, but nobody read the (French) papers.
So, I thought predicate
must_be/2 from library(error) would be more like it, throwing if unsure, succeeding if the check passes, and failing otherwise (being succeed/fail/throw). But actually not!
must_be/2 doesn’t fail, it throws instead (i.e. its behaviour is succeed/throw/throw).
On the other hand,
is_of_type/2 uses the old-school succeed/fail/fail behaviour.
What’s the design rationale behind
must_be/2, and is there a predicate that does succeed/fail/throw?
(Also I don’t understand
current_type/3 … what does it do?)
Here is some test code (update: fixed because the catcher in
test(_,throws(Catcher)) cannot be a free variable that is set to a catcher term in the test body. (But why))
:- begin_tests(must_be). % --- % Old school testing for atom-icity % Silently fails on fresh variable (instead of throwing). % --- test(oldschool_yes) :- atom(foo). test(oldschool_no, fail) :- atom(1/137). test(oldschool_unknown, fail) :- atom(_). % --- % must_be/2: Likes to throw too much. % Test "must_be_no" had better fail instead of throwing? % --- test(must_be_yes) :- must_be(atom,foo). test(must_be_no, error(type_error(_,_),_)) :- must_be(atom,1/137). test(must_be_unknown, error(instantiation_error)) :- must_be(atom,_). % doesn't run backwards test(must_be_fwd_only, error(instantiation_error)) :- bagof(X, must_be(X,foo), _Types). % --- % is_of_type/2: Behaves old-school-ish % --- test(is_of_type_yes) :- is_of_type(atom,foo). test(is_of_type_no, fail) :- is_of_type(atom,1/137). test(is_of_type_unknown, fail) :- is_of_type(atom,_). % doesn't run backwards test(is_of_type_fwd_only, error(instantiation_error)) :- bagof(X, is_of_type(X,foo), _Types). :- end_tests(must_be). rt :- run_tests(must_be).