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>

[Jan Wielemaker]

Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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

[Paulo Moura]

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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:***@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------

[Günter Kniesel]

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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

[Paulo Moura]

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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
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.
since all the others are disjoint cases.
@ 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:***@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------

[Günter Kniesel]

Post by Paulo Moura

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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.

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.

Post by Paulo Moura

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.

Post by Paulo Moura

In the case of foo you are actually talking about modes, more precisely the conjunction of two modes
- 'mandatory free' (--) and
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.
since all the others are disjoint cases.
@ 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

[Paulo Moura]

Post by Günter Kniesel

Post by Paulo Moura

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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.

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.

Post by Paulo Moura

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.

Post by Paulo Moura

In the case of foo you are actually talking about modes, more precisely the conjunction of two modes
- 'mandatory free' (--) and
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.
since all the others are disjoint cases.
@ 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:***@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------

[Günter Kniesel]

Post by Paulo Moura

Post by Günter Kniesel

Post by Paulo Moura

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
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.

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.

Post by Paulo Moura

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.

Post by Paulo Moura

In the case of foo you are actually talking about modes, more precisely the conjunction of two modes
- 'mandatory free' (--) and
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.
since all the others are disjoint cases.
@ 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?

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
clause(+head, -callable_term)
clause(+head, +callable_term)
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

Post by Paulo Moura
Cheers,
Paulo
-----------------------------------------------------------------
Paulo Moura
Logtalk developer
Web: <http://logtalk.org/>
-----------------------------------------------------------------

[Jan Wielemaker]

Post by Günter Kniesel

Post by Paulo Moura

Post by Günter Kniesel
In the case of foo you are actually talking about modes, more
precisely the conjunction of two modes
- 'mandatory free' (--) and
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.
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.

Post by Günter Kniesel

Post by Paulo Moura

Post by Günter Kniesel
@ 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.

Post by Günter Kniesel

Post by Paulo Moura
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

[Kuniaki Mukai]

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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.

Post by Jan Wielemaker
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.

Post by Jan Wielemaker
but the arguments are never altered, while --X
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

Post by Jan Wielemaker
Cheers --- Jan
_______________________________________________
SWI-Prolog mailing list
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>

[Paulo Moura]

Post by Kuniaki Mukai

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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.

Post by Jan Wielemaker
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

Post by Kuniaki Mukai

Post by Jan Wielemaker
but the arguments are never altered, while --X
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

Post by Jan Wielemaker
Cheers --- Jan
_______________________________________________
SWI-Prolog mailing list
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
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

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

Email: <mailto:***@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------

[Kuniaki Mukai]

Post by Paulo Moura

Post by Kuniaki Mukai

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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.

Post by Jan Wielemaker
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.

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

Post by Paulo Moura
Cheers,
Paulo

Post by Kuniaki Mukai

Post by Jan Wielemaker
but the arguments are never altered, while --X
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

Post by Jan Wielemaker
Cheers --- Jan
_______________________________________________
SWI-Prolog mailing list
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
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

-----------------------------------------------------------------
Paulo Moura
Logtalk developer
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>

[Richard A. O'Keefe]

Post by Kuniaki Mukai
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.

[Michael Hendricks]

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.

Post by Jan Wielemaker
At some point, I think we need a

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

Post by Jan Wielemaker
--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).

[Jan Wielemaker]

Post by Michael Hendricks
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.
At some point, I think we need a
I too would like a more powerful language for describing modes and
determinism. What do we want this system to accomplish? I have three
* 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.

Post by Michael Hendricks
--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.

Post by Michael Hendricks
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
:- 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).
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.
%% 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)).

Post by Michael Hendricks
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.

Post by Michael Hendricks
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

[Michael Hendricks]

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.

Post by Michael Hendricks
%% 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

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.

[Abramo Bagnara]

Post by Michael Hendricks
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.

Post by Jan Wielemaker
At some point, I think we need a

I too would like a more powerful language for describing modes and
determinism. What do we want this system to accomplish? I have three
* 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

Post by Jan Wielemaker
--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
:- 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).
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.
%% 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.

Post by Michael Hendricks
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).

[Kuniaki Mukai]

Hi Jan,

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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

Post by Jan Wielemaker
The predicate is `multi` though: it succeeds one or
two times (a rarely used qualifier). At some point, I think we need a
--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
claim that var is not a type.
Cheers --- Jan
_______________________________________________
SWI-Prolog mailing list
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>

[Wouter Beek]

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: ***@vu.nl
WWW: www.wouterbeek.com
Tel.: [phone]

Post by Jan Wielemaker
Hi Kuniaki,

Post by Kuniaki Mukai
Hi,
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
--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
claim that var is not a type.
Cheers --- Jan
_______________________________________________
SWI-Prolog mailing list
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog

-------------- next part --------------
HTML attachment scrubbed and removed

[Richard A. O'Keefe]

Post by Kuniaki Mukai
Hi,
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 ).
^^

[Kuniaki Mukai]

Post by Richard A. O'Keefe

Post by Kuniaki Mukai
Hi,
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

Post by Richard A. O'Keefe
_______________________________________________
SWI-Prolog mailing list
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>