pldoc: how to specify predicates with arguments unbound.

classic Classic list List threaded Threaded
21 messages Options
12
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

pldoc: how to specify predicates with arguments unbound.

Kuniaki Mukai

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.

Kuniaki Mukai





-------------- 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/0ddd7d53/signature.asc>
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Jan Wielemaker-5
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.

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
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Wouter Beek-2
In reply to this post by Kuniaki Mukai
Hi Jan,

I would very much appreciate the inclusion of an advanced mode system and
of ++ and -- to plDoc. This would also widen the opportunities for add-on
writers who want to utilize plDoc annotations in order to perform some
automated tests, e.g. Michael Hendricks' Mavis
<http://www.swi-prolog.org/pack/list?p=mavis>.

I gradly volunteer to make such improvements to the existing documentation.

---
Best regards!,
Wouter Beek.

E-mail: [hidden email]
WWW: www.wouterbeek.com
Tel.: 0647674624


On Tue, Sep 16, 2014 at 9:30 AM, Wielemaker, J. <[hidden email]> 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.
>
> 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
> [hidden email]
> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
>
-------------- next part --------------
HTML attachment scrubbed and removed
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Paulo Moura-2
In reply to this post by Jan Wielemaker-5

On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>
> 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,

My choice when using Logtalk's mode/2 directives is similar:

:- mode(foo(@var, @var), one).  % 'one' means one solution

> but most LP people claim that var is not a type.

Yet, we have an official standard with sections "7.1 Types" and "7.1.1 Variable" with the text "The type of any term is determined by its abstract syntax (6.1.2)." plus sections "8.3 Type testing", "8.3.1 var/1", and "8.3.7 nonvar/1".

Cheers,

Paulo

-----------------------------------------------------------------
Paulo Moura
Logtalk developer

Email: <mailto:[hidden email]>
Web:   <http://logtalk.org/>
-----------------------------------------------------------------




_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Kuniaki Mukai
In reply to this post by Jan Wielemaker-5

On Sep 16, 2014, at 16:30, Jan Wielemaker <[hidden email]> 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
> [hidden email]
> 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
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Günter Kniesel
In reply to this post by Paulo Moura-2


Am 16.09.2014 10:58, schrieb Paulo Moura:

>
> On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>>
>> 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. [Paulo: Calling this type testing is an
inaccuracy that was forgivable in a language without types. But when one
is discussing how to add types one should not perpetuate inaccurate old
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
predicate 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 understand. How can something be output, if it was not free
initially?).

Regards,
Günter
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Paulo Moura-2

On 16/09/2014, at 10:51, Günter Kniesel <[hidden email]> wrote:

>
>
> Am 16.09.2014 10:58, schrieb Paulo Moura:
>>
>> On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>>>
>>> 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 standard:

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 section "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the section 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 in a language without types.

Nowhere in my previous message I call it "type testing".

> But when one is discussing how to add types one should not perpetuate inaccurate old terminology.]

I don't necessarily disagree with you here. Just quoting the official ISO Prolog Core standard.

> 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 predicate 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 understand. 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.

Cheers,

Paulo

-----------------------------------------------------------------
Paulo Moura
Logtalk developer

Email: <mailto:[hidden email]>
Web:   <http://logtalk.org/>
-----------------------------------------------------------------




_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Paulo Moura-2
In reply to this post by Kuniaki Mukai

On 16/09/2014, at 10:42, Kuniaki Mukai <[hidden email]> wrote:

>
> On Sep 16, 2014, at 16:30, Jan Wielemaker <[hidden email]> 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
>> [hidden email]
>> 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
> [hidden email]
> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

-----------------------------------------------------------------
Paulo Moura
Logtalk developer

Email: <mailto:[hidden email]>
Web:   <http://logtalk.org/>
-----------------------------------------------------------------




_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Kuniaki Mukai

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

>
> On 16/09/2014, at 10:42, Kuniaki Mukai <[hidden email]> wrote:
>
>>
>> On Sep 16, 2014, at 16:30, Jan Wielemaker <[hidden email]> 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
>>> [hidden email]
>>> 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
>> [hidden email]
>> https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
>
> -----------------------------------------------------------------
> Paulo Moura
> Logtalk developer
>
> Email: <mailto:[hidden email]>
> 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>
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Günter Kniesel
In reply to this post by Paulo Moura-2


