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
2

Throwing in the event of incorrect instantiation allows us to see where we have logical errors in the domain. Silent failure is not always a nice way to proceed when the domain has been accidentally expanded to a class we didn’t expect. If you mean for a predicate to choose amongst options, or silently fail on a given type then you don’t want must_be/2, but if you think the contract of a predicate should ensure that it is never called without passing a given type, then you can ensure the buck stops there.

I’ve found silent failure to be very irritating and confusing during debugging and so I often either insert assertions, write smaller chunks or code defensively. Ultimately it would be nice to have a very seamless system that allows a combination of static and dynamic reasoning to avoid these problems. Maven gets us part of the way there - another useful piece of the puzzle is Schriver’s “type-check” - but neither of them are not quite ergonomic enough to really be used in anger (yet).

A perhaps less important point is that it allows you to reason about predicates in such a way that we can use flow analysis to determine whether type checks are required. This could (in principle) be used to do things like unboxing or other optimisations while being less precise (subsequent disjunction/choice-points do not need to be treated specially) than would be required otherwise.

For instance:


p(X) :- 
  must_be(integer, X).

r(X,Y) :- 
  Y is X + 1.

q(X,1) :- 
  p(X).
q(X,Y) :-
  r(X,Y).

Once we have encountered p/1 we know that X is going to be an integer in r/2.

1 Like
4

That’s exactly the point. In fact, I have come to this conclusion:

  1. Traditional Prolog type tests atom/1, integer/1 etc. are faulty because they “silently fail”:
  • Type match: Success
  • Type mismatch: Failure
  • Cannot decide because a fresh variable was passed: Silent failure
  1. The intent of must_be/2 is to do contract checks on predicate entry (or exit). That’s why it is in library(error). So its behaviour is as expected:
  • Type match: Success
  • Type mismatch: Throw
  • Cannot decide: Throw
  1. The intent of is_of_type/2 is to mirror the behaviour of traditional type-checking in a more flexible way. Thus:
  • Type match: Success
  • Type mismatch: Failure
  • Cannot decide because a fresh variable was passed: Silent failure
  1. We still need the atom_si/1 , integer_si/1 , list_si/1 etc. which are nowhere to be found currently, so that we can have:
  • Type match: Success
  • Type mismatch: Failure
  • Cannot decide: Throw
5

It seems that typing has been on on-and-off-affair since the 80s (there is even the old-ish paper collection, June 1992: Types in Logic Programming - I have a copy). It would probably not hurt to have at least “sorts” one day. (And now the functional programming languages are starting to use Dependent Types … what does that imply?)

For SWI-Prolog there is this (among others):

Clojure people seem to avoid typing, even though Typed Clojure exists (someone said "we stopped using it, spending too much type on getting the type definitions right), instead, “specs” (runtime checks, precondition, postcondition, invariants) are preferred: clojure.spec. Another case of “worse is better” (or at least more flexible)?

Prolog has a its own spec library plspec, a work in progress. Provides the possibility to perform runtime checks on precondition, postconditions and invariants:

Here is Covington et al. giving a bit of dubious advice:

Covington et al. says on page 30:

Develop your own ad hoc run-time type and mode checking system. Many problems during development (especially if the program is large and/or there are several developers involved) are caused by passing incorrect arguments. Even if the documentation is there to explain, for each predicate, which arguments are expected on entry and on successful exit, they can be, and all too often they are, overlooked or ignored. Moreover, when a “wrong” argument is passed, erratic behavior can manifest itself far from where the mistake was made (and of course, following Murphy’s laws, at the most inconvenient time).

In order to significantly mitigate such problems, do take the time to write your own predicates for checking the legality of arguments on entry to and on exit from your procedures. In the production version, the goals you added for these checks can be compiled away using goal_expansion/2.

The above is fun, but is not a scalable approach.

7

I find it easier to mark predicates that must succeed because my errors tend to be not matching complex structures rather than having int/atom style mismatches. library(rdet) is a good start, but needs some work (e.g., it’s also useful to check that a deterministic predicate is truly deterministic but library(rdet) doesn’t do that). [library(rdet) throws an error, of course]

1 Like
8

Its a difficult topic as we have both types and instantiation. The Ciao team probably has the most mature view on these things. They (hope I rephrase correctly) claim indeed that atom/1, etc are wrong. What they want is is_type/1 for every type and type/1 for every type. type/1 then means the argument is compatible with the type. We should read that the argument either is instantiated to something that satisfies the type or can still be instantiated to something that satisfy the type. So, a variable passes all type/1 tests.

Finally we have modes that determine det/semidet/nondet/… for inputs satisfying some type and instantiation. If you want to describe all that such that the programming style that is permitted and commonly used in dynamically typed Prolog you can a rather complex annotation that is computationally not tractable with acceptable performance.

That (in my understanding) is why we have not yet seem a type system that has been widely accepted in the Prolog community. My vision out there in the long run is to have a rather simple type and mode annotation system and try to find obvious type violations rather than proving correctness. This gets closer to the linting approach with which we do have some success and that Paulo took a step further in Logtalk recently.

4 Likes
10

must_be/2 is not optimized in any way. It is no more and no less than a cheap and explicit way to add type checks intended primarily for public APIs of libraries. Some people tend to stick it in everywhere. That may seriously slow down the code. I almost never use it in cases where built-in predicates do a reasonable job anyway.

I think the most pragmatic solutions is what @edison is using (AFAIK): a simplified version of the Ciao assertion language for type declarations that is used to insert runtime checks, I guess typically use only during development.

1 Like
11

Ciao Prolog’s assertion system: REGTYPE

This gives us a relatively compact way to represent a lot of information, the mode, the compatible types, pre-conditions which must be satisfied on calls, post-conditions which must be satisfied on exit, and global conditions. And even a comment which can provide the warning/error text in the event of failure.

I think this is very useful documentation about what a predicate is supposed to achieve in terms of interface, even if what you write is completely ignored by the host system.

However, we could do as Jan suggested, and take a linting approach with three phases.

  • Static: In cases that we can determine a conflict with the conditions, we throw a warning or error.
  • Dynamic: In test mode we insert dynamic checks to ensure that the properties hold or throw an error.
  • Production: In production mode we leave the code as written.

In terms of dependent types, representing these in prolog is not terribly difficult. You just need to parameterise your types with concrete terms. However, calls like must_be would need to be able to take a parametric type argument. A Linting approach could attempt to check some reasonable fragment - and at runtime / dynamically this is really quite simple - just run the code and see if it fails.

3 Likes
13

This sounds like the thread’s “solution” (if it needs to have any). Lots of good pointers, thank you everyone.

14

As final post, here is a simple plunit block to illustrate the various “approaches” (can one call them that) to type testing:

16

The drop-down only shows the manual. This comes from a pack. The documentation does include the documentation of predicates in the packs but does not include it in the search. Probably that is a bad idea and should be removed.