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

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 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 =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. =


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

8.3 Type testing

These built-in predicates test the type associated with a term as defined i=
n 7.1.
...

There are no reference to "modes" in this section. Interestingly, in sectio=
n "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the sect=
ion starts with the text "The type of each argument is defined by one of th=
e 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".

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

I don't necessarily disagree with you here. Just quoting the official ISO P=
rolog Core standard.

> In the case of foo you are actually talking about modes, more precisely t=
he 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?).

The argument can be a variable or a partly instantiated term on input and f=
urther instantiated by the call.

Cheers,

Paulo

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

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