Am 16.09.2014 12:15, schrieb Paulo Moura:

>
> On 16/09/2014, at 10:51, Günter Kniesel <[hidden email]> wrote:
>
>>
>>
>> Am 16.09.2014 10:58, schrieb Paulo Moura:
>>>
>>> On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>>>>
>>>> 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 standard:
>
> 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 section "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the section 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 in 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 inaccurate 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 predicate 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 understand. 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ünter
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Paulo Moura-2

On 16/09/2014, at 13:34, Günter Kniesel <[hidden email]> wrote:

>
>
> Am 16.09.2014 12:15, schrieb Paulo Moura:
>>
>> On 16/09/2014, at 10:51, Günter Kniesel <[hidden email]> wrote:
>>
>>>
>>>
>>> Am 16.09.2014 10:58, schrieb Paulo Moura:
>>>>
>>>> On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>>>>>
>>>>> 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 standard:
>>
>> 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 section "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the section 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 in 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 inaccurate 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 predicate 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 understand. 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?

With a combination with type information, I don't see the need for what you call conjunctive use. For example (again quoting the standard):

clause(+head, ?callable_term)

+head means that its an input argument that can be further instantiated.

?callable_term means that the argument can be either a variable or a (possibly partially) instantiated term on call but that will be instantiated to a callable term on exit

You could write instead:

clause(+head, -callable_term)
clause(+head, +callable_term)

But I don't see the need for splitting the two cases. For me, "?" clearly expresses "partly instantiated terms that will be further instantiated". Otherwise we would use "@" instead.

Am I missing something in your argument?

Cheers,

Paulo

-----------------------------------------------------------------
Paulo Moura
Logtalk developer

Email: <mailto:[hidden email]>
Web:   <http://logtalk.org/>
-----------------------------------------------------------------




_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Günter Kniesel


Am 16.09.2014 14:54, schrieb Paulo Moura:

