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

On 16/09/2014, at 13:34, G=FCnter Kniesel <[email protected]> wrote:

> =

> =

> Am 16.09.2014 12:15, schrieb Paulo Moura:
>> =

>> On 16/09/2014, at 10:51, G=FCnter Kniesel <[email protected]> wrote:
>> =

>>> =

>>> =

>>> 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 ar=
e always unbound
>>>>>> (var(X), var(Y) are always true).  I often wrote such predicates.
>>>>>> =

>>>>>> Reading pldoc document, the following seems only possible form for f=
oo/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 ste=
adfast
>>>>>        wrt this argument.  Notably, it does *not* mean X must be unbo=
und.
>>>>>   @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 deman=
ds
>>>>> 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 actuall=
y mode testing predicates.
>> =

>> Note that's not how they are described in the official ISO Prolog Core s=
tandard:
>> =

>> 8.3 Type testing
>> =

>> These built-in predicates test the type associated with a term as define=
d in 7.1.
>> ...
>> =

>> There are no reference to "modes" in this section. Interestingly, in sec=
tion "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the s=
ection starts with the text "The type of each argument is defined by one of=
 the following types:").
>> =

>>> [Paulo: Calling this type testing is an inaccuracy that was forgivable =
in a language without types.
>> =

>> Nowhere in my previous message I call it "type testing".
> =

> You quoted the standard, which uses this terminology.
> =

>>> But when one is discussing how to add types one should not perpetuate i=
naccurate old terminology.]
>> =

>> I don't necessarily disagree with you here. Just quoting the official IS=
O Prolog Core standard.
> =

> Thanks for clarifying that quoting the standard does not mean suggesting =
the further use of its 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 predica=
te 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 understa=
nd. How can something be output, if it was not free initially?).
>> =

>> The argument can be a variable or a partly instantiated term on input an=
d further instantiated by the call.
> =

> If it is partly instantiated overlaps with +
> =

> Thus + and - are additional candidates for conjunctive use since +-
> would express exactly the partly instantiated terms that will be further =
instantiated. Or how would one express them otherwise?

With a combination with type information, I don't see the need for what you=
 call conjunctive use. For example (again quoting the standard):

clause(+head, ?callable_term)

+head means that its an input argument that can be further instantiated.

?callable_term means that the argument can be either a variable or a (possi=
bly partially) instantiated term on call but that will be instantiated to a=
 callable term on exit =


You could write instead:

clause(+head, -callable_term)
clause(+head, +callable_term)

But I don't see the need for splitting the two cases. For me, "?" clearly e=
xpresses "partly instantiated terms that will be further instantiated". Oth=
erwise we would use "@" instead.

Am I missing something in your argument?

Cheers,

Paulo

-----------------------------------------------------------------
Paulo Moura
Logtalk developer

Email: <mailto:[email protected]>
Web:   <http://logtalk.org/>
-----------------------------------------------------------------