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

Am 16.09.2014 10:58, schrieb Paulo Moura:
>
> On 16/09/2014, at 08:30, Jan Wielemaker <[email protected]> wrote:
>
>> 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) =3D:=3D 2, X=3D=3DY;  true).
>>>
>>> foo is designed so that it returns information on the current state
>>> on unification (constraint)   X=3D=3DY or X\=3D=3DY.  So X, and Y are a=
lways 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 =3D X.  I.e., it is stead=
fast
>>         wrt this argument.  Notably, it does *not* mean X must be unboun=
d.
>>    @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 t=
he
>> 	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.

Var is indeed not a type but a mode, and var/1 and nonvar/1 are actually =

mode testing predicates. [Paulo: Calling this type testing is an =

inaccuracy that was forgivable in a language without types. But when one =

is discussing how to add types one should not perpetuate inaccurate old =

terminology.]

In the case of foo you are actually talking about modes, more precisely =

the conjunction of two modes
  - 'mandatory free' (--) and
  - 'readonly' (@)

So the logical solution for specifying foo is to write @-- for saying
that a variable must be free and only mode testing will be performed
on it.

Which boils down to allowing conjunction of modes in the syntax.
More precisely, to allowing @ (readonly) as conjunction to any other,
since all the others are disjoint cases.

Conjunction of @ and any other mode also makes sense because it makes
explicit that we have here two categories of modes:

@ talks about how  an argument is used internally by the called =

predicate whereas all the others talk about the value of the argument at =

call time (However, I'm unsure about - whose difference to -- I don't =

fully understand. How can something be output, if it was not free =

initially?).

Regards,
G=FCnter