>
> On 16/09/2014, at 13:34, Günter Kniesel <[hidden email]> wrote:
>
>>
>>
>> Am 16.09.2014 12:15, schrieb Paulo Moura:
>>>
>>> On 16/09/2014, at 10:51, Günter Kniesel <[hidden email]> wrote:
>>>
>>>>
>>>>
>>>> Am 16.09.2014 10:58, schrieb Paulo Moura:
>>>>>
>>>>> On 16/09/2014, at 08:30, Jan Wielemaker <[hidden email]> 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.
>>>>>>
>>>>>> 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 standard:
>>>
>>> 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 section "8.1.2.1 Type of an argument", "nonvar" is listed but not "var" (the section 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 in 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 inaccurate 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 predicate 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 understand. 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?
>
> With a combination with type information, I don't see the need for what you call conjunctive use. For example (again quoting the standard):
>
> clause(+head, ?callable_term)
>
> +head means that its an input argument that can be further instantiated.
>
> ?callable_term means that the argument can be either a variable or a (possibly partially) instantiated term on call but that will be instantiated to a callable term on exit
>
> You could write instead:
>
> clause(+head, -callable_term)
> clause(+head, +callable_term)
>
> But I don't see the need for splitting the two cases. For me, "?" clearly expresses "partly instantiated terms that will be further instantiated". Otherwise we would use "@" instead.
>
> Am I missing something in your argument?

In the proposal cited in this mail ? means "+ or -" and says nothing
about whether further instantiation will happen.

If there IS a need to express that further instantiation will happen,
then I see no other way than combining + and - to +-

If there IS NO need to make this distinction than I don't see any
need to distinguish + and - at all.

Am I missing something?

Cheers,
Günter


> Cheers,
>
> Paulo
>
> -----------------------------------------------------------------
> Paulo Moura
> Logtalk developer
>
> Email: <mailto:[hidden email]>
> Web:   <http://logtalk.org/>
> -----------------------------------------------------------------
>
>
>
>

--
Günter Kniesel

--------------------------------------------------------------------
Dr. Günter Kniesel                    http://www.cs.uni-bonn.de/~gk/
Institut für Informatik III                        [hidden email]
Universität Bonn
Römerstr. 164 (Raum A107)                      Tel (+49 228) 73-4511
D-53117 Bonn                                   Fax (+49 228) 73-4382
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Jan Wielemaker-5
In reply to this post by Günter Kniesel
On 09/16/2014 02:34 PM, Günter Kniesel wrote:

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

We forgot one: ":", which is used to denote that the argument is module
sensitive. I.e. if can be written as module:Value and if this is not
done the system will turn Value into module:Value, using the corrent
context module. That too is not really a mode :-( It is not a type
either though. Typically, :X means :++X:callable (i.e., module sensitive
and must be instantiated to a callable term at entry), but there are
several exceptions where the argument has different modes and types.

This suggests ++, +, -, -- as core modes, @ and : as modifiers.

>>> 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
>>> predicate 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 understand. How can something be output, if it was not
>>> free initially?).

- means stead-fastness. Typically is/2 is referenced as is(-,+) (should
be ++ in the proposed mode annotation). But, `3 is 1+2` is completely
fine.  We could of course define that we have modes

   -  is ++
   ++ is ++

That is a lot of typing and pratically all predicates that have a -
argument accept that this argument is already (partially or fully)
instantiated with the correct output. In the proposed notation, -
captures this. For some predicates, the output must be unbound or the
predicate will produce the wrong answer. Such predicates are not
steadfast and should be fixed. For some predicates though, this is
meaningless. E.g.

   ?- open(file, read, 42).

is an error. Read will create a stream, give it a guaranteed unique
(ground) value and tries to unify this with 42. That will fail, so
Ulrich proposed the `uninstantiation_error` for these cases. It would be
nice if a type and mode annotation can express this is invalid.  Such
an annotation can trap common errors, such as reusing a Stream variable
for opening two different streams.

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

As Paulo and you claimin further mails, combining + with - is not very
meaningful.  + and - have a very different meaning though, as + means
that the argument must be instantiated to the type and - means it may
be partially instantiated.  So, we have sort(+, -) which means that
these are fine:

   sort([2,3], X),
   sort([2,3], [5|Y]),

but this is not:

   sort([2|_], L).

Same with Paulo's argument: clause(+head, -callable_term) means that
we get:

   5 ?- clause(H, true).
   ERROR: Arguments are not sufficiently instantiated
   ERROR: In:
   ERROR:    [6] clause(_G4381,true)

Well, I think we can assemble a good set of modes from Ciao's assertion
language, Edison's simplication thereof and the various documentation
systems.  Ideally, the modes when combined with types, provide pre and
post conditions for goals.  Someone?

        Cheers --- Jan



_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Michael Hendricks
In reply to this post by Jan Wielemaker-5
I'm glad this conversation has come up.  Wouter and I talked about this a
couple weeks ago and it's been on my mind a lot since then.


On Tue, Sep 16, 2014 at 1:30 AM, Jan Wielemaker <[hidden email]> wrote:

> At some point, I think we need a
> more advanced mode system, which I think should be:
>

I too would like a more powerful language for describing modes and
determinism.  What do we want this system to accomplish?  I have three
personal goals:

    * provide clear, concise documentation of how a predicate should be used
    * allow for runtime checks of argument instantiation and predicate
backtracking behavior
    * allow for static analysis (like check/0) to find misuses early


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

I'd like to move away from sigils (to borrow Perl's terminology) for
indicating modes.  We have a limited number of punctuation characters but
nearly limitless mode possibilities.  It's also difficult to remember the
meaning of each punctuation.  Even those who do remember the punctuation
seem to have varying interpretations of their meaning.

I suggest that we define modes similar to how we define types.  I take
error:has_type/2 as my model.  The Mercury documentation
<http://mercurylang.org/information/doc-release/mercury_ref/Insts-modes-and-mode-definitions.html#Insts-modes-and-mode-definitions>
defines a mode as "a mapping from the initial state of instantiation of the
arguments of the predicate ... to their final state of instantiation".  So
perhaps we have something like this:

:- multifile error:has_mode/3.
error:has_mode(in, before, X) :-    % like -
    nonvar(X).
error:has_mode(in, after, X) :-
    nonvar(X).
