What's the rationale for `must_be/2` to throw on type mismatch?

Help!
1

In Type tests in Prolog (YouTube presentation of the series “The Power of Prolog”), the type-testing predicates atom_si/1, integer_si/1, list_si/1 (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 atom/1, 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 atom/1, integer/1 and compound/1 would (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:

An answer false to 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).
1 Like