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

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 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 fo=
o/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 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 st=
andard:
>
> 8.3 Type testing
>
> These built-in predicates test the type associated with a term as defined=
 in 7.1.
> ...
>
> There are no reference to "modes" in this section. Interestingly, in sect=
ion "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the se=
ction 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 i=
n 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 in=
accurate old terminology.]
>
> I don't necessarily disagree with you here. Just quoting the official ISO=
 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 predicat=
e 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 understan=
d. 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=
 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?

Cheers,
G=FCnter