error:has_mode(out, before, X) :-    % like +
    true.
error:has_mode(out, after, X) :-
    nonvar(X).
error:has_mode(strict_out, before, X) :-     % like --
    var(X).
error:has_mode(strict_out, after, X) :-
    ground(X).
error:has_mode(mod, before, X) :-    % like :
    X = Module:Goal,
    ground(Module),
    nonvar(Goal).
error:has_mode(mod,after,X) :-
    true.
error:has_mode(strict_list,before,X) :-  % not a partial list
    is_list(X).
error:has_mode(strict_list,after,X) :-
    true.
...

This gives us human-readable names for each mode.  It also gives us a
precise definition of what each mode means.  If we forget what "out" means,
we can run listing(error:has_mode(out,_,_)) to remind ourselves.  We also
have the full power of Prolog for defining these modes.  Some data
structures, like lists or maps, have instantiation patterns that must be
defined recursively.

Perhaps we use the mode definitions like this:

%% open(in(Src), in(Mode), strict_out(Stream))
%% sort(list(List):list, out(Sorted):list)

For brevity, perhaps we make +, -, ? and : notation as aliases for in, out,
any and mod, respectively.

I think of determinism as defining the minimum and maximum number of
solutions expected on backtracking.  Fortunately the number is only 0, 1 or
many.  Because minimum must be less than or equal to maximum, we have only
6 combinations.  Those map nicely onto keywords fail, semidet, nondet, det
and multi.  We don't have a keyword for minimum=maximum=many (as in
Kuniaki's foo/2 example).


--
Michael
-------------- next part --------------
HTML attachment scrubbed and removed
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Jan Wielemaker-5
On 09/16/2014 04:37 PM, Michael Hendricks wrote:

> I'm glad this conversation has come up.  Wouter and I talked about this
> a couple weeks ago and it's been on my mind a lot since then.
>
>
> On Tue, Sep 16, 2014 at 1:30 AM, Jan Wielemaker <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     At some point, I think we need a
>     more advanced mode system, which I think should be:
>
>
> I too would like a more powerful language for describing modes and
> determinism.  What do we want this system to accomplish?  I have three
> personal goals:
>
>      * provide clear, concise documentation of how a predicate should be
> used
>      * allow for runtime checks of argument instantiation and predicate
> backtracking behavior
>      * allow for static analysis (like check/0) to find misuses early

So far I agree, except that you leave types out of the equation.  Do
not forget the work on Ciao.  My lesson learned is that the assertion
language is too complicated and statically proving correctness isn't
feasible for large realistic programs.  They did a lot of work getting
the concepts right though.  See also Edison's work (some of which is
in the system in the Ciao dialect of the library) to base runtime
checking on a simplified version of the assertion language.

An important lesson is that we have types and terms can satisfy a
type or can be _compatible with_ a type.  The latter means that there
is a way to instantiate the term such that it satisfies the type.

>        --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.
>
>
> I'd like to move away from sigils (to borrow Perl's terminology) for
> indicating modes.  We have a limited number of punctuation characters
> but nearly limitless mode possibilities.  It's also difficult to
> remember the meaning of each punctuation.  Even those who do remember
> the punctuation seem to have varying interpretations of their meaning.

I'm not so sure we have that many modes. Yes, if you include types into
the mode annotation, you have. You probably also have to accept that not
all predicates can be fully described using any simple notation. The
assertion language allows specifying arbitrary pre and post conditions.
That might be nice to have, but I don't see much value for the average
Prolog programmer.

