[m-rev.] for review: rewrite of Modes chapter

[Mark Brown]

On 21-Feb-2003, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 20-Feb-2003, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > @@ -2190,6 +2128,7 @@
> >  :- mode out == free >> ground.
> >  @end example
> >  
> > + at noindent
> >  Prolog fans who want to use the symbols @samp{+} and @samp{-}
> >  can do so by simply defining them using a mode declaration:
> 
> The @noindent there is wrong; this is a new paragraph.

Fixed.  I also moved the sentence which read "These two modes are enough
for most predicates and functions" so it applies to 'in' and 'out', rather
than the Prolog synonyms.

> > @@ -2436,24 +2303,177 @@
> >  it reports an error if no satisfactory order exists.
> >  Finally it checks that
> >  the resulting instantiatedness of the procedure's arguments
> > -is the same as the one given by the procedure's declaration.
> > +matches the one given by the procedure's declaration.
> > +For the simple insts we have seen so for,
> > +the word ``matches'' just means ``is the same as'';
> > +we will extend this definition as new insts are introduced.
> 
> Didn't you introduce user-defined insts already?

No, because I couldn't think of a useful example at that point, where
the only insts defined are 'free' and 'ground'.

The first user-defined inst is introduced just below that point, and
I've addressed your following remark there:

> If so, insts should match if they are the same after
> all user-defined insts have been replaced with their bodies.

> > + at node Uniqueness ordering
> > + at section Uniqueness ordering
> ...
> > +For inst @var{A} to be more instantiated than inst @var{B},
> > +it is necessary that @var{A} be of equal or less uniqueness than @var{B}
> > +according to the above ordering,
> > +in addition to the rules that apply for the corresponding
> > + at code{free}, @code{ground} and @code{bound} insts.
> > +
> > +For inst @var{A} to match inst @var{B},
> > +the uniqueness ordering is reversed:
> > +it is necessary that @var{A} be of equal or greater uniqueness than @var{B}
> > +according to the above ordering,
> > +in addition to the rules that apply for the corresponding
> > + at code{free}, @code{ground} and @code{bound} insts.
> 
> s/the uniqueness ordering/the uniqueness ordering condition/
> 
> (I found the thought of reversing the uniquess ordering confusing...
> ``now, let time run backwards...'' :-)

*chuckle*

Fixed, as you suggested.

> > +A higher-order inst @var{A} is at least as instantiated as inst @var{B} iff
> > + at var{A} is identical to @var{B}.
> > +Higher-order terms are considered ground,
> > +and there is no way for them to become more ground.
> 
> I think this is wrong.  The "is at least as instantiated as" ordering
> should be the same as the "matches" ordering for higher-order insts.

Agreed.

> Likewise, there should be a description of when "ground" is considered
> at least as instantiated as a subtype inst and vice versa.

I'm not completely sure about when ground matches/is as instantiated as
bound, but I think I've got it right.  See the relative diff.

I've also followed your other suggestions.

On 22-Feb-2003, David Overton <dmo at cs.mu.OZ.AU> wrote:
> On Thu, Feb 20, 2003 at 12:41:08PM +1100, Mark Brown wrote:
> >
> >     - Require the final inst to be "at least as instantiated as" the
> >       initial inst.  XXX is this correct?  The thesis draft suggests
> >       that these are the only allowable transitions, but the compiler
> >       does actually allow modes such as 'citrus >> ground'.
>
> The compiler doesn't explicitly check for and disallow a predicate with
> a mode declaration such as this.  However, when analysing a call to such
> a predicate, the final inst from the mode declaration is abstractly
> unified with the inst of the argument before the call.  So if someone
> declares a mode of `citrus >> ground' the mode is really `citrus >> citrus'.
> I.e. the compiler doesn't through away inst information unnecessarily in
> such cases.

Okay, I've changed that part of the diff to read "Modes should reflect
this" rather than "Modes must reflect this" and explained that the
compiler doesn't check it, but that modes that don't reflect this
generally aren't useful.

I've followed your other suggestions also.

