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

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.

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/>
-----------------------------------------------------------------