What kind of meta argument is the first argument of predicate_property/2?

In other words, should it be 0 or : or something else? The Prolog systems SICStus, YAP, and SWI all indicate this as :. Is this appropriate? Shouldn't it be rather a 0 which means a term that can be called by call/1?

To check your system type:

| ?- predicate_property(predicate_property(_,_),P).
P = (meta_predicate predicate_property(:,?)) ? ;
P = built_in ? ;
P = jitted ? ;
no

I should add that meta-arguments — at least as in the form used here — cannot guarantee the same algebraic properties we expect from pure relations:

?- S=user:false, predicate_property(S,built_in).
S = user:false.

?- predicate_property(S,built_in), S=user:false.
false.

Here is the relevant part from ISO/IEC 13211-2:

7.2.2 predicate_property/2

7.2.2.1 Description

predicate_property(Prototype, Property) is true in the
calling context of a module M iff the procedure associated with the
argument Prototype has predicate property Property.

...

7.2.2.2 Template and modes

predicate_property(+prototype, ?predicate_property)

7.2.2.3 Errors

a) Prototype is a variable
— instantiation_error.

...

c) Prototype is neither a variable nor a callable term
— type_error(callable, Prototype).

...

7.2.2.4 Examples
Goals attempted in the context of the module
bar.

predicate_property(q(X), exported).
    succeeds, X is not instantiated.
...

Solution

Thats an interesting question. First I think there are two kinds of predicate_property/2 predicates. The first kind takes a callable and is intended to work smoothly with for example vanilla interpreters and built-ins such as write/1, nl/0, etc.., i.e.:

solve((A,B)) :- !, solve(A), solve(B).
solve(A) :- predicate_property(A, built_in), !, A.
solve(A) :- clause(A,B), solve(B).

For the first kind, I guess the 0 meta argument specifier would work fine. The second kind of predicate_property/2 predicates works with predicate indicators. Callable and predicate indicators are both notions already defined in the ISO core standard.

A predicate indicator has the form F/N, where F is an atom and N is an integer. Matters get a little bit more complicated if modules are present, especially because of the operator precedence of (:)/2 versus (/)/2. If predicate property works with predicate indicators, we can still code the vanilla interpreter:

solve((A,B)) :- !, solve(A), solve(B).
solve(A) :- functor(A,F,N), predicate_property(F/N, built_in), !, A.
solve(A) :- clause(A,B), solve(B).

Here we loose the connection of a possible meta argument 0, for example of solve/1, with predicate property. Because functor/3 has usually no meta predicate declaration. Also to transfer module information via functor/3 to predicate_property/2 is impossible, since functor/3 is agnostic to modules, it usually has no realization that can deal with arguments that contain module qualification.

There are now two issues:
1) Can we give typing and/or should we give typing to predicates such as functor/3.
2) Can we extend functor/3 so that it can convey module qualification.

Here are my thoughts:
1) Would need a more elaborate type system. One that would allow overloading of predicates with multiple types. For example functor/3 could have two types:

  :- meta_predicate functor(?,?,?).
  :- meta_predicate functor(0,?,?).

The real power of overloading multiple types would only shine in predicates such as (=)/2. Here we would have:

  :- meta_predicate =(?,?).
  :- meta_predicate =(0,0).

Thus allowing for more type inference, if one side of (=)/2 is a goal we could deduced that the other side is also a goal.

But matter are not so simple, it would possibly make sense to have also a form of type cast, or some other mechanism to restrict the overloading. Something which is not covered by introducing just a meta predicate directive. This would require further constructs inside the terms and goals.

Learning form lambda Prolog or some dependent type system, could be advantageous. For example (=)/2 can be viewed as parametrized by a type A, i.e.:

 :- meta_predicate =(A,A).

2) For Jekejeke Prolog I have provided an alternative functor/3 realization. The predicate is sys_modfunc_site/2. And it works bidirectionally like functor/3, but returns and accepts the predicate indicator as one whole thing. Here are some example runs:

 ?- sys_modfunc_site(a:b(x,y), X).
 X = a:b/2
 ?- sys_modfunc_site(X, a:b/2).
 X = a:b(_A,_B)

The result of the predicate could be called a generalized predicate indicator. It is what SWI-Prolog already understands for example in listing/1. So it could have the same meta argument specification as listing/1 has. Which is current : in SWI-Prolog. So we would have, and subsequently predicate_property/2 would take the : in its first argument:

 :- meta_predicate sys_modfunc_site(?,?).
 :- meta_predicate sys_modfunc_site(0,:).

The vanilla interpreter, that can also deal with modules, then reads as follows. Unfortunately a further predicate is needed, sys_indicator_colon/2, which compresses a qualified predicate indicator into an ordinary predicate indicator, since our predicate_property/2 does not understand generalized predicate indicators for efficiency reasons:

solve((A,B)) :- !, solve(A), solve(B).
solve(A) :- 
      sys_modfunc_site(A,I), 
      sys_indicator_colon(J,I), 
      predicate_property(J, built_in), !, A.
solve(A) :- clause(A,B), solve(B).

The above implements a local semantic of the colon (:)/2, compared to the rather far reaching semantic of the colon (:)/2 as described in the ISO module standard. The far reaching semantic imputes a module name on all the literals of a query. The local semantic only expects a qualified literal and just applies the module name to that literal.

Jekejeke only implements local semantic with the further provision that call-site is not changed. So under the hood sys_modfunc_site/2 and sys_indicator_colon/2 have also to transfer the call-site so that predicate_property/2 makes the right decision for unqualified predicates, i.e. resolving the predicate name by respecting imports etc..

Finally a little epilog:
The call-site transfer of Jekejeke Prolog is a pure runtime thing, and doesn't need some compile time manipulation, especially no ad hoc adding of module qualifiers at compile time. As a result certain algebraic properties are preserved. For example assume we have the following clause:

 ?- [user].
 foo:bar.
 ^D

Then the following things work fine, since not only sys_modfunc_site/2 is bidirectional, but also sys_indicator_colon/2:

  ?- S = foo:bar/0, sys_indicator_colon(R,S), predicate_property(R,static).
  S = foo:bar/0,
  R = 'foo%bar'/0
  ?- predicate_property(R,static), sys_indicator_colon(R,S), S = foo:bar/0.
  R = 'foo%bar'/0,
  S = foo:bar/0

And of course predicate_property/2 works with different input and output modes. But I guess the SWI-Prolog phaenomenom has first an issue that a bare bone variable is prefixed with the current module. And since false is not in user, but in system, it will not show false. In output mode it will not show predicates which are equal by resolution. Check out in SWI-Prolog:

 ?- predicate_property(X, built_in), write(X), nl, fail; true.
 portray(_G2778)
 ignore(_G2778)
 ...
 ?- predicate_property(user:X, built_in), write(X), nl, fail; true.
 prolog_load_file(_G71,_G72)
 portray(_G71)
 ...
 ?- predicate_property(system:X, built_in), write(X), nl, fail; true.
 ...
 false
 ...

But even if the SWI-Prolog predicate_property/2 predicate would allow bar bone variables, i.e. output goals, we would see less commutativity in the far reaching semantic than in the local semantic. In the far reaching semantic M:G means interpreting G inside the module M, i.e. respecting the imports of the module M, which might transpose the functor considerable.

The far reaching semantic is the cause that user:false means system:false. On the other hand, in the local semantics, where M:G means M:G and nothing else, we have the algebraic property more often. In the local semantics user:false would never mean system:false.

Bye