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

Mark Brown dougl at cs.mu.OZ.AU
Thu Feb 20 12:41:08 AEDT 2003
Previous message: [m-rev.] diff: fix extras/trailed_update/samples/interpreter
Next message: [m-rev.] for review: rewrite of Modes chapter
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Hi,

Here is a first attempt at rewriting the Modes chapter, along the lines
suggested earlier.  The new text defines the two partial orders used to
specify the rules of the language, but the definitions are spread
throughout so it may also be useful to add another section that summarizes
the rules for the two partial orders which are defined.  If so, this section
should go somewhere after the section on higher-order modes -- perhaps in
an appendix?

This is for review by Fergus and/or David (preferably both).

Cheers,
Mark.

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 two abstract partial
	  orders, which are written "is at least as instantiated as" and
	  "matches".  As each new kind of inst is introduced, the definitions
	  of the partial orders are 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.

	  (An alternative is "to approximate"; any other suggestions?)

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

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

	- 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.  (XXX Is this
	  correct?)

	- 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" as the conjunction of "is at least as
	  instantiated as" and "matches".

	- Add a section to the uniqueness chapter, defining the partial
	  ordering amongst unique insts.

	- Define the partial orders for higher-order insts.

Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.271
diff -u -r1.271 reference_manual.texi
--- doc/reference_manual.texi	12 Feb 2003 22:58:15 -0000	1.271
+++ doc/reference_manual.texi	20 Feb 2003 01:21:20 -0000
@@ -2080,6 +2080,9 @@
 @menu
 * Insts modes and mode definitions::
 * Predicate and function mode declarations::
+* Insts defined using bound::
+* Partially instantiated data structures::
+ at c * Dynamic modes::
 * Constrained polymorphic modes::
 * Different clauses for different modes::
 @end menu
@@ -2087,90 +2090,21 @@
 @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 be bound to.
+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.
+
+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.
+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:
-
- 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 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
+Mercury allows the user to specify modes directly
 by expressions such as @code{inst1 >> inst2},
 or to give them a name using declarations such as
 
@@ -2178,6 +2112,10 @@
 :- mode m == inst1 >> inst2.
 @end example
 
+ at noindent
+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,
 however this syntax is deprecated and may not be supported in future.
@@ -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:
 
@@ -2198,41 +2137,11 @@
 :- mode (-) == out.
 @end example
 
+ at noindent
 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
@@ -2241,43 +2150,34 @@
 @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
+so that for example the mode @samp{in} is the same as @samp{in(ground)}.
 
-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.
+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.
+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}.
+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
 
 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).
@@ -2287,25 +2187,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
@@ -2325,12 +2216,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{type::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
@@ -2340,32 +2235,20 @@
 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 instantiated 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.
@@ -2375,30 +2258,12 @@
 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,
-
- at itemize @bullet
- at 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.
-
- at item
-if the node is ``bound'',
-then the corresponding node in the term (if any)
-is a function symbol.
-
- at end itemize
-
 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
@@ -2409,6 +2274,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
 
@@ -2417,7 +2284,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
@@ -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.
 
 The mode analysis algorithm annotates each call with the mode used.
 
+
+ at node Insts defined using bound
+ at section Insts defined using @samp{bound}
+
+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
+This inst 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} 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.
+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 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.
+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}.
+
 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.
 
@@ -2463,7 +2483,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))}.
@@ -2496,7 +2516,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
@@ -2637,6 +2656,7 @@
 @menu
 * Destructive update::
 * Backtrackable destructive update::
+* Uniqueness ordering::
 * Limitations of the current implementation::
 @end menu
 
@@ -2651,7 +2671,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
@@ -2675,8 +2695,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
@@ -2719,6 +2739,43 @@
 :- mode mdi == mostly_unique >> mostly_dead.
 @end example
 
+ at node Uniqueness ordering
+ at section Uniqueness ordering
+
+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 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.
+Note that since the ordering 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
 
@@ -3861,14 +3918,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
@@ -3939,6 +3994,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} 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
+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
 
 @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
--------------------------------------------------------------------------
Previous message: [m-rev.] diff: fix extras/trailed_update/samples/interpreter
Next message: [m-rev.] for review: rewrite of Modes chapter
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the reviews mailing list