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

On Sep 16, 2014, at 19:19, Paulo Moura <[email protected]> wrote:

> 
> On 16/09/2014, at 10:42, Kuniaki Mukai <[email protected]> wrote:
> 
>> 
>> On Sep 16, 2014, at 16: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) =:= 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.
>> 
>> It looks symmetric, nice, and easy to memorise.  Description 
>> is clear.
>> 
>> However, I have a basic question  about mode declaration.  
>> As you know, Prolog is a relational language, and input and output of prolog process 
>> are constraints. From that established point of view on Prolog, what is the 
>> mode declaration  for ?  So, I supposed that it is only for Prolog compiler not 
>> for human, to produce efficient and safe codes.  In fact, I never have custom 
>> to see mode declarations, which, of course, I never recommended to others.
>> 
>>> 
>>> 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,
>> 
>> Any current mode declaration to my foo above seems not appropriate. 
>> So, giving up mode declaration, I should describe f(X, Y) as 
>> 
>> 	X and Y are unified if such and such condition hold,
>> 
>> which is according to the Prolog principle as constraint language.
>> 
>> For curious, I wanted know what mode declaration  did you give 
>> to =/2. But edit(=) fails.
> 
> The standard specifies it as:
> 
> 8.2.1.2 Template and modes
> 
> '='(?term, ?term?)
> 
> which can be seen as the most general template and modes for a predicate.


Thank you for your kindness.  

I wish someone will introduce powerful "mode inference" system 
to SWI-Prolog in the near future. 

Regards

Kuniaki

> 
> Cheers,
> 
> Paulo
> 
>>> 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.
>> 
>> I have no idea of such discussions. My favourite interpretation of 
>> the var type could be based on the standard model of first-order unification 
>> (Colmerauer's style,  for  instance) that the var type 
>> is its current equivalent class of terms including variables wrt unification
>> I think most LP people agrees on this, though such var semantics 
>> is a kind of  "meta type". So interpreted, as you say
>> var is a type.  I can not say any more on this.
>> 
>> Thank you for your reply. I will start to use  pldoc
>> with more easy-going mind as for mode declaration. 
>> 
>> 
>> Kuniaki 
>> 
>> 
>> 
>>> 
>>> 	Cheers --- Jan
>>> _______________________________________________
>>> SWI-Prolog mailing list
>>> [email protected]
>>> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
>> 
>> -------------- next part --------------
>> A non-text attachment was scrubbed...
>> Name: signature.asc
>> Type: application/pgp-signature
>> Size: 496 bytes
>> Desc: Message signed with OpenPGP using GPGMail
>> URL: <https://lists.iai.uni-bonn.de/pipermail/swi-prolog/attachments/20140916/5cba5c2e/signature.asc>
>> _______________________________________________
>> SWI-Prolog mailing list
>> [email protected]
>> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
> 
> -----------------------------------------------------------------
> Paulo Moura
> Logtalk developer
> 
> Email: <mailto:[email protected]>
> Web:   <http://logtalk.org/>
> -----------------------------------------------------------------
> 
> 
> 
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://lists.iai.uni-bonn.de/pipermail/swi-prolog/attachments/20140916/84c81b8a/signature.asc>