Re: pldoc: how to specify predicates with arguments unbound.

Jan Wielemaker <[email protected]> Tue, 16 Sep 2014 09:30:02 +0200
Newsgroups gmane.comp.ai.prolog.swi
Message-ID <[email protected]>
Hi Kuniaki,

On 09/16/2014 07:57 AM, Kuniaki Mukai wrote:
>
> Hi,
>
> Using pldoc, how do we specify a predicate such as follows:
>
>	foo(X, Y) :-  (random(3) =:= 2, X==Y;  true).
>
> foo is designed so that it returns information on the current state
> on unification (constraint)   X==Y or X\==Y.  So X, and Y are always unbound
>  (var(X), var(Y) are always true).  I often wrote such predicates.
>
> Reading pldoc document, the following seems only possible form for foo/2.
>
> % foo(-X, -Y)  is det.
>
> Is it right ?  Or, is there any other neat form of specification
> to tell such intention of programmer of foo above.

Seems close to me. The predicate is `multi` though: it succeeds one or
two times (a rarely used qualifier). At some point, I think we need a
more advanced mode system, which I think should be:

  --X	X *must* be unbound on input (e.g. the stream argument of open/3).
        Typically used for output arguments that cannot be predicted by
	the caller and thus providing an instantiated argument will always
	cause failure.
   -X   X is output.  It's binding has no impact on the semantics and the
        predicate behaves as p(NewVar), NewVar = X.  I.e., it is steadfast
        wrt this argument.  Notably, it does *not* mean X must be unbound.
   @X   X is examined, but not altered in any way (e.g., type checks).
   ?X	Either -X or +X.  Can be used as a shorthand for listing 2**N
        modes (where N is the number of ?X args).  E.g., we do not want
        to list 8 modes for append/3.  atom_concat(?,?,?) however is
        wrong because at least two of the arguments must be +.
   +X   X is input.  It must have a value that is *compatible* with the
        type.  I.e., X is a generalization of at least one instance of the
	type.  As far as I'm concerned, this would also mean that
	if the type is `any`, a variable satisfies.
  ++X   X is input and bound to an instance of the type.  I.e.,
	sort(++List, -Result) because sort cannot sort partial lists.

If there sufficient consensus to add ++ and -- to PlDoc and add this to
the documentation? Then we only need a volunteer to go through the
manuals ...

I'm afraid this is still not really a good answer to foo/2. --X demands
the right instantiation, but the arguments are never altered, while --X
args are typically instantiated by the predicate. That would suggest @X,
but this allows for nonvar. @X:var could be used, but most LP people
claim that var is not a type.

	Cheers --- Jan