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

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.

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