> I suggest that we define modes similar to how we define types.  I take
> error:has_type/2 as my model.  The Mercury documentation
> <http://mercurylang.org/information/doc-release/mercury_ref/Insts-modes-and-mode-definitions.html#Insts-modes-and-mode-definitions>
> defines a mode as "a mapping from the initial state of instantiation of
> the arguments of the predicate ... to their final state of
> instantiation".  So perhaps we have something like this:
>
> :- multifile error:has_mode/3.
> error:has_mode(in, before, X) :-    % like -
>      nonvar(X).
> error:has_mode(in, after, X) :-
>      nonvar(X).
> error:has_mode(out, before, X) :-    % like +
>      true.
> error:has_mode(out, after, X) :-
>      nonvar(X).
> error:has_mode(strict_out, before, X) :-     % like --
>      var(X).
> error:has_mode(strict_out, after, X) :-
>      ground(X).
> error:has_mode(mod, before, X) :-    % like :
>      X = Module:Goal,
>      ground(Module),
>      nonvar(Goal).
> error:has_mode(mod,after,X) :-
>      true.
> error:has_mode(strict_list,before,X) :-  % not a partial list
>      is_list(X).
> error:has_mode(strict_list,after,X) :-
>      true.
> ...
>
> This gives us human-readable names for each mode.  It also gives us a
> precise definition of what each mode means.  If we forget what "out"
> means, we can run listing(error:has_mode(out,_,_)) to remind ourselves.
>   We also have the full power of Prolog for defining these modes.  Some
> data structures, like lists or maps, have instantiation patterns that
> must be defined recursively.
>
> Perhaps we use the mode definitions like this:
>
> %% open(in(Src), in(Mode), strict_out(Stream))
> %% sort(list(List):list, out(Sorted):list)

Hmmm.  I kind of prefer open(+Src, +Mode, --Stream) and
sort(+List, -Set) or:

   open(+Src:text, +Mode:mode, --Stream:stream)
   sort(+List:list(Type), -Set:ordered_set(Type)).

> For brevity, perhaps we make +, -, ? and : notation as aliases for in,
> out, any and mod, respectively.

What I like is that you can indeed define your modes. Defining modes
without types seems dubious to me. If we want to move ahead easily, I
think we should define modes as terms satisfying or being compatible
with certain types (both pre and post). Perhaps we can still leave the
type language out of the equation and just define that a type is
represented by a Prolog term.  Leaving the exact definition of types
out of the equation avoids a lot of discussion.

> I think of determinism as defining the minimum and maximum number of
> solutions expected on backtracking.  Fortunately the number is only 0, 1
> or many.  Because minimum must be less than or equal to maximum, we have
> only 6 combinations.  Those map nicely onto keywords fail, semidet,
> nondet, det and multi.  We don't have a keyword for minimum=maximum=many
> (as in Kuniaki's foo/2 example).

I agree that Mercuries determinism system (which is what we adopted) is
satisfactory.

        Cheers --- Jan

_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Abramo Bagnara
In reply to this post by Michael Hendricks
Il 16/09/2014 16:37, Michael Hendricks ha scritto:

> I'm glad this conversation has come up.  Wouter and I talked about this a
> couple weeks ago and it's been on my mind a lot since then.
>
>
> On Tue, Sep 16, 2014 at 1:30 AM, Jan Wielemaker <[hidden email]> wrote:
>
>> At some point, I think we need a
>> more advanced mode system, which I think should be:
>>
>
> I too would like a more powerful language for describing modes and
> determinism.  What do we want this system to accomplish?  I have three
> personal goals:
>
>     * provide clear, concise documentation of how a predicate should be used
>     * allow for runtime checks of argument instantiation and predicate
> backtracking behavior
>     * allow for static analysis (like check/0) to find misuses early
>
>
>>   --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.
>>
>
> I'd like to move away from sigils (to borrow Perl's terminology) for
> indicating modes.  We have a limited number of punctuation characters but
> nearly limitless mode possibilities.  It's also difficult to remember the
> meaning of each punctuation.  Even those who do remember the punctuation
> seem to have varying interpretations of their meaning.
>
> I suggest that we define modes similar to how we define types.  I take
> error:has_type/2 as my model.  The Mercury documentation
> <http://mercurylang.org/information/doc-release/mercury_ref/Insts-modes-and-mode-definitions.html#Insts-modes-and-mode-definitions>
> defines a mode as "a mapping from the initial state of instantiation of the
> arguments of the predicate ... to their final state of instantiation".  So
> perhaps we have something like this:
>
> :- multifile error:has_mode/3.
> error:has_mode(in, before, X) :-    % like -
>     nonvar(X).
> error:has_mode(in, after, X) :-
>     nonvar(X).
> error:has_mode(out, before, X) :-    % like +
>     true.
> error:has_mode(out, after, X) :-
>     nonvar(X).
> error:has_mode(strict_out, before, X) :-     % like --
>     var(X).
> error:has_mode(strict_out, after, X) :-
>     ground(X).
> error:has_mode(mod, before, X) :-    % like :
>     X = Module:Goal,
>     ground(Module),
>     nonvar(Goal).
> error:has_mode(mod,after,X) :-
>     true.
> error:has_mode(strict_list,before,X) :-  % not a partial list
>     is_list(X).
> error:has_mode(strict_list,after,X) :-
>     true.
> ...
>
> This gives us human-readable names for each mode.  It also gives us a
> precise definition of what each mode means.  If we forget what "out" means,
> we can run listing(error:has_mode(out,_,_)) to remind ourselves.  We also
> have the full power of Prolog for defining these modes.  Some data
> structures, like lists or maps, have instantiation patterns that must be
> defined recursively.
>
> Perhaps we use the mode definitions like this:
>
> %% open(in(Src), in(Mode), strict_out(Stream))
> %% sort(list(List):list, out(Sorted):list)
>
> For brevity, perhaps we make +, -, ? and : notation as aliases for in, out,
> any and mod, respectively.
>
> I think of determinism as defining the minimum and maximum number of
> solutions expected on backtracking.  Fortunately the number is only 0, 1 or
> many.  Because minimum must be less than or equal to maximum, we have only
> 6 combinations.  Those map nicely onto keywords fail, semidet, nondet, det