Relative diff follows (once again, the full version is in
~dougl/mars/m3/mercury/doc/*).

Cheers,
Mark.

diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi	20 Feb 2003 01:21:20 -0000
+++ doc/reference_manual.texi	23 Feb 2003 05:28:15 -0000
@@ -2080,7 +2080,7 @@
 @menu
 * Insts modes and mode definitions::
 * Predicate and function mode declarations::
-* Insts defined using bound::
+* Structured insts::
 * Partially instantiated data structures::
 @c * Dynamic modes::
 * Constrained polymorphic modes::
@@ -2091,28 +2091,31 @@
 @section Insts, modes, and mode definitions
 
 In Mercury, the state of instantiation, or @dfn{inst}, of a variable
-is a description of the terms that the variable may be bound to.
+is a description of the terms that the variable may hold.
 The simplest insts are @samp{free}, which describes any distinct variable
 (that is, any free variable not aliased to another variable),
 and @samp{ground} which describes any ground term;
-more complex insts are also possible.
+more complex insts are also possible, and are described later.
 
 The @dfn{mode} of a predicate or function
-describes how the inst of each argument and return value (if there is one)
-changes between a call to that predicate or function and an exit from it.
+describes the inst which each argument and return value (if there is one)
+may have when the predicate or function is called,
+and the corresponding inst that each will have
+if the predicate or function succeeds.
 The mode of an argument or return value is a pair of insts,
 the initial inst and the final inst,
 which we write as @code{Initial >> Final}.
 
 Mercury allows the user to specify modes directly
-by expressions such as @code{inst1 >> inst2},
+by expressions such as @code{@var{inst1} >> @var{inst2}},
 or to give them a name using declarations such as
 
 @example
-:- mode m == inst1 >> inst2.
+:- mode m == @var{inst1} >> @var{inst2}.
 @end example
 
 @noindent
+and then refer to them by name.
 There must not be more than one mode definition
 with the same name and arity in the same module.
 
@@ -2129,6 +2132,8 @@
 @end example
 
 @noindent
+These two modes are enough for most functions and predicates.
+
 Prolog fans who want to use the symbols @samp{+} and @samp{-}
 can do so by simply defining them using a mode declaration:
 
@@ -2137,9 +2142,6 @@
 :- mode (-) == out.
 @end example
 
- at noindent
-These two modes are enough for most functions and predicates.
-
 Mode definitions may be parametric;
 an argument to a parametric mode must be an inst.
 The standard library provides the parametric modes
@@ -2153,11 +2155,18 @@
 so that for example the mode @samp{in} is the same as @samp{in(ground)}.
 
 As execution proceeds, variables may become more instantiated.
-Modes must reflect this:
-the final inst must be at least as instantiated as the initial inst.
+Modes should reflect this:
+the final inst should be at least as instantiated as the initial inst.
 The inst @code{ground} is more instantiated than @code{free},
-so the above definition of @code{out} as @samp{free >> ground} is valid,
-but it would be an error to try to use the mode @samp{ground >> free}.
+so the above definition of @code{out} as @samp{free >> ground} is useful.
+Although the compiler does not enforce this condition,
+it is generally not useful to use a mode such as @samp{ground >> free}
+because no variable which is ground at the point of call
+will be free at any point of success.
+
+Not only is @code{free} less instantiated than @code{ground},
+it is also less instantiated than any other inst;
+that is, it is the least element of the instantiatedness partial order.
 As more insts are introduced below,
 we will extend the definition of what it means to be
 ``at least as instantiated as''.
@@ -2224,7 +2233,7 @@
 
 @noindent
 If any argument or return value in such a declaration
-is of the form @samp{type::mode}, then all of them must be.
+is of the form @samp{@var{type}::@var{mode}}, then all of them must be.
 
 If there is no mode declaration for a function, the compiler assumes
 a default mode for the function in which all the arguments have mode @samp{in}
@@ -2311,8 +2320,8 @@
 The mode analysis algorithm annotates each call with the mode used.
 
 
- at node Insts defined using bound
- at section Insts defined using @samp{bound}
+ at node Structured insts
+ at section Structured insts
 
 Mercury's mode system allows users to declare names for insts
 using declarations such as
@@ -2322,7 +2331,18 @@
 @end example
 
 @noindent
-This inst describes any non-variable whose top functor is @samp{[|]}/2,
+and then refer to them by name.
+There must not be more than one inst definition
+with the same name and arity in the same module.
+
+When checking whether one inst is at least as instantiated as another,
+or whether one inst matches another,
+it makes no difference whether the inst is referred to directly
+or by a declared name.
+That is, names are expanded before either of these orderings is checked.
+
+The inst @code{non_empty_list} describes any non-variable
+whose top functor is @samp{[|]}/2,
 and whose arguments are both described by @samp{ground};
 in other words, this inst describes
 any ground term which is a non-empty list.
@@ -2381,12 +2401,35 @@
 the same function symbol appears in @code{Bs},
 and each argument of the former is at least as instantiated as
 the corresponding argument of the latter.
+ at var{A} is at least as instantiated as @code{ground} iff
+every argument of every function symbol in @code{As}
+is at least as instantiated as @code{ground}.
+
 Similarly, @var{A} matches @var{B} iff
 for every function symbol in @code{As}
 the same function symbol appears in @code{Bs},
 and each argument of the former matches
 the corresponding argument of the latter.
+ at var{A} matches @code{ground} iff
+every argument of every function symbol in @code{As} matches @code{ground}.
 
+By using type information the compiler can consider @code{ground} to be
+at least as instantiated as an inst such as @samp{bound( As )},
+but only if all of the function symbols
+which appear in the type of the variable in question are known.
+If this is the case, then @code{ground}
+is at least as instantiated as @samp{bound( As )} iff
+for every function symbol in the type definition
+the same function symbol appears in @code{As},
+and for each type argument of the former,
+ at code{ground} with that type is at least as instantiated as
+the corresponding argument of the latter.
+
+Similarly, @code{ground} matches @samp{bound( As )} iff
+for every function symbol in the type definition
+the same function symbol appears in @code{As},
+and for each type argument of the former,
+ at code{ground} with that type matches the corresponding argument of the latter.
 
 @node Partially instantiated data structures
 @section Partially instantiated data structures
@@ -2766,12 +2809,12 @@
 @code{free}, @code{ground} and @code{bound} insts.
 
 For inst @var{A} to match inst @var{B},
-the uniqueness ordering is reversed:
+the uniqueness ordering condition is reversed:
 it is necessary that @var{A} be of equal or greater uniqueness than @var{B}
 according to the above ordering,
 in addition to the rules that apply for the corresponding
 @code{free}, @code{ground} and @code{bound} insts.
-Note that since the ordering is reversed,
+Note that since the ordering condition is reversed,
 this implies that for two insts to be compatible
 they must have the same level of uniqueness
 (@pxref{Constrained polymorphic modes}).
@@ -3974,9 +4017,9 @@
         all [X] (call(P, X) <=> call(Q, X)).
 @end example
 
-Note that the compiler will only catch direct attempts at higher-order
+The compiler will only catch direct attempts at higher-order
 unifications; indirect attempts (via polymorphic predicates, for
-example @samp{(list__append([], [P], [Q])} may result in an error at
+example @samp{list__append([], [P], [Q])}) may result in an error at
 run-time rather than at compile-time.
 
 In order to call a higher-order term, the compiler must know its higher-order
@@ -3995,11 +4038,7 @@
 inst information may be lost, such as to a polymorphic predicate where the
 argument mode is @samp{in}.
 
-A higher-order inst @var{A} is at least as instantiated as inst @var{B} iff
- at var{A} is identical to @var{B}.
-Higher-order terms are considered ground,
-and there is no way for them to become more ground.
-A higher-order inst @var{A} matches inst @var{B} iff
+A higher-order inst @var{A} matches higher-order inst @var{B} iff
 all of the following conditions are satisified:
 
 @itemize @bullet
@@ -4016,6 +4055,19 @@
 (That is, @samp{pred} and @samp{func} insts are
 covariant in the final insts, with respect to the ``matches'' ordering.)
 @end itemize
+
+For @var{A} to be at least as instantiated as @var{B},
+exactly the same conditions must be met.
+That is, @var{A} is at least as instantiated as @var{B} iff
+ at var{A} matches @var{B}.
+
+Any higher-order inst is compatible with @code{ground},
+in the sense of @ref{Constrained polymorphic modes}.
+In other words, if @var{A} is a higher-order inst then
+ at var{A} is at least as instantiated as @code{ground}
+and @var{A} matches @code{ground}.
+The converse is not true:
+ at code{ground} neither matches nor is as instantiated as any higher-order inst.
 
 @node Modules
 @chapter Modules
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------