Must_be, can_be, is_not

Scryer Prolog has a can_be predicate: scryer-prolog/error.pl at c1218fc98688a397080ec41d6ba57ef5e70a05e1 · mthom/scryer-prolog · GitHub

Looking for similar in SWI-Prolog, I see is_not but it appears to be private. swipl-devel/error.pl at 7bcfc8546b9acf3b966b1d80d36d4cecb086721b · SWI-Prolog/swipl-devel · GitHub.

Is there a reason not to expose it?

If it was exposed, could I do something like this:
can_be(Type, Term) :- \+ is_not(Type, Term).

I’m not sure about can_be’s purpose, but code is linked to at must_be/2 - is it helpful?

must_be guarantees a term is a particular type. The purpose of can_be is to say that as it stands, a term can later be unified to type.

The notes in the example you linked to say:

The corresponding predicates do not exist. We add an implmentation for “atom” for illustration.

I’m suggesting: the corresponding predicates might easily exist or be implemented. IF we had access to is_not.

You can use freeze/2:

?- freeze(X, must_be(integer, X)), X = 1.
X = 1.
?- must_be(integer, X).
ERROR: Arguments are not sufficiently instantiated
   ...

Good to know about freeze, thanks. But still not at useful as can_be for this purpose. For example, this will cause problems (even though L can be a list):

freeze(L, must_be(list, L)), L = [1|T], T = [].

Yes, there ought to be “freeze” versions of the various must_be/2 predicates, and proper_list would need to be implemented differently than freeze(L, must_be(proper_list, L)).

(If can_be/2 does nothing when the variable is uninstantiated, then it’s rather misleading.)

How so? If I want a predicate to test that a term can be unified with a list, what should I call it? Whatever the answer, let’s call it that.

What is the meaning of can_be(list, X), X = an_atom? If can_be/2 succeeds if the argument is uninstantiated, then this seems to be logically nonsense (because X = an_atom, can_be(list, X) will fail.

It is definitely not is_not/2. That predicate is part of must_be/2 and responsible for the error message. So, if X is not a list we call is_not(list, X) which will figure out which error to throw (basically an instantiation error or a type error).

The idea of a can_be/2 makes sense. Shouldn’t be too hard to add to library(error). If someone likes to give it a try, I’m happy to consider the PR.

It might better (?) relate to work that is sleeping for a long time and defines Prolog types as constraints. So, you can do ?- type(X, atom), type(Y, integer), X = Y. and it will fail :slight_smile: On the other hand, this library is more intended for abstract interpretation/type checking. I assume can_be/2 is no constraint, so we can happily do this?

?- can_be(integer, X), X = a.
1 Like

Yes, I see that now.

Indeed, it’s expected to work this way.

In the “Power of Prolog” video I linked, Markus Triska explains it as:

Silent failure for wrong types is default practice in Prolog code.
Type errors help us determine the exact location of mistakes.
However, a sound distinction between type errors and instantiation errors is hard to get right manually.
Therefore, if you want type errors, use:

  • must_be/2 for arguments that must be sufficiently instantiated
  • can be/2 for output and general arguments

:+1:

1 Like