I think it is called 'failure' in swi prolog modes.

> and multi.  We don't have a keyword for minimum=maximum=many (as in
> Kuniaki's foo/2 example).

Please don't forget the need to specify the determinism info for
meta_predicate arguments. In our code we use something like that:

:- meta_pred(first_match(nondet(0), det(0))).

This would be fundamental for our big shared dream to have a static mode
checker for prolog code. In our experience our first enemies are
unexpected failures and unexpected nondets.

This is so true that if I could write Prolog code prefixing goal that
might fail or that might generate multiple solutions with some prefix
and after that I'll get a crash where a non prefixed goal fails or leave
a choice point I would be more than happy to manually add the missing
prefixes to all our code (this would help also the readability of the
clauses and the involved algorithms).

Of course the reverse (i.e. add a det/1 wrapper to all other goals), is
too heavy (also with term_expansion/2 due to runtime penalties).


--
Abramo Bagnara
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Michael Hendricks
In reply to this post by Jan Wielemaker-5
On Tue, Sep 16, 2014 at 9:11 AM, Jan Wielemaker <[hidden email]> wrote:

> Do not forget the work on Ciao.  My lesson learned is that the assertion
> language is too complicated
>

Yes, they've done some great work.  Unfortunately, as I understand it, they
confound modes and types.  I believe those two are orthogonal and should
kept independent.

I agree that Ciao's approach is too complicated.


> An important lesson is that we have types and terms can satisfy a
> type or can be _compatible with_ a type.  The latter means that there
> is a way to instantiate the term such that it satisfies the type.


As an aside, I think I've failed to see how compatibility with a type is
useful as a mode.  Maybe some examples will help me see what I'm missing.
 Using your notation, we have four possibilities for an input argument:

  +X
  ++X
  +X:type
  ++X:type

The first two are equivalent since all values are compatible with the
implicit "any" type.  They both allow variables, as you mentioned.  Of
course, since they both allow variables, one could have written any of: X,
+X, ++X, -X.  So a user gets no benefit from mode annotation without a type.

+X:type also accepts a variable since a free variable is a generalization
of all types.   That leads me to see no distinction between: X:type,
+X:type and -X:type.

++X:type does not allow a free variable so there's no overlap with other
mode annotations.  Since this is the only mode annotation that's distinct
from the others, why don't we call it + instead?

Maybe +X:type implicitly requires nonvar(X)?


> I'm not so sure we have that many modes. Yes, if you include types into
> the mode annotation, you have.


Maybe we don't have as many modes as I think, but defining them as I
described gives us space to learn that as we go.

My sloppy "list" mode was a bad example because it blurs the distinction
between modes and types.  I intended that mode to describe the
instantiation pattern where free variable are prohibited the end of a term
chain.  It may be better defined like:

