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

Hi Jan, 

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.

I am not sure in what sense we are close. Rather, I am having a hard time to follow
this thread *as usual* because lack of background knowledge,  
but also, I am learning interesting ideas on modes and types 
in prolog for the first time for me: 

1)  (boolean) combinations are possible over modes,
2)  var is not a type (LP majority opinion)
3)  a mode indicates instantiation difference between terms at in and out.
4)  Mercury has already lot of good works on mode inference.

So understanding, the following declaration for my example foo/2,
I guess, might be close to what Jan might have in mind.

    foo(var, var)  is det.

Is it close or getting far ? 

I would like to understand  1) as follows:  var, arithmetics, atom, string, term
are modes, that is, all syntactical categories of prolog standard terms, including 
prolog variables and lists  are (basic) modes.  In particular, 'term' is 
the largest (universal) mode,  and, for instance, the following is a complex mode
constructed with boolean operators  or and not:

  (atom or integer) and  not(ground)

"+" prefix sign of mode, say m, should means that the argument passed to the argument place
will be *properly* instantiated toward a term of mode m during the process.  
The argument without sign mode m mode *may be* instantiated toward a term of mode m.  

However, I have found I can not find place for + @ ? sign for mode declaration. So
I am missing some important points of mode declaration under discussions. 
I only hope my naive intuition on mode inspired gets some points 
under discussions.

Kuniaki

> 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.
> 
> 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.
> 
> 	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/20140917/cb1b79de/signature.asc>