[m-rev.] for review: rewrite of Modes chapter
Mark Brown
dougl at cs.mu.OZ.AU
Tue Feb 25 13:30:27 AEDT 2003
On 24-Feb-2003, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> I'm going to need to think again about what
> partial order(s) would be most useful to present the material that we
> want to present. I'll post a full diff after doing that, and addressing
> the above issue.
I've discussed this in person with David. The conclusion was that, since the
reference manual doesn't go into detail about the mode analysis algorithm,
there is no great need to use the "is at least as instantiated as" ordering;
the "matches" partial order is the important one for the reference manual.
I've dealt with the implied modes issue by giving a more direct description
of what the implied modes are.
Here's the new log message and full diff. I've also attached the relative
diff.
Estimated hours taken: 12
Branches: main
Rewrite the Modes chapter of the reference manual, following the style of
David Overton's thesis draft. This was suggested in review comments for
the subtypes documentation.
The major structural changes are as follows:
- Initially, we only discuss 'free' and 'ground', since these
are the most commonly used insts. Discussion of more complex
insts, involving partial instantiation for example, is left
until later sections of the chapter.
- To accommodate the above, some examples have been moved or
modified.
- The mode system rules are defined in terms of the "matches"
abstract partial order. As each new kind of inst is introduced,
the definitions of the partial order is extended to cover the new
cases, until finally the full definition has been given.
Terminological changes:
- The word "inst" is defined at the start, and is used throughout
in place of "state of instantiation", "instantiatedness tree", etc.
- I've used the verb "to describe" for the relationship between
insts and terms which can have that inst. E.g., any ground term
is described by inst 'ground', the inst 'free' describes any free
variable. For each kind of inst, we state which terms are
described by that inst.
- I've avoided saying that a mode is a "mapping" from one initial
inst to final inst, since I find this misleading. Instead, a
mode is defined as a "pair" of insts. I've also replaced
occurrences of the phrase "mode mapping" with "mode", where
appropriate.
Detailed changes follow.
doc/reference_manual.texi:
- Two new sections are added to the modes chapter. One is for
user defined insts (including a discussion of insts that provide
subtype information), and the other is for partially instantiated
modes. Another section should be added for dynamic insts (which
are currently undocumented), but this can be done later.
- Remove the definition of "instantiatedness tree". Discussion of
the mode system is based on the partial order rather than the
instantiatedness tree. Likewise remove the definition of when
a term "satisfies" an inst; this just means that the inst describes
the term.
- Move the database example to the section on partial instantiation.
- Move the length/1 example to the partial instantiation section.
Replace the original example with reverse/1.
- Explicitly mention the requirement that if any argument has a mode
specified, then all arguments must.
- Move the discussion of append(in_listskel, ...) to the partial
instantiation section.
- When discussing the mode set constraint, include each implied
mode as a distinct element of the mode set. This simplifies
the discussion slightly.
- When discussing "well-moded with respect to a given declaration",
add the antecedent that p is called with argument terms that are
described by the initial insts of the mode declaration. Without
this condition, there is no way to conclude that p satisfies the
mode set constraint of all the procedures it calls.
- Require the inst resulting from mode analysis to "match" the
one in the declaration, rather than be "the same as".
- Use the example non_empty_list to demonstrate user defined insts.
This example illustrates the point that insts are not necessarily
tied to a particular type: non_empty_list doesn't cover every
function symbol of list/1; conversely, non-lists are also
described by this inst.
- Use the fruit/citrus example to demonstrate subtype information.
- Define "compatible". It has the same rules as "matches", except
that the uniqueness condition is tighter.
- Add a section to the uniqueness chapter, defining the partial
ordering amongst unique insts.
- Define the partial order for higher-order insts.
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.273
diff -u -r1.273 reference_manual.texi
--- doc/reference_manual.texi 21 Feb 2003 01:57:23 -0000 1.273
+++ doc/reference_manual.texi 25 Feb 2003 02:18:07 -0000
@@ -2091,6 +2091,9 @@
@menu
* Insts modes and mode definitions::
* Predicate and function mode declarations::
+* Structured insts::
+* Partially instantiated data structures::
+ at c * Dynamic modes::
* Constrained polymorphic modes::
* Different clauses for different modes::
@end menu
@@ -2098,96 +2101,34 @@
@node Insts modes and mode definitions
@section Insts, modes, and mode definitions
-The @dfn{mode} of a predicate, or function, is a mapping
-from the initial state of instantiation of the arguments of the predicate,
-or the arguments and result of a function,
-to their final state of instantiation.
-To describe states of instantiation,
-we use information provided by the type system.
-Types can be viewed as regular trees with two kinds of nodes:
-or-nodes representing types
-and and-nodes representing constructors.
-The children of an or-node are the constructors
-that can be used to construct terms of that type;
-the children of an and-node are the types
-of the arguments of the constructors.
-We attach mode information to the or-nodes of type trees.
-
-An @dfn{instantiatedness tree} is an assignment
-of an @dfn{instantiatedness} --- either @dfn{free} or @dfn{bound} ---
-to each or-node of a type tree,
-with the constraint that all descendants of a free node must be free.
+In Mercury, the state of instantiation, or @dfn{inst}, of a variable
+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, and are described later.
+
+The @dfn{mode} of a predicate or function
+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}.
-A term is @dfn{approximated by} an instantiatedness tree
-if for every node in the instantiatedness tree,
-
- at itemize @bullet
- at item
-if the node is ``free'',
-then the corresponding node in the term (if any)
-is a free variable that does not share with any other variable
-(we call such variables @dfn{distinct});
-
- at item
-if the node is ``bound'',
-then the corresponding node in the term (if any)
-is a function symbol.
-
- at end itemize
-
-When an instantiatedness tree tells us that a variable is bound,
-there may be several alternative function symbols to which it could be bound.
-The instantiatedness tree does not tell us which of these it is bound to;
-instead for each possible function symbol it tells us exactly
-which arguments of the function symbol will be free and which will be bound.
-The same principle applies recursively to these bound arguments.
-
-Mercury's mode system allows users
-to declare names for instantiatedness trees using declarations such as
-
- at example
-:- inst listskel == bound( [] ; [free | listskel] ).
- at end example
-
-This instantiatedness tree describes lists
-whose skeleton is known but whose elements are distinct variables.
-As such, it approximates the term @code{[A,B]}
-but not the term @code{[H|T]} (only part of the skeleton is known),
-the term @code{[A,2]} (not all elements are variables),
-or the term @code{[A,A]} (the elements are not distinct variables).
-
-As a shorthand, the mode system provides @samp{free} and @samp{ground}
-as names for instantiatedness trees
-all of whose nodes are free and bound respectively.
-The shape of these trees is determined by
-the type of the variable to which they apply.
-
-A more concise, alternative syntax exists for @samp{bound} instantiatedness
-trees:
+Mercury allows the user to specify modes directly
+by expressions such as @code{@var{inst1} >> @var{inst2}},
+or to give them a name using declarations such as
@example
-:- inst maybeskel ---> no ; yes(ground).
+:- mode m == @var{inst1} >> @var{inst2}.
@end example
@noindent
-which is equivalent to writing
-
- at example
-:- inst maybeskel == bound(no ; yes(ground)).
- at end example
-
-As execution proceeds, variables may become more instantiated.
-A @dfn{mode mapping} is a mapping
-from an initial instantiatedness tree to a final instantiatedness tree,
-with the constraint that no node of the type tree
-is transformed from bound to free.
-Mercury allows the user to specify mode mappings directly
-by expressions such as @code{inst1 >> inst2},
-or to give them a name using declarations such as
-
- at example
-:- mode m == inst1 >> inst2.
- at end example
+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.
It is also possible to write mode declarations using @code{::}
and @code{->} instead of @code{==} and @code{>>} respectively,
@@ -2201,6 +2142,9 @@
:- mode out == free >> ground.
@end example
+ at 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:
@@ -2209,41 +2153,8 @@
:- mode (-) == out.
@end example
-These two modes are enough for most functions and predicates.
-Nevertheless, Mercury's mode system is sufficiently
-expressive to handle more complex data-flow patterns,
-including those involving partially instantiated data structures.
-(The current implementation does not handle
-partially instantiated data structures yet.)
-
-For example, consider an
-interface to a database that associates data with keys, and provides
-read and write access to the items it stores. To represent accesses to
-the database over a network, you would need declarations such as
-
- at example
-:- type operation
- ---> lookup(key, data)
- ; set(key, data).
-:- inst request
- ---> lookup(ground, free)
- ; set(ground, ground).
-:- mode create_request == free >> request.
-:- mode satisfy_request == request >> ground.
- at end example
-
- at samp{inst} and @samp{mode} declarations can be parametric.
-For example, the following declaration
-
- at example
-:- inst maybeskel(Inst) ---> no ; yes(Inst).
- at end example
-
- at noindent
-defines the inst @samp{listskel(Inst)} to be a list skeleton
-whose elements have inst @samp{Inst}; you can the use insts
-such as @samp{listskel(listskel(free))}, which represents
-the instantiation state of a list of lists of free variables.
+Mode definitions may be parametric;
+an argument to a parametric mode must be an inst.
The standard library provides the parametric modes
@example
@@ -2252,43 +2163,24 @@
@end example
@noindent
-so that for example the mode @samp{create_request} defined above
-could have be defined as
-
- at example
-:- mode create_request == out(request).
- at end example
-
-There must not be more than one inst definition with the same name
-and arity in the same module. Similarly, there must not be more
-than one mode definition with the same name and arity in the same module.
+so that for example the mode @samp{in} is the same as @samp{in(ground)}.
@node Predicate and function mode declarations
@section Predicate and function mode declarations
A @dfn{predicate mode declaration}
-assigns a mode mapping to each argument of a predicate.
+assigns a mode to each argument of a predicate.
A @dfn{function mode declaration}
-assigns a mode mapping to each argument of a function,
-and a mode mapping to the function result.
+assigns a mode to each argument of a function,
+and a mode to the function result.
Each mode of a predicate or function is called a @dfn{procedure}.
-For example, given the mode names defined by
+For example, the (type and) mode declarations
+of the function reverse and predicate append could be as follows:
@example
-:- mode out_listskel ==
- free >> listskel.
-:- mode in_listskel ==
- listskel >> listskel.
- at end example
-
- at noindent
-the (type and) mode declarations of the function length and predicate append
-are as follows:
-
- at example
-:- func length(list(T)) = int.
-:- mode length(in_listskel) = out.
-:- mode length(out_listskel) = in.
+:- func reverse(list(T)) = list(T).
+:- mode reverse(in) = out.
+:- mode reverse(out) = in.
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
@@ -2298,25 +2190,16 @@
Note that functions may have more than one mode, just like predicates;
functions can be reversible.
-Alternately, the mode declarations for @samp{length} could use
-the standard library modes @samp{in/1} and @samp{out/1}:
-
- at example
-:- func length(list(T)) = int.
-:- mode length(in(listskel)) = out.
-:- mode length(out(listskel)) = in.
- at end example
-
As for type declarations, a predicate or function can be defined
to have a given higher-order inst (@pxref{Higher-order modes}) by using
@code{`with_inst`} in the mode declaration.
For example,
+if @code{foldl_pred} is defined as @samp{pred(in, in, out) is det},
+and @code{foldl_func} is defined as @samp{func(in, in) = out is det},
+then
@example
-:- inst foldl_pred == (pred(in, in, out) is det).
-:- inst foldl_func == (func(in, in) = out is det).
-
:- mode p(in) `with_inst` foldl_pred.
:- mode f(in) `with_inst` foldl_func.
@end example
@@ -2336,12 +2219,16 @@
declaration can be combined:
@example
-:- func length(list(T)::in) = (int::out).
+:- func reverse(list(T)::in) = (list(T)::out).
:- pred append(list(T)::in, list(T)::in, list(T)::out).
:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.
@end example
+ at noindent
+If any argument or return value in such a declaration
+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}
and the result of the function has mode @samp{out}. (However, there
@@ -2351,65 +2238,59 @@
A function or predicate mode declaration is an assertion by the programmer
that for all possible argument terms and (if applicable) result term
for the function or predicate
-that are approximated (in our technical sense)
-by the initial instantiatedness trees of the mode declaration
+that are described by the initial inst of the mode declaration
and all of whose free variables are distinct,
if the function or predicate succeeds then
the resulting binding of those argument terms and (if applicable)
-result term will in turn be approximated
-by the final instantiatedness trees of the mode declaration,
+result term will in turn be described
+by the final inst of the mode declaration,
with all free variables again being distinct.
We refer to such assertions as @dfn{mode declaration constraints}.
These assertions are checked by the compiler,
which rejects programs if it cannot prove
that their mode declaration constraints are satisfied.
-Note that with the usual definition of append, the mode
-
- at example
-:- mode append(in_listskel, in_listskel, out_listskel).
- at end example
-
- at noindent
-would not be allowed, since it would create aliasing between the
-different arguments --- on success of the predicate, the list elements
-would be free variables but they would not be distinct.
-
In Mercury it is always possible to call a procedure with an
-argument that is is more bound than the initial inst specified for that
+argument that is more bound than the initial inst specified for that
argument in the procedure's mode declaration. In such cases, the
compiler will insert additional unifications to ensure that the
argument actually passed to the procedure will have the inst specified.
-For example, if the predicate @code{p/1} has mode @samp{p(out)}, you
-can still call @samp{p(X)} if @code{X} is ground. The compiler will
+For example, if the predicate @code{p/1} is declared with mode @samp{p(out)},
+you can still call @samp{p(X)} if @code{X} is ground. The compiler will
transform this code to @samp{p(Y), X = Y} where @code{Y} is a fresh
variable. It is almost as if the predicate @code{p/1} has another mode
@samp{p(in)}; we call such modes ``implied modes''.
-To make this concept precise, we introduce the following definition.
-A term @dfn{satisfies} an instantiatedness tree
-if for every node in the instantiatedness tree,
+More precisely, given any declared mode @var{D},
+a mode @var{M} is an implied mode iff the following conditions are both met.
@itemize @bullet
@item
-if the node is ``free'',
-then the corresponding node in the term (if any)
-is either a distinct free variable,
-or a function symbol.
-
+Each final inst in @var{M} is identical to
+the corresponding final inst in @var{D}.
@item
-if the node is ``bound'',
-then the corresponding node in the term (if any)
-is a function symbol.
-
+Each initial inst in @var{M} can be derived from
+the corresponding initial inst in @var{D}
+by replacing one or more occurrences of @samp{free} in @var{D}
+with any other inst.
@end itemize
+ at noindent
+Note that although the final insts of an implied mode
+are identical to those of the declared mode,
+the inst of an argument after the procedure succeeds
+may be affected by the additional unifications.
+For example, if @code{q/1} is declared with mode @samp{q(free >> free)}
+but is called as @samp{q(X)} where @code{X} is ground,
+then after @code{q} succeeds
+ at code{X} will be @code{ground} rather than @code{free}.
+
The @dfn{mode set} for a predicate or function
-is the set of mode declarations for the predicate or function.
+is the set of mode declarations and implied modes
+for the predicate or function.
A mode set is an assertion by the programmer
that the predicate should only be called with argument terms
-that satisfy the initial instantiatedness trees
-of one of the mode declarations in the set
+that are described by the initial insts of one of the modes in the set
(i.e.@: the specified modes and the modes they imply
are the only allowed modes for this predicate or function).
We refer to the assertion associated with a mode set
@@ -2420,6 +2301,8 @@
with respect to a given mode declaration}
if given that the predicates and functions called by @var{p}
all satisfy their mode declaration constraints,
+and given that @var{p} is called with argument terms that are
+described by the initial insts of the mode declaration,
there exists an ordering of the conjuncts in each conjunction
in the clauses of @var{p} such that
@@ -2428,7 +2311,7 @@
@var{p} satisfies its mode declaration constraint, and
@item
@var{p} satisfies the mode set constraint of all of the predicates and
-functions it calls
+functions it calls.
@end itemize
We say that a predicate or function is well-moded
@@ -2437,34 +2320,216 @@
and we say that a program is well-moded
if all its predicates and functions are well-moded.
+The mode system uses a concept of ``matching'' insts.
+One inst matches another if it specifies an identical binding
+(that is, the inst is no more or less free than the other)
+and, where the insts are not free, gives at least as much other information.
+For the simple insts we have seen so for,
+``matches'' just means ``is the same as'';
+we will extend this definition as new insts are introduced.
+
+ at c Note: the matches relation described here corresponds to
+ at c inst_matches_final in the compiler. The effect of inst_matches_initial
+ at c is achieved by combining the matches partial order with our definition
+ at c of implied modes, given above.
+
The mode analysis algorithm checks one procedure at a time.
It abstractly interprets the definition of the predicate or function,
-keeping track of the instantiatedness of each variable,
-and selecting a mode for each call and unification in the definition.
+starting with the declared initial insts of the procedure's parameters,
+and keeps track of the instantiatedness of each variable.
+For each call and unification in the definition,
+a matching mode is selected.
To ensure that
the mode set constraints of called predicates and functions are satisfied,
the compiler may reorder the elements of conjunctions;
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.
+the resulting instantiatedness of the procedure's parameters
+matches the one given by the procedure's declaration.
The mode analysis algorithm annotates each call with the mode used.
+ at node Structured insts
+ at section Structured insts
+
+Mercury's mode system allows users to declare names for insts
+using declarations such as
+
+ at example
+:- inst non_empty_list == bound( [ground | ground] ).
+ at end example
+
+ at noindent
+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 matches another,
+it makes no difference whether the inst is referred to directly
+or by a declared name.
+That is, names are expanded before the ``matches'' relation 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.
+Note that other (non-list) terms are also described by this inst,
+since the second argument does not itself have to be a list.
+
+The argument to @code{bound}/1 must be a semicolon-separated sequence of
+function symbols, each of which has insts as arguments.
+The function symbols appearing in a variable's inst
+do not have to include every function symbol in the variable's type;
+if the inst only covers a subset of the possible function symbols,
+this can be thought of as giving ``subtype'' information
+about that variable.
+
+For example, given the declarations
+
+ at example
+:- type fruit ---> apple ; orange ; lemon.
+:- inst citrus == bound( orange ; lemon ).
+ at end example
+
+ at noindent
+the inst @samp{citrus} represents a subset of the values of type @samp{fruit},
+and can therefore be considered a subtype of @code{fruit}.
+
+A more concise, alternative syntax exists for @samp{bound} insts:
+
+ at example
+:- inst maybeskel ---> no ; yes(ground).
+ at end example
+
+ at noindent
+which is equivalent to writing
+
+ at example
+:- inst maybeskel == bound( no ; yes(ground) ).
+ at end example
+
+As with mode definitions, inst definitions may be parametric.
+For example,
+
+ at example
+:- inst listskel(Inst) ---> [] ; [Inst | listskel(Inst)].
+ at end example
+
+ at noindent
+defines the inst @samp{listskel(Inst)} to be a list skeleton
+whose elements have inst @samp{Inst};
+you can then use insts such as @samp{listskel(listskel(citrus))},
+which represents the instantiation state of a list of lists of citrus fruit.
+
+Let inst @var{A} be @samp{bound( As )}
+and inst @var{B} be @samp{bound( Bs )}.
+Then @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 match 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} 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.
+
+ at node Partially instantiated data structures
+ at section Partially instantiated data structures
+
+Mercury's mode system is sufficiently
+expressive to handle more complex data-flow patterns,
+including those involving partially instantiated data structures.
+(The current implementation does not handle
+partially instantiated data structures yet.)
+
+For example, consider an
+interface to a database that associates data with keys, and provides
+read and write access to the items it stores. To represent accesses to
+the database over a network, you would need declarations such as
+
+ at example
+:- type operation
+ ---> lookup(key, data)
+ ; set(key, data).
+:- inst request
+ ---> lookup(ground, free)
+ ; set(ground, ground).
+:- mode create_request == free >> request.
+:- mode satisfy_request == request >> ground.
+ at end example
+
+Any ``free'' parts of a inst describe distinct variables;
+there is no way to describe the fact that two variables are aliased.
+For example, the inst @samp{listskel(free)} describes
+lists whose skeleton is known but whose elements are distinct variables.
+As such, it describes the term @code{[A,B]}
+(where @code{A} and @code{B} are distinct)
+but not the term @code{[H|T]} (only part of the skeleton is known),
+the term @code{[A,2]} (not all elements are variables),
+or the term @code{[A,A]} (the elements are not distinct variables).
+
+Consider the definition
+
+ at example
+:- inst listskel == listskel(free).
+ at end example
+
+ at noindent
+where @code{listskel}/1 is defined as above.
+The usual definition of @code{length} can be given the mode
+
+ at example
+:- mode length(in(listskel)) = out.
+ at end example
+
+ at noindent
+since the implementation doesn't need to look at the elements;
+the length of a list can be calculated by just looking at the list skeleton.
+However, with the usual definition of @code{append} the mode
+
+ at example
+:- mode append(in(listskel), in(listskel), out(listskel)).
+ at end example
+
+ at noindent
+would not be allowed, since it would create aliasing between the
+different arguments --- on success of the predicate, the list elements
+would be free variables but they would not be distinct.
+
+
+ at c @node Dynamic modes
+ at c @section Dynamic modes
+ at c
+ at c XXX
+
+
@node Constrained polymorphic modes
@section Constrained polymorphic modes
Mode declarations for predicates and functions may also have inst parameters.
However, such parameters must be constrained to be @emph{compatible} with some
-other inst.
+other inst,
+in the sense that they can be used anywhere the other inst is required.
+For the insts we have seen so far,
+the rules for when inst @var{A} is compatible with inst @var{B}
+are the same as the rules for matching.
+When unique modes are considered, however,
+there is an extra requirement that the uniqueness of @var{A} and @var{B}
+should be the same; see @ref{Unique modes}.
+
In a predicate or function mode declaration,
an inst of the form @samp{@var{InstParam} =< @var{Inst}},
where @var{InstParam} is a variable and @var{Inst} is an inst,
-states that
- at var{InstParam} is constrained to be @emph{compatible} with @var{Inst},
-that is,
- at var{InstParam} represents some inst that can be used anywhere where
- at var{Inst} is required.
+states that @var{InstParam} is compatible with @var{Inst}.
If an inst parameter occurs more than once in a declaration, it must have the
same constraint on each occurrence.
@@ -2474,7 +2539,7 @@
out(list_skel(I =< ground))).
@end example
@noindent
- at code{I} is an inst parameter which is constrained to be ground.
+ at code{I} is an inst parameter which is compatible with ground.
If @samp{append} is called with the first two arguments having an inst of, say,
@samp{list_skel(bound(f))} then after @samp{append} returns, all three arguments
will have inst @samp{list_skel(bound(f))}.
@@ -2507,7 +2572,6 @@
:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I))).
@end example
-
Constrained polymorphic modes are particularly useful when passing
objects with higher-order types to polymorphic predicates
since they allow the higher-order mode information to be retained
@@ -2648,6 +2712,7 @@
@menu
* Destructive update::
* Backtrackable destructive update::
+* Uniqueness levels::
* Limitations of the current implementation::
@end menu
@@ -2662,7 +2727,7 @@
corresponding value. There is also an inst @samp{dead} which means
that there are no references to the corresponding value, so the compiler
is free to generate code that reuses that value.
-There are three standard modes for manipulation unique values:
+There are three standard modes for manipulating unique values:
@example
% unique output
@@ -2686,8 +2751,8 @@
only useful for code whose determinism is @samp{det} or @samp{cc_multi}
(@pxref{Determinism}).
-Unlike @samp{bound} instantiatedness trees, there is no alternative
-syntax for @samp{unique} instantiatedness trees.
+Unlike @samp{bound} insts, there is no alternative
+syntax for @samp{unique} insts.
@node Backtrackable destructive update
@section Backtrackable destructive update
@@ -2730,6 +2795,46 @@
:- mode mdi == mostly_unique >> mostly_dead.
@end example
+ at node Uniqueness levels
+ at section Uniqueness levels
+
+Mercury insts can be placed in order of least unique to most unique
+as follows
+(note that free variables are distinct, and hence ``unique''):
+
+ at itemize @bullet
+ at item
+ at code{dead},
+ at item
+ at code{mostly_dead},
+ at item
+ at code{ground}, and insts defined using @code{bound}/1,
+ at item
+ at code{mostly_unique},
+ at item
+ at code{unique}, insts defined using @code{unique}/1, and @code{free}.
+ at end itemize
+
+For inst @var{A} to match inst @var{B} when uniqueness is considered,
+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.
+
+For example, @samp{unique( f ; g )} matches @samp{bound( f ; g )},
+since the corresponding @code{bound} inst of the former matches the latter,
+and the former is more unique than the latter.
+However, @samp{unique( f ; g )} doesn't match @samp{bound( f )}
+(because it doesn't give enough subtype information),
+and neither does @samp{bound( f )} match @samp{unique( f ; g )}
+(because it is not unique enough).
+
+For inst @var{A} to be compatible with inst @var{B},
+it is necessary that @var{A} be the same level of uniqueness as @var{B}
+according to the above ordering,
+in addition to the rules that apply for compatibility of the corresponding
+ at code{free}, @code{ground} and @code{bound} insts.
+
@node Limitations of the current implementation
@section Limitations of the current implementation
@@ -3872,14 +3977,12 @@
@dots{}
@end example
-These insts represent the instantiation state of variables bound
-to higher-order predicate and function terms with the appropriate mode
-and determinism.
-For example, @samp{pred(out) is det} represents the instantiation state
-of being bound to a higher-order predicate term which is @samp{det}
-and accepts one output argument; the term @samp{sum([1,2,3])} from the
-example above is one such higher-order predicate term which matches
-this instantiation state.
+These insts describe higher-order predicate and function terms
+with the appropriate mode and determinism.
+For example, @samp{pred(out) is det} describes a higher-order predicate term
+which is @samp{det} and accepts one output argument;
+the term @samp{sum([1,2,3])} from the example above
+is one such higher-order predicate term which is described by this inst.
As a convenience, the language also contains builtin @samp{mode} values
of the same name (and they are what we have been using in the examples
@@ -3930,9 +4033,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
@@ -3950,6 +4053,28 @@
term that does not match this standard mode to somewhere where its higher-order
inst information may be lost, such as to a polymorphic predicate where the
argument mode is @samp{in}.
+
+A higher-order inst @var{A} matches higher-order inst @var{B} iff
+all of the following conditions are satisified:
+
+ at itemize @bullet
+ at item
+They are both predicates, or both functions.
+ at item
+They have the same determinism.
+ at item
+Each initial inst of @var{B} matches the corresponding initial inst of @var{A}.
+(That is, @samp{pred} and @samp{func} insts are
+contravariant in the initial insts, with respect to the ``matches'' ordering.)
+ at item
+Each final inst of @var{A} matches the corresponding final inst of @var{B}.
+(That is, @samp{pred} and @samp{func} insts are
+covariant in the final insts, with respect to the ``matches'' ordering.)
+ at end itemize
+
+Any higher-order inst matches @code{ground},
+but the converse is never true:
+ at code{ground} does not match any higher-order inst.
@node Modules
@chapter Modules
Relative diff:
diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi 23 Feb 2003 05:28:15 -0000
+++ doc/reference_manual.texi 25 Feb 2003 02:18:07 -0000
@@ -2080,9 +2080,6 @@
@menu
* Insts modes and mode definitions::
* Predicate and function mode declarations::
-* Structured insts::
-* Partially instantiated data structures::
- at c * Dynamic modes::
* Constrained polymorphic modes::
* Different clauses for different modes::
@end menu
@@ -2094,6 +2091,9 @@
@menu
* Insts modes and mode definitions::
* Predicate and function mode declarations::
+* Structured insts::
+* Partially instantiated data structures::
+ at c * Dynamic modes::
* Constrained polymorphic modes::
* Different clauses for different modes::
@end menu
@@ -2165,23 +2165,6 @@
@noindent
so that for example the mode @samp{in} is the same as @samp{in(ground)}.
-As execution proceeds, variables may become more instantiated.
-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 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''.
-
@node Predicate and function mode declarations
@section Predicate and function mode declarations
@@ -2268,16 +2251,40 @@
that their mode declaration constraints are satisfied.
In Mercury it is always possible to call a procedure with an
-argument that is more instantiated than the initial inst specified for that
+argument that is more bound than the initial inst specified for that
argument in the procedure's mode declaration. In such cases, the
compiler will insert additional unifications to ensure that the
argument actually passed to the procedure will have the inst specified.
-For example, if the predicate @code{p/1} has mode @samp{p(out)}, you
-can still call @samp{p(X)} if @code{X} is ground. The compiler will
+For example, if the predicate @code{p/1} is declared with mode @samp{p(out)},
+you can still call @samp{p(X)} if @code{X} is ground. The compiler will
transform this code to @samp{p(Y), X = Y} where @code{Y} is a fresh
variable. It is almost as if the predicate @code{p/1} has another mode
@samp{p(in)}; we call such modes ``implied modes''.
+More precisely, given any declared mode @var{D},
+a mode @var{M} is an implied mode iff the following conditions are both met.
+
+ at itemize @bullet
+ at item
+Each final inst in @var{M} is identical to
+the corresponding final inst in @var{D}.
+ at item
+Each initial inst in @var{M} can be derived from
+the corresponding initial inst in @var{D}
+by replacing one or more occurrences of @samp{free} in @var{D}
+with any other inst.
+ at end itemize
+
+ at noindent
+Note that although the final insts of an implied mode
+are identical to those of the declared mode,
+the inst of an argument after the procedure succeeds
+may be affected by the additional unifications.
+For example, if @code{q/1} is declared with mode @samp{q(free >> free)}
+but is called as @samp{q(X)} where @code{X} is ground,
+then after @code{q} succeeds
+ at code{X} will be @code{ground} rather than @code{free}.
+
The @dfn{mode set} for a predicate or function
is the set of mode declarations and implied modes
for the predicate or function.
@@ -2313,24 +2320,35 @@
and we say that a program is well-moded
if all its predicates and functions are well-moded.
+The mode system uses a concept of ``matching'' insts.
+One inst matches another if it specifies an identical binding
+(that is, the inst is no more or less free than the other)
+and, where the insts are not free, gives at least as much other information.
+For the simple insts we have seen so for,
+``matches'' just means ``is the same as'';
+we will extend this definition as new insts are introduced.
+
+ at c Note: the matches relation described here corresponds to
+ at c inst_matches_final in the compiler. The effect of inst_matches_initial
+ at c is achieved by combining the matches partial order with our definition
+ at c of implied modes, given above.
+
The mode analysis algorithm checks one procedure at a time.
It abstractly interprets the definition of the predicate or function,
-keeping track of the instantiatedness of each variable,
-and selecting a mode for each call and unification in the definition.
+starting with the declared initial insts of the procedure's parameters,
+and keeps track of the instantiatedness of each variable.
+For each call and unification in the definition,
+a matching mode is selected.
To ensure that
the mode set constraints of called predicates and functions are satisfied,
the compiler may reorder the elements of conjunctions;
it reports an error if no satisfactory order exists.
Finally it checks that
-the resulting instantiatedness of the procedure's arguments
+the resulting instantiatedness of the procedure's parameters
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.
The mode analysis algorithm annotates each call with the mode used.
-
@node Structured insts
@section Structured insts
@@ -2346,11 +2364,10 @@
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,
+When checking 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.
+That is, names are expanded before the ``matches'' relation is checked.
The inst @code{non_empty_list} describes any non-variable
whose top functor is @samp{[|]}/2,
@@ -2407,16 +2424,7 @@
Let inst @var{A} be @samp{bound( As )}
and inst @var{B} be @samp{bound( Bs )}.
-Then @var{A} is at least as instantiated as @var{B} iff
-for every function symbol in @code{As}
-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
+Then @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
@@ -2424,19 +2432,11 @@
@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 )},
+By using type information the compiler can consider @code{ground}
+to match 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
+If this is the case, then @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,
@@ -2519,10 +2519,12 @@
However, such parameters must be constrained to be @emph{compatible} with some
other inst,
in the sense that they can be used anywhere the other inst is required.
-More precisely,
-inst @var{A} is compatible with inst @var{B} iff
- at var{A} is at least as instantiated as @var{B},
-and also @var{A} matches @var{B}.
+For the insts we have seen so far,
+the rules for when inst @var{A} is compatible with inst @var{B}
+are the same as the rules for matching.
+When unique modes are considered, however,
+there is an extra requirement that the uniqueness of @var{A} and @var{B}
+should be the same; see @ref{Unique modes}.
In a predicate or function mode declaration,
an inst of the form @samp{@var{InstParam} =< @var{Inst}},
@@ -2710,7 +2712,7 @@
@menu
* Destructive update::
* Backtrackable destructive update::
-* Uniqueness ordering::
+* Uniqueness levels::
* Limitations of the current implementation::
@end menu
@@ -2793,8 +2795,8 @@
:- mode mdi == mostly_unique >> mostly_dead.
@end example
- at node Uniqueness ordering
- at section Uniqueness ordering
+ at node Uniqueness levels
+ at section Uniqueness levels
Mercury insts can be placed in order of least unique to most unique
as follows
@@ -2813,22 +2815,25 @@
@code{unique}, insts defined using @code{unique}/1, and @code{free}.
@end itemize
-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}
+For inst @var{A} to match inst @var{B} when uniqueness is considered,
+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.
-For inst @var{A} to match inst @var{B},
-the uniqueness ordering condition is reversed:
-it is necessary that @var{A} be of equal or greater uniqueness than @var{B}
+For example, @samp{unique( f ; g )} matches @samp{bound( f ; g )},
+since the corresponding @code{bound} inst of the former matches the latter,
+and the former is more unique than the latter.
+However, @samp{unique( f ; g )} doesn't match @samp{bound( f )}
+(because it doesn't give enough subtype information),
+and neither does @samp{bound( f )} match @samp{unique( f ; g )}
+(because it is not unique enough).
+
+For inst @var{A} to be compatible with inst @var{B},
+it is necessary that @var{A} be the same level of uniqueness as @var{B}
according to the above ordering,
-in addition to the rules that apply for the corresponding
+in addition to the rules that apply for compatibility of the corresponding
@code{free}, @code{ground} and @code{bound} insts.
-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}).
@node Limitations of the current implementation
@section Limitations of the current implementation
@@ -4067,18 +4072,9 @@
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.
+Any higher-order inst matches @code{ground},
+but the converse is never true:
+ at code{ground} does not match 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
--------------------------------------------------------------------------
More information about the reviews
mailing list