is_proper(X) :-
    var(X),
    !,
    fail.
is_proper(X) :-
    atomic(X).
is_proper(X) :-
    X =.. [_,_,T],
    is_proper(T).



> You probably also have to accept that not
> all predicates can be fully described using any simple notation.


I agree.  If we try to cover all possible predicates, our notation becomes
far too complex.


> The
> assertion language allows specifying arbitrary pre and post conditions.
> That might be nice to have, but I don't see much value for the average
> Prolog programmer.
>

I mostly agree.  The average Prolog programmer doesn't define new clauses
for error:has_type/2 either.  She uses the ones defined in the library or
uses sugar like library(typedef) to handle the details.

However, by having well-defined pre- and post-conditions, the average
programmer does get runtime mode checking (a simple addition to
library(mavis)).  That seems valuable.



> Perhaps we use the mode definitions like this:
>>
>> %% open(in(Src), in(Mode), strict_out(Stream))
>> %% sort(list(List):list, out(Sorted):list)
>>
>
> Hmmm.  I kind of prefer open(+Src, +Mode, --Stream) and
> sort(+List, -Set) or:
>

Sure.  That's just a disagreement on whether we spell the mode "in" or "+"
:-)

Defining modes without types seems dubious to me.


I'm surprised to hear that.  I think the SWI-Prolog documentation does a
great job of using modes without types where the types would be too
complicated.  format(+Format,:Args) and with_output_to(+Output,:Goal) come
to mind.

--
Michael
-------------- next part --------------
HTML attachment scrubbed and removed
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Richard A. O'Keefe
In reply to this post by Kuniaki Mukai

On 16/09/2014, at 5:57 PM, Kuniaki Mukai wrote:

>
> Hi,
>
> Using pldoc, how do we specify a predicate such as follows:
>
> foo(X, Y) :-  (random(3) =:= 2, X==Y;  true).

This is logically equivalent to foo(_, _).
Did you mean

        foo(X, Y) :- ( random(3) =:= 2 -> X == Y ; true ).
                                       ^^


_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Richard A. O'Keefe
In reply to this post by Kuniaki Mukai

On 16/09/2014, at 10:48 PM, Kuniaki Mukai wrote:

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

If you want a logic programming language in which the compiler
understands modes, Mercury exists and has been in use for quite
a few years now.  I urge anyone who wants modes in SWI Prolog
to do some serious programming in Mercury for a bit to find out
what it's like.

Modes of course express a programmer's intentions.
When you write Prolog, it's far from unusual to have
a predicate which *ought* to be logically invertible
but does not in fact *work* when used in modes you did
not think of.

What's really sad is when an interface *could* be implemented
in a multi-modal way but wasn't because the programmer never
thought of it.

_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Kuniaki Mukai
In reply to this post by Richard A. O'Keefe

On Sep 17, 2014, at 12:51, Richard A. O'Keefe <[hidden email]> wrote:

>
> On 16/09/2014, at 5:57 PM, Kuniaki Mukai wrote:
>
>>
>> Hi,
>>
>> Using pldoc, how do we specify a predicate such as follows:
>>
>> foo(X, Y) :-  (random(3) =:= 2, X==Y;  true).
>
> This is logically equivalent to foo(_, _).
> Did you mean
>
> foo(X, Y) :- ( random(3) =:= 2 -> X == Y ; true ).
>                                       ^^

What I intended to write is the following:

foo(X, Y) :-  (random(3) =:= 2, X=Y;  true), !.

?- foo(X, Y), X==Y.
%@ X = Y .
?- foo(X, Y), X==Y.
%@ false.
?- foo(X, Y), X==Y.
%@ X = Y .

I wrote a unifier on rational trees on Edinburgh Prolog in ancient time
writing clauses  for unbound arguments to test whether two variables are
already unified or not.  I am afraid that such kind of prolog programming
is no more recommended nowadays from view of mode declaration.

Thank you for pointing my careless typo.

Kuniaki Mukai

>
>
> _______________________________________________
> SWI-Prolog mailing list
> [hidden email]
> 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/cbeac09e/signature.asc>
_______________________________________________
SWI-Prolog mailing list
[hidden email]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog
12
Loading...