Return to eval.tex CVS log

Up to [Research Unix] / researchv10no / cmd / sml / doc / refman

Annotation of researchv10no/cmd/sml/doc/refman/eval.tex, revision 1.1

1.1     ! root        1: \chapter{Evaluation}
        !             2: \label{eval}
        !             3: \section{Environments and Values}
        !             4: Evaluation of phrases takes place in the presence of an {\em environment} and a
        !             5: {\em store}.  An {\em value environment} E maps identifiers to values, value constructors, and
        !             6: exception constructors.  A {\em store} S maps references to values; references
        !             7: are themselves values.  (Type environments TE, are
        !             8: ignored here since they are relevant only to
        !             9: type-checking and compilation, not to evaluation.  Other environments
        !            10: having to do with the module system are also ignored here.)
        !            11: 
        !            12: A value $v$ is either a constant (a nullary constructor), a
        !            13: construction (a constructor applied to a value), a record, a
        !            14: reference, or a function value.  A record value is a set of
        !            15: label-value pairs, written \{ label = value , \rep{0} , label = value \},
        !            16: in which the labels are distinct; note that the order of components
        !            17: is immaterial.  Labels may be identifiers or integer numerals; both
        !            18: kinds of labels may appear in the same record value.  A function
        !            19: value is a partial function which, given a value, may return a
        !            20: value or may raise an exception; it may also change the store as a side-effect.
        !            21: 
        !            22: An exception $e$, associated to an exception name  {\em exn} in a value
        !            23: environment, is a special kind of constructor.  Exception
        !            24: constructors may be nullary or value-carrying, just as may ordinary
        !            25: constructors.  Nullary exception constructors, and constructed
        !            26: exceptions (exception constructors applied to values), are ordinary
        !            27: values of type {\em exn}.
        !            28: 
        !            29: Evaluation of a phrase returns a {\em result}---a value $v$,
        !            30: a value-environment $E$, or a store $S$ as follows:
        !            31: 
        !            32: \begin{tabular}{l l}
        !            33: {\bf \ \ Phrase}&{\bf \  Value} \\
        !            34: Expression & v and S, or raise(v) and S\\
        !            35: Value binding & E and S, or raise(v) and S\\
        !            36: Type binding & {\it no effect on E or S} \\
        !            37: Datatype binding & E \\
        !            38: Exception binding & E \\
        !            39: Declaration & E and S, or raise(v) and S
        !            40: \end{tabular}
        !            41: 
        !            42: The remainder of this chapter describes the semantics of various
        !            43: phrases in terms of values $v$ and environments $E$.
        !            44: 
        !            45: The semantics of stores ($S$) are discussed in
        !            46: Chapter~\ref{reference};
        !            47: for the remainder of this chapter, the
        !            48: effect of various phrases on stores will be ignored.
        !            49: The semantics of exceptions is discussed in
        !            50: Chapter~\ref{exception}.
        !            51: 
        !            52: 
        !            53: For every phrase except a \verb"handle" expression, whenever its
        !            54: evaluation demands the evaluation of an immediate subphrase which
        !            55: returns a raised exception {\em raise(v)} as a result, no further
        !            56: evaluation of subphrases occurs and {\em raise(v)} is also the result
        !            57: of the phrase.  This rule should be remembered while reading the
        !            58: evaluation rules below.
        !            59: 
        !            60: In presenting the rules, explicit type
        !            61: constraints (:ty) have been ignored since they have no effect on
        !            62: evaluation.
        !            63: 
        !            64: \section{Environment manipulation}
        !            65: We may write $\{ i_1 \mapsto v_1 , ... , i_n \mapsto v_n \}$ for a
        !            66: value environment E (the identifiers $i_k$ being distinct).  Then
        !            67: $E(i_k)$ denotes $v_k$, $\{\}$ is the empty value environment, and
        !            68: $E+E'$ means the environment in which the associations of $E'$
        !            69: supersede those of $E$.
        !            70: 
        !            71: \section{Matching patterns}
        !            72: Patterns serve in ML both as formal parameters of functions, and
        !            73: as indices in case statements.  When a function or a case statement
        !            74: is applied to a particular value, one of its patterns may match the
        !            75: value.
        !            76: 
        !            77: A nullary constructor (like \verb"nil") used as a pattern
        !            78: will match only the corresponding nullary constructor value.  A
        !            79: value-carrying constructor $c$, applied to a pattern $p_1$, makes a pattern
        !            80: $c(p_1)$;
        !            81: this constructed pattern will match a value $c(v_1)$
        !            82: built with the same value-carrying constructor, and only if the
        !            83: pattern $p_1$ matches the value $v_1$.
        !            84: 
        !            85: A record pattern 
        !            86: \verb"{" ${\it lab}_1$ \verb"=" ${\it pat}_1$ , \underline{\ \ \ } , ${\it lab}_n$ \verb"=" ${\it pat}_n$ \verb"}"
        !            87: matches a record value whose labels are the same, and only if each
        !            88: pattern matches the corresponding value.
        !            89: If the ellipsis (\verb"...") is used at the end of a record pattern,
        !            90: then it will match a record value with {\it at least} the labels
        !            91: specified in the pattern.
        !            92: 
        !            93: An identifier (i.e. a variable)
        !            94: used as a pattern will match any value; when this happens, the
        !            95: variable will also be bound to that value throughout the variable's
        !            96: scope.  When a variable is a component of a record or constructor
        !            97: pattern, then it is bound to a particular component of the record
        !            98: value or constructed value.
        !            99: 
        !           100: An underscore will match any value.
        !           101: 
        !           102: Sometimes it is desired to bind a variable to a value only
        !           103: if the value matches a particular pattern.  The pattern 
        !           104: {\it id}\verb" as "{\it pat} binds the value to the variable {\it
        !           105: id}, but only if the {\it pat} matches.
        !           106: 
        !           107: Type constraints may be applied to patterns.  {\it pat\verb":"ty}
        !           108: matches the same values that {\it pat} does, but the compiler will
        !           109: guarantee that the pattern will only be applied to values  of type
        !           110: {\it ty}.
        !           111: 
        !           112: \subsection*{A more formal description}
        !           113: The matching of a pattern to a value $v$ either {\em fails} or yields
        !           114: a value environment.  Failure is distinct from raising an exception,
        !           115: but an exception will be raised when all patterns fail in applying a
        !           116: match to a value (see Sections~\ref{raisematch}, \ref{raisebind}, and \ref{reraise}).  In the following rules, if any
        !           117: component pattern fails to match then the whole pattern fails to
        !           118: match.
        !           119: 
        !           120: The following is the effect of matching a pattern  to a value $v$ in the
        !           121: environment $E$, for
        !           122: each of the kinds of pattern (with failure if any condition is not
        !           123: satisfied):
        !           124: \begin{description}
        !           125: \item[\protect\verb"\_"\hfill]  {\it (underscore)} the empty value environment $\{\}$ is
        !           126: returned
        !           127: \item[id\hfill] if $E(id)$ is not a constructor, then the value environment
        !           128: $\{id \mapsto v\}$ is returned
        !           129: \item[id\hfill] if $E(id)$ is a nullary constructor, then if $E(id)=v$,
        !           130: then $\{\}$ is returned, else failure
        !           131: \item[id pat\hfill]  if $E(id)$ is a value-carrying constructor $c$, and 
        !           132: $v = c v'$, then pat is matched to $v'$, else failure.
        !           133: \item[id \protect\verb"as" pat\hfill]  pat is matched to $v$ returning $E$;
        !           134: then $\{id \mapsto v\}+E$ is returned.
        !           135: \item[\protect\verb"\{" ${\it lab}_1$ \protect\verb"=" ${\it pat}_1$ , \underline{\ \ \ } , ${\it lab}_n$ \protect\verb"=" ${\it pat}_n$ \protect\verb"\}" \hfill]  
        !           136: if $v = \{ {\it lab}_1 = v_1 , ... , {\it lab}_n = v_n \}$ then 
        !           137: ${\it pat}_i$ is matched to $v_i$ returning $E_i$, for each $i$; then 
        !           138: $E_1 + ... + E_n$ is returned.
        !           139: 
        !           140: \item[\protect\verb"\{" ${\it lab}_1$ \protect\verb"=" ${\it pat}_1$ , \underline{\ \ \ } , ${\it lab}_n$ \protect\verb"=" ${\it pat}_n$ \protect\verb", ... \}" \hfill]  
        !           141: if $v = \{ {\it lab}'_1 = v_1 , ... , {\it lab}'_m = v_m \}$ then if
        !           142: the ${\it lab}_i$ are a subset of the ${\it lab}'_j$ then
        !           143: ${\it pat}_i$ is matched to $v_j$ returning $E_i$, for each $i,j$ such that
        !           144: ${\it lab}_i = {\it lab}'_j$; then 
        !           145: $E_1 + ... + E_n$ is returned.
        !           146: \end{description}
        !           147: No pattern may contain the same variable twice.
        !           148: No record pattern, record expression, or record type may use the same
        !           149: label twice.
        !           150: \section{Applying a match}
        !           151: Assume environment $E$.  Applying a match
        !           152: $ {\it pat}_1 \protect\verb"=>" {\it exp}_1 \mid ... 
        !           153: \mid {\it pat}_n \protect\verb"=>" {\it exp}_n $ to value $v$ returns a value
        !           154: or raises an exception as follows.  Each ${\it pat}_i$ is matched to
        !           155: $v$ in turn, from left to right, until one succeeds returning $E_i$;
        !           156: then ${\it exp}_i$ is evaluated in $E+E_i$.  If none succeeds, then
        !           157: an exception is raised, depending on the syntactic context in which
        !           158: the match occurs (see Sections~\ref{raisematch}, \ref{raisebind}, and \ref{reraise}).
        !           159: \label{matchwarn}
        !           160: If a match contains a redundant pattern (where any value that could
        !           161: satisfy it will be matched by a previous pattern in the match), the
        !           162: compiler will issue a warning message.  If the match (except those
        !           163: that form exception-handlers) is not exhaustive (some value matches
        !           164: none of the patterns) then the compiler will issue a warning message.
        !           165: 
        !           166: Thus, for each $E$, a match denotes a function value.
        !           167: 
        !           168: \section{Evaluation of expressions}
        !           169: Evaluating an expression in the environment $E$ returns a value (or raises an
        !           170: exception) as follows, in each of the cases for exp:
        !           171: \begin{description}
        !           172: \item[id\hfill]  the value $E(id)$ is returned; id may be a variable-id or a
        !           173: constructor-id
        !           174: \item[const\hfill]  the value denoted by the constant (an integer, real, or
        !           175: string literal) is returned.
        !           176: \item[${\bf exp}_1 {\bf exp}_2$\hfill] ${\bf exp}_1$ is evaluated, 
        !           177: returning function $f$; then ${\it exp}_2$
        !           178: is evaluated, returning value $v$; then $f(v)$ is returned.
        !           179: \item[\protect\verb"\{" ${\it lab}_1$ \protect\verb"=" ${\it exp}_1$ , \underline{\ \ \ } , ${\it lab}_n$ \protect\verb"=" ${\it exp}_n$ \protect\verb"\}" \hfill]  
        !           180: the ${\it exp}_i$ are evaluated in sequence, from left to right,
        !           181: returning $v_i$ respectively; then the record 
        !           182: $\{ {\it lab}_1 = v_1 , ... , {\it lab}_n = v_n \}$ is returned.
        !           183: \item[\protect\verb"raise" exp\hfill]  exp is evaluated, returning $v$; then 
        !           184: the exception-value $v$ is raised.
        !           185: 
        !           186: \item[exp \verb"handle" match\hfill]  exp is evaluated; if exp returns a
        !           187: value $v$, then $v$ is returned.  If exp raises an exception $e$ then
        !           188: the match is applied to $e$.  If the match fails, then $e$ is raised
        !           189: (as the value of the \verb"handle" expression).  If the match
        !           190: succeeds, then the resulting value is returned.
        !           191: 
        !           192: \item[\verb"let" dec \verb"in" exp \verb"end"\hfill]  dec is evaluated,
        !           193: returning $E'$; then exp is evaluated in the environment $E+E'$.
        !           194: 
        !           195: \item[\verb"fn" match\hfill]  $f$ is returned, where $f$ is the function of
        !           196: $v$ gained by applying match to $v$ in the environment $E$, and such
        !           197: that if the match fails, an exception \verb"Match" will be raised.
        !           198: \label{raisematch}
        !           199: But matches that may fail are to be detected by the
        !           200: compiler and flagged with a warning; see Section~\ref{matchwarn}.
        !           201: \end{description}
        !           202: 
        !           203: \section{Evaluation of value bindings}
        !           204: Evaluating a value binding in environment $E$ returns a value
        !           205: environment $E'$  or raises an exception as follows:
        !           206: \begin{description}
        !           207: \item[pat \verb"=" exp\hfill]  exp is evaluated in $E$, returning value
        !           208: $v$; then pat is matched to $v$; if this returns $E'$ then $E'$ is
        !           209: returned.  If the pattern fails to match then the exception 
        !           210: \verb"Bind" will be raised.
        !           211: \label{raisebind}
        !           212: But bindings that may fail are to be detected by the
        !           213: compiler and flagged with a warning; see Section~\ref{bindwarn}.
        !           214: 
        !           215: \item[${\bf vb}_1$ \verb"and" \underline{\ \ \ } \verb"and" ${\bf vb}_n$\hfill]
        !           216: The value bindings ${\bf vb}_1$ through ${\bf vb}_n$ are evaluated in
        !           217: $E$ from left to right, returning $E_1 , ... E_n$; then $E_1 + ... +
        !           218: E_n$ is returned.
        !           219: 
        !           220: \item[\verb"rec" vb\hfill]  {\bf vb} is evaluated in $E'$, returning $E''$,
        !           221: where $E' = E + E''$.  Because the values bound by \verb"rec" {\bf
        !           222: vb} must be function values, $E'$ is well defined by ``tying knots''
        !           223: (Landin).
        !           224: \end{description}
        !           225: No binding may bind the same identifier twice.
        !           226: 
        !           227: \label{bindwarn}
        !           228: For each value binding ``pat = exp'' the compiler will issue a
        !           229: warning message if {\it either} pat is not exhaustive {\it or} pat
        !           230: contains no variable.  This will (on both counts) detect a mistaken
        !           231: declaration like \verb"val nil = f(x)" in which the user expects to
        !           232: declare a new variable nil (whereas the language dictates that
        !           233: \verb"nil" here is a constant pattern, so no variable gets declared).
        !           234: However, these warnings need not be given at top level in the
        !           235: interactive system.
        !           236: \section{Evaluation of type and datatype bindings}
        !           237: The value environment $E$ does not affect the evaluation of type
        !           238: bindings or datatype bindings ($TE$ affects their type-checking and
        !           239: compilation).  Evaluation of a type binding just returns the empty
        !           240: value environment $\{\}$; the purpose of type bindings is merely to
        !           241: provide an abbreviation for a compound type.
        !           242: 
        !           243: Evaluation of a
        !           244: datatype binding {\bf db} returns a value environment $E'$ (it cannot
        !           245: raise an exception) as follows:
        !           246: 
        !           247: \begin{description}
        !           248: \item[tyvars id = ${\bf constr}_1 \mid \underline{\ \ \ } \mid {\bf constr}_n$\hfill]
        !           249: New constructors ${\bf con}_1, ... , {\bf con}_n$ are created.
        !           250: The value environment $E' = \{ id_1 \mapsto v_1 , ... , id_n \mapsto
        !           251: v_n \} $ is returned, where $v_i$ is either the constant value
        !           252: ${\bf con}_i$ (if ${\bf constr}_i$ is just ${\bf id}_i$), or else the
        !           253: function which maps $x$ to ${\bf con}_i(x)$ (if ${\bf constr}_i$ is
        !           254: ${\bf id}_i$ \verb"of" {\bf ty}).
        !           255: 
        !           256: \item[${\bf db}_1$ \verb"and" \underline{\ \ \ } \verb"and" ${\bf db}_n$\hfill]
        !           257: The bindings ${\bf db}_1 , ... , {\bf db}_n$
        !           258: are evaluated from left to right, returning $E_1 , ... , E_n$; then
        !           259: $E_1 + ... + E_n$ is returned.
        !           260: \end{description}
        !           261: In the left hand side ``tyvars id'' of a type of datatype binding,
        !           262: no type-variable may appear twice in ``tyvars.''
        !           263: The right hand side may contain only the type variables
        !           264: mentioned on the left.  Within the scope of the declaration of
        !           265: ``id,'' any occurrence of the type constructor ``id'' must be
        !           266: accompanied by as many type arguments as indicated by the (possibly empty)
        !           267: tyvar sequence ``tyvars'' in the declaration.
        !           268: 
        !           269: No binding may bind the same identifier twice.
        !           270: \section{Evaluation of exception bindings}
        !           271: The evaluation of an exception binding in an environment $E$ returns an
        !           272: environment $E'$ as follows:
        !           273: \begin{description}
        !           274: \item[id\hfill]   A new exception constructor {\bf con} is generated, and
        !           275: the environment $\{{\bf id} \mapsto {\bf con} \}$ is returned.
        !           276: 
        !           277: \item[id \verb"of" ty \hfill]  A new exception constructor {\bf con} is generated,
        !           278: and the environment $\{{\bf id} \mapsto v\}$ is returned, where $v$ is the
        !           279: function of $x$ that returns ${\bf con}(x)$.
        !           280: 
        !           281: \item[${\bf id}_1$ \verb"=" ${\bf id}_2$ \hfill]  The environment
        !           282: $\{ {\bf id}_1 \mapsto E({\bf id}_2) \}$ is returned; that is, 
        !           283: ${\bf id}_1$ is bound to the same exception constructor as ${\bf id}_2$.
        !           284: 
        !           285: \item[${\bf eb}_1$ \verb"and" \underline{\ \ \ } \verb"and" ${\bf eb}_n$\hfill]
        !           286: The bindings ${\bf eb}_1 , ... , {\bf eb}_n$
        !           287: are evaluated from left to right, returning $E_1 , ... , E_n$; then
        !           288: $E_1 + ... + E_n$ is returned.
        !           289: \end{description}
        !           290: No binding may bind the same identifier twice.
        !           291: \section{Evaluation of declarations}
        !           292: 
        !           293: Evaluating a declaration in a value environment $E$ returns a value
        !           294: environment $E'$ or raises an exception as follows (as usual in this chapter,
        !           295: the effect on type environments is ignored):
        !           296: 
        !           297: \begin{description}
        !           298: \item[\verb"val" vb\hfill] The value binding {\rm vb} is evaluated,
        !           299: returning $E'$; then $E'$ is returned.
        !           300: 
        !           301: \item[\verb"type" tb\hfill] The empty environment $\{\}$ is returned.
        !           302: 
        !           303: \item[\verb"datatype" db\hfill]  {\rm db} is evaluated, returning
        !           304: $E'$, which is returned.
        !           305: 
        !           306: \item[\verb"exception" eb\hfill]  {\rm eb} is evaluated, returning
        !           307: $E'$, which is returned.
        !           308: 
        !           309: \item[\verb"local" ${\bf dec}_1$ \verb"in" ${\bf dec}_2$ \verb"end"\hfill]
        !           310: ${\rm dec}_1$ is evaluated in $E$, returning $E_1$; then 
        !           311: ${\rm dec}_2$ is evaluated in $E+E_1$, returning $E_2$; then $E+E_2$
        !           312: is returned.
        !           313: 
        !           314: \item[${\bf dec}_1$ ${\bf dec}_2$\hfill]
        !           315: ${\rm dec}_1$ is evaluated in $E$, returning $E_1$; then 
        !           316: ${\rm dec}_2$ is evaluated in $E+E_1$, returning $E_2$; then $E_1+E_2$
        !           317: is returned.
        !           318: 
        !           319: \item[${\bf dec}$ \verb";"\hfill] has the same effect as {\bf dec}.
        !           320: \end{description}
        !           321: \section{Evaluation of a program}
        !           322: The evaluation of a program ${\bf dec}_1$ \verb";" \underline{\ \ \ }
        !           323: \verb";" ${\bf dec}_n$ takes place in the initial presence of the
        !           324: standard top-level environment $E_0$ containing all the standard
        !           325: bindings (see Appendix~\ref{library}).  For $i>0$ the top-level environment
        !           326: $E_i$, present after the evaluation of ${\bf dec}_i$ in the program,
        !           327: is defined recursively as follows:  ${\bf dec}_i$ is evaluated in
        !           328: $E_{i-1}$ returning environment ${E'}_i$, and then $E_i =
        !           329: E_{i-1}+{E'}_i$.

This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.