From 49f309eee587647fb8183c832adae20b401ae8c7 Mon Sep 17 00:00:00 2001 From: Lars Bergstrom Date: Thu, 26 Sep 2013 20:05:46 -0500 Subject: [PATCH] SML90 definition, updated for LaTeX 2e --- README.md | 24 +- app1.tex | 271 ++++++++++++ app2.tex | 266 ++++++++++++ app3.tex | 208 +++++++++ app4.tex | 222 ++++++++++ app5.tex | 423 +++++++++++++++++++ dyncor.tex | 842 +++++++++++++++++++++++++++++++++++++ dynmod.tex | 427 +++++++++++++++++++ index.tex | 887 +++++++++++++++++++++++++++++++++++++++ intro.tex | 124 ++++++ mac.tex | 752 +++++++++++++++++++++++++++++++++ notes.tex | 634 ++++++++++++++++++++++++++++ preface.tex | 227 ++++++++++ prog.tex | 129 ++++++ root.tex | 115 +++++ rootagfa.tex | 114 +++++ statcor.tex | 1134 ++++++++++++++++++++++++++++++++++++++++++++++++++ statmod.tex | 1049 ++++++++++++++++++++++++++++++++++++++++++++++ syncor.tex | 477 +++++++++++++++++++++ synmod.tex | 310 ++++++++++++++ 20 files changed, 8633 insertions(+), 2 deletions(-) create mode 100644 app1.tex create mode 100644 app2.tex create mode 100644 app3.tex create mode 100644 app4.tex create mode 100644 app5.tex create mode 100644 dyncor.tex create mode 100644 dynmod.tex create mode 100644 index.tex create mode 100644 intro.tex create mode 100644 mac.tex create mode 100644 notes.tex create mode 100644 preface.tex create mode 100644 prog.tex create mode 100644 root.tex create mode 100644 rootagfa.tex create mode 100644 statcor.tex create mode 100644 statmod.tex create mode 100644 syncor.tex create mode 100644 synmod.tex diff --git a/README.md b/README.md index 530358a..165f883 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,24 @@ -definition +The Definition of Standard ML ========== -The definition of Standard ML +These sources are currently based on the SML90 version of the Definition of +Standard ML. To build a PDF, perform the following steps in a terminal window: +``` +pdflatex root +bibtex root +peflatex root +pdflatex root +``` + +The file root.pdf will be produced. + +## Obtaining a printed copy of the book + +MIT Press has graciously allowed us to release this work in PDF form and +continue to extend it again. If you would like a printed copy of this work, +please purchase one from their site: + +[http://mitpress.mit.edu/books/definition-standard-ml] + + + diff --git a/app1.tex b/app1.tex new file mode 100644 index 0000000..635b932 --- /dev/null +++ b/app1.tex @@ -0,0 +1,271 @@ +\section{Appendix: Derived Forms} +\label{derived-forms-app} +Several derived\index{66.1} grammatical forms are provided in the Core; they are presented +in Figures~\ref{der-exp}, \ref{der-pat} and \ref{der-dec}. Each derived form is +given with its equivalent form. Thus, each row of the tables should be +considered as a rewriting rule +\[ \mbox{Derived form \ $\Longrightarrow$\ Equivalent form} \] +and these rules may be applied repeatedly to a phrase until it is transformed +into a phrase of the bare language. +See Appendix~\ref{core-gram-app} for the full Core grammar, including all the +derived forms. + +In the derived forms for tuples, in terms of records, we use $\overline{n}$ to +mean the ML numeral which stands for the natural number $n$. + +Note that a new phrase class ~FvalBind~ of function-value bindings is introduced, +accompanied by a new declaration form ~\FUN\ \fvalbind~. The mixed forms +~\VAL\ \REC\ \fvalbind~, ~\VAL\ \fvalbind~ and ~\FUN\ \valbind~ are not +allowed -- though the first form arises during translation into the bare +language. + +The following notes refer to Figure~\ref{der-dec}: +\begin{itemize} +%\item In the equivalent form for a function-value binding, the +% variables ~$\var_1$, $\cdots$, $\var_n$~ must be chosen not to +% occur in the derived form. The condition $m,n\geq 1$ applies. +\item There is a version of the derived form for function-value binding + which allows the function identifier to be infixed; + see Figure~\ref{dec-gram} in Appendix~\ref{core-gram-app}. +\item In the two forms involving ~\WITHTYPE~, the identifiers bound + by ~\datbind~ and by ~\typbind~ must be distinct. Then the + transformed binding ~\datbind$\/'$~ in the equivalent form is + obtained from ~\datbind~ by expanding out all the definitions + made by ~\typbind. More precisely, if ~\typbind~ is + \[ \tyvarseq_1\ \tycon_1\ \mbox{\ml{=}} \ty_1\ \ \AND + \ \cdots\ \AND + \ \ \tyvarseq_n\ \tycon_n\ \mbox{\ml{=}} \ty_n\ \] + then ~\datbind$\/'$~ is the result of simultaneous replacement + (in ~\datbind~) of every type expression ~$\tyseq_i\ \tycon_i$~ + ($1\leq i\leq n$) + by the corresponding defining expression + \[ \ty_i\{\tyseq_i/\tyvarseq_i\}\] +%\item The abbreviation of ~\VAL\ {\tt it =} \exp~ to ~\exp~ is only +% permitted at top-level, i.e. as a ~\program~. +\end{itemize} + +Figure~\ref{functor-der-forms-fig} shows derived forms for functors. +They allow functors to take, say, a single type or value as a parameter, +in cases where it would seem clumsy to ``wrap up'' the argument as a +structure expression. +These forms are currently more experimental than the bare syntax of modules, +but we recommend implementers to include them so that they can be +tested in practice. +In the derived forms for functor bindings and functor signature expressions, +$\strid$ is a new structure identifier and +the form of $\sigexp'$ depends +on the form of $\sigexp$ as follows. +If $\sigexp$ is simply a signature identifier +$\sigid$, then $\sigexp'$ is also $\sigid$; otherwise $\sigexp$ must take +the form ~$\SIG\ \spec_1\ \END$~, +and then $\sigexp'$ is +$\mbox{\SIG\ \LOCAL\ \OPEN\ \strid\ \IN\ $\spec_1$\ \END\ \END}$. +%(where $\strid$ is new). + +\begin{figure} + +\begin{tabular}{|l|l|l} +\multicolumn{1}{c}{Derived Form} & \multicolumn{1}{c}{Equivalent Form} & +\multicolumn{1}{c}{}\\ +\multicolumn{3}{c}{}\\ +\multicolumn{2}{l}{{\bf Expressions} \exp}\\ +%\multicolumn{2}{l}{EXPRESSIONS \exp}\\ +\cline{1-2} +\ml{()} & \ml{\lttbrace\ \rttbrace} \\ +\cline{1-2} +\ml{(}$\exp_1$ \ml{,} $\cdots$ \ml{,} $\exp_\n$\ml{)} + & \ml{\lttbrace 1=}$\exp_1$\ml{,}\ $\cdots$\ml{,}\ + $\overline{n}$\ml{=}$\exp_\n$\ml{\rttbrace} + & $(\n\geq 2)$\\ +\cline{1-2} +\ml{\#}\ \lab & \FN\ \ml{\lttbrace}\lab\ml{=}\var\ml{,...\rttbrace\ => }\var + & (\var\ new)\\ +%\cline{1-2} +%\RAISE\ \longexn & \RAISE\ \longexn\ \WITH\ \ml{()} \\ +\cline{1-2} +\CASE\ \exp\ \OF\ \match + & \ml{(}\FN\ \match\ml{)(}\exp\ml{)} \\ +\cline{1-2} +\IF\ $\exp_1$\ \THEN\ $\exp_2$\ \ELSE\ $\exp_3$ + & \CASE\ $\exp_1$\ \OF\ \TRUE\ \ml{=>}\ \exp$_2$\\ + & \ \ \qquad\qquad\ml{|}\ \FALSE\ \ml{=>}\ \exp$_3$ \\ +\cline{1-2} +\exp$_1$\ \ORELSE\ \exp$_2$ + & \IF\ \exp$_1$\ \THEN\ \TRUE\ \ELSE\ \exp$_2$ \\ +\cline{1-2} +\exp$_1$\ \ANDALSO\ \exp$_2$ + & \IF\ \exp$_1$\ \THEN\ \exp$_2$\ \ELSE\ \FALSE \\ +\cline{1-2} +\ml{(}$\exp_1$ \ml{;} $\cdots$ \ml{;} $\exp_\n$ \ml{;} \exp\ml{)}\ + & \CASE\ \exp$_1$\ \OF\ \ml{(\_) =>} + & $(\n\geq 1)$ \\ + & \qquad$\cdots$ \\ + & \CASE\ \exp$_n$\ \OF\ \ml{(\_) =>}\ \exp \\ +\cline{1-2} +\LET\ \dec\ \IN + & \LET\ \dec\ \IN & $(\n\geq 2)$ \\ +\qquad$\exp_1$ \ml{;} $\cdots$ \ml{;} $\exp_\n$ \END + & \ \ \ml{(}$\exp_1$ \ml{;} $\cdots$ \ml{;} $\exp_\n$\ml{)}\ + \END\\ +\cline{1-2} +\WHILE\ \exp$_1$\ \DO\ \exp$_2$ + & \LET\ \VAL\ \REC\ \var\ \ml{=}\ \FN\ \ml{() =>} + & (\var\ new)\\ + & \ \ \IF\ \exp$_1$\ \THEN\ + \ml{(}\exp$_2$\ml{;}\var\ml{())}\ \ELSE\ \ml{()} \\ + & \ \ \IN\ \var\ml{()}\ \END\\ +\cline{1-2} +\ml{[}$\exp_1$ \ml{,} $\cdots$ \ml{,} $\exp_\n$\ml{]} + & \exp$_1$\ \ml{::}\ $\cdots$\ \ml{::}\ \exp$_n$\ + \ml{::}\ \NIL & $(n\geq 0)$ \\ +\cline{1-2} +\multicolumn{3}{c}{}\\ +\end{tabular} +\caption{Derived forms of Expressions\index{67.1}} +\label{der-exp} +\end{figure} + +\begin{figure} + +\begin{tabular}{|l|l|l} +\multicolumn{1}{c}{Derived Form} & \multicolumn{1}{c}{Equivalent Form} & +\multicolumn{1}{c}{}\\ +\multicolumn{3}{c}{}\\ +\multicolumn{2}{l}{{\bf Patterns} \pat}\\ +%\multicolumn{2}{l}{PATTERNS \pat}\\ +\cline{1-2} +\ml{()} & \ml{\lttbrace\ \rttbrace} \\ +\cline{1-2} +\ml{(}$\pat_1$ \ml{,} $\cdots$ \ml{,} $\pat_\n$\ml{)} + & \ml{\lttbrace 1=}$\pat_1$\ml{,}\ $\cdots$ \ml{,}\ + $\overline{n}$\ml{=}$\pat_\n$\ml{\rttbrace} + & $(\n\geq 2)$ \\ +\cline{1-2} +\ml{[}$\pat_1$ \ml{,} $\cdots$ \ml{,} $\pat_\n$\ml{]} + & \pat$_1$\ \ml{::}\ $\cdots$\ \ml{::}\ \pat$_n$\ + \ml{::}\ \NIL & $(n\geq 0)$ \\ +\cline{1-2} +\multicolumn{3}{c}{}\\ +\multicolumn{2}{l}{{\bf Pattern Rows} \labpats}\\ +%\multicolumn{2}{l}{PATTERN ROWS \labpats}\\ +\cline{1-2} +\id$\langle$\ml{:}\ty$\rangle + \ \langle\AS\ \pat\rangle + \ \langle$\ml{,} \labpats$\rangle$ + & \id\ml{ = }\id$\langle$\ml{:}\ty$\rangle + \ \langle\AS\ \pat\rangle + \ \langle$\ml{,} \labpats$\rangle$ \\ +\cline{1-2} +\multicolumn{3}{c}{}\\ +\multicolumn{2}{l}{{\bf Type Expressions} \ty}\\ +%\multicolumn{2}{l}{TYPE EXPRESSIONS \ty}\\ +\cline{1-2} +$\ty_1$ \ml{*} $\cdots$ \ml{*} $\ty_\n$ + & \ml{\lttbrace 1:}$\ty_1$\ml{,}\ $\cdots$ \ml{,}\ + $\overline{n}$\ml{:}$\ty_\n$\ml{\rttbrace} + & $(\n\geq 2)$ \\ +\cline{1-2} +\multicolumn{3}{c}{}\\ +\end{tabular} +\caption{Derived forms of Patterns and Type Expressions\index{67.2}} +\label{der-pat} +\end{figure} + +\begin{figure} + +\begin{tabular}{|l|l|} +\multicolumn{1}{c}{Derived Form} & \multicolumn{1}{c}{Equivalent Form}\\ +\multicolumn{2}{c}{}\\ +\multicolumn{2}{l}{{\bf Function-value Bindings} \fvalbind}\\ +%\multicolumn{2}{l}{FUNCTION-VALUE BINDINGS \fvalbind}\\ +\hline + & $\langle\OP\rangle$\var\ \ml{=} \FN\ \var$_1$\ml{=>} $\cdots$ + \FN\ \var$_n$\ml{=>} \\ + & \CASE\ + \ml{(}\var$_1$\ml{,} $\cdots$ \ml{,} \var$_n$\ml{)} \OF \\ +\ \ $\langle\OP\rangle\var\ \atpat_{11}\cdots\atpat_{1n} + \langle$\ml{:}\ty$\rangle$ + \ml{=} \exp$_1$ + & \ \ \ml{(}\atpat$_{11}$\ml{,}$\cdots$\ml{,}\atpat$_{1n}$ + \ml{)=>}\exp$_1\langle$\ml{:}\ty$\rangle$\\ +\ml{|}$\langle\OP\rangle\var\ \atpat_{21}\cdots\atpat_{2n} + \langle$\ml{:}\ty$\rangle$ + \ml{=} \exp$_2$ + & \ml{|(}\atpat$_{21}$\ml{,}$\cdots$\ml{,}\atpat$_{2n}$ + \ml{)=>}\exp$_2\langle$\ml{:}\ty$\rangle$\\ +\ml{|}\qquad$\cdots\qquad\cdots$ + & \ml{|}\qquad$\cdots\qquad\cdots$\\ +\ml{|}$\langle\OP\rangle\var\ \atpat_{m1}\cdots\atpat_{mn} + \langle$\ml{:}\ty$\rangle$ + \ml{=} \exp$_m$ + & \ml{|(}\atpat$_{m1}$\ml{,}$\cdots$\ml{,}\atpat$_{mn}$ + \ml{)=>}\exp$_m\langle$\ml{:}\ty$\rangle$\\ +\qquad\qquad\qquad$\langle\AND\ \fvalbind\rangle$ + & \qquad\qquad\qquad$\langle\AND\ \fvalbind\rangle$\\ +\hline +\multicolumn{2}{r}{($m,n\geq1$; $\var_1,\cdots,\var_n$ distinct and new)}\\ +\multicolumn{2}{c}{}\\ +\multicolumn{2}{l}{{\bf Declarations} \dec}\\ +%\multicolumn{2}{l}{DECLARATIONS \dec}\\ +\hline +\FUN\ \fvalbind + & \VAL\ \REC\ \fvalbind \\ +\hline +\DATATYPE\ \datbind\ \WITHTYPE\ \typbind + & \DATATYPE\ \datbind$\/'$\ \ml{;}\ \TYPE\ \typbind \\ +\hline +\ABSTYPE\ \datbind\ \WITHTYPE\ \typbind + & \ABSTYPE\ \datbind$\/'$ \\ +\qquad\qquad\WITH\ \dec\ \END + & \qquad\WITH\ \TYPE\ \typbind\ \ml{;}\ \dec\ \END\\ +\hline +\multicolumn{2}{r}{(see note in text concerning \datbind$\/'$)}\\ +\multicolumn{2}{c}{}\\ +\end{tabular} +\caption{Derived forms of Function-value Bindings and Declarations\index{68.1}} +\label{der-dec} +\end{figure} + +% Derived forms of functors: + +\begin{figure} +\begin{tabular}{|l|l|} +\multicolumn{1}{c}{Derived Form} & \multicolumn{1}{c}{Equivalent Form} \\ +\multicolumn{2}{c}{}\\ +\multicolumn{2}{l}{{\bf Structure Expressions} \strexp}\\ +%\multicolumn{2}{l}{STRUCTURE EXPRESSIONS \strexp}\\ +\cline{1-2} +\funappdec & \mbox{\funid\ \ml{(} \STRUCT\ \strdec\ \END\ \ml{)}}\\ +\cline{1-2} +\multicolumn{2}{c}{}\\ +%\multicolumn{2}{l}{FUNCTOR BINDINGS \funbind}\\ +\multicolumn{2}{l}{{\bf Functor Bindings} \funbind}\\ +\cline{1-2} +\mbox{\funid\ \ml{(}\ \spec\ \ml{)}\ $\langle$\ml{:}\ \sigexp$\rangle$\ \ml{=}}& +\mbox{\funid\ \ml{(}\ \strid\ \ml{:} \SIG\ \spec\ \END\ \ml{)} + $\langle$\ml{:}\ $\sigexp'\rangle$\ \ml{=}}\\ +\mbox{\ \ \strexp\ $\langle$\AND\ \funbind$\rangle$} & + \mbox{\ \ \LET\ \OPEN\ \strid\ \IN\ \strexp\ \END\ $\langle$\AND\ \funbind$\rangle$} \\ +\cline{1-2} +\multicolumn{2}{r}{($\strid$ new; see note in text concerning $\sigexp'$)}\\ +\multicolumn{2}{c}{}\\ +\multicolumn{2}{l}{{\bf Functor Signature Expressions} \funsigexp}\\ +%\multicolumn{2}{l}{FUNCTOR SIGNATURES \funsigexp}\\ +\cline{1-2} +\longfunsigexp & \mbox{\ml{(} \strid\ \ml{:}\ \SIG\ \spec\ \END\ \ml{)} + \ml{:}\ \sigexp$'$} \\ +\cline{1-2} +\multicolumn{2}{r}{($\strid$ new; see note in text concerning $\sigexp'$)}\\ +\multicolumn{2}{c}{}\\ +\multicolumn{2}{l}{{\bf Top-level Declarations} \topdec}\\ +\cline{1-2} +\exp & \VAL\ \ml{it =} \exp \\ +\cline{1-2} +\multicolumn{2}{c}{}\\ +\end{tabular} +\caption{Derived forms of Functors and Top-level Declarations\index{68.2}} +\label{functor-der-forms-fig} +\end{figure} + + + diff --git a/app2.tex b/app2.tex new file mode 100644 index 0000000..bfdda44 --- /dev/null +++ b/app2.tex @@ -0,0 +1,266 @@ +\section{Appendix: Full Grammar} +\label{core-gram-app} +%In\index{69.1} this Appendix, the full Core +%grammar is given for reference purposes. +The full grammar of programs is exactly as given at the start of +Section~\ref{prog-sec}. + +The\index{69.1} full grammar of Modules consists of the grammar of +Figures \ref{mod-phr}--\ref{prog-syn} in Section~\ref{syn-mod-sec}, +together with the derived forms of Figure~\ref{functor-der-forms-fig} +in Appendix~\ref{derived-forms-app}. + +The remainder of this Appendix is devoted to the full grammar of the +Core. +Roughly, it consists of the grammar of Section~\ref{syn-core-sec} augmented by +the derived forms of Appendix~\ref{derived-forms-app}. But there is a further +difference: two additional subclasses of the phrase class ~Exp~ are introduced, +namely ~AppExp~ (application expressions) and ~InfExp~ (infix expressions). +The inclusion relation among the four classes is as follows: +\[ {\rm AtExp}\ \subset\ {\rm AppExp}\ + \subset\ {\rm InfExp}\ \subset\ {\rm Exp} \] +The effect is that certain phrases, such as +``\ml{2 + while $\cdots$ do $\cdots$ }'', are now disallowed. + +The grammatical rules are displayed in Figures~\ref{exp-gram}, +\ref{dec-gram}, \ref{pat-gram} and \ref{typ-gram}. +The grammatical conventions are exactly as in +Section~\ref{syn-core-sec}, namely: +\begin{itemize} + \item The brackets ~$\langle\ \rangle$~ enclose optional phrases. + \item For\index{69.3} any syntax class X (over which $x$ ranges) +we define the syntax class Xseq (over which {\it xseq} ranges) as follows: + \begin{quote} + \begin{tabular}{rcll} + {\it xseq} & $::=$ & $x$ & (singleton sequence)\\ + & & & (empty sequence)\\ + & & \ml{(}$x_1$\ml{,}$\cdots$\ml{,}$x_n$\ml{)} + & (sequence,~$n\geq 1$) \\ + \end{tabular} + \end{quote} +(Note that the ``$\cdots$'' used here, a meta-symbol indicating syntactic +repetition, must not be +confused with ``$\wildrec$'' which is a reserved word of the language.) + \item Alternative\index{69.4} forms for each phrase class are in order of decreasing + precedence. This precedence resolves ambiguity in parsing in +the following way. Suppose that a phrase class --- we take $\exp$ as +an example --- has two alternative forms $F_1$ and $F_2$, such that $F_1$ ends +with an $\exp$ and $F_2$ starts with an $\exp$. A specific case is +\begin{tabbing} +\qquad\=$F_1$:\quad\=\IF\ $\exp_1$\ \THEN\ $\exp_2$\ \ELSE\ $\exp_3$\+\\ + $F_2$: \>\handlexp +\end{tabbing} +It will be enough to see how ambiguity is resolved in this specific case. + +Suppose that the lexical sequence +\[\cdots\ \cdots\ \IF\ \cdots\ \THEN\ \cdots\ \ELSE\ \exp\ \HANDLE\ \cdots\ \cdots\] +is to be parsed, where $\exp$ stands for a lexical sequence which +is already determined as a subphrase (if necessary by applying the +precedence rule). +Then the higher precedence of $F_2$ (in this case) dictates that $\exp$ +associates to the right, i.e. that the correct parse takes the form +\[\cdots\ \cdots\ \IF\ \cdots\ \THEN\ \cdots\ \ELSE\ (\exp\ \HANDLE\ \cdots)\ \cdots\] +not the form +\[\cdots\ (\cdots\ \IF\ \cdots\ \THEN\ \cdots\ \ELSE\ \exp)\ \HANDLE\ \cdots\ \cdots\] +Note particularly that the use of precedence does not decrease the class +of admissible phrases; it merely rejects alternative ways of parsing certain +phrases. In particular, the purpose is not to prevent a phrase, +which is an instance of a form with higher precedence, having a constituent +which is an instance of a form with lower precedence. Thus for example +\[\IF\ \cdots\ \THEN\ \WHILE\ \cdots\ \DO\ \cdots\ \ELSE\ \WHILE\ \cdots\ \DO\ \cdots\] +is quite admissible, and will be parsed as +\[\IF\ \cdots\ \THEN\ (\WHILE\ \cdots\ \DO\ \cdots)\ \ELSE\ (\WHILE\ \cdots\ \DO\ \cdots)\] + \item L (resp. R)\index{69.5} means left (resp. right) association. + +\item The syntax of types binds more tightly than that of expressions. + +\item Each\index{69.7} iterated construct (e.g. $\match$, $\cdots$ ) +extends as far +right as possible; thus, parentheses may be needed around an expression which +terminates with a match, e.g. ``$\FN\ \match$'', if this occurs within a +larger +match. +\end{itemize} + +\begin{figure}[h] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \atexp& ::= & \scon & special constant\cr + & & \opp\longvar & value variable\cr + & & \opp\longcon & value constructor\cr + & & \opp\longexn & exception constructor\cr + & & \verb+{ +\recexp\verb+ }+ & record\cr + & & \ml{\#}\ \lab & record selector\cr + & & \ml{()} & 0-tuple\cr + & & \ml{(}$\exp_1$ \ml{,} $\cdots$ \ml{,} $\exp_\n$\ml{)} + & $n$-tuple, $n\geq 2$\cr + & & \ml{[}$\exp_1$ \ml{,} $\cdots$ \ml{,} $\exp_\n$\ml{]} + & list, $n\geq 0$\cr + & & \ml{(}$\exp_1$ \ml{;} $\cdots$ \ml{;} $\exp_\n$\ml{)} + & sequence, $n\geq 2$\cr + & & \LET\ \dec\ \IN\ + $\exp_1$ \ml{;} $\cdots$ \ml{;} $\exp_\n$ \END + & local declaration, $n\geq 1$\cr + & & \parexp & \cr +\noalign{\vspace{6pt}} +\labexps& ::= & \longlabexps & expression row\cr +\noalign{\vspace{6pt}} + \apexp & ::= & \atexp & \cr + & & \apexp\ \atexp& application expression\cr +\noalign{\vspace{6pt}} +\inexp & ::= & \apexp & \cr + & & $\inexp_1$\ \id\ $\inexp_2$ + & infix expression\cr +\noalign{\vspace{6pt}} + \exp & ::= & \inexp & \cr + & & \typedexp & typed (L)\cr + & & $\exp_1$\ \ANDALSO\ $\exp_2$ + & conjunction\cr + & & $\exp_1$\ \ORELSE\ $\exp_2$ + & disjunction\cr + & & \handlexp & handle exception\cr + & & \raisexp & raise exception\cr + & & \IF\ $\exp_1$\ \THEN\ $\exp_2$\ \ELSE\ $\exp_3$ + & conditional\cr + & & \WHILE\ \exp$_1$\ \DO\ \exp$_2$ + & iteration\cr + & & \CASE\ \exp\ \OF\ \match + & case analysis\cr + & & \fnexp & function\cr +\noalign{\vspace{6pt}} +\match & ::= & \longmatch & \cr +\noalign{\vspace{6pt}} +\mrule & ::= & \longmrule & \cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Expressions and Matches\index{70}} +\label{exp-gram} +\end{figure} + +\begin{figure}[h] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \dec & ::= & \valdec & value declaration\cr + & & \FUN\ \fvalbind + & function declaration\cr + & & \typedec & type declaration\cr + & & \datatypedeca & datatype declaration\cr + & & \abstypedeca & abstype declaration\cr + & & \qquad\WITH\ \dec\ \END + & \cr + & & \exceptiondec & exception declaration\cr + & & \localdec & local declaration\cr + & & \openstrdec & open declaration, $n\geq 1$\cr + & & \emptydec & empty declaration\cr + & & \seqdec & sequential declaration\cr + & & \longinfix & infix (L) directive, $n\geq 1$\cr + & & \longinfixr & infix (R) directive, $n\geq 1$\cr + & & \longnonfix & nonfix directive, $n\geq 1$\cr +% & & \exp & expression (top-level only)\cr +\noalign{\vspace{6pt}} +\valbind& ::= & \longvalbind & \cr + & & \recvalbind & \cr +\noalign{\vspace{6pt}} +\fvalbind& ::= & \ \ $\langle\OP\rangle\var\ \atpat_{11}\cdots\atpat_{1n} + \langle$\ml{:}\ty$\rangle$\ml{=}\exp$_1$ & $m,n\geq 1$\cr + & & \ml{|}$\langle\OP\rangle\var\ \atpat_{21}\cdots\atpat_{2n} + \langle$\ml{:}\ty$\rangle$\ml{=}\exp$_2$ & See also note + below\cr + & & \ml{|}\qquad$\cdots\qquad\cdots$ &\cr + & & \ml{|}$\langle\OP\rangle\var\ \atpat_{m1}\cdots\atpat_{mn} + \langle$\ml{:}\ty$\rangle$\ml{=}\exp$_m$ &\cr + & & \qquad\qquad\qquad$\langle\AND\ \fvalbind\rangle$ &\cr +\noalign{\vspace{6pt}} +\typbind& ::= & \longtypbind & \cr +\noalign{\vspace{6pt}} +\datbind& ::= & \longdatbind & \cr +\noalign{\vspace{6pt}} +\constrs& ::= & \opp\longconstrs & \cr +\noalign{\vspace{6pt}} +\exnbind& ::= & \generativeexnbind & \cr + & & \eqexnbind & \cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +Note: In the $\fvalbind$ form, if $\var$ has infix status then either +~\OP~ must be present, or $\var$ must be infixed. Thus, at the start of +any clause, ``~\OP\ \var\ \ml{(}\atpat\ml{,}\atpat$'$\ml{)} $\cdots$'' may be +written +``\ml{(}\atpat\ \var\ \atpat$'$\ml{)} $\cdots$''; the parentheses may also be +dropped if ``\ml{:}\ty'' or ``\ml{=}'' follows immediately. +\caption{Grammar: Declarations and Bindings\index{71}} +\label{dec-gram} +\end{figure} + +\begin{figure}[h] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \atpat& ::= & \wildpat & wildcard\cr + & & \scon & special constant\cr + & & \opp\var & variable\cr + & & \opp\longcon & constant\cr + & & \opp\longexn & exception constant\cr + & & \verb+{ +\recpat\verb+ }+ & record\cr + & & \ml{()} & 0-tuple\cr + & & \ml{(}$\pat_1$ \ml{,} $\cdots$ \ml{,} $\pat_\n$\ml{)} + & $n$-tuple, $n\geq 2$\cr + & & \ml{[}$\pat_1$ \ml{,} $\cdots$ \ml{,} $\pat_\n$\ml{]} + & list, $n\geq 0$\cr + & & \parpat & \cr +\noalign{\vspace{6pt}} +\labpats& ::= & \wildrec & wildcard\cr + & & \longlabpats & pattern row\cr + & & \id$\langle$\ml{:}\ty$\rangle + \ \langle\AS\ \pat\rangle + \ \langle$\ml{,} \labpats$\rangle$ + & label as variable\cr +\noalign{\vspace{6pt}} + \pat & ::= & \atpat & atomic\cr + & & \opp\conpat & value construction\cr + & & \opp\exconpat & exception construction\cr + & & \infpat & infixed value construction\cr + & & \infexpat & infixed exception construction\cr + & & \typedpat & typed\cr + & & \opp\layeredpat & layered\cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Patterns\index{72.1}} +\label{pat-gram} +\end{figure} + +\begin{figure}[h] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \ty & ::= & \tyvar & type variable\cr + & & \verb+{ +\rectype\verb+ }+ & record type expression\cr + & & \constype & type construction\cr + & & $\ty_1$ \ml{*} $\cdots$ \ml{*} $\ty_\n$ + & tuple type, $\n\geq 2$ \cr + & & \funtype & function type expression\cr + & & \partype & \cr +\noalign{\vspace{6pt}} +\labtys & ::= & \longlabtys & type-expression row\cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Type expressions\index{72.2}} +\label{typ-gram} +\end{figure} diff --git a/app3.tex b/app3.tex new file mode 100644 index 0000000..45d6a5a --- /dev/null +++ b/app3.tex @@ -0,0 +1,208 @@ +%\appendix +\section{Appendix: The Initial Static Basis} +\label{init-stat-bas-app} +We\index{73.1} shall indicate components of the initial basis by the subscript 0. +The initial static basis is +\[ \B_0\ =\ (\M_0,\T_0),\F_0,\G_0,\E_0\] +where +\begin{itemize} +\item $\M_0\ =\ \emptyset$ +\item $\T_0\ =\ \{\BOOL,\INT,\REAL,\STRING,\LIST,\REF,\EXCN,\INSTREAM,\OUTSTREAM\}$ +\item $\F_0\ =\ \emptymap$ +\item $\G_0\ =\ \emptymap$ +\item $\E_0\ =\ \longE{0}$ +\end{itemize} +The members of $\T_0$ are type names, not type constructors; for convenience +we have used type-constructor identifiers +to stand also for the type names which are bound to them in the initial +static type environment $\TE_0$. Of these type names, +~\LIST~ and ~\REF~ +have arity 1, the rest have arity 0; all except \EXCN, \INSTREAM~ +and ~\OUTSTREAM~ admit equality. + +The components of $\E_0$ are as follows: +\begin{itemize} +\item $\SE_0\ =\ \emptymap$ +\item $\VE_0$ is shown in Figures~\ref{stat-ve} and \ref{stat-veio}. Note that + $\Dom\VE_0$ contains those identifiers ({\tt true},{\tt false},{\tt nil}, + \verb+::+) which are basic value constructors, + for reasons discussed in Section~\ref{stat-proj}. + $\VE_0$ also includes $\EE_0$, for the same reasons. +\item $\TE_0$ is shown in Figure~\ref{stat-te}. Note that the type + structures in $\TE_0$ contain the type schemes of all basic value + constructors. +\item $\Dom\EE_0\ =\ \BasExc$~, the set of basic exception names listed in +Section~\ref{bas-exc}. +In each case the associated type is ~\EXCN~, except that +~$\EE_0({\tt Io})=\STRING\rightarrow\EXCN$. +\end{itemize} + +\begin{figure} +\begin{tabular}{|rl|rl|} +\multicolumn{2}{c}{NONFIX}& \multicolumn{2}{c}{INFIX}\\ +\hline +$\var$ & $\mapsto\ \tych$ + & $\var$ & $\mapsto\ \tych$\\ +\hline +{\tt map} & $\mapsto\ \forall\atyvar\ \btyvar.\ (\atyvar\to\btyvar)\to$ + & \multicolumn{2}{l|}{Precedence 7 :} \\ + & \qquad$\atyvar\ \LIST\to\btyvar\ \LIST$ + & \verb+/+ & $\mapsto\ \REAL\ \ast\ \REAL + \to\REAL$\\ +{\tt rev} & $\mapsto\ \forall\atyvar.\ \atyvar\ \LIST\to\atyvar\ \LIST$ + & {\tt div} & $\mapsto\ \INT\ \ast\ \INT\to\INT$\\ +{\tt not} & $\mapsto\ \BOOL\to\BOOL$ + & {\tt mod} & $\mapsto\ \INT\ \ast\ \INT\to\INT$\\ +\verb+~+ & $\mapsto\ \NUM\to\NUM$ + & \verb+*+ & $\mapsto\ \NUM\ \ast\ \NUM\to\NUM$\\ +{\tt abs} & $\mapsto\ \NUM\to\NUM$ + & \multicolumn{2}{l|}{Precedence 6 :} \\ +{\tt floor}& $\mapsto\ \REAL\to\INT$ + & \verb-+- & $\mapsto\ \NUM\ \ast\ \NUM\to\NUM$\\ +{\tt real} & $\mapsto\ \INT\to\REAL$ + & \verb+-+ & $\mapsto\ \NUM\ \ast\ \NUM\to\NUM$\\ +{\tt sqrt} & $\mapsto\ \REAL\to\REAL$ + & \verb+^+ & $\mapsto\ \STRING\ \ast\ \STRING + \to\STRING$\\ +{\tt sin} & $\mapsto\ \REAL\to\REAL$ + & \multicolumn{2}{l|}{Precedence 5 :} \\ +{\tt cos} & $\mapsto\ \REAL\to\REAL$ + & \verb+::+ & $\mapsto\ \forall\atyvar. + \atyvar\;{\ast}\;\atyvar\;\LIST + \to\atyvar\;\LIST$\\ +{\tt arctan} + & $\mapsto\ \REAL\to\REAL$ + & \verb+@+ & $\mapsto\ \forall\atyvar.\ + \atyvar\ \LIST\ $\\ +{\tt exp} & $\mapsto\ \REAL\to\REAL$ + & & $\qquad\ast\ \atyvar\ \LIST\to + \atyvar\ \LIST$\\ +{\tt ln} & $\mapsto\ \REAL\to\REAL$ + & \multicolumn{2}{l|}{Precedence 4 :}\\ +{\tt size} & $\mapsto\ \STRING\to\INT$ + & \verb+=+ & $\mapsto\ \forall\aetyvar.\ + \aetyvar\ \ast\ \aetyvar\to\BOOL$\\ +{\tt chr} & $\mapsto\ \INT\to\STRING$ + & \verb+<>+ & $\mapsto\ \forall\aetyvar.\ + \aetyvar\ \ast\ \aetyvar\to\BOOL$\\ +{\tt ord} & $\mapsto\ \STRING\to\INT$ + & \verb+<+ & $\mapsto\ \NUM\ \ast\ \NUM + \to\BOOL$\\ +{\tt explode} + & $\mapsto\ \STRING\to\STRING\ \LIST$ + & \verb+>+ & $\mapsto\ \NUM\ \ast\ \NUM + \to\BOOL$\\ +{\tt implode} + & $\mapsto\ \STRING\ \LIST\to\STRING$ + & \verb+<=+ & $\mapsto\ \NUM\ \ast\ \NUM + \to\BOOL$\\ +\verb+!+ & $\mapsto\ \forall\atyvar.\ \atyvar\ \REF\to\atyvar$ + & \verb+>=+ & $\mapsto\ \NUM\ \ast\ \NUM + \to\BOOL$ \\ +\REF & $\mapsto\ \forall\ \aityvar\ .\ \aityvar\to\aityvar\ \REF$ + & \multicolumn{2}{l|}{Precedence 3 :} \\ +{\tt true} & $\mapsto\ \BOOL$ + & \verb+:=+ & $\mapsto\ \forall\atyvar.\ + \atyvar\ \REF\ \ast\ \atyvar\to\UNIT$\\ +{\tt false}& $\mapsto\ \BOOL$ + & {\tt o} & $\mapsto\ \forall\atyvar\ \btyvar\ + \ctyvar.\ (\btyvar\to\ctyvar)$\\ +{\tt nil} & $\mapsto\ \forall\atyvar.\ \atyvar\ \LIST$ + & & \qquad + $\ast\ (\atyvar\to\btyvar)\to(\atyvar\to\ctyvar) $ \\ +\hline +\end{tabular} +\vspace{3pt} + +Notes: +\begin{itemize} +\item In type schemes we have taken the liberty of writing +$\ty_1\ast\ty_2$ in place of +$\{\mbox{\tt 1}\mapsto\ty_1,\mbox{\tt 2}\mapsto\ty_2\}$. + +\item An identifier with type involving ~\NUM~ stands for two functions -- +one in which ~\NUM~ is replaced by ~\INT~ in its type, +and another in which ~\NUM~ is replaced by ~\REAL~ in its type. +Sometimes an explicit type constraint will be needed if the +surrounding text does not determine the type of a particular +occurrence of \verb-+- (for example). For this purpose, the +surrounding text is no larger than the enclosing top-level +declaration; an implementation may require that a smaller +context determines the type. +%In the case +%that both types can be inferred for an occurrence of the identifier, an +%explicit type constraint is needed to determine which type is intended. +%version 2: \item The type schemes associated with special +%constants are given in Figure~\ref{stat-te} which shows the initial +%static type environment. +\end{itemize} +\caption{Static $\VE_0$ (except for Input/Output and $\EE_0$)\index{74}} +\label{stat-ve} +\end{figure} + +\begin{figure} +\begin{center} +\begin{tabular}{|rl|} +\hline +$\var$ & $\mapsto\ \tych$\\ +\hline +{\tt std\_in} & $\mapsto\ \INSTREAM$\\ +{\tt open\_in} & $\mapsto\ \STRING\to\INSTREAM$\\ +{\tt input} & $\mapsto\ \INSTREAM\ \ast\ \INT\to\STRING$\\ +{\tt lookahead} & $\mapsto\ \INSTREAM\to\STRING$\\ +{\tt close\_in} & $\mapsto\ \INSTREAM\to\UNIT$\\ +{\tt end\_of\_stream} + & $\mapsto\ \INSTREAM\to\BOOL$\\ +\multicolumn{2}{|c|}{}\\ +{\tt std\_out} & $\mapsto\ \OUTSTREAM$\\ +{\tt open\_out} & $\mapsto\ \STRING\to\OUTSTREAM$\\ +{\tt output} & $\mapsto\ \OUTSTREAM\ \ast\ \STRING\to\UNIT$\\ +{\tt close\_out} & $\mapsto\ \OUTSTREAM\to\UNIT$\\ +\hline +\end{tabular} +\end{center} +\vspace{3pt} +\caption{Static $\VE_0$ (Input/Output)\index{75.1}} +\label{stat-veio} +\end{figure} + +\begin{figure} +\begin{center} +\begin{tabular}{|rll|} +\hline +$\tycon$ & $\mapsto\ \{\ \typefcn$, & $\{\con_1\mapsto\tych_1,\ldots,\con_n\mapsto\tych_n\}\ \}\quad (n\geq0)$\\ +\hline +\UNIT & $\mapsto\ \{\ \Lambda().\{ \}$, + & $\emptymap\ \}$ \\ +\BOOL & $\mapsto\ \{\ \BOOL$, & $\{\TRUE\mapsto\BOOL, + \ \FALSE\mapsto\BOOL\}\ \}$\\ +\INT & $\mapsto\ \{\ \INT$, & $\{\}\ \}$\\ +\REAL & $\mapsto\ \{\ \REAL$, & $\{\}\ \}$\\ +\STRING & $\mapsto\ \{\ \STRING$, & $\{\}\ \}$\\ +%version 2: \INT & $\mapsto\ \{\ \INT$, & $\{i\mapsto\INT\ ;\ +% i$ an integer constant$\}\ \}$\\ +%\REAL & $\mapsto\ \{\ \REAL$, & $\{r\mapsto\REAL\ ;\ +% r$ a real constant$\}\ \}$\\ +%\STRING & $\mapsto\ \{\ \STRING$, & $\{s\mapsto\STRING\ ;\ +% s$ a string constant$\}\ \}$\\ +\LIST & $\mapsto\ \{\ \LIST$, & $\{\NIL\mapsto\forall\atyvar\ .\ \atyvar\ \LIST$,\\ + & & $\ \mbox{\texttt+::+}\ \mapsto\forall\atyvar\ . + \ \atyvar\ast\atyvar\ \LIST + \to\atyvar\ \LIST\}\ \}$\\ +%\LIST & \multicolumn{2}{l|}{$\mapsto\ \{\ \LIST, \{\NIL\mapsto +% \forall\alpha.\alpha\LIST,\ +% \ml{::}\mapsto\forall\alpha. +% \alpha\ast\alpha\LIST +% \to\alpha\LIST\}\ \}$ +% }\\ +\REF & $\mapsto\ \{\ \REF$, & $\{\REF\mapsto\forall\ \aityvar\ .\ + \aityvar\to\aityvar\ \REF\}\ \}$\\ +\EXCN & $\mapsto\ \{\ \EXCN$, & $\emptymap\ \}$\\ +\INSTREAM & $\mapsto\ \{\ \INSTREAM$,& $\emptymap\ \}$ \\ +\OUTSTREAM & $\mapsto\ \{\ \OUTSTREAM$,& $\emptymap\ \}$ \\ +\hline +\end{tabular} +\end{center} +\caption{Static $\TE_0$\index{75.2}} +\label{stat-te} +\end{figure} diff --git a/app4.tex b/app4.tex new file mode 100644 index 0000000..37fd8ff --- /dev/null +++ b/app4.tex @@ -0,0 +1,222 @@ +\section{Appendix: The Initial Dynamic Basis} +\label{init-dyn-bas-app} +We\index{76.1} shall indicate components of the initial basis by the subscript 0. +The initial dynamic basis is +\[ \B_0\ =\ \F_0,\G_0,\E_0\] +where +\begin{itemize} +\item $\F_0\ =\ \emptymap$ +\item $\G_0\ =\ \emptymap$ +\item $\E_0\ =\ \E_0'+\E_0''$ +\end{itemize} +$\E_0'$ contains bindings of identifiers to the basic values BasVal and +basic exception names \BasExc; in fact +~$\E_0'\ =\ \SE_0',\VE_0',\EE_0'$~, where: +\begin{itemize} +\item $\SE_0'\ =\ \emptymap$ +\item $\VE_0'\ =\ \{\id\mapsto\id\ ;\ \id\in$ BasVal$\} + \cup\{$\verb+:=+ $\mapsto$ \verb+:=+$\}$ +\item $\EE_0'\ =\ \{\id\mapsto\id\ ;\ \id\in$ \BasExc$\}$ +\end{itemize} +Note that $\VE_0'$ is the identity function on BasVal; this is because +we have chosen to denote these values by the names of variables +to which they are initially bound. +The semantics of these basic values (most of which are functions) +lies principally in their behaviour under APPLY, which we describe below. +On the other hand the semantics of \verb+:=+ is provided by a special +semantic rule, rule~\ref{assapp-dyn-rule}. +Similarly, $\EE_0'$ is the identity function on \BasExc, the set of +basic exception names, because we have also chosen +these names to be just those exception constructors to which they +are initially bound. +These exceptions are raised by APPLY as described below. + + $\E_0''$ contains initial variable bindings which, unlike BasVal, are + definable in ML; it is the result of evaluating + the following declaration in the basis $\F_0,\G_0,\E_0'$. For convenience, + we have also included all basic infix directives in this declaration. + \begin{verbatim} + infix 3 o + infix 4 = <> < > <= >= + infix 5 @ + infixr 5 :: + infix 6 + - ^ + infix 7 div mod / * + + fun (F o G)x = F(G x) + + fun nil @ M = M + | (x::L) @ M = x::(L @ M) + + fun s ^ s' = implode((explode s) @ (explode s')) + + fun map F nil = nil + | map F (x::L) = (F x)::(map F L) + + fun rev nil = nil + | rev (x::L) = (rev L) @ [x] + + fun not true = false + | not false = true + + fun ! (ref x) = x + \end{verbatim} + +We now\index{77.1} describe the effect of APPLY upon each value +$b\in\BasVal$. For special values, we shall normally use $i$, $r$, +$n$, $s$ to range over integers, reals, numbers (integer or real), +strings respectively. We also take the liberty of abbreviating +``APPLY(\mbox{{\tt abs}}, $r$)'' to ``\mbox{{\tt abs}}($r$)'', +``APPLY({\tt mod}, $\{\verb+1+\mapsto i,\verb+2+\mapsto d\}$)'' to +``$i\ {\tt mod}\ d$'', etc. . +\begin{itemize} +\item \verb+~+($n$)~ returns the negation of $n$, or the + packet ~[{\tt Neg}]~ if the result is out of range. +\item \mbox{{\tt abs}}($n$)~ returns the absolute value of $n$, or + the packet ~[{\tt Abs}]~ if the result is out of range. +\item {\tt floor}($r$)~ returns the largest integer $i$ not greater than $r$; + it returns the packet ~[{\tt Floor}]~ if $i$ is out of range. +\item {\tt real}($i$)~ returns the real value equal to $i$. +\item {\tt sqrt}($r$)~ returns the square root of $r$, or the packet + ~[{\tt Sqrt}]~ if r is negative. +\item {\tt sin}($r$)~, {\tt cos}($r$)~ return the result of the appropriate + trigonometric functions. +\item {\tt arctan}($r$)~ returns the result of the appropriate + trigonometric function in the range $\underline{+}\pi/2$. +\item {\tt exp}($r$)~, {\tt ln}($r$)~ return respectively the exponential + and the natural logarithm of $r$, or an exception packet + ~[{\tt Exp}]~ or ~[{\tt Ln}]~ if the result is out of range. +\item {\tt size}($s$)~ returns the number of characters in $s$. +\item {\tt chr}($i$)~ returns the character numbered $i$ (see Section~\ref{cr:speccon}) if $i$ is in the interval $[0,255]$, and the packet + ~[{\tt Chr}]~ otherwise. +\item {\tt ord}($s$)~ returns\index{78.0} the number of the first character + in $s$ (an integer in the interval $[0,255]$, see Section~\ref{cr:speccon}), + or the packet ~[{\tt Ord}]~ if $s$ is empty. +\item {\tt explode}($s$)~ returns the list of characters (as single-character + strings) of which $s$ consists. +\item {\tt implode}($L$)~ returns the string formed by concatenating all members + of the list $L$ of strings. +\item The arithmetic\index{78.1} functions ~\verb+/+,\verb+*+,\verb-+-,\verb+-+~ all + return the results of the usual + arithmetic operations, or exception packets respectively + [{\tt Quot}], [{\tt Prod}], [{\tt Sum}], [{\tt Diff}] + if the result is undefined or out of range. +\item $i\ {\tt mod}\ d$~,~$i\ {\tt div}\ d$~ return integers $r,q$ + (remainder, quotient) determined by the equation $d\times q +r=i$, + where either $0\leq r+,\verb+<=+,\verb+>=+~ return + boolean values in accord with their usual meanings. +\item $v_1$\verb+ = +$v_2$~ returns {\TRUE} or {\FALSE} according as + the values $v_1$ and $v_2$ are, or are not, identical. + The type discipline (in particular, the fact that function types + do not admit equality) ensures that equality is only ever applied + to special values, nullary constructors, addresses, and values + built out of such by record formation and constructor application. +%version 2:\item $v_1$\verb+ = +$v_2$~ returns the boolean value of $v_1=v_2$, +% where the equality of values (=) is defined recursively as follows: +% \begin{itemize} +% \item If $v_1,v_2$ are constants (including nullary constructors) or +% addresses, then $v_1=v_2$ iff $v_1$ and $v_2$ are identical. +% \item $(\con_1,v_1)=(\con_2,v_2)$ iff $\con_1,\con_2$ are identical and +% $v_1=v_2$. +% \item $r_1=r_2$ (for records $r_1,r_2$) iff $\Dom r_1=\Dom r_2$ and, for +% each $\lab\in\Dom r_1$, $r_1(\lab)=r_2(\lab)$. +% \end{itemize} +% The type discipline (in particular, the fact that function types +% do not admit equality) makes it unnecessary to specify equality in +% any other cases. +\item $v_1$\verb+ <> +$v_2$ returns the opposite boolean value to + $v_1$\verb+ = +$v_2$. +\end{itemize} +It remains to define the effect of APPLY upon basic values concerned with +input/output; we therefore proceed to describe the ML input/output system. + +Input/Output in ML uses the concept of a {\sl stream}. A stream is a finite or +infinite sequence of characters; if finite, it may or may not be terminated. +(It may be convenient to think of a special end-of-stream character +signifying termination, provided one realises that this ``character'' is +never treated as data). +Input streams -- or {\sl instreams} -- +are of type ~\INSTREAM~ and will be denoted by ~$is$~; +output streams -- or {\sl outstreams} -- are of type ~\OUTSTREAM~ and will +be denoted by ~$os$~. Both these types of stream are {\sl abstract}, in the +sense that streams may only be manipulated by the functions provided in +BasVal. + +Associated with an instream is a {\sl producer}, normally an I/O device or +file; similarly an outstream is associated with a {\sl consumer}. After this +association has been established -- either initially or by the ~{\tt open\_in}~ +or ~{\tt open\_out}~ function -- the stream acts as a vehicle for character +transmission from producer to program, or from program to consumer. +The association can be broken by the ~{\tt close\_in}~ or ~{\tt close\_out}~ +function.\index{79.1} +A closed stream permits no further character transmission; a closed +instream is equivalent to one which is empty and terminated. + +There\index{79.1.1} are two streams in BasVal: +\begin{itemize} +\item {\tt std\_in}: an instream whose producer is the terminal. +\item {\tt std\_out}: an outstream whose consumer is the terminal. +\end{itemize} +The other basic values concerned with Input/Output are all functional, and +the effect of APPLY upon each of them given below. We take the +liberty of abbreviating ``APPLY({\tt open\_in}, $s$)'' to +``{\tt open\_in}($s$)'' +etc., and +we shall use ~$s$~ and ~$n$~ to range over strings and integers +respectively. +\begin{itemize} +\item {\tt open\_in}($s$)~ returns a new instream ~$is$~, whose producer is + the external file named ~$s$~. It returns exception packet + \begin{quote} + [$(${\tt Io},\verb+"Cannot open +$s$\verb+"+$)$] + \end{quote} + if file ~$s$~ does not exist or does not provide read access. +\item {\tt open\_out}($s$)~ returns a new outstream ~$os$~, whose consumer is + the + external file named ~$s$~. If file $s$ is non-existent, it is taken to + be initially empty. +\item {\tt input}($is,n$)~ returns a string ~$s$~ containing the first $n$ + characters of ~$is$~, also removing them from ~$is$~. If only $k < > <= >= + std_in std_out open_in open_out close_in close_out + input output lookahead end_of_stream +\end{verbatim} +The meaning of basic values (almost all of which are functions) is +represented by the function +\[ \APPLY\ :\ \BasVal\times\Val\to\Val\cup\Pack \] + which is detailed in Appendix~\ref{init-dyn-bas-app}. + +\subsection{Basic Exceptions} +\label{bas-exc} +A\index{49.2} subset $\BasExc\subset\Exc$ of the exception names are bound to predefined +exception constructors. +These names are denoted by the identifiers to which they are bound in the +initial dynamic basis (see Appendix~\ref{init-dyn-bas-app}), +and are as follows: +\begin{verbatim} + Abs Ord Chr Div Mod Quot Prod + Neg Sum Diff Floor Sqrt Exp Ln + Io Match Bind Interrupt +\end{verbatim} +The exceptions on the first two lines are raised by +corresponding basic functions, where \verb+~+ {\tt /} {\tt *} +{\tt +} {\tt -} correspond respectively to {\tt Neg} {\tt Quot} +{\tt Prod} {\tt Sum} {\tt Diff}. The details are given +in Appendix~\ref{init-dyn-bas-app}. The exception $(\mbox{{\tt Io}},s)$, +where $s$ is a string, is raised +by certain of the basic input/output functions, +as detailed in Appendix~\ref{init-dyn-bas-app}. +The exceptions ~\ml{Match}~ and +~\ml{Bind}~ +are raised upon failure of pattern-matching in evaluating a +function {\fnexp} or a +$\valbind$, as detailed in the rules to follow. Finally, ~\ml{Interrupt}~ +is raised by external intervention. + +Recall from Section~\ref{further-restrictions-sec} +that in the context {\fnexp}, the $\match$ +must be irredundant and exhaustive and that the compiler should flag +the {\match} if it violates these restrictions. The exception~\ml{Match} +can only be raised for a match which is not exhaustive, and has therefore +been flagged by the compiler. + +%In a match of the form $\pat_1\ \ml{=>}\ \exp_1\ \ml{|}\ \ldots\ \ml{|}\ +% \pat_n\ \ml{=>}\ \exp_n$ +%the pattern sequence $\pat_1,\ldots,\pat_n$ should be {\sl irredundant}; +%that is, each $\pat_j$ must match some value +%(of the right type) which is not matched by $\pat_i$ for any $i+, 3 +\subitem in a match rule, 8, 71 +\item \verb+->+, 3, 9, 29, 73 +\item \verb+~+, 3, 4, 48, 75, 78 +\item \verb+.+ (period) +\subitem in real constants, 3 +\subitem in long identifiers, 4 +\item \verb+"+, 3 +\item \verb+\+, 3, 4 +\item \verb+!+, 4, 75, 78 +\item \verb+%+, 4 +\item \verb+&+, 4 +\item \verb+$+, 4 +\item \verb+#+, 3, 4, 67, 71 +\item \verb(+(, 4, 48, 75, 77, 79 +\item \verb+-+, 4, 48, 75, 77, 79 +\item \verb+/+, 4, 48, 75, 77, 79 +\item \verb+:+ (see also type constraint), 4 +\item \verb+::+, 74--77 +\item \verb+:=+ (assignment), 47, 51, 75, 77 +\item \verb+<+, 4, 48, 75, 77, 79 +\item \verb+>+, 4, 48, 75, 77, 79 +\item \verb+<=+, 48, 75, 77, 79 +\item \verb+>=+, 48, 75, 77, 79 +\item \verb+<>+, 48, 75, 77, 79 +\item \verb+?+, 4 +\item \verb+@+, 4, 75, 77 +\item \verb+'+, 4 +\item \verb+^+, 3, 4, 75, 77 +\item \verb+*+, 4, 48, 67, 73, 75, 77, 79 +\item $\emptymap$ (empty map), 17 +\item $+$ (modification), 17, 18, 50 +\item $\oplus$, 18, 31 +\item $\Lambda$ (in type function), 17, 19, 27 +\item $\forall$ (in type scheme), 17, 19 +\subitem see also generalisation +\item $\alpha$ (see type variable) +\item $\varrho$ (see record type) +\item $\tau$ (see type) +\item $\tauk$ (type vector), 17, 19 +\item $\tych$ (type scheme), 17, 19, 21, 23, 27, 34, 42, 75, 76 +\item $\longtych$ (see type scheme) +\item $\rightarrow$ (function type), 17, 24, 29 +\item $\downarrow$ (restriction), 58 +\item $\typefcn$ (see type function) +\item $(\theta,\CE)$ (see type structure) +\item $\typefcnk$ (see type function) +\item $\sig$ (see signature) +\item $\longsig{}$ (see signature) +\item $\funsig$ (see functor signature) +\item $\longfunsig{}$ (see functor signature) +\item $\tyrea$ (type realisation), 33 +\item $\strrea$ (structure realisation), 33 +\item $\rea$ (realisation), 33, 35, 45 +\item $\geq$ (see instance) +\item $\succ$ (see generalisation and enrichment) +\item $\ts$ (turnstile), 2, 23, 24, 37, 49, 58, 63 +\item $\tsdyn$ (evaluation), 63 +\item $\tsstat$ (elaboration), 63 +\item $\ra$, 2, 23, 37, 49, 58, 63 +\item $\langle\ \rangle$ (see options) +\item $\langle'\rangle$, 39 +\indexspace +\parbox{65mm}{\hfil{\large\bf A}\hfil} +\indexspace +\item $a$ (see address) +\item $\Abs$ (abstype operation), 22, 25 +\item {\tt abs}, 48, 75, 78 +\item {\tt Abs}, 48, 78 +\item $\ABSTYPE$, 3, 8, 22, 25, 68, 72 +\item abstype declaration, 8, 22, 25, 72 +\item addition of numbers (\ml{+}), 4, 48, 75, 77, 79 +\item $\Addr$ (addresses), 46, 47 +\item address ($\A$), 46 +\subitem fresh, 51 +\item admissibility, 33, 35 +\item admit equality, 18, 19, 21, 22, 26, 33, 36, 40, 41, 74, 79 +\item $\AND$, 3, 12--14, 72 +\item \ANDALSO, 3, 67, 71 +\item appending lists (\verb+@+), 4, 75, 77 +\item $\apexp$ (application expression), 69, 71 +\item application, 8, 24 +\subitem of basic value ($\APPLY$), 48, 52, 78 +\subitem of (function) closure, 52 +\subitem of value constructor, 51 +\subitem of exception name, 51 +\subitem of {\tt ref}, 51 +\subitem of {\tt :=}, 51, 75 +\subitem infixed, 8 +\item application of functor (see functor application) +\item application of type function, 19, 29 +\item application expression, 69, 71 +\item applicative type variable (see type variable) +\item $\APPLY$ (see application) +\item $\AppTyVar$ (applicative type variables), 4 +\item $\apptyvars$ (free applicative type variables), 17 +\item {\tt arctan}, 48, 75, 78 +\item arity +\subitem of type name, 16 +\subitem of type function, 19, 41 +\item arrow type (see function type expression) +\item \AS, 3, 9, 29, 56, 73 +\item assignment (\ml{:=}), 47, 51, 75, 77 +\item $\atexp$ (atomic expression), 7, 8, 23, 50, 67, 71 +\item atomic expression, 7, 8, 23, 50, 67, 71 +\subitem as expression, 8, 24, 51 +\item atomic pattern, 7, 9, 28, 54, 67, 73 +\subitem as pattern, 9, 29, 55, 73 +\item $\atpat$ (atomic pattern), 7, 9, 28, 54, 67, 73 +\indexspace +\parbox{65mm}{\hfil{\large\bf B}\hfil} +\indexspace +\item $b$ (see basic value) +\item $\B$ (see basis) +\item $\B_0$ (initial basis) +\subitem static, 74 +\subitem dynamic, 77 +\item bare language, 1 +\item $\BasExc$ (basic exception names), 48, 77 +\item basic value ($b$), 46--48, 77--80 +\item basis ($\B$), 1 +\subitem static, 23, 31, 37, 63, 74 +\subitem dynamic, 57, 63, 77 +\subitem combined, 63 +\item $\Basis$ (bases), 31, 57, 63 +\item $\BasVal$ (basic values), 46--48, 77--80 +\item $\Bdyn$ (dynamic basis), 63 +\item {\tt Bind} (exception), 48, 54 +\item $\BOOL$, 74, 76 +\item bound names, 31--33 +\item $\Bstat$ (static basis), 63 +\indexspace +\parbox{65mm}{\hfil{\large\bf C}\hfil} +\indexspace +\item $\C$ (context), 17, 18, 23--30 +\item ``{\tt Cannot open} $s$'', 80 +\item \CASE, 3, 67, 71 +\item $\CE$ (constructor environment), 17, 21, 22, 27, 43 +\item {\tt chr}, 48, 75, 78 +\item {\tt Chr}, 48, 78 +\item $\cl{}{}$ (closure of types etc.), 21, 25, 27, 40, 42 +\item \verb+close_in+, 48, 76, 79, 80 +\item \verb+close_out+, 48, 76, 80 +\item $\Closure$ (function closures), 47 +\subitem recursion, 49 +\item closure rules (signatures and functors), 14, 40, 43, 44 +\item coercion of numbers (\ml{real}), 48, 75, 78 +\item comments, 4, 5 +\item composition of functions (\ml{o}), 75, 77 +\item $\con$ (see value constructor) +\item $\Con$ (value constructors), 4, 47 +\item $\constrs$ (constructor binding), 7, 8, 27, 72 +\item $\ConBind$ (constructor bindings), 7, 46 +\item concatenating strings (\verb+^+), 4, 75, 77 +\item $\condesc$ (constructor description), 11--13, 42, 57 +\item ConDesc (constructor descriptions), 11, 57 +\item $\ConEnv$ (constructor environments), 17 +\item ``consing'' an element to a list (\ml{::}), 74--77 +\item consistency +\subitem of type structures, 32, 43 +\subitem of semantic object, 32, 33, 42 +\item constant (see also value constant and exception constant) +\subitem special (see special constant) +\item construction (see value construction and exception construction) +\item constructor binding ($\constrs$), 7, 8, 27, 72 +\item constructor description, 11--13, 42, 57 +\item constructor environment ($\CE$), 17, 21, 22, 27, 43 +\item $\ConsType$ (constructed types), 17 +\item contents of (see dereferencing) +\item context ($\C$), 17, 18, 23--30 +\item $\Context$ (contexts), 17 +\item control character, 3 +\item Core Language, 1 +\subitem syntax, 3 +\subitem static semantics, 16 +\subitem dynamic semantics, 46 +\item Core Language Programs, 64 +\item {\tt cos}, 48, 75, 78 +\item cover, 35 +\item cycle-freedom, 32, 33 +\indexspace +\parbox{65mm}{\hfil{\large\bf D}\hfil} +\indexspace +\item \DATATYPE, 3, 8, 13, 25, 40, 57, 68, 72 +\item datatype binding, 7, 8, 27, 72 +\item datatype declaration, 8, 25, 72 +\item datatype description, 11, 13, 42 +\item datatype specification, 13, 40, 57 +\item $\datbind$ (datatype binding), 7, 8, 27, 72 +\item DatBind (datatype bindings), 7, 46 +\item $\datdesc$ (datatype description), 11, 13, 42 +\item DatDesc (datatype descriptions), 11, 57 +\item $\dec$ (declaration), 7, 8, 25, 53, 68, 72 +\item Dec (declarations), 7 +\item declaration (Core), 7, 8, 25, 53, 68, 72 +\subitem as structure-level declaration, 12, 38, 59 +\item dereferencing (\ml{!}), 4, 75, 78 +\item derived forms, 1, 6, 10, 66--68 +\item {\tt Diff}, 48, 79 +\item digit +\subitem in identifier, 4 +\subitem in integers and reals, 3 +\item $\dir$ (fixity directive), 6, 8, 10 +\item directive, 8 +\item {\tt div}, 48, 75, 77, 79 +\item {\tt Div}, 48, 79 +\item division of reals (\ml{/}), 48, 75, 77, 79 +\item \DO, 3, 67, 71 +\item $\Dom$ (domain), 17 +\item dynamic +\subitem semantics (Core), 46 +\subitem semantics (Modules), 57 +\subitem basis (see basis) +\indexspace +\parbox{65mm}{\hfil{\large\bf E}\hfil} +\indexspace +\item $\exval$ (exception value), 47 +\item $[\exval]$ (see packet) +\item \verb+E+\ (exponent), 3 +\item $\E$ (environment) +\subitem static, 17, 22, 23, 25, 26 +\subitem dynamic, 47, 50--56, 58, 59 +\item $\EE$ (see exception constructor environment) +\item elaboration, 1, 2, 23, 37, 63 +\item \ELSE, 3, 67, 71 +\item empty +\subitem declaration (Core), 8, 26, 53, 72 +\subitem functor declaration, 14, 43, 62 +\subitem functor specification, 14, 43 +\subitem signature declaration, 12, 40, 60 +\subitem specification, 13, 41, 61 +\subitem structure-level declaration, 12, 38, 59 +\item $\e$ (exception name), 46, 54 +\item \END, 3, 8, 12, 13, 71, 72 +\item \verb+end_of_stream+, 48, 76, 80 +\item enrichment ($\succ$), 30, 34, 37, 39, 44 +\item $\excs$ (exception name set), 47, 54 +\item $\Env$ (environments), 17, 47 +\item \EQTYPE, 10, 13, 40, 57 +\item equality +\subitem admit equality, 18, 19, 21, 22, 26, 33, 36, 40, 41, 74, 79 +\subitem maximise equality, 21, 25 +\subitem on abstract types, 21, 22 +\subitem of structures (sharing), 42 +\subitem of type functions (sharing), 19, 42, 43 +\subitem of type schemes, 19 +\subitem of values, 18, 75, 77, 79 +\subitem -principal, 36, 39, 40, 43, 44 +\subitem respect equality, 21, 26, 35, 36 +\item equality attribute +\subitem of type name, 16, 19, 21, 22, 33, 36, 40 +\subitem of type variable, 4, 16, 18, 19 +\item equality type, 18, 19, 75 +\item equality type function, 19 +\item equality type specification, 13, 40, 57 +\item equality type variable, 4, 16, 18, 19 +\item escape sequence, 3 +\item evaluation, 1, 2, 49, 58, 63 +\item $\exnbind$ (exception binding), 7, 8, 27, 54, 72 +\item ExBind (exception bindings), 7 +\item \EXCEPTION, 3, 8, 13, 25, 40, 53, 60, 72 +\item exception binding, 7, 8, 27, 54, 72 +\item exception constant ($\exn$ or $\longexn$) +\subitem as atomic pattern, 9, 28, 54, 55, 73 +\item exception construction +\subitem as pattern, 9, 29, 55, 73 +\subitem infixed, as pattern, 6, 9, 73 +\item exception constructor +\subitem as atomic expression, 8, 23, 51, 71 +\item exception constructor environment ($\EE$) +\subitem static, 17, 18, 27, 58 +\subitem dynamic, 47, 54, 58 +\item exception convention, 50--52, 64 +\item exception declaration, 8, 25, 53, 72 +\item exception description, 11, 13, 42, 61 +\item exception name ($\e$), 46 +\subitem fresh, 54 +\item exception name set ($\excs$), 47, 54 +\item exception packet (see packet) +\item exception specification, 13, 40, 60 +\item exception value ($\exval$), 47 +\item $\exn$ (see exception constant or constructor) +\item $\Exn$ (exception constructors), 4 +\item $\ExnEnv$ (exception constructor environments), 17, 47 +\item $\exns$ (exeption constructor set), 57, 61 +\item $\exndesc$ (exception description), 11, 13, 42, 61 +\item ExDesc (exception descriptions), 11 +\item execution, 1, 63 +\item exhaustive patterns, 30, 48 +\item $\EXCN$, 24, 28, 29, 42, 74, 76 +\item $\Exc$ (exception names), 46 +\item $\ExcSet$ (exception name sets), 47 +\item $\exp$ (expression), 7, 8, 24, 51, 67, 71 +\item Exp (expressions), 7 +\item {\tt exp} (exponential), 48, 75, 78 +\item {\tt Exp}, 48, 78 +\item expansive expression, 20, 21 +\item {\tt explode} (a string), 48, 75, 79 +\item expression, 7, 8, 24, 51, 67, 71 +\item expression row, 7, 8, 24, 51, 71 +\item $\labexps$ (expression row), 7, 8, 24, 51, 71 +\item ExpRow (expression rows), 7 +\item $\ExVal$ (exception values), 47 +\indexspace +\parbox{65mm}{\hfil{\large\bf F}\hfil} +\indexspace +\item $\F$ (functor environment), 31, 43, 44, 57, 61, 62 +\item $\FAIL$ (failure in pattern matching), 46, 50--56 +\item \FALSE, 74--76 +\item $\finfun{}{}$ (finite map), 16 +\item $\Fin$ (finite subset), 16 +\item {\tt floor}, 48, 75, 78 +\item {\tt Floor}, 48, 78 +\item \FN, 3, 8, 9, 24, 52, 71 +\item formatting character, 3 +\item \FUN, 3, 66, 68, 72 +\item $\funbind$ (functor binding), 11, 14, 44, 61, 66, 68 +\item FunBind (functor bindings), 11 +\item function ($\fnexp$), 8, 24, 52, 71 +\item function declaration (see $\FUN$) +\item function type ($\rightarrow$), 17, 24, 29 +\item function type expression (\verb+->+), 9, 29, 73 +\item function-value binding ($\fvalbind$), 30, 66, 68, 72 +\item \FUNCTOR, 10, 14, 43, 62 +\item functor application, 12, 37, 59, 68 +\item functor binding, 11, 14, 44, 61, 66, 68 +\item functor closure, 57, 59, 61 +\item functor declaration, 11, 14, 43, 62 +\subitem as top-level declaration, 14, 44, 62 +\item functor description, 11, 14, 43 +\item functor environment ($\F$), 31, 43, 44, 57, 61, 62 +\item functor identifier ($\funid$), 10, 12, 14 +\item functor signature ($\funsig$), 31, 43--45 +\item functor signature expression, 11, 14, 43, 68 +\item functor signature matching, 11, 45 +\item functor specification, 11, 14, 43 +\item $\FunctorClosure$ (functor closures), 57 +\item $\fundec$ (functor declaration), 11, 14, 43, 62 +\item FunDec (functor declarations), 11 +\item $\fundesc$ (functor description), 11, 14, 43 +\item FunDesc (functor descriptions), 11 +\item $\FunEnv$ (functor environments), 31, 57 +\item $\funid$ (functor identifier), 10, 12, 14 +\item $\FunId$ (functor identifiers), 10 +\item $\funsigexp$ (functor signature expression), 11, 14, 43, 68 +\item FunSigExp (functor signature expressions), 11 +\item $\funspec$ (functor specification), 11, 14, 43 +\item FunSpec (functor specifications), 11 +\item $\FunType$ (function types), 17 +\item $\fvalbind$ (function-value binding), 66, 68, 72 +\subitem exhaustive, 30 +\indexspace +\indexspace +\indexspace +\parbox{65mm}{\hfil{\large\bf G}\hfil} +\indexspace +\item $\G$ (signature environment), 31, 40, 57, 60 +\item generalisation ($\succ$), 19, 23, 28--30, 34 +\item generative signature expression, 12, 39, 60 +\item generative structure expression, 12, 37, 59 +\item grammar, 1 +\subitem for the Core, 6, 69 +\subitem for Modules, 10 +\indexspace +\parbox{65mm}{\hfil{\large\bf H}\hfil} +\indexspace +\item \HANDLE, 3, 8, 24, 52, 71 +\indexspace +\parbox{65mm}{\hfil{\large\bf I}\hfil} +\indexspace +\item $\I$ (interface), 57, 60, 61 +\item $\IB$ (interface basis), 57, 58, 60, 61 +\item identifier ($\id$), 4, 10 +\subitem alphanumeric, 4 +\subitem long, 4, 65 +\subitem qualified, 4 +\subitem symbolic, 4 +\item $\IE$ (interface environment), 57, 61 +\item \IF, 3, 67, 71 +\item imperative attribute, 16, 19 +\item imperative type, 19, 27 +\item imperative type variable (see type variable) +\item implementation, 1, 63 +\item {\tt implode} (a string list), 48, 75, 79 +\item $\ImpTyVar$ (imperative type variables), 4 +\item $\imptyvars$ (free imperative type variables), 17, 44 +\item $\In$ (injection), 18 +\item \IN, 3, 8, 12, 13, 67, 71, 72 +\item \INCLUDE, 10, 13, 41, 61 +\item inference, 2 +\item inference rules +\subitem static semantics (Core), 23 +\subitem static semantics (Modules), 37 +\subitem dynamic semantics (Core), 49 +\subitem dynamic semantics (Modules), 58 +\item $\inexp$ (infix expression), 69, 71 +\item InfExp (infix expressions), 69, 71 +\item \INFIX, 3, 5, 6, 8, 72 +\item infix expression, 6, 8, 69, 71 +\item infix pattern, 6, 9, 73 +\item infixed identifiers, 5, 6, 8, 10, 71--73, 75 +\item \INFIXR, 3, 5, 6, 8, 72 +\item initial basis, 2, 74, 77 +\item injection (\In), 18 +\item {\tt input}, 48, 76, 80 +\item input/output, 76, 79 +\item instance ($\geq$) +\subitem of signature, 34, 35, 39, 41 +\subitem of functor signature, 34, 37 +\subitem in matching, 35 +\item $\INSTREAM$, 74, 76, 79 +\item $\INT$, 74, 76 +\item $\Int$ (interfaces), 57 +\item $\IntBasis$ (interface bases), 57 +\item integer constant, 3, 76 +\item $\IntEnv$ (interface environments), 57 +\item $\Inter$, 57, 60, 61 +\item interaction, 1, 63 +\item interface ($\I$), 57, 60, 61 +\item interface basis ($\IB$), 57, 58, 60, 61 +\item interface environment ($\IE$), 57, 61 +\item {\tt Interrupt}, 48, 64 +\item {\tt Io}, 48, 80 +\item irredundant patterns, 30, 48 +\item {\tt it}, 68 +\indexspace +\parbox{65mm}{\hfil{\large\bf L}\hfil} +\indexspace +\item L (left associative), 7, 70 +\item $\lab$ (label), 4, 5 +\item $\Lab$ (labels), 4, 5 +\item \LET, 3 +\subitem expression (Core), 8, 24, 51, 67, 71 +\subitem expression (Modules), 12, 37, 59 +\item letter in identifer, 4 +\item lexical analysis, 5, 6 +\item $\LIST$, 74, 76 +\item list reversal (\ml{rev}), 75, 78 +\item {\tt ln}, 48, 75, 78 +\item {\tt Ln}, 48, 78 +\item \LOCAL, 3 +\subitem declaration (Core), 8, 26, 53, 72 +\subitem declaration (Modules), 12, 38, 59 +\subitem specification (Modules), 13, 41, 61 +\item long identifiers (e.g. $\longexn$), 4, 65 +\item {\tt lookahead}, 48, 76, 80 +\indexspace +\parbox{65mm}{\hfil{\large\bf M}\hfil} +\indexspace +\item $\m$ (structure name), 16--18, 31--34, 39, 42, 47 +\subitem fresh, 37, 38 +\item $\M$ (structure name set), 31, 37 +\item \ml{map}, 75, 78 +\item match ($\match$), 7, 8, 25, 53 +\subitem irredundant, 30, 48 +\subitem exhaustive, 30, 48 +\subitem in closure, 47, 49 +\item $\Match$, 7 +\item {\tt Match} (exception), 48, 52 +\item match rule, 7, 8, 25, 53 +\item matching +\subitem signatures (see signature matching) +\subitem functor signatures (see functor signature matching) +\item maximise equality, 21, 25 +\item $\mem$ (memory), 47, 51, 56 +\item $\Mem$ (memories), 47 +\item memory ($\mem$), 47, 51, 56 +\item {\tt mod}, 48, 75, 77, 79 +\item {\tt Mod}, 48, 79 +\item modification ($+$) +\subitem of finite maps, 17 +\subitem of environments, 18, 50 +\item module, 11 +\item Modules, 1 +\item $\mrule$ (match rule), 7, 8, 25, 53 +\item Mrule (match rules), 7 +\item multiplication of numbers (\ml{*}), 48, 75, 77, 79 +\indexspace +\parbox{65mm}{\hfil{\large\bf N}\hfil} +\indexspace +\item $\n$ (name, see structure name, type name and exception name) +\item $\N$ (name set), 31, 37 +\item $n$-tuple, 67, 71, 73 +\item name +\subitem of structure ($\m$), 16--18, 31--34, 37--39, 42, 47 +\item name set ($\N$), 31, 37 +\item $\NamesFcn$ (free names), 31, 32, 37, 44 +\item $\NameSets$ (name sets), 31 +\item Natural Semantics, 2 +\item {\tt Neg}, 48, 78 +\item negation of booleans (\ml{not}), 75, 78 +\item negation of numbers (\verb+~+), 3, 48, 75, 78 +\item \NIL, 67, 74--76 +\item non-expansive expression, 20, 21 +\item \NONFIX, 3, 6, 8, 10, 72, 75 +\item nonfix identifiers, 6, 8, 10, 72, 75 +\item \ml{not}, 75, 78 +\item \NUM, 75 +\indexspace +\parbox{65mm}{\hfil{\large\bf O}\hfil} +\indexspace +\item \ml{o} (function composition), 75, 77 +\item occurrence +\subitem substructure, 31 +\item $\of{}{}$ (projection), 18, 31 +\item $\OF$, 3 +\subitem in $\CASE$ expression, 67, 71 +\subitem in constructor binding, 8 +\subitem in exception binding, 8, 46 +\subitem in exception description, 13, 57 +\item \OP, 3, 6 +\subitem on variable or constructor, 8, 9, 71--73 +\subitem in constructor binding, 8, 72 +\item \OPEN, 3, 8, 13, 26, 41, 53, 57, 61, 65, 68, 72 +\item \verb+open_in+, 48, 76, 79, 80 +\item \verb+open_out+, 48, 76, 79, 80 +\item opening structures in declarations, 8, 26, 53, 72 +\item opening structures in specifications, 13, 14, 41, 61 +\item options, 7 +\subitem first ($\langle\ \rangle$), 23, 39 +\subitem second ($\langle\langle\ \rangle\rangle$), 23 +\item {\tt ord} (of string), 48, 75, 79 +\item {\tt Ord}, 48, 79 +\item \ORELSE, 3, 67, 71 +\item {\tt output}, 48, 76, 80 +\item ``{\tt Output stream is closed}'' , 80 +\item $\OUTSTREAM$, 74, 76, 79 +\indexspace +\parbox{65mm}{\hfil{\large\bf P}\hfil} +\indexspace +\item $\p$ (see packet) +\item $\Pack$ (packets), 47 +\item packet ($\p$), 47, 50, 52, 58, 63, 64 +\item parsing, 1, 63 +\item $\pat$ (pattern), 7, 9, 29, 55, 67, 73 +\item Pat (patterns), 7 +\item $\labpats$ (pattern row), 7, 9, 28, 55, 67, 73 +\item PatRow (pattern rows), 7 +\item pattern, 7, 9, 29, 55, 67, 73 +\subitem layered, 9, 29, 56, 73 +\item pattern matching, 30, 46, 48, 55 +\subitem with $\REF$, 55, 56 +\item pattern row, 7, 9, 28, 55, 67, 73 +\item polymorphic +\subitem functions, 23, 25, 28 +\subitem references, 20, 21, 25, 44, 75 +\subitem exceptions, 20, 27, 42, 44 +\item precedence, 7, 69 +\item principal +\subitem environment, 30, 38 +\subitem equality-, 36, 39, 40, 43, 44 +\subitem signature, 35, 36, 39, 40, 43, 44 +\item printable character, 3 +\item {\tt Prod}, 48, 79 +\item product type (\verb+*+), 67, 73 +\item program ($\program$), 1, 63, 64 +\item Program (programs), 63 +\item projection ($\of{}{}$), 18, 31 +\indexspace +\parbox{65mm}{\hfil{\large\bf Q}\hfil} +\indexspace +\item qualified identifier, 4 +\item {\tt Quot}, 48, 79 +\indexspace +\parbox{65mm}{\hfil{\large\bf R}\hfil} +\indexspace +\item $\r$ (record), 47, 51, 55 +\item R (right associative), 7, 70 +\item \RAISE, 3, 8, 24, 25, 50, 52, 63, 71 +\item $\Ran$ (range), 17 +\item $\REAL$ +\subitem the type, 74, 76 +\subitem coercion, 48, 75, 78 +\item real constant, 3, 76 +\item realisation ($\rea$), 33, 35, 45 +\item $\REC$, 3, 8, 9, 26, 49, 54, 72 +\item $\Rec$ (recursion operator), 49, 52, 54 +\item record +\subitem $\r$, 47, 51, 55 +\subitem as atomic expression, 8, 24, 51, 67, 71 +\subitem as atomic pattern, 9, 28, 55, 67, 73 +\subitem selector (\ml{\#}\ {\it lab}), 3, 67, 71 +\subitem type expression, 9, 29, 73 +\subitem type ($\varrho$), 17, 24, 28, 30 +\item Record (records), 47 +\item $\RecType$ (record types), 17 +\item recursion (see $\REC$, $\Rec$, and $\FUN$) +\item $\REF$ +\subitem the type constructor, 74, 76 +\subitem the type name, 19, 74--76 +\subitem the value constructor, 46, 51, 55, 56, 75, 76, 78 +\item reserved words, 3, 10 +\item respect equality (see equality) +\item restrictions +\subitem closure rules (see these) +\subitem syntactic (Core), 9, 30 +\subitem syntactic (Modules), 12 +\item \ml{rev}, 75, 78 +\indexspace +\parbox{65mm}{\hfil{\large\bf S}\hfil} +\indexspace +\item $\s$ (state), 47, 49, 51, 56, 58, 63, 64 +\item $\S$ (structure), 17, 31, 32, 34, 37, 39, 47 +\item {\SCon} (special constants), 3 +\item {\scon} (see special constant) +\item scope +\subitem of constructor, 5, 18 +\subitem of value variable, 5, 18 +\subitem of fixity directive, 6, 10 +\subitem of explicit type variable, 20, 26 +\item $\SE$ (structure environment) +\subitem static, 17, 18, 31, 34, 39, 42, 74 +\subitem dynamic, 47, 58, 60, 77 +\item semantic object, 2 +\subitem simple (Static), 16 +\subitem simple (Dynamic), 46 +\subitem compound (Core, Static), 16, 17 +\subitem compound (Core, Dynamic), 47 +\subitem compound (Modules, Static), 31 +\subitem compound (Modules, Dynamic), 57 +\item sentence, 2, 23, 37, 49, 58, 63 +\item separate compilation, 11, 14, 15, 45 +\item sequential +\subitem expression, 67, 71 +\subitem declaration (Core), 8, 26, 53, 72 +\subitem functor declarations, 14, 44, 62 +\subitem functor specification, 14, 43 +\subitem signature declaration, 12, 40, 60 +\subitem specification, 13, 41, 61 +\subitem structure-level declaration, 12, 38, 59 +\item $\shareq$ (sharing equation), 11, 13, 42, 57 +\item SharEq (sharing equations), 11, 57 +\item sharing, 14, 15, 38, 39, 41, 42, 45 +\subitem equations, 11, 13, 42, 57 +\subitem specification, 13, 41 +\subitem of structures, 13, 42 +\subitem of types, 13, 42, 43 +\subitem multiple, 13, 42 +\item \SHARING, 10, 13, 41 +\item side-condition, 49, 58 +\item side-effect, 58, 64 +\item \SIG, 10, 12, 39, 60 +\item $\Sig$ (signatures), 31 +\item $\sigbind$ (signature binding), 11, 12, 40, 60 +\item SigBind (signature bindings), 11 +\item $\sigdec$ (signature declaration), 11, 12, 40, 60 +\item SigDec (signature declarations), 11 +\item $\SigEnv$ (signature environments), 31, 57 +\item $\sigexp$ (signature expression), 11, 12, 39, 60 +\item SigExp (signature expressions), 11 +\item $\sigid$ (signature identifier), 10, 12, 39, 60 +\item $\SigId$ (signature identifiers), 10 +\item signature ($\sig$), 31--36, 39, 40, 43--45, 58 +\item \SIGNATURE, 10, 12, 40, 60 +\item signature binding, 11, 12, 40, 60 +\item signature declaration, 11, 12, 40, 60 +\subitem in top-level declaration, 14, 44, 62 +\item signature environment ($\G$) +\subitem static, 31, 40, 44 +\subitem dynamic, 57, 58, 60, 62 +\item signature expression, 11, 12, 39, 60 +\item signature identifier, 10, 12, 39, 60 +\item signature instantiation (see instance) +\item signature matching, 35, 37--39, 44 +\item {\tt sin}, 48, 75, 78 +\item {\tt size} (of strings), 48, 75, 78 +\item $\spec$ (specification), 11, 13, 40, 60 +\item Spec (specifications), 11 +\item special constant (\scon), 3, 16 +\subitem as atomic expression, 8, 23, 50, 71 +\subitem in pattern, 9, 28, 54, 73 +\item special value ($\sv$), 46 +\item specification, 11, 13, 40, 60 +\item {\tt sqrt} (square root), 48, 75, 78 +\item {\tt Sqrt}, 48, 78 +\item state ($\s$), 47, 49, 51, 56, 58, 63, 64 +\item $\State$, 47 +\item state convention, 50, 51 +\item static +\subitem basis, 1, 23, 31, 37, 63, 74 +\subitem semantics (Core), 16 +\subitem semantics (Modules), 31 +\item \verb+std_in+, 48, 76, 80 +\item \verb+std_out+, 48, 76, 80 +\item $\Str$ (structures), 17 +\item $\strbind$ (structure binding), 11, 12, 39, 60 +\item StrBind (structure bindings), 11 +\item $\strdec$ (structure-level declaration), 11, 12, 38, 59, 64 +\item StrDec (structure-level declarations), 11 +\item $\strdesc$ (structure description), 11, 13, 42, 61 +\item StrDesc (structure descriptions), 11 +\item stream (input/output), 79 +\item $\StrEnv$ (structure environments), 17, 47 +\item $\strexp$ (structure expression), 11, 12, 37, 59, 68 +\item $\StrExp$ (structure expressions), 11 +\item $\strid$ (structure identifier), 4 +\subitem as structure expression, 12, 37, 59 +\item $\StrId$ (structure identifiers), 4 +\item $\STRING$, 74, 76 +\item string constant, 3, 76 +\item $\StrNames$ (structure names), 16 +\item $\StrNamesFcn$ (free structure names), 31 +\item $\StrNameSets$ (structure name sets), 31 +\item $\STRUCT$, 10, 12, 37, 59, 68 +\item structure ($\S$ or $(\m,\E)$), 17, 31, 32, 34, 37, 39, 47 +\item $\STRUCTURE$, 10, 12, 13, 38, 40, 59, 61 +\item structure binding ($\strbind$), 11, 12, 39, 60 +\item structure declaration, 12, 38, 59 +\item structure description ($\strdesc$), 11, 13, 42, 61 +\item structure environment ($\SE$) +\subitem static, 17, 18, 31, 34, 39, 42, 74 +\subitem dynamic, 47, 58, 60, 77 +\item structure expression ($\strexp$), 11, 12, 37, 59, 68 +\item structure identifier ($\strid$), 4 +\subitem as structure expression, 12, 37, 59 +\item structure-level declaration ($\strdec$), 11, 12, 38, 59, 64 +\subitem in top-level declaration, 14, 44, 62, 64 +\item structure name ($\m$, see name) +\item structure name set ($\M$), 31, 37 +\item structure realisation ($\strrea$), 33 +\item structure specification, 13, 40, 61 +\item substructure, 31 +\subitem proper, 31, 32 +\item subtraction of numbers (\ml{-}), 48, 75, 77, 79 +\item {\tt Sum}, 48, 79 +\item {\SVal} (special values), 46 +\item $\Supp$ (support), 33 +\item $\sv$ (special value), 46 +\item symbol, 4 +\item syntax, 3, 10, 46, 57, 69 +\indexspace +\parbox{65mm}{\hfil{\large\bf T}\hfil} +\indexspace +\item $\t$ (type name), 16, 19, 21, 22, 25, 27, 30--34, 42, 76 +\item $\T$ (type name set), 17, 31 +\item $\TE$ (type environment), 17, 21, 22, 27, 34, 42, 58 +\item \THEN, 3, 67, 71 +\item $\topdec$ (top-level declaration), 11, 14, 44, 62, 64 +\subitem in program, 63, 64 +\item TopDec (top-level declarations), 11 +\item top-level declaration, 1, 11, 14, 44, 62, 64 +\item $\TRUE$, 74--76 +\item truncation of reals (\ml{floor}), 48, 75, 78 +\item tuple, 67, 71, 73 +\item tuple type, 67, 73 +\item $\ty$ (type expression), 7, 9, 29, 46, 67, 73 +\item Ty (type expressions), 7, 9, 46 +\item $\tycon$ (type constructor), 4, 8, 9, 13, 17, 21, 22, 27, 29, 32, 34, 42, 76 +\item $\TyCon$ (type constructors), 4 +\item $\TyEnv$ (type environments), 17 +\item $\TyNames$ (type names), 16 +\item $\TyNamesFcn$ (free type names), 17, 37 +\item $\TyNameSets$ (type name sets), 17 +\item $\typbind$ (type binding), 7, 8, 27, 46, 72 +\item TypBind (type bindings), 7, 46 +\item $\typdesc$ (type description), 11, 13, 41, 57 +\item TypDesc (type descriptions), 11, 57 +\item type ($\tau$), 17--19, 21, 23--25, 28, 29 +\item $\Type$ (types), 17 +\item $\TYPE$, 3, 8, 13, 25, 40, 42, 46, 57, 72 +\item $\scontype$ (function on special constants), 16, 23, 28 +\item type binding, 7, 8, 27, 46, 72 +\item type constraint (\verb+:+) +\subitem in expression, 8, 24, 46, 71 +\subitem in pattern, 9, 29, 46, 73 +\item type construction, 9, 29 +\item type constructor ($\tycon$), 4, 8, 9, 13, 17, 21, 22, 27, 29, 32, 34, 42, 76 +\item type constructor name (see type name) +\item type declaration, 8, 25, 46, 72 +\item type description ($\typdesc$), 11, 13, 41, 57 +\item type environment ($\TE$), 17, 21, 22, 27, 34, 42, 58 +\item type explication, 33--35, 38, 39, 44 +\item type-explicit signature (see type explication) +\item type expression, 7, 9, 29, 46, 67, 73 +\item type-expression row ($\labtys$), 7, 9, 30, 46, 73 +\item type function ($\typefcn$), 17, 19, 21, 22, 27, 32--34, 41--43, 76 +\item type name ($\t$), 16, 19, 21, 22, 25, 27, 30--34, 42, 76 +\item type name set, 17, 31 +\item type realisation ($\tyrea$), 33 +\item type scheme ($\tych$), 17, 19, 21, 23, 28, 34, 42, 75, 76 +\item type specification, 13, 40, 57 +\item type structure $(\theta,\CE)$, 17, 21, 22, 25, 27, 29, 32, 34, 40--43, 75, 76 +\item type variable ($\tyvar$, $\alpha$), 4, 9, 16 +\subitem in type expression, 9, 29, 73 +\subitem equality, 4, 16, 18, 19 +\subitem imperative, 4, 16, 18, 19, 21, 25, 27, 30, 44 +\subitem applicative, 4, 16, 18, 19, 21, 25, 27 +\subitem explicit, 20, 25, 26 +\item type vector ($\tauk$), 17, 19 +\item $\TypeFcn$ (type functions), 17 +\item $\TypeScheme$ (type schemes), 17 +\item $\labtys$ (type-expression row), 7, 9, 30, 46, 73 +\item TyRow (type-expression rows), 7, 9, 46 +\item $\TyStr$ (type structures), 17 +\item $\tyvar$ (see type variable) +\item $\TyVar$ (type variables), 4, 16 +\item $\TyVarFcn$ (free type variables), 17 +\item $\tyvarseq$ (type variable sequence), 7 +\item $\TyVarSet$, 17 +\indexspace +\parbox{65mm}{\hfil{\large\bf U}\hfil} +\indexspace +\item $\U$ (explicit type variables), 17, 18, 20, 25, 26 +\item $\UNIT$, 76 +\item unguarded type variable, 20 +\indexspace +\parbox{65mm}{\hfil{\large\bf V}\hfil} +\indexspace +\item $\V$ (value), 47, 50--53 +\item $\sconval$ (function on special constants), 46, 50, 54 +\item $\Val$ (values), 47 +\item $\VAL$, 3, 8, 13, 25, 40, 53, 60, 72 +\item $\valbind$ (value binding), 7, 8, 20, 21, 25, 26, 54, 72 +\subitem simple, 8, 26, 54, 72 +\subitem recursive, 8, 26, 54, 72 +\item Valbind (value bindings), 7 +\item $\valdesc$ (value description), 11, 13, 41, 61 +\item ValDesc (value descriptions), 11 +\item value binding ($\valbind$), 7, 8, 20, 21, 25, 26, 54, 72 +\subitem simple, 8, 26, 54, 72 +\subitem recursive, 8, 26, 54, 72 +\item value constant ($\con$) +\subitem in pattern, 9, 28, 54, 73 +\item value constructor ($\con$), 4 +\subitem as atomic expression, 8, 23, 51, 71 +\subitem scope, 5, 18 +\item value construction +\subitem in pattern, 9, 29, 55, 73 +\subitem infixed, in pattern, 9, 73 +\item value declaration, 8, 20, 25, 53, 72 +\item value description ($\valdesc$), 11, 13, 41, 61 +\item value variable ($\var$), 4 +\subitem as atomic expression, 8, 23, 50, 71 +\subitem in pattern, 9, 28, 54, 73 +\item value specification, 13, 40, 60 +\item $\var$ (see value variable) +\item $\Var$ (value variables), 4 +\item $\VarEnv$ (variable environments), 17, 47 +\item variable (see value variable) +\item variable environment ($\VE$) +\subitem static, 17, 18, 21, 25--29, 34, 41, 42, 58, 75, 76 +\subitem dynamic, 47, 49, 54, 55, 58, 77 +\item $\vars$ (set of value variables), 57, 61 +\item $\VE$ (see variable environment) +\item via $\rea$, 35, 45 +\item view of a structure, 39, 42, 57, 59, 60 +\indexspace +\parbox{65mm}{\hfil{\large\bf W}\hfil} +\indexspace +\item well-formed +\subitem assembly, 32, 33 +\subitem functor signature, 32 +\subitem signature, 32 +\subitem type structure, 21 +\item \WHILE, 3, 67, 71 +\item wildcard pattern (\verb+_+), 9, 28, 54, 73 +\item wildcard pattern row (\verb+...+), 3, 9, 28, 30, 55, 73 +\item \WITH, 3, 8, 72 +\item \WITHTYPE, 3, 66, 68, 72 +\indexspace +\parbox{65mm}{\hfil{\large\bf Y}\hfil} +\indexspace +\item $\Yield$, 33 +\end{theindex} \ No newline at end of file diff --git a/intro.tex b/intro.tex new file mode 100644 index 0000000..5c57efd --- /dev/null +++ b/intro.tex @@ -0,0 +1,124 @@ +\section{Introduction} + +This document formally defines Standard ML. + +To understand the method of definition, at least in broad terms, it helps to +consider how an implementation of ML is naturally +organised. ML is an interactive +language,\index{4.1} +and a {\sl program}\index{4.2} consists of a sequence of {\sl top-level +declarations};\index{4.3} the execution +of each declaration modifies the top-level environment, which we call +a {\sl basis}, and reports the modification to the user. + +In the execution of a declaration there are three phases: +{\sl parsing}, {\sl elaboration}, and {\sl evaluation}. +Parsing +determines the grammatical form of a declaration. Elaboration, the +{\sl static} phase, determines whether it is well-typed and +well-formed in other ways, and records relevant type or form information +in the basis. Finally evaluation, the {\sl dynamic} phase, determines the +value of the declaration and records relevant value information in the +basis. Corresponding to these phases, our formal definition divides +into three parts: grammatical rules, elaboration rules, and evaluation +rules. Furthermore, the basis is divided into the {\sl static} +basis and the {\sl dynamic} basis; for example, a variable which has been +declared is associated with a type in the static basis and with a value in +the dynamic basis. + +In an implementation, the basis need not be so divided. But for the +purpose of formal definition, it eases presentation and understanding to +keep the static and dynamic parts of the basis separate. +This is further justified by programming experience. A large proportion +of errors in ML programs are discovered during elaboration, and identified +as errors of type or form, so it follows that it is useful to perform +the elaboration phase separately. In fact, elaboration without +evaluation is just what is normally called {\sl compilation}; once +a declaration (or larger entity) is compiled one wishes to evaluate it -- +repeatedly -- without re-elaboration, from which it follows that it is +useful to perform the evaluation phase separately. + +A further factoring of the formal definition is possible, +because of the structure of the language. ML consists of a lower level +called the {\sl Core language} (or {\sl Core} for short), a middle level +concerned with programming-in-the-large called {\sl Modules}, +and a very small upper level called {\sl Programs}. +With the three phases described above, there is therefore +a possibility of nine components in the +complete language definition. We have allotted one section to each +of these components, except that we have combined the parsing, +elaboration and evaluation of Programs in one section. The +scheme for the ensuing seven sections is therefore as follows: + +\vspace*{3mm} +\begin{tabular}{rccc} + & {\em Core} & {\em Modules} & {\em Programs} \\ +\cline{2-4} +{\em Syntax} &\multicolumn{1}{|c}{Section 2} + &\multicolumn{1}{|c}{Section 3} + &\multicolumn{1}{|c|}{ }\\ +\cline{2-3} +{\em Static Semantics} + &\multicolumn{1}{|c}{Section 4} + &\multicolumn{1}{|c}{Section 5} + &\multicolumn{1}{|c|}{Section 8}\\ +\cline{2-3} +{\em Dynamic Semantics} + &\multicolumn{1}{|c}{Section 6} + &\multicolumn{1}{|c}{Section 7} + &\multicolumn{1}{|c|}{}\\ +\cline{2-4} +\end{tabular} +\vspace*{3mm} + +%The Core is +%a complete language in its own right, and its embedding in the full +%language is simple; therefore each of the three parts of the formal +%description is further divided into two -- one for the Core, and one for +%Modules. + +The Core provides many phrase classes, for programming convenience. +But about half of these classes are derived forms, whose meaning can be +given by translation into the other half which we call the +{\sl Bare} language. +Thus each of the three parts for the Core treats only the bare language; +the derived forms are treated in Appendix~\ref{derived-forms-app}. +This appendix also contains a few derived forms for Modules. +A full grammar for the language is presented in +Appendix~\ref{core-gram-app}. + +In\index{5.0} Appendices~\ref{init-stat-bas-app} and~\ref{init-dyn-bas-app} +the {\sl initial basis} is detailed. This basis, +divided into its static and dynamic parts, contains the static and +dynamic meanings of all predefined identifiers. + +The semantics is presented in a form known as Natural +Semantics.\index{5.1} It consists of a set of rules allowing +{\sl sentences} of the form +\[ A \vdash phrase \Rightarrow A' \] +to be inferred, where $A$ is often a basis (static or dynamic) and $A'$ a +semantic object +-- often a type in the static semantics and a value in the dynamic +semantics. One should read such a sentence as follows: ``against +the background provided by +$A$, the phrase $phrase$ elaborates -- or evaluates -- to the object +$A'$''. +Although the rules themselves are formal the semantic +objects, particularly the static ones, are the subject of a mathematical +theory which is presented in a succinct form in the relevant sections. +This theory, particularly the theory of types and signatures, will +benefit from a more pedagogic treatment in other publications; the +treatment here is +probably the minimum required to understand the meaning of the rules. + +The robustness of the semantics depends upon theorems. +Usually these have been proven, but the proof is not included. +In two cases, however, they are presented as ``claims'' rather than +theorems; these are the claim of principal environments in +Section~\ref{principal-env-sec}, and the claim of principal signatures +in Section~\ref{prinsig-sec}. We need further confirmation of our +detailed proofs of these claims, before asserting them as theorems. + + + + diff --git a/mac.tex b/mac.tex new file mode 100644 index 0000000..3ee1f90 --- /dev/null +++ b/mac.tex @@ -0,0 +1,752 @@ +\newcommand{\ml}[1]{{\tt #1}} +\renewcommand{\cdots}{\mbox{$\cdot\!\cdot\!\cdot$}} + + % Core Language +\newcommand{\ttlbrace}{\mbox{\tt\char'173}} +\newcommand{\ttrbrace}{\mbox{\tt\char'175}} +\newcommand{\lttbrace}{\mbox{\tt\char'173}} +\newcommand{\rttbrace}{\mbox{\tt\char'175}} +\newcommand{\ttprime}{\mbox{\tt\char'047}} +\newcommand{\ABSTYPE}{{\tt abstype}} +\newcommand{\AND }{{\tt and}} +\newcommand{\ANDALSO }{{\tt andalso}} +\newcommand{\AS}{{\tt as}} +\newcommand{\CASE}{{\tt case}} +\newcommand{\DO}{{\tt do}} +\newcommand{\DATATYPE}{{\tt datatype}} +\newcommand{\ELSE}{{\tt else}} +\newcommand{\END}{{\tt end}} +\newcommand{\EXCEPTION}{{\tt exception}} +\newcommand{\FUN}{{\tt fun}} +\newcommand{\FN}{{\tt fn}} +\newcommand{\HANDLE}{{\tt handle}} +\newcommand{\IF}{{\tt if}} +\newcommand{\IN}{{\tt in}} +\newcommand{\INFIX}{{\tt infix}} +\newcommand{\INFIXR}{{\tt infixr}} +\newcommand{\LET}{{\tt let}} +\newcommand{\LOCAL}{{\tt local}} +\newcommand{\NONFIX}{{\tt nonfix}} +\newcommand{\OF}{{\tt of}} +\newcommand{\OP}{{\tt op}} +\newcommand{\ORELSE}{{\tt orelse}} +\newcommand{\RAISE}{{\tt raise}} +\newcommand{\REC}{{\tt rec}} +\newcommand{\THEN}{{\tt then}} +\newcommand{\TYPE}{{\tt type}} +\newcommand{\VAL}{{\tt val}} +\newcommand{\WITH}{{\tt with}} +\newcommand{\WITHTYPE}{{\tt withtype}} +\newcommand{\WHILE}{{\tt while}} + + % Modules +\newcommand{\EQTYPE}{\ml{eqtype}} +\newcommand{\FUNCTOR}{\ml{functor}} +\newcommand{\INCLUDE}{\ml{include}} +\newcommand{\SIG}{\ml{sig}} +\newcommand{\OPEN}{\ml{open}} +\newcommand{\SHARING}{\ml{sharing}} +\newcommand{\SIGNATURE}{\ml{signature}} +\newcommand{\STRUCT}{\ml{struct}} +\newcommand{\STRUCTURE}{\ml{structure}} + % Identifier class names +\newcommand{\Var}{{\rm Var}} +\newcommand{\Con}{{\rm Con}} +\newcommand{\SCon}{{\rm SCon}} +\newcommand{\Exn}{{\rm ExCon}} +\newcommand{\TyVar}{{\rm TyVar}} +\newcommand{\ImpTyVar}{{\rm ImpTyVar}} +\newcommand{\AppTyVar}{{\rm AppTyVar}} +\newcommand{\TyCon}{{\rm TyCon}} +\newcommand{\Lab}{{\rm Lab}} +\newcommand{\StrId}{{\rm StrId}} +\newcommand{\FunId}{{\rm FunId}} +\newcommand{\SigId}{{\rm SigId}} + + % Identifier class variables +\newcommand{\id}{{\it id}} +\newcommand{\var}{{\it var}} +\newcommand{\con}{{\it con}} +\newcommand{\scon}{{\it scon}} +\newcommand{\exn}{{\it excon}} +\newcommand{\tyvar}{{\it tyvar}} +\newcommand{\atyvar}{\mbox{\tt \ttprime a}} +\newcommand{\btyvar}{\mbox{\tt \ttprime b}} +\newcommand{\ctyvar}{\mbox{\tt \ttprime c}} +\newcommand{\aityvar}{\mbox{\tt \ttprime\_a}} +\newcommand{\aetyvar}{\mbox{\tt \ttprime\ttprime a}} +\newcommand{\tycon}{{\it tycon}} +\newcommand{\lab}{{\it lab}} +\newcommand{\strid}{{\it strid}} + +\newcommand{\longvar}{{\it longvar}} +\newcommand{\longcon}{{\it longcon}} +\newcommand{\longexn}{{\it longexcon}} +\newcommand{\longtycon}{{\it longtycon}} +\newcommand{\longstrid}{{\it longstrid}} + + % General classes +\newcommand{\phrase}{{\it phrase}} + + % Core Syntax Classes +\newcommand{\apexp}{{\it appexp}} +\newcommand{\atpat}{{\it atpat}} +\newcommand{\atexp}{{\it atexp}} +\newcommand{\bind}{{\it bind}} +\newcommand{\constrs}{{\it conbind}} +\newcommand{\ConBind}{{\rm ConBind}} +\newcommand{\datbind}{{\it datbind}} +\newcommand{\dec}{{\it dec}} +\newcommand{\dir}{{\it dir}} +\newcommand{\exnbind}{{\it exbind}} +\renewcommand{\exp}{{\it exp}} +\newcommand{\fvalbind}{{\it fvalbind}} +\newcommand{\handler}{{\it handler}} +\newcommand{\hanrule}{{\it hrule}} +\newcommand{\inexp}{{\it infexp}} +\newcommand{\labexps}{{\it exprow}} +\newcommand{\labpats}{{\it patrow}} +\newcommand{\labtys}{{\it tyrow}} +\newcommand{\match}{{\it match}} +\newcommand{\pat}{{\it pat}} +\newcommand{\mrule}{{\it mrule}} +\newcommand{\ty}{{\it ty}} +\newcommand{\tyseq}{{\it tyseq}} +\newcommand{\tyvarseq}{{\it tyvarseq}} +\newcommand{\typbind}{{\it typbind}} +\newcommand{\valbind}{{\it valbind}} + + % ranged over by the variables + + + + + % Modules syntax classes + +\newcommand{\datdesc}{{\it datdesc}} +\newcommand{\condesc}{{\it condesc}} +\newcommand{\exndesc}{{\it exdesc}} +\newcommand{\funbind}{{\it funbind}} +\newcommand{\fundec}{{\it fundec}} +\newcommand{\fundesc}{{\it fundesc}} +\newcommand{\funid}{{\it funid}} +\newcommand{\funsigexp}{{\it funsigexp}} +\newcommand{\funspec}{{\it funspec}} +\newcommand{\funtyp}{{\it funtyp}} +\newcommand{\longstridk}{\strid_1.\cdots.\strid_k} +\newcommand{\longtyconk}{\strid_1.\cdots.\strid_k.\tycon} +\newcommand{\topdec}{{\it topdec}} +\newcommand{\program}{{\it program}} +\newcommand{\sigid}{{\it sigid}} +\newcommand{\shareq}{{\it shareq}} +\newcommand{\sigbind}{{\it sigbind}} +\newcommand{\sigdec}{{\it sigdec}} +\newcommand{\sigexp}{{\it sigexp}} +\newcommand{\spec}{{\it spec}} +\newcommand{\strbind}{{\it strbind}} +\newcommand{\strdec}{{\it strdec}} +\newcommand{\strexp}{{\it strexp}} +\newcommand{\strdesc}{{\it strdesc}} +\newcommand{\typdesc}{{\it typdesc}} +\newcommand{\valdesc}{{\it valdesc}} + % Core Language Phrases + + % Expressions + +\newcommand{\recexp}{\mbox{$\langle\labexps\rangle$}} +\newcommand{\longlabexps}{\mbox{\lab\ \ml{=} \exp\ + $\langle$ \ml{,} \labexps$\rangle$}} +\newcommand{\parexp}{\mbox{\ml{(} \exp\ \ml{)}}} +\newcommand{\appexp} + {\mbox{\exp\ \atexp}} +\newcommand{\infexp} + {\mbox{$\exp_1\ \id\ \exp_2$}} +\newcommand{\opp} + {\mbox{$\langle\OP\rangle$}} +\newcommand{\typedexp} + {\mbox{\exp\ \ml{:} \ty}} +\newcommand{\handlexp} + {\mbox{\exp\ \HANDLE\ \match}} +\newcommand{\raisexp} + {\mbox{\RAISE\ \exp}} +\newcommand{\letexp} + {\mbox{\LET\ \dec\ \IN\ \exp\ \END}} +\newcommand{\fnexp} + {\mbox{\FN\ \match}} + + % Matches and Handlers +\newcommand{\longmatch} + {\mbox{\mrule\ $\langle$ \ml{|} \match$\rangle$}} +\newcommand{\longmatcha} + {\mbox{\mrule\ \ml{|} \match}} +\newcommand{\longmrule} + {\mbox{\pat\ \ml{=>} \exp}} +\newcommand{\longhandler} + {\mbox{\hanrule\ $\langle$ \ml{||} \handler$\rangle$}} +\newcommand{\longhandlera} + {\mbox{\hanrule\ \ml{||} \handler}} +\newcommand{\longhanrule} + {\mbox{\longexn\ \WITH\ \match}} +\newcommand{\lasthanrule} + {\mbox{? \ml{=>} \exp}} + + % Declarations +\newcommand{\valdec} + {\mbox{\VAL\ \valbind}} +\newcommand{\valdecS} + {\mbox{$\VAL_{\U}$\ \valbind}} +\newcommand{\typedec} + {\mbox{\TYPE\ \typbind}} +\newcommand{\datatypedec} + {\mbox{\DATATYPE\ \datbind}} +\newcommand{\datatypedeca} + {\mbox{\DATATYPE\ \datbind\ $\langle\WITHTYPE\ \typbind\rangle$}} +\newcommand{\abstypedec} + {\mbox{\ABSTYPE\ \datbind\ \WITH\ \dec\ \END}} +\newcommand{\abstypedeca} + {\mbox{\ABSTYPE\ \datbind\ $\langle\WITHTYPE\ \typbind\rangle$}} +\newcommand{\exceptiondec} + {\mbox{\EXCEPTION\ \exnbind}} +\newcommand{\localdec} + {\mbox{\LOCAL\ $\dec_1\ \IN\ \dec_2$\ \END}} +\newcommand{\emptydec} + {\mbox{\qquad}} +\newcommand{\seqdec} + {\mbox{$\dec_1\ \langle\ml{;}\rangle\ \dec_2$}} +\newcommand{\longinfix} + {\mbox{$\INFIX\ \langle d\rangle\ \id_1\ \cdots\ \id_n$}} +\newcommand{\longinfixr} + {\mbox{$\INFIXR\ \langle d\rangle\ \id_1\ \cdots\ \id_n$}} +\newcommand{\longnonfix} + {\mbox{$\NONFIX\ \id_1\ \cdots\ \id_n$}} + + % Bindings +\newcommand{\longvalbind} + {\mbox{\pat\ \ml{=} \exp\ $\langle\AND\ \valbind\rangle$}} +\newcommand{\recvalbind} + {\mbox{\REC\ \valbind}} +\newcommand{\longtypbind} + {\mbox{\tyvarseq\ \tycon\ \ml{=} \ty + \ $\langle\AND\ \typbind\rangle$}} +\newcommand{\longdatbind} + {\mbox{\tyvarseq\ \tycon\ \ml{=} \constrs + \ $\langle\AND\ \datbind\rangle$}} +\newcommand{\longconstrs} + {\mbox{$\con\ \langle\OF\ \ty\rangle\ + \langle$ \ml{|} \constrs$\rangle$}} +\newcommand{\longerconstrs} + {\mbox{$\con\ \langle\OF\ \ty\rangle\ + \langle\langle$ \ml{|} \constrs$\rangle\rangle$}} +\newcommand{\generativeexnbind} + {\mbox{$\langle\OP\rangle\exn\ \langle\OF\ \ty\rangle\ + \langle\AND\ \exnbind\rangle$}} +\newcommand{\eqexnbind} + {\mbox{$\langle\OP\rangle$\exn\ \ml{=} + $\langle\OP\rangle\longexn\ + \langle\AND\ \exnbind\rangle$}} +\newcommand{\longexnbinda} + {\mbox{\exn\ $\langle\OF\ \ty\rangle$\ + $\langle\langle\AND\ \exnbind\rangle\rangle$}} +\newcommand{\longexnbindaa} + {\mbox{\exn\ + $\langle\AND\ \exnbind\rangle$}} +\newcommand{\longexnbindb} + {\mbox{\exn\ \ml{=}\ \longexn\ $\langle\AND\ \exnbind\rangle$}} +% from version 1: +%\newcommand{\longexnbind} +% {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle +% \langle$\ml{=} $\longexn\rangle +% \ \langle\AND\ \exnbind\rangle$}} +%\newcommand{\longexnbinda} +% {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle +% \ \langle\langle\AND\ \exnbind\rangle\rangle$}} +%\newcommand{\longexnbindaa} +% {\mbox{\exn\ +% $\langle\AND\ \exnbind\rangle$}} +%\newcommand{\longexnbindb} +% {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle +% \ $\ml{=} $\longexn +% \ \langle\langle\AND\ \exnbind\rangle\rangle$}} +%\newcommand{\longexnbindbb} +% {\mbox{\exn\ \ml{=} \longexn\ +% $\langle\AND\ \exnbind\rangle$}} + + % Patterns +\newcommand{\wildpat}{\mbox{\ml{\_}}} +\newcommand{\recpat}{\mbox{$\langle\labpats\rangle$}} +\newcommand{\wildrec}{\mbox{\ml{...}}} +\newcommand{\longlabpats}{\mbox{\lab\ \ml{=} \pat\ + $\langle$ \ml{,} \labpats$\rangle$}} +\newcommand{\parpat}{\mbox{\ml{(} \pat\ \ml{)}}} +\newcommand{\conpat} + {\mbox{\longcon\ \atpat}} +\newcommand{\exconpat} + {\mbox{\longexn\ \atpat}} +\newcommand{\infpat} + {\mbox{$\pat_1\ \con\ \pat_2$}} +\newcommand{\infexpat} + {\mbox{$\pat_1\ \exn\ \pat_2$}} +\newcommand{\typedpat} + {\mbox{\pat\ \ml{:} \ty}} +\newcommand{\layeredpat} + {\mbox{\var$\langle$\ml{:} \ty$\rangle$ \AS\ \pat}} +\newcommand{\layeredpata} + {\mbox{\var\ \AS\ \pat}} + + % Types +\newcommand{\rectype}{\mbox{$\langle\labtys\rangle$}} +\newcommand{\longlabtys}{\mbox{\lab\ \ml{:} \ty\ + $\langle$ \ml{,} \labtys$\rangle$}} +\newcommand{\constype} + {\mbox{\tyseq\ \longtycon}} +\newcommand{\funtype} + {\mbox{\ty\ \ml{->} \ty$'$}} +\newcommand{\partype}{\mbox{\ml{(} \ty\ \ml{)}}} +\newcommand{\longtyseq}{\mbox{\ml{(} $\ty_1,\cdots\,\ty_k$ \ml{)}}} +\newcommand{\longtyvarseq}{\mbox{\ml{(} $\tyvar_1,\cdots,\tyvar_k$ \ml{)}}} + + % Modules Phrases + +\newcommand{\emptyphrase}{\qquad} + + + % structure-level declarations + +\newcommand{\singstrdec}{\mbox{$\STRUCTURE\ \strbind $}} +\newcommand{\localstrdec}{\mbox{$\LOCAL\ \strdec_1\ \IN\ \strdec_2\ \END $}} +\newcommand{\openstrdec}{\mbox{$\OPEN\ \longstrid_1\ \cdots\ \longstrid_n $}} +\newcommand{\emptystrdec}{\emptyphrase} +\newcommand{\seqstrdec}{\mbox{$\strdec_1\ \langle$\ml{;}$\rangle\ \strdec_2 $}} + + + % structure bindings + +\newcommand{\strbinder} + {\mbox{$\strid\ \langle$\ml{:}$\ \sigexp\rangle$ + \ml{=} $\strexp\ \langle\langle\AND\ \strbind\rangle\rangle$}} +\newcommand{\strbindera} + {\mbox{$\strid\ \langle$\ml{:}$\ \sigexp\rangle$ + \ml{=} $\strexp\ \langle\AND\ \strbind\rangle$}} + + + % structure expressions + +\newcommand{\encstrexp}{\mbox{\STRUCT\ \strdec\ \END}} +\newcommand{\funappdec}{\mbox{\funid\ \ml{(}\ \strdec\ \ml{)} }} +\newcommand{\funappstr}{\mbox{\funid\ \ml{(}\ \strexp\ \ml{)} }} +\newcommand{\letstrexp}{\mbox{\LET\ \strdec\ \IN\ \strexp\ \END}} + + % specifications + +\newcommand{\valspec}{\mbox{\VAL\ \valdesc}} +\newcommand{\typespec}{\mbox{\TYPE\ \typdesc}} +\newcommand{\eqtypespec}{\mbox{\EQTYPE\ \typdesc}} +\newcommand{\datatypespec}{\mbox{\DATATYPE\ \datdesc}} +\newcommand{\exceptionspec}{\mbox{\EXCEPTION\ \exndesc}} +\newcommand{\structurespec}{\mbox{\STRUCTURE\ \strdesc}} +\newcommand{\sharingspec}{\mbox{\SHARING\ \shareq}} +\newcommand{\localspec}{\mbox{$\LOCAL\ \spec_1\ \IN\ \spec_2\ \END$}} +\newcommand{\openspec}{\mbox{$\OPEN\ \longstrid_1\ \cdots\ \longstrid_n $}} +\newcommand{\emptyspec}{\emptyphrase} +\newcommand{\seqspec}{\mbox{$\spec_1\ \langle$\ml{;}$\rangle\ \spec_2$}} +\newcommand{\inclspec}{\mbox{$\INCLUDE\ \sigid_1\ \cdots\ \sigid_n $}} + + + % descriptions + +\newcommand{\valdescription} + {\mbox{\var\ \ml{:} $\ty\ \langle\AND\ \valdesc\rangle$}} + +\newcommand{\typdescription} + {\mbox{\tyvarseq\ \tycon\ $\langle\AND\ \typdesc\rangle$}} + +\newcommand{\datdescription} + {\mbox{\tyvarseq\ \tycon\ \ml{=} \condesc + \ $\langle\AND\ \datdesc\rangle$}} + +\newcommand{\condescription} + {\mbox{$\con\ \langle\OF\ \ty\rangle\ + \langle$ \ml{|} \condesc$\rangle$}} + +\newcommand{\longcondescription} + {\mbox{$\con\ \langle\OF\ \ty\rangle\ + \langle\langle$ \ml{|} \condesc$\rangle\rangle$}} + +\newcommand{\exndescription} + {\mbox{\exn\ $\langle\OF\ \ty\rangle$ + \ $\langle\AND\ \exndesc\rangle$}} + +\newcommand{\exndescriptiona} + {\mbox{\exn\ $\langle\OF\ \ty\rangle$ + \ $\langle\langle\AND\ \exndesc\rangle\rangle$}} + +\newcommand{\strdescription} + {\mbox{\strid\ \ml{:} \sigexp + \ $\langle\AND\ \strdesc\rangle$}} + + % sharing equations + +\newcommand{\strshareq}{\mbox{$\longstrid_1$ \ml{=} $\cdots$ + \ml{=} $\longstrid_n$ }} +\newcommand{\typshareq}{\mbox{$\TYPE\ \longtycon_1$ \ml{=} $\cdots$ + \ml{=} $\longtycon_n$ }} +\newcommand{\multshareq}{\mbox{$\shareq_1\ \AND\ \shareq_2$}} + + + % signature expressions + +\newcommand{\encsigexp}{\mbox{\SIG\ \spec\ \END}} + + % signature declarations + +\newcommand{\singsigdec}{\mbox{$\SIGNATURE\ \sigbind $}} +\newcommand{\emptysigdec}{\emptyphrase} +\newcommand{\seqsigdec}{\mbox{$\sigdec_1\ \langle$\ml{;}$\rangle\ \sigdec_2 $}} + + + % signature bindings + +\newcommand{\sigbinder} + {\mbox{\sigid\ \ml{=} \sigexp + \ $\langle\AND\ \sigbind\rangle$}} + + + % functor declarations + +\newcommand{\singfundec}{\mbox{$\FUNCTOR\ \funbind $}} +\newcommand{\emptyfundec}{\emptyphrase} +\newcommand{\seqfundec}{\mbox{$\fundec_1\ \langle$\ml{;}$\rangle\ \fundec_2 $}} + + + % functor bindings + +\newcommand{\funbinder} + {\mbox{\funid\ \ml{(} \spec\ \ml{)} + $\langle$\ml{:}$\ \sigexp\rangle$\ \ml{=} $\strexp$ + $\langle\langle\AND\ \funbind\rangle\rangle$}} +\newcommand{\funbindera} + {\mbox{\funid\ \ml{(} \spec\ \ml{)} + $\langle$\ml{:}$\ \sigexp\rangle$\ \ml{=} $\strexp$}} +\newcommand{\funstrbinder} + {\mbox{\funid\ \ml{(}\ \strid\ \ml{:}\ \sigexp\ \ml{)} + $\langle$\ml{:}$\ \sigexp'\rangle$\ \ml{=} $\strexp$}} +\newcommand{\optfunbind} + {\mbox{$\langle\langle\AND\ \funbind\rangle\rangle$}} +\newcommand{\optfunbinda} + {\mbox{$\langle\AND\ \funbind\rangle$}} +\newcommand{\funstrbindera} + {\mbox{\funid\ \ml{(}\ \strid\ \ml{)}\ \ml{=} \strexp + \ $\langle\AND\ \funbind\rangle$}} + + + %functor signature expressions + +\newcommand{\longfunsigexp} + {\mbox{\ml{(}\ \spec\ \ml{)} + \ml{:}\ \sigexp}} +\newcommand{\longfunsigexpa} + {\mbox{\ml{(}\ \strid\ \ml{:}\ \sigexp\ \ml{)} + \ml{:}\ \sigexp$'$}} + + + % functor specifications + +\newcommand{\singfunspec}{\mbox{\FUNCTOR\ \fundesc}} +\newcommand{\emptyfunspec}{\emptyphrase} +\newcommand{\seqfunspec} + {\mbox{$\funspec_1\ \langle$\ml{;}$\rangle\ \funspec_2$}} + + + % functor descriptions + +\newcommand{\longfundesc} + {\mbox{\funid\ \funsigexp\ $\langle\AND\ \fundesc\rangle$}} + + + % programs +\newcommand{\longprog}{\mbox{\topdec\ \ml{;}\ $\langle\program\rangle$}} +\newcommand{\seqprog} + {\mbox{$\program_1\ \langle$\ml{;}$\rangle\ \program_2$}} +% **************** END SYNTAX ************************* +\newcommand{\ML}{{\rm ML}} + + +% finite sets and maps (assume math mode) +% +\newcommand{\Fin}{\mathop{\rm Fin}\nolimits} +\newcommand{\Dom}{\mathop{\rm Dom}\nolimits} +\newcommand{\Ran}{\mathop{\rm Ran}\nolimits} +\newcommand{\finfun}[2]{#1\stackrel{{\rm fin}}{\to}#2} +\newcommand{\emptymap}{\{\}} +\newcommand{\kmap}[2]{\{#1_1\mapsto#2_1,\cdots,#1_k\mapsto#2_k\}} +\newcommand{\plusmap}[2]{#1 + #2} +% +\newcommand{\TyVarSet}{{\rm TyVarSet}} +% +% +% Names (assume math mode) +\newcommand{\TyNames}{{\rm TyName}} +\newcommand{\TyNameSets}{{\rm TyNameSet}} +\newcommand{\StrNames}{{\rm StrName}} +\newcommand{\StrNameSets}{{\rm StrNameSet}} + +\newcommand{\NameSets}{{\rm NameSet}} +\newcommand{\TyNamesk}{\TyNames^{(k)}} +\newcommand{\Addr}{{\rm Addr}} +\newcommand{\Exc}{{\rm ExName}} +\newcommand{\BasVal}{{\rm BasVal}} +\newcommand{\SVal}{{\rm SVal}} +\newcommand{\BasExc}{{\rm BasExName}} +\newcommand{\BasTyp}{{\rm BasTyp}} +\newcommand{\CONT}{{\tt !}} +\newcommand{\ASS}{{\tt :=}} +\newcommand{\FAIL}{{\rm FAIL}} +\newcommand{\Fail}{{\rm FAIL}} +\newcommand{\fail}{{\rm FAIL}} +\newcommand{\APPLY}{{\rm APPLY}} + +\newcommand{\A}{a} +\newcommand{\e}{\mbox{\it en}} +\newcommand{\sv}{\mbox{\it sv}} +\newcommand{\exval}{e} +\newcommand{\excs}{\mbox{\it ens}} +\newcommand{\exns}{\mbox{\it excons}} % used in the dynamic sem. of mod. +\newcommand{\f}{f} +\newcommand{\m}{m} +\newcommand{\mem}{\mbox{\it mem}} +\newcommand{\M}{M} +\newcommand{\n}{n} +\newcommand{\N}{N} +\newcommand{\p}{p} +\renewcommand{\r}{r} +\newcommand{\res}{\mbox{\it res}} +\newcommand{\s}{s} +\renewcommand{\t}{t} +\newcommand{\T}{T} +\newcommand{\U}{U} +\newcommand{\V}{v} +\newcommand{\vars}{\mbox{\it vars}} +\newcommand{\X}{X} + + % Compound Objects (Core Language) +\newcommand{\TyEnv}{{\rm TyEnv}} +\newcommand{\TE}{\mbox{$T\!E$}} +\newcommand{\TyStr}{{\rm TyStr}} + +\newcommand{\ConEnv}{{\rm ConEnv}} +\newcommand{\CE}{\mbox{$C\!E$}} + +\newcommand{\VarEnv}{{\rm VarEnv}} +\newcommand{\VE}{\mbox{$V\!E$}} + +\newcommand{\ExnEnv}{{\rm ExConEnv}} +\newcommand{\EE}{\mbox{$E\!E$}} + +\newcommand{\IntEnv}{{\rm IntEnv}} +\newcommand{\IE}{\mbox{$I\!E$}} + +\newcommand{\Env}{{\rm Env}} +\newcommand{\E}{E} +\newcommand{\longE}[1]{(\SE_{#1},\TE_{#1},\VE_{#1},\EE_{#1})} + +\newcommand{\StrEnv}{{\rm StrEnv}} +\newcommand{\SE}{\mbox{$S\!E$}} + +\newcommand{\Str}{{\rm Str}} +\renewcommand{\S}{S} +\newcommand{\longS}[1]{(\m_{#1},(\SE_{#1},\TE_{#1},\VE_{#1},\EE_{#1}))} + +\newcommand{\Int}{{\rm Int}} +\newcommand{\I}{I} + +\newcommand{\Context}{\rm Context} +\newcommand{\C}{C} + + +\newcommand{\Record}{{\rm Record}} +\newcommand{\ExVal}{{\rm ExVal}} +\newcommand{\Fun}{{\rm Fun}} % used? +\newcommand{\Pack}{{\rm Pack}} +\newcommand{\Closure}{{\rm Closure}} +\newcommand{\FunctorClosure}{{\rm FunctorClosure}} +\newcommand{\Match}{{\rm Match}} +\newcommand{\State}{{\rm State}} +\newcommand{\StrExp}{{\rm StrExp}} +\newcommand{\Mem}{{\rm Mem}} +\newcommand{\ExcSet}{{\rm ExNameSet}} +\newcommand{\Val}{{\rm Val}} + +\newcommand{\arity}{\mathop{\rm arity}\nolimits} +\renewcommand{\k}{\mbox{$k$}} +\newcommand{\longtauk}{(\tau_1,\cdots,\tau_k)} +\newcommand{\tauk}{\mbox{$\tau^{(k)}$}} +\newcommand{\longalphak}{(\alpha_1,\cdots,\alpha_k)} +\newcommand{\alphak}{\mbox{$\alpha^{(k)}$}} +\newcommand{\alphakt}{\mbox{$\alpha^{(k)}t$}} +% +\newcommand{\thetak}{\mbox{$\theta^{(k)}$}} +\newcommand{\tk}{\mbox{$\t^{(k)}$}} +\newcommand{\typefcn}{\theta} +\newcommand{\typefcnk}{\Lambda\alphak.\tau} +\newcommand{\Type}{{\rm Type}} +\newcommand{\ConsType}{{\rm ConsType}} +\newcommand{\RecType}{{\rm RecType}} +\newcommand{\FunType}{{\rm FunType}} +\newcommand{\constypek}{\t(\tau_1,\cdots,\tau_k)} +\newcommand{\TypeScheme}{{\rm TypeScheme}} +\newcommand{\tych}{\sigma} +\newcommand{\longtych}{\forall\alphak.\tau} +\newcommand{\Abs}{\mathop{\rm Abs}\nolimits} +\newcommand{\Inter}{\mathop{\rm Inter}\nolimits} +\newcommand{\Rec}{\mathop{\rm Rec}\nolimits} +\newcommand{\TypeFcn}{{\rm TypeFcn}} +\newcommand{\TyConFcn}{\mathop{\rm TyCon}\nolimits} % used? +\newcommand{\TyVarFcn}{\mathop{\rm tyvars}\nolimits} +\newcommand{\imptyvars}{\mathop{\rm imptyvars}\nolimits} +\newcommand{\apptyvars}{\mathop{\rm apptyvars}\nolimits} +\newcommand{\scontype}{\mathop{\rm type}\nolimits} +\newcommand{\sconval}{\mathop{\rm val}\nolimits} +% +% Compound Objects (Modules) +% +% +\newcommand{\Sig}{{\rm Sig}} +\newcommand{\sig}{\Sigma} +\newcommand{\longsig}[1]{(\N_{#1})\S_{#1}} +\newcommand{\FunSig}{{\rm FunSig}} +\newcommand{\funsig}{\Phi} +\newcommand{\longfunsig}[1]{(\N_{#1})(\S_{#1},(\N_{#1}')\S_{#1} +')} +\newcommand{\FunEnv}{{\rm FunEnv}} +\newcommand{\F}{F} + +\newcommand{\SigEnv}{{\rm SigEnv}} +\newcommand{\G}{G} + +\newcommand{\Basis}{{\rm Basis}} +\newcommand{\B}{B} +\newcommand{\Bstat}{B_{\rm STAT}} +\newcommand{\Bdyn}{B_{\rm DYN}} + +\newcommand{\IntBasis}{{\rm IntBasis}} +\newcommand{\IB}{\mbox{$I\!B$}} + + +% Selection of Components +% +\newcommand{\of}[2]{#1 \mathbin{\rm of} #2} +\newcommand{\In}{\mbox{\rm in}} +% +% Names in Structures +\newcommand{\StrNamesFcn}{\mathop{\rm strnames}\nolimits} +\newcommand{\TyNamesFcn}{\mathop{\rm tynames}\nolimits} +\newcommand{\TyVarsFcn}{\mathop{\rm tyvars}\nolimits} +\newcommand{\NamesFcn}{\mathop{\rm names}\nolimits} +% +% Type Schemes (assume math mode) +% +\newcommand{\cl}[2]{{\rm Clos}_{#1}#2} +% +% Realisations (assume math mode) +% +\newcommand{\tyrea}{\varphi_{\rm Ty}} +\newcommand{\strrea}{\varphi_{\rm Str}} +\newcommand{\rea}{\varphi} +\newcommand{\longrea}{(\tyrea,\strrea)} +% +% Support (assume math mode) +% +\newcommand{\Supp}{\mathop{\rm Supp}\nolimits} +\newcommand{\Yield}{\mathop{\rm Yield}\nolimits} +% +% Instantiation (assume math mode) +% +\newcommand{\siginst}[3]{#1 {\geq_{#2}} #3} +\newcommand{\sigord}[3]{#1 {\geq_{#2}} #3} +\newcommand{\funsiginst}[3]{#1 {\geq_{#2}} #3} +% +% Inference Rules +% +% +\newcommand{\ts}{\vdash} +\newcommand{\tsdyn}{\vdash_{\rm DYN}} +\newcommand{\tsstat}{\vdash_{\rm STAT}} + +\newcommand{\ra}{\Rightarrow} + +% Initial Static Basis + +% Type names +\newcommand{\BOOL}{\mbox{\tt bool}} +\newcommand{\INT}{\mbox{\tt int}} +\newcommand{\REAL}{\mbox{\tt real}} +\newcommand{\NUM}{\mbox{\tt num}} +\newcommand{\EXCN}{\mbox{\tt exn}} +\newcommand{\STRING}{\mbox{\tt string}} +\newcommand{\LIST}{\mbox{\tt list}} +\newcommand{\INSTREAM}{\mbox{\tt instream}} +\newcommand{\OUTSTREAM}{\mbox{\tt outstream}} + +% Constructors +\newcommand{\FALSE}{\mbox{\tt false}} +\newcommand{\TRUE}{\mbox{\tt true}} +\newcommand{\NIL}{\mbox{\tt nil}} +\newcommand{\REF}{\mbox{\tt ref}} +\newcommand{\UNIT}{\mbox{\tt unit}} + +% Basic Values BasVal +%\newcommand{\MAP}{\mbox{\tt map}} +%\newcommand{\REV}{\mbox{\tt rev}} +%\newcommand{\NOT}{\mbox{\tt not}} +%\newcommand{\NEG}{\mbox{\verb-~-}} +%\newcommand{\ABS}{\mbox{\tt abs}} +%\newcommand{\FLOOR}{\mbox{\tt floor}} +%\newcommand{\REAL}{\mbox{\tt real}} +%\newcommand{\SQRT}{\mbox{\tt sqrt}} +%\newcommand{\SIN}{\mbox{\tt sin}} +%\newcommand{\COS}{\mbox{\tt cos}} +%\newcommand{\ARCTAN}{\mbox{\tt arctan}} +%\newcommand{\EXP}{\mbox{\tt exp}} +%\newcommand{\LN}{\mbox{\tt ln}} +%\newcommand{\SIZE}{\mbox{\tt size}} +%\newcommand{\CHR}{\mbox{\tt chr}} +%\newcommand{\ORD}{\mbox{\tt ord}} +%\newcommand{\EXPLODE}{\mbox{\tt explode}} +%\newcommand{\IMPLODE}{\mbox{\tt implode}} +%\newcommand{\REALDIV}{\mbox{\tt /}} +%\newcommand{\DIV}{\mbox{\tt div}} +%\newcommand{\MOD}{\mbox{\tt mod}} +%\newcommand{\TIMES}{\mbox{\tt *}} +%\newcommand{\PLUS}{\mbox{\tt +}} +%\newcommand{\MINUS}{\mbox{\tt -}} +%\newcommand{\APPEND}{\mbox{\verb-@-}} +%\newcommand{\EQ}{\mbox{\verb-=-}} +%\newcommand{\NEQ}{\mbox{\verb-<>-}} +%\newcommand{\LESS}{\mbox{\verb-<-}} +%\newcommand{\GREATER}{\mbox{\verb->-}} +%\newcommand{\LEQ}{\mbox{\verb-<=-}} +%\newcommand{\GEQ}{\mbox{\verb->=-}} +%\newcommand{\COMP}{\mbox{\tt o}} + +%\newcommand{\STDIN}{\mbox{\tt std\_in}} +%\newcommand{\OPENIN}{\mbox{\tt open\_in}} +%\newcommand{\INPUT}{\mbox{\tt input}} +%\newcommand{\LOOKAHEAD}{\mbox{\tt lookahead}} +%\newcommand{\CLOSEIN}{\mbox{\tt close\_in}} +%\newcommand{\ENDSTREAM}{\mbox{\tt end\_of\_stream}} +%\newcommand{\STDOUT}{\mbox{\tt std\_out}} +%\newcommand{\OPENOUT}{\mbox{\tt open\_out}} +%\newcommand{\OUTPUT}{\mbox{\tt output}} +%\newcommand{\CLOSEOUT}{\mbox{\tt close\_out}} +%\newcommand{\IOFAILURE}{\mbox{\tt io\_failure}} +\newcommand{\comment}{{\it Comment:\ }} +\newcommand{\comments}{{\it Comments:\ }} +\newcommand{\rulesec}[2]{\subsection*{{\bf#1}\hfill\fbox{$#2$}}} +% +\font\msxm=msxm10 +\textfont10=\msxm +\mathchardef\restrict="0A16 +% +% $$f\restrict_A$$ % Example of use +%alignment +%\halign{\indent$#$&\quad$#$&\quad$#$\hfil&\quad\parbox[t]{6cm}{\strut#\strut}\cr diff --git a/notes.tex b/notes.tex new file mode 100644 index 0000000..6237521 --- /dev/null +++ b/notes.tex @@ -0,0 +1,634 @@ +\documentstyle[12pt]{article} +\title{The Semantics of Standard ML\\RECORD OF CHANGES AND VERSIONS} +\author{Mads Tofte} +\begin{document} +\maketitle +\begin{center} \bf 1987 \end{center} +\vspace{1cm} +\begin{description} +\item{13 August 87} ``The Semantics of Standard ML, Version 1'' +by Robert Harper, Robin Milner and Mads Tofte. ECS-LFCR-87-36, +August 87. + +\item{13 August 87 (annotated).} A copy of [13 August 87] +annotated by RM. There are annotations in blue (regarding +exceptions) and other corrections (marked in red). + +\item{25 November 87} ``The Semantics of Standard ML''. The semantics +of 13 August changes so as to accomodate exception constructors (MacQueen's +proposal). +All changes from [13 August 87] are taken from [13 August 87, +annotated] (blue corrections only) and marked in the margin. +Does not include polymorphic exceptions or references. +Copy sent of to MacQueen for approval 18 Jan 88. +Original with me. +\end{description} + +\newpage +\begin{center} \bf 1988 \end{center} +\vspace{1cm} +\begin{description} +\item{21 June 88} ``The definition of Standard ML, Version 2''. +I have done and checked Robin's corrections to [25 Nov 87] +as listed on my ``cover letter'' [ad 25 Nov 87]. +Also, I have done and checked the red corrections +of [13 August 87, annotated]. In addition the following changes. + +\begin{enumerate} +\item +Exceptions have monotypes only. Rule (30) and restriction 1 +in Section 4.9 have been modified accordingly. + +\item +The type constructor {\tt excn} has been changed to {\tt exn}. +(I have maintained {\it exn} to range over exeption names.) + +\item +The type {\tt exn} does not admit equality. This has been +made explicit on the first page of appendix C. + +\item +The third example of a real constant in Section 2.2 has been +corrected (RM had earlier corrected master copy by hand). + +\item +Abstype should hide equality outside the with part. Changes to +Section~4.7 and the present rule (19), formerly (21). + +\item +The rule for constants in atomic patterns in the dynamic semantics +of the core (rule 36 in Version 1) changed so as to make the +types of constants more obvious. + +\item +I have inserted sentences in Section 4.4 (Version 1) to the effect +that the equality attribute of a bound type variable in a type +function does not matter. Also, I have inserted sentences in Section 4.5 +(Version 1) to the effect that the equality attributes of bound type +variables in type schemes do matter. + +\item +My scheme for polymorphic references and exceptions tentatively +included. See ``Polymorphic References and Exceptions in the +ML Semantics'', 20 May 88, Mads Tofte, for a detailed list of +changes. In particular, I have undone the above change (that +exceptions have monotypes only) to allow exceptions +to have imperative types. (30 May 88) + +\item +Basic exception constructors changed to start with a capital +letter (Bind, Match etc) in accordance with ``Unifying +Exceptions with Constructors in Standard ML (30 May)''. +(30 May 88, mt) + +\item +Semantics of programs, henceforth Section 8, included. +Corrections to the semantics of modules as detailed in +``Changes to ML Semantics to deal with Programs properly'', +RM 17/5/88 with my added handwritten notes.(31 May 88, mt) + +\item +Previously ``applied'' functor forms have been turned into +derived forms and moved to Appendix A. +The previously ``pure'' forms new appear directly in the grammar. (1 June 88,mt) + +\item +Comments added in the section ``Closure Restrictions'' to clarify +the closure restrictions. Comments also added on the rules for +signature declaration, functor specification and functor declaration +in the static semantics for modules for the same purpose. +(2 June 88, mt) + +\item +The sentence stating that there are no derived forms form modules (first page +in the introduction) has been replaced by a reference to Appendix A. +(6 June 88) + +\item +In Figure 2, Pats has been changed to Pat. (6 June 88) + +\item +A section ``Signature Matching'' has been inserted in the static +semantics for modules, after Section 5.10 (Enrichment). This defines +matching as a combination of instantiation and enrichment. +Also, the definition of functor matching in Section 5.13 has been +simplified using the notion of matching. (8 June 88, mt) + +\item +Section 6.2 (Simple Objects), below figure. The following has been deleted: +`` or of a failing attempt to handle an exception with a handle rule''. +(9 June 88) + +\item +Section 6.3, last paragraph. ``completely separately'' replaced by ``separately'', because of the new Section 8. (9 June 88) + +\item +Page 55, Version 1. Wrong heading ``Labelled Patterns'' replaced by +``Pattern Rows''. (9 June 88) + +\item +Page 40, Version 1. Heading ``Structure-level Bindings'' replace by +``Structure Bindings'' in accordance with page 15 and page 60. +(9 June 88) + +\item +Page, 64, Figure 18. The derived form for raise expression has been +deleted. (9 June 88) + +\item +Page 65, Figure 19. Wrong heading ``LABELLED PATTERNS'' has been replaced by +``PATTERN ROWS''. Moreove, in the same figure, ``TYPES'' has been +replaced by ``TYPE EXPRESSIONS''.(9 June 88) + +\item +In the display in Section 6.4 (Basic Values), the \verb+\+ has +been replace by \verb+/+ (division of reals). (13 June 88) + +\item +Section 2.5, the first sentence. A reference to Section 2.7 has been +added, since \verb+#+{\it lab} introduces a new lexical item. This has +been added to Section 2.7. (13 June 88) + +\item +Section 3. Since there are at present derived forms for functors, +the introduction to Section 3 has been changed. (13 June 88) + +\item +Rule 91 (Version 1) has been corrected. (The result part of +a functor signature resulting from the elaboration of a +functor signature expression must be principal).(14 June 88) + +\item +The heading ``Functor Signatures'' in Figure 20 (current version) +concerning derived forms has been replace by ``Functor Signature +Expressions''. Also, the compound ``functor signatures'' has +been replaced by ``functor signature expressions'' on the first +page of Appendix A (Derived Forms). (15 June 88) + +\item +We use the term ``constructor binding'' instead of ``datatype construction''. +The syntactic classes are renamed accordingly. + +\item +The title of the document has been changed to ``The definition +of Standard ML''. (15 June 88) + +\item +Appendix C, bottom of first page: \verb+io_failure+ has been changed to +\verb+Io+. (15 June 88) + +\item +Section 3.1 (Reseved Words, Syntax of Modules). The {\tt open} +has been removed since it is already in the core langugae. +(15 June 88) + +\item +Section 8. Changed ``store'' to ``state'' throughout. (16 June 88). + +\item +Syntax of the Core, Figure 2. Replaced ``type expression rows'' +by ``type-expression rows''. (17 June 88). + +\item +Page 75 (current version). Templates added at the top of Figure 26 and 27. +(17 June 88). + +\item +Section 7.1 (Reduced Syntax, Dynamic semantics of modules), first +item. The ``are omitted from exception bindings'' has been replaced +by ``are omitted from exception descriptions''. (20 June 88) +\end{enumerate} + +\item{24 June 88.}``The definition of Standard ML, Version 2''. +Most of the following changes are prompted by Robin's reading +of [21 June]. +\begin{enumerate} +\item +The preface to Version 2 has been revised following RM's notes (not +followed to the letter, however). (23 June 88) + +The term ``functor matching'' has been replaced by ``functor signature +matching'' throughout. (23 June 88) + +\item +The term ``store attribute'' has been replaced by ``imperative attribute''. +(23 June 88) + +\item +Page 44, rule 85 regarding type sharing. The premise corrected. $\theta$s +have been inserted. A comment to the rule has been inserted. This change +is also mentioned in the preface to Version 2. +(23 June 88) + +\item +The varible {\it exn}, which ranges over exception names, has been +renamed to {\it en}. (23 June 88) + +\item +The class Exn of exception names has been renamed to ExName. + (23 June 88) +\item +The variable {\it exns}, which ranges over finite sets of exception +names, has been renamed to {\it ens}. + (23 June 88) +\item +The class ExnSet of finite sets of exception names has been renamed +to ExNameSet in accordance with TyNameSet , NameSet and StrNameSet. + (23 June 88) +\item +The class BasExn of basic exception names has been renamed +to BasExName. + (23 June 88) +\end{enumerate} + +\item{July 19} Several small changes to June 24. +\begin{enumerate} +\item The ``definition'' changed to ``Definition'' in the title of the +document (also in the preface to Version 2). The title has been moved +to the front. Page numbering is changed, page 1 is the first page of +Section 1. + +\item \# introduced as keyword and allowed in symbolic identifiers. + +\item A comment about consistency added for the type sharing rule. + +\item Subscripts 1 and 2 interchanged in the last paragraph of Section +5.11. +\end{enumerate} + +\item{1 August 88.} Several minor changes to July 19, as listed in +the annotated copy of the latter as detailed in 4 handwritten sheets +of paper. + +Two copies printed on the Plw16 3 August 88. +\end{description} + +\newpage +\begin{center} \bf 1989 \end{center} +\vspace{1cm} +\begin{description} +\item{4 April 89} Began changes towards ``The definition of Standard ML, Version 3'', +starting from Version 2. (Page refs to version 2) +\begin{enumerate} +\item Changed version number in title to 3 and date to 1 May 89. +\item Did the corrections of the errata with modifications indicated in +``MORE CORRECTIONS''. +\item Several changes to the two first paragraphs of page 81. +\item Small changes on pages iv, v, 4, 5 ( * is excluded from TyCon ), 7, +11, 14, 19, 31 (remark to the effect that change of bound names does +not change arity or equality attribute), 32 (change of the definition +of consistency), 36, 39, 41, 48, 61, 62, 63, 65, 66, 67, 68, 72, 73, 74, 77, +79, 80, 81, 88 as marked in ``MORE CORRECTIONS''. +\end{enumerate} +\item{5 April 89} More corrections: +\begin{enumerate} +\item Introduced the basic exceptions Abs and Neg, pages 46, 74, 87 and 92. +\item Replaced all occurrences of `keyword' by `reserved word', pages 6 and 10. +\item To avoid that the parsing of \quad local in end \quad declarations + interact with the requirement that there be no free imperative type + variables, the side condition on rule 55 (structure-level declarations) + has been moved to the rules for top-level declarations (rules 96--98). + See pages 37, 42, 43, 91, 93 and 96. +\item Clarification concerning the disambiguation in parsing inserted + in Appendix B, page 66. +\item The rules for the use of the reserved word {\tt op} have + been clarified, see page 6. +\item A new section ``Core language Programs'' has been added at the + end of Section 8, see page 62. +\end{enumerate} +\item{6 April '89} More corrections: +\begin{enumerate} +\item Introduced syntax for long and short identifiers. Pages + 4, 91, 92, 94 +\item Type constraints on non-expansive expressions are allowed + and do not make the expression expansive (page 20). +\item Section 2.9 (Syntactic Restrictions), page 8, last bullet: + The function expression on the right-hand side of a recursive + value binding is allowed to be constrained by type constraints. +\item A new subsection ``Type Explication'' has been inserted in the + static semantics of modules, after Section 5.7, page 33. +\item Other changes concerning type explication: Comment added in + Section 5.8, page 33; comment added in Section 5.11, page 34. +\item Small correction in the second and third paragraph of the comment + on the rule for functor application (page 37). +\item New inference rule for signature expressions added (page 38). +\item Rule 60 concerning structure bindings (page 38) altered so + as to make sure that the signature expression elaborates to + a type-explicit signature. +\item Similar change to rule 66 concerning signature bindings (page 39). + The comment adjusted accordingly. +\item Similar change to rule 91 concerning functor signature + expressions (page 42). Comment added. +\item Similar change to rule 95 concerning functor bindings (page 42). + The comment adjusted accordingly. +\item Several changes to make sure that {\tt op} does not occur in + signatures. Details are as follows: +\item A new syntactic class ConDesc of constructor descriptions has + been introduced (page 11). +\item The syntax for specifications (Figure 7, page 13) has been modified + by changing the syntax of data descriptions and introducing a + rule for constructor descriptions. +\item The syntactic restriction (page 12, second bullet) has been + extended to include constructor descriptions. +\item An optional {\tt op} has been included in the syntax for + exception bindings, page 8 and 68. +\item Rule 81 concerning Datatype Descriptions has been adjusted + to the new syntax. Page 40. +\item New rule for static semantics of constructor descriptions has + been added after rule 81. +\item Constructor descriptions added to the list in the third bullet + of Section 7.1 (page 55). +\item Introduction of special constants (scon and Scon); many changes: +\item Indtroduce scon and Scon (pages 3, 88, 93, 94). +\item Syntax for scon as atomic expression introduced (page 8). +\item Syntax for scon as atomic pattern introduced (page 9). +\item Added paragraph at the end of 4.1 (page 16) giving types + to special constants. +\item Added new rule for scon as atomic expression before rule 1 + (page 23) +\item Added new rule for scon as atomic pattern after rule 32 + (page 28). +\item Introduced special values (sv and SVal), page 44 and Figure 13, + page 45. +\end{enumerate} +\item{7 April '89,} More changes: +\begin{enumerate} +\item New rule for special constants as atomic expressions added, page 48, + before rule 99. +\item Two new rules for special constants as atomic pattern added, page 52, + after rule 135. +\item scon included in the grammar for atomic expressions (page 67) and + atomic patterns (page 69). +\item Last blob of Figure 23, page71, concerning the types of special + constants has been deleted. (These types are given by the function + called type). +\item Figure 25, page 72, modified so that the constructor environments + of int, real and string become empty. +\item Small insertion on page 74, firt para., first line. +\item The blob on equality, page 75, rewritten. +\item Page 46, several replacements of mathematical = sign by ML = sign. +\item page 2, l.3, small correction. +\item page 5, Section 2.5, line 2, small correction. +\item page 5, Section 2.6, l -2: insert : ``(Note that qualified identifiers + never have infix status.)'' +\end{enumerate} +\item{10 Apr 89} Late 7 Apr I printed a version with the corrections +so far (including many changes to the index) all of which are marked +in ``MORE CORRECTIONS''. Checking the changes, led to more corrections: +(references now to the version printed 7 April). +\begin{enumerate} +\item Several changes in index.ml (the ML program) so that entries + are collapsed to intervals, when possible and so that intervals + will not be trivial. +\item page 4, Sec. 3.4, line 7 : ``The qualified identifiers'' +\item page 30, Sec. 4.11, bullet 2, line 1: {\tt |}, twice +\item page 33, line -3, ``is type-explicit and every name in $N_1$ occurs + in $S_1$'' +\item page 34, line -2, same change +\item page 37, line 4, ``is type-explicit and N subseteq names $S_f$'' +\item page 39, rule for signature bindings, conclusion: repl. + $(N)S$ by $\Sigma$. +\item page 40, rule for seq. spec, second premise: change subscript + from 1 to 2. +\item page 43, comment on rule for Functor Bindings, l4 ``can match (N)S + (assuming N subseteq names S).'' +\item page 45, Sec. 6.1, last bullet: change variables to classes (also + in index) +\item page 54, comments: ``because of rule 142, rule '' +\item page 55, comments: ``because of rule 142, rule '' +\item page 56, Sec. 7.1, last bullet, change variables to classes (also + in index). +\item page 60, rule for local spec, second premise: change 1 to 2 +\item page 64, bullet 3: ``syntax class of declarations {\it dec}'' +\item page 89, entry for $\{\ \}$ in pattern: change 53 to 54. +\item page 91, entry for condesc: add 56 +\item page 91, entry for ConDesc: add 56 +\item page 91, entry for constructor description: add 56 +\item page 91, entry for core language programs: move below subitems +\item page 92, entry for equality: change basics value and identifier + to of values +\item page 92, entry for equality of type function: insert 41 +\item page 92, entry for exception constant as atomic pattern: change + 53 to 53-54. +\item page 93, entry for FAIL: add 54 +\item page 94, entry for identifier, long: insert 64 +\item page 94, entry for imptyvars: replace 43-43 by 43 +\item page 95, entry for open: add 40 +\item page 96, entry for polymorphic references: repl. 43-43 by 43 +\item page 96, entry for polymorphic exceptions: repl. 43-43 by 43 +\item page 96, entry for (r) record : repl. 53 by 54 +\item page 96, entry for record (r): repl. 53 by 54 +\item page 96, entry for record as atomic pattern: repl. 53 by 54 +\item page 97, entry for signature (Sigma), delete extra 35 +\item page 99, entry for type variable, imperative: replace 43-43 by 43 +\end{enumerate} +\item{11 April 89} More changes +\begin{enumerate} +\item Changed index.ml so that an interval of pages from i to i+1 is + printed i, i+1 (rather than i--i+1). +\item page 93, entry for FAIL: add 52 +\item page 96, entry for polymorphic exceptions: repl. 43-41 by 41, 43 +\item page 96, entry for pattern matching: repl. 45, 47-30 by 30, 45,47 +\end{enumerate} +\item{14 April '89} Changes to the version printed 7--11 April, following +Robin's annotations. +\begin{enumerate} +\item page iii, several minor changes. +\item page vi, item 15: yet an attempt to get rid of blanks +\item page 1, several minor changes. +\item page 3, Section 2.2 (Special Constants), third paragraph, after first +sentence; insert: +``We assume an underlying alphabet of 256 different characters (numbered +0 to 255) which is such that the characters with numbers 0 to 127 coincide +with the ASCII character set.'' +\item page 3, Section 2.2 (Special Constants), fourth line of display; replace + line by: +\begin{quote} + ddd The single character with number ddd (3 decimal digits + denoting an integer in the interval [0,255]). +\end{quote} +\item page 4, removed the recent definition of short identifiers +\item page 6, line 2 and 4: similar adjustments +\item page 94, entry for identifier: replace ``short'' by ``qualified'' +\item page 12, Section 3.5, second bullet: replace condesc by datdesc. +\item page 30, Section 4.11, second bulled, line 1: use cdots +\item page 32, Section 5.3: change the definition of well-formed + signature. +\item page 33, Section 5.9, line -4: delete ``and every name in N1 + occurs in S1'' +\item page 34, Section 5.12, line -2: same change +\item page 37, comment (55): delete ``and N subseteq names Sf'' + + + +\item page 38: replace ``must elaborate'' by ``is elaborated'' +\item page 43, comment on (99): delete ``(assuming N subseteq names S)'' +\item page 45, line -6: replace second ``denoted by'' by ``written'' +\item page 47, Section 6.5 : more space in display +\item page 54, rule 149 (paraenthesised pattern): change VE to VE/FAIL + both in the premise and in the conclusion. +\item page 62, line -9: replace ``ranged over BDyn'' by ``and let us + use BDyn to range over DynamicBasis.'' +\item page 63, line 9: replace ``).'' by ``.)'' +\item page 64, bullet 4.: delete ``short'' and end the sentence + ``, i.e. omit qualified identifiers''. +\item page 66, Figure 15, entry for {\tt if}: number subsexpression 1, 2 and 3. +\item page 68, line -2: ``Suppose the lexical sequence'' +\item page 68--89: use cdots +\item page 69, line 1: ``where $\exp$ stands for a lexical sequence which + is already determined as a subphrase (if necessary by applying the + precedence rule).'' +\item page 78, bullet for equality: small adjustments +\item page 89, entry for = : first ref made into an entry by itself +\item page vi, item 15: yet another attempt to get rid of blanks!!!! +\item the index: replace ``coersion'' by ``coercion'' (twice) + + +\item page 77, bullet for chr(i); replace by: +\begin{quote} + chr(i) returns the character numbered i (see Section 2.2) + if i is in the interval [0, 255], and the packet [Chr] otherwise. +\end{quote} +\item page 78, bullet for ord(s); replace by: +\begin{quote} + ord(s) returns the number of the first character in s (an integer + in the interval [0,255], see Section 2.2), or the packet [Ord] + if s is empty. +\end{quote} +\end{enumerate} +\end{description} +\begin{description} +\item{8 May 89} Tiny corrections: +\begin{enumerate} +\item page iii, middle: replace ``overriden'' by ``overridden''. +\item page 1, par. beginning ``A further factoring'', second sentence: +new punctuation. +\item page 4, Sect. 2.4: replace ``identifers'' by ``identifiers''. +\item page 32, Sect. 5.2: replace reference to the concept of disjoining +names (which was deleted earlier) by its definition. +\item page 47, Sect. 6.5, third line after display: ``The exception +(Io,s)''. Similar on page 79. +\item page 54, topmost comments: start with ``(142),(145),(147)'' +\item page 66, Fig. 15, entry for {\tt if}: correct indices on the +right-hand side {\tt case} form. +\item page 79, entry for end of stream: slightly revised description. +\end{enumerate} +\end{description} +\begin{center} +\large Version 4 (for publication) +\end{center} +\begin{description} +\item{25 July 89} +\begin{enumerate} +\item Page 3. Several small changes to clarify what printable characters +are and what \verb+\^+$c$ means. +\item Page5, last par. of Sect. 2.4. The word ``parser'' has been +replace by ``compiler'' as the classification of variables, +value constructors and exception constructors cannot be done +in normal context free parsing (the scope of constructors is more +conveniently dealt with during type checking). +\item Page 9, Fig. 4. For uniformity, has been allowed in front +of longcon and longexcon in atpat. +\item Page 21--22. Section 4.9 has been substantially revised +in reaction to Simon Finn's comments on the well-formedness +of type structures. There are new concepts of type structures +being well-formed and of type structures and type environments +respecting equality. Rules 19 and 20 have been given as side +condition that TE respect equality. The comments to these +rules have been revised accordingly. +\item Page 33, Sect. 5.3. The two first lines, which referred to +the well-formedness of type environenments, have been deleted. +item Page 35, Sect.5.13. The definition of principal signatures +has been modified to allude to structures respecting equality. +\item Page 72. Inserted in front of constants and exception +constants in atomic patterns. +\item Index: inserted entries for \verb;^;, control charater and printable +character. Also entries for respecting equality. Entry for well-formed +type environments deleted. +\end{enumerate} +\item{27 July} More changes +\begin{enumerate} +\item Page 2. Last paragraph of the Introduction has been rewritten. +\item Pages 3--4. Slanted font for defined terms in Section 2 (integer +constant, real constant, string constant, comment and identifiers). +\item Page 21. The title of Sect. 4.9 has been shortened to +``Type Structures and Type Environments''. +\item Page 33. Sect. 5.5 has been modified to require the {\sl +combined} admissibility of the basis and the result of the elaboration. +\item Page 35. Section on Principal Signatures has been extended to +cover the notion of a basis {\sl covering} a structure. This is +needed in order to get signatures. In Version 3 there are {\sl not} +principal signatures, due to examples like +\begin{quote} +\begin{verbatim} +structure A = + struct + structure B1 = struct end + structure B2 = struct end + end +structure A: sig structure B1: sig end end = A; +signature Sig = + sig + structure A1 : sig structure B1: sig end + structure B2: sig end + end + sharing A1 = A + end; +\end{verbatim} +\end{quote} +\end{enumerate} +\item{3 August, more changes:} +\begin{enumerate} +\item Page 2. `in the basis' repl. by `against the background provided' +\item Page 2, last paragraph about `claims' adjusted +\item Page 23, side conditions in slant. +\item Page 17, Remark about $\cup$ before figure +\item Page 21, $con(v)$ repl. by $(con,v)$. Definition of `respecting equality' added. +Definition of what it means for $TE$ to maximise equality added. +\item Page 25: repl. `respects' by `maximises' in rules 19,20 +\item Page 34, Sect. 5.9: repl. `we claim' by `it can be shown' +\item Page 35, Sect. 5.12: repl. `we claim' by `it can be shown' +\item Page 35, Sect. 5.13: {\bf Principal signatures rewritten} +\item Page 38, rule 65, repl. `principal' by `equality-principal' +\item Page 30, end of Sect. 4.12, slight rephrasing +\item Page 47, line -5, `nil' made teletype +\item Page 39, rule 69: slight change to mention equality principal +\item Page 43, rule 99: slight change to mention equality principal +\end{enumerate} +\item{4 August, more changes:} +\begin{enumerate} +\item End of Sect. 4.9: Replace Abs(E,TE) by Abs(TE,E) twice. Replace E+Abs(TE) +by Abs(TE)+E. Sililar change in rule 20. +\item replace `implementor' by `implementer' throughout. +\item page 26, comment on rule 20: page reference changed from 21 to 22. +\item page 35, small corrections to `Principal Signatures' +\item Index: several changes. +\end{enumerate} +\item{10 August 1989, More corrections; page numbers refer to version 3} +\begin{enumerate} +\item Robin's new preface has replaced the previous three prefaces. +\item page 30, Section 4.12. Local definition of enrichment for +the core language has been inserted. Also two new index entries. +Also shortening of Sect. 4.11 to fit it all in one page. +\item Page 37, inserted `for dec' in rule 57 +\item page 40, repl. hypotesis by hypotesis. +\item page 40, insert $m_i$ in comment to rule 79. +\item page 51, comment on rules 112-118: deleted last line ', so v will be +$\ldots$ ' +\item Sect. 5.5 about admissibility has been strengthened to require +the admissibility of entire proofs, as far as signature elaborations +are concerned. +\item Sect. 5.13 about Principal signatures: items 1 and 2 have +been shortened. +\end{enumerate} +\item 21 August 89 (after camera-ready had been sent) +\begin{enumerate}Changed Sigma_0 to Sigma on page 36 in the +definition of equality-principal signature. Robin sent that page +to Prior. +\end{enumerate} +\end{description} +\begin{description} +\item{4 Sept 89}, page 3, section 2.2, second par. line 4. Removed the ++ in front of 3.32E5. Also decreased hoffset by 8mm to get centering +on page. +\end{document} diff --git a/preface.tex b/preface.tex new file mode 100644 index 0000000..329f3d1 --- /dev/null +++ b/preface.tex @@ -0,0 +1,227 @@ +\section*{Preface} +A precise description of a programming language is a prerequisite for its +implementation and for its use. The description can take many forms, +each suited to a different purpose. A common form is a reference manual, +which is usually a careful narrative description of the meaning of each +construction in the language, often backed up with a formal presentation +of the grammar (for example, in Backus-Naur form). +This gives the programmer enough +understanding for many of his purposes. But it is ill-suited for use +by an implementer, or by someone who wants to formulate laws for +equivalence of programs, or by a programmer who wants to design programs with +mathematical rigour. + +This document is a formal description of both the {\sl grammar} and the +{\sl meaning} of a language which is both designed for large projects and +widely used. As such, it aims to serve the whole community of people +seriously concerned with the language. At a time when it is increasingly +understood that programs must withstand rigorous analysis, particular for +systems where safety is critical, a rigorous language presentation is even +important for negotiators and contractors; for a robust program +written in an insecure language is like a house built upon sand. + + +Most people have not looked at a rigorous language presentation before. +To help them particularly, but also to put the present work in perspective +for those more theoretically prepared, it will be useful here to say something +about three things: the nature of Standard ML, the task of language definition +in general, and the form of the present Definition. + +\subsubsection*{Standard ML} +Standard ML is a functional programming language, in the sense that the +full power of mathematical functions is present. But it grew in response +to a particular programming task, for which it was equipped also +with full imperative power, and a sophisticated exception mechanism. +It has an advanced form of parametric modules, aimed at organised +development of large programs. Finally it is strongly typed, and it was +the first language to provide a particular form of polymorphic type which +makes the strong typing remarkably flexible. This combination of +ingredients has not made it unduly large, but their novelty has been +a fascinating challenge to semantic method (of which we say more below). + +ML has evolved over fourteen +years as a fusion of many ideas from many people. This evolution is +described in some detail in Appendix E of the book, where also we +acknowledge all those who have contributed to it, both in design +and in implementation. + +`ML' stands for +{\sl meta language}; this is the term logicians use for a language in which +other (formal or informal) languages are discussed and analysed. +Originally ML was conceived as a medium for finding and performing +proofs in a logical language. Conducting rigorous argument as dialogue +between person and machine has been a strong research interest at Edinburgh +and elsewhere, throughout these fourteen years. The difficulties are enormous, +and make stern demands +upon the programming language which is used for this dialogue. Those who are +not familiar with computer-assisted reasoning may be surprised that a +programming language, which was designed for this rather esoteric activity, +should ever lay claim to being {\sl generally} useful. +On reflection, they should not be surprised. LISP is a prime example of +a language invented for esoteric purposes and becoming widely used. LISP +was invented for use in artificial intelligence (AI); the important thing +about AI here is not that it is esoteric, but that +it is difficult and varied; so much so, that anything which works well for +it must work well for many other applications too. + +The same can be said about the initial purpose of ML, but with a different +emphasis. Rigorous proofs are complex things, which need varied +and sophisticated presentation -- particularly on the screen in interactive +mode. Furthermore the proof methods, or +strategies, involved are some of the most complex algorithms which we know. +This all applies equally to AI, but one demand is made more strongly +by proof than perhaps by any other application: the demand for rigour. + +This demand established the character of ML. In order to be sure that, +when the user and the computer claim to have together performed a rigorous +argument, their claim is justified, it was seen +that the language must be strongly typed. On the other hand, to be +useful in a difficult application, the type system had to be rather +flexible, and permit the machine to guide the user rather than impose +a burden upon him. A reasonable solution was found, in which the machine +helps the user significantly by +inferring his types for him. Thereby the machine also confers complete +reliability on his programs, in this sense: +If a program claims that a certain result +follows from the rules of reasoning which the user has supplied, then the +claim may be fully trusted. + +The principle of inferring useful structural information about programs +is also represented, at the level of program modules, by the inference of +{\sl signatures}. +Signatures describe the interfaces between modules, and are vital for robust +large-scale programs. When the user combines modules, the signature +discipline prevents him from mismatching their interfaces. By programming +with interfaces and parametric modules, it becomes possible to focus on the +structure of a large system, and to compile parts of it in isolation from +one another -- even when the system is incomplete. + +This emphasis on types and signatures has had a profound effect on the +language Definition. Over half this document is devoted to inferring types +and signatures for programs. But the method used is exactly the same as for +inferring what {\sl values} a program delivers; indeed, a type or signature is +the result of a kind of abstract evaluation of a program phrase. + +In designing ML, +the interplay among three activities -- language design, definition and +implementation -- was extremely close. This was particularly true for the +newest part, the parametric modules. This part of the language grew from an +initial proposal by David MacQueen, itself highly developed; but both +formal definition and implementation had a strong influence on the detailed +design. In general, those who took part in the three activities cannot now +imagine how they could have been properly done separately. + +\subsubsection*{Language Definition} +Every programming language presents its own conceptual view of +computation. This view is usually indicated by the names used for the phrase +classes of the language, or by its keywords: terms like package, module, +structure, exception, channel, type, procedure, reference, sharing, \ldots. +These terms also have their abstract counterparts, which may be called +{\sl semantic objects}; these are what people really have in mind when they use +the language, or discuss it, or think in it. Also, it is these objects, +not the syntax, which represent the particular conceptual view of each +language; they are the character of the language. Therefore a definition +of the language must be in terms of these objects. + +As is commonly done in programming language semantics, we shall loosely +talk of these semantic objects as {\sl meanings}. Of course, it is +perfectly possible to understand the semantic theory of a language, and +yet be unable to to understand the meaning of a particular program, in the +sense of its {\sl intention} or {\sl purpose}. The aim of a language +definition is not to formalise everything which could possibly be called the +meaning of a program, but to establish a theory of semantic objects +upon which the understanding of particular programs may rest. + +The job of a language-definer is twofold. First -- as we have already +suggested -- he must create a world of meanings appropriate for the language, +and must find a way of saying +what these meanings precisely are. Here, he meets a problem; notation +of {\sl some} kind must be used to denote and describe these meanings -- +but not a {\sl programming language} notation, unless he is passing the +buck and defining one programming language in terms of another. Given +a concern for rigour, mathematical notation is an obvious choice. Moreover, +it is not enough just to +write down mathematical definitions. The world of meanings only becomes +meaningful if the objects possess nice properties, which make them tractable. +So the language-definer really has to develop a small {\sl theory} of his +meanings, in the same way that a mathematician develops a theory. +Typically, after initially defining some objects, the mathematician goes on to +verify properties which indicate that they are objects worth studying. +It is this part, a kind of scene-setting, which the language-definer shares +with the +mathematician. Of course he can take many objects and their theories +directly from mathematics, such as functions, relations, +trees, sequences, \ldots. But he must also give some special theory for the +objects which make his language particular, as we do for types, structures and +signatures in this book; otherwise his language definition may be +formal but will give no insight. + +The second part of the definer's job is to define {\sl evaluation} precisely. +This means that he must define at least {\sl what} meaning, $M$, results +from evaluating any phrase $P$ of his language (though he need not explain +exactly {\sl how} the meaning results; that is he need not give the full +detail of every computation). This part of his job must be formal +to some extent, if only because the phrases $P$ of his language are indeed +formal objects. But there is another reason for formality. The task is +complex and error-prone, and therefore demands a high level of explicit +organisation (which is, largely, the meaning of `formality'); moreover, +it will be used to specify an equally complex, error-prone and formal +construction: an implementation. + +We shall now explain the keystone of our semantic method. First, we need a +slight but important refinement. A phrase $P$ is never evaluated {\sl in +vacuo} to a meaning $M$, but always {\sl against a background}; this +background -- call it $B$ -- is itself a semantic object, +being a distillation of the meanings +preserved from evaluation of earlier phrases (typically variable declarations, +procedure declarations, etc.). In fact evaluation is background-dependent +-- $M$ depends upon $B$ as well as upon $P$. + +The keystone of the method, then, is a certain kind of assertion about +evaluation; it takes the form +\[ B\vdash P\Rightarrow M\] +and may be pronounced: `Against the background $B$, the phrase $P$ evaluates +to the meaning $M$'. {\sl The formal purpose of this Definition is no more, +and no less, than to decree exactly which assertions of this form are true.} +This could be achieved in many ways. We have chosen to do it in a structured +way, as others have, by giving rules which allow assertions about a +{\sl compound} phrase $P$ to be inferred from assertions about its +{\sl constituent} phrases $P_1,\ldots,P_n$. + +\subsubsection*{The form of the Definition\footnote{ + The Definition has evolved through a sequence of three previous versions, + circulated as Technical Reports. For those who have followed the + sequence, we should point out that the treatment of {\sl equality types} + and of {\sl admissibility} has been slightly modified in this publication + to meet the claim for principal signatures. The changes are mainly + in Sections~4.9, 5.5 and 5.13 and in the inference rules~19, 20, + 29 and 65.}} +We have written the Definition in a form suggested by the previous remarks. +That is, we have defined our semantic objects in mathematical +notation which is completely independent of Standard ML, and we have +developed just enough of their theory to give sense to our rules of +evaluation. + Following another suggestion above, we have factored our task +by describing {\sl abstract} evaluation -- the inference and checking of +types and signatures (which can be done at compile-time) -- completely +separately from {\sl concrete} evaluation. +It really is a factorisation, because a {\sl full} value in all its glory -- +you can think of it as a concrete object with a type +attached -- never has to be presented. + + The resulting document is, we hope, valuable as the essential point of +reference for Standard ML. If it is to play this role well, it must +be supplemented by other literature. Some expository books have already been +written, and this Definition will be useful as a +background reference for their readers. We have also become convinced, while +writing the Definition, that we could not discuss many questions without +making it far too long. Such questions are: Why were certain design choices +made? What are their implications for programming? +Was there a good alternative meaning for some constructs, or was our +hand forced? What different forms of phrase are equivalent? What is the proof +of certain claims? Many of these +questions will not be answered by pedagogic texts either. So we are writing +a Commentary on the Definition which will assist people in reading it, and +which will serve as a bridge between the Definition and other texts. +\begin{flushright} Edinburgh\\August 1989 \end{flushright} + diff --git a/prog.tex b/prog.tex new file mode 100644 index 0000000..c3d5316 --- /dev/null +++ b/prog.tex @@ -0,0 +1,129 @@ +\section{Programs} +\label{prog-sec} +The phrase class Program of programs is defined as follows +\[\program ::= \longprog\] + +Hitherto,\index{64.1} the semantic rules have not exposed the interactive +nature of the language. +During an ML session the user can type in a phrase, more +precisely a phrase of the form $\topdec$ as defined in Figure~\ref{prog-syn}, +page~\pageref{prog-syn}. Upon the following semicolon, +the machine will then attempt to parse, elaborate and +evaluate the phrase returning either a result or, if any +of the phases fail, an error message. +The outcome is significant for what the user subsequently types, +so we need to answer questions such as: if the elaboration +of a top-level declaration succeeds, but its evaluation +fails, then does the result of the elaboration get +recorded in the static basis? + +In practice, ML implementations may provide a directive as +a form of top-level declaration for including +programs from files rather than directly from the terminal. +In case a file consists of a sequence of top-level declarations +(separated by semicolons) and the machine detects an error in one of these, +it is probably sensible to abort the execution of the directive. +Rather than introducing a distinction between, +say, batch programs and interactive programs, we shall tacitly regard +all programs as interactive, and leave to implementers to +clarify how the inclusion of files, if provided, affects the +updating of the static and dynamic basis. +Moreover, we shall focus on elaboration and evaluation and leave the +handling of parse errors to implementers (since it naturally depends +on the kind of parser being employed). Hence, in this section the +{\sl execution} of a program means the combined elaboration +and evaluation of the program. + +So far, for simplicity, we have used the same notation $\B$ +to stand for both a static and a dynamic basis, and this has +been possible because we have never needed to discuss static +and dynamic semantics at the same time. +In giving the semantics of programs, however, let us rename as +\mbox{StaticBasis} the class Basis defined in the static +semantics of modules, Section~\ref{statmod-sem-obj-sec}, +and let us use $\Bstat$ to range over StaticBasis. Similarly, let +us rename as \mbox{DynamicBasis} the class Basis defined in the +dynamic semantics of modules, Section~\ref{dynmod-comp-obj-sec}, +and let us use $\Bdyn$ to range over \mbox{DynamicBasis}. +We now define +\[\B\ {\rm or} \ (\Bstat,\Bdyn)\in{\rm Basis}={\rm Static Basis} +\times {\rm DynamicBasis}.\] +Further, we shall use $\tsstat$ for elaboration as defined in +Section~\ref{statmod-sec}, and $\tsdyn$ for evaluation +as defined in Section~\ref{dynmod-sec}. +Then $\ts$ will be reserved for the execution of +programs, which thus is expressed by a sentence of the +form +\[\s,\B\ts\program\ra\B',\s'\] +This may be read as follows: +starting in basis $\B$ with state $\s$ the execution of +$\program$ results in a basis $\B'$ and a state $\s'$. + +It\index{64.2} must be understood that executing a program never results in an +exception. If the evaluation of a $\topdec$ yields an exception +(for instance because of a $\RAISE$ expression or external intervention) then +the result of executing the program ``$\topdec\ \mbox{\ml{;}}$'' is the +original basis together with the state which is in force when the exception is +generated. In particular, the exception convention\index{65.1} of +Section~\ref{dyncor-inf-rules-sec} +is not applicable to the ensuing rules. + +We represent the non-elaboration of a top-level declaration by\linebreak +$\ldots\tsstat\topdec\not\ra$. (This covers also the case in which a +user interrupts the elaboration.) + +\rulesec{Programs}{\s,\B\ts\program\ra\B',s'} +\begin{equation} % failing elaboration +\label{fail-elab-prog-rule} +\frac{\of{\Bstat}{\B}\tsstat\topdec\not\ra\qquad + \langle\s,\B\ts\program\ra\B',s'\rangle} + {\s,\B\ts\longprog\ra\B\langle'\rangle,s\langle'\rangle}\index{65.2} +\end{equation} + +\begin{equation} % evaluation raising exception +\label{dyn-exc-prog-rule} +\frac{\begin{array}{lr} + \of{\Bstat}{\B}\tsstat\topdec\ra\Bstat^{(1)} & \\ + \s,\of{\Bdyn}{\B}\tsdyn\topdec\ra\p,\s' & + \langle\s',\B\ts\program\ra\B',\s''\rangle + \end{array}} + {\s,\B\ts\longprog\ra\B\langle'\rangle,\s'\langle'\rangle} +\end{equation} + +\begin{equation} % success +\label{success-prog-rule} +\frac{\begin{array}{ll} + \of{\Bstat}{\B}\tsstat\topdec\ra\Bstat^{(1)} & \\ + \s,\of{\Bdyn}{\B}\tsdyn\topdec\ra\Bdyn^{(1)},s'& + \B'=\B\oplus(\Bstat^{(1)},\Bdyn^{(1)})\\ + & \langle\s',\B'\ts\program\ra\B'',s''\rangle + \end{array} + } + {\s,\B\ts\longprog\ra\B'\langle'\rangle,\s'\langle'\rangle} +\end{equation} +\comments +\begin{description} +\item{(\ref{fail-elab-prog-rule})} + A failing elaboration has no effect whatever. +\item{(\ref{dyn-exc-prog-rule})} + An evaluation which yields an exception nullifies +the change in the static basis, but does not +nullify side-effects on the state which may have occurred +before the exception was raised. +\end{description} +\subsection*{Core language Programs} +A\index{65.4} program is called a {\sl core language program\/} if it can be +parsed in the reduced grammar defined as follows: +\begin{enumerate} +\item Replace the definition of top-level declarations by +\[\topdec\ ::=\ \strdec\] +\item Replace the definition of structure-level declarations by +\[\strdec\ ::=\ \dec\] +\item Omit\index{65.5} the {\OPEN} declaration from the syntax class of +declarations $\dec$ +\item Restrict the long identifier classes to identifiers, i.e. +omit qualified identifiers. +\end{enumerate} +This means that several components of a basis, for example the +signature and functor environments, are irrelevant to the execution +of a core language program. \ No newline at end of file diff --git a/root.tex b/root.tex new file mode 100644 index 0000000..6678269 --- /dev/null +++ b/root.tex @@ -0,0 +1,115 @@ +% this is file `root', the root of the whole semantics +\documentclass[a4,12pt,twoside]{article} +\title{The Definition of Standard ML} +\author{Robin Milner \and Mads Tofte \and Robert Harper \\ +Laboratory for Foundations of Computer Science\\ +Department of Computer Science\\ +University of Edinburgh} +%Edinburgh EH9 3JZ, Scotland} +\date{%\today} +} +\include{mac} % macros +\makeindex +% +%\includeonly{intro,syncor,statcor,statmod} +%for agfa: \voffset -12mm +%4 Sept. 89, for lw16: +\advance\hoffset by -8mm +\begin{document} +\pagestyle{empty} +\maketitle +\cleardoublepage +\pagestyle{plain} +\setcounter{page}{3} +\renewcommand{\thepage}{\roman{page}} +\include{preface} +\tableofcontents +\cleardoublepage +\pagestyle{headings} +\setcounter{page}{1} +\renewcommand{\thepage}{\arabic{page}} +\include{intro} +\include{syncor} +\include{synmod} +\include{statcor} +\include{statmod} +\include{dyncor} +\include{dynmod} +\include{prog} +\appendix +\include{app1} +\include{app2} +\include{app3} +\include{app4} +\include{app5} +%\include{index} +\end{document} + + HOW TO REVISE THE INDEX + +The index is made using partly LaTex and partly an ML progam; +the latter is found on the file ``index.ml''. + +When LaTex is run on input ``root.tex'' it produces a file ``root.idx''. +Each line in this file is of the form + + \indexentry{idxkey}{pageref} + +where idxkey is a key inserted precisely one place in the document +(in the form of a LaTex command \index{idxkey}) +and pageref is the page number of the page LaTex was printing +by the time it encountered the \index{idxkey} command. + +A typical idxkey is 45.1 , which will occur in the TeX file +somewhere near what produces page 45 in the final document. +In fact, when the keys were first inserted in the TeX file, +45.1 would be the first key on page 45, but as the document changes, +one cannot get the pageref from the idxkey simple by taking the +prefix of the idxkey up to the full stop. + +There are many entries in the index that refer to the same +idxkey. Thus the number of idxkeys has been kept relatively +small, typically 2 or 3 pr page. The basic idea, then, is that +there is an ML program (on file ``index.ml'') which +associates entries in the final index with idxkeys by +a sequence of expressions + + ....... + item ``handle'' [p``45.4'',``57.3''to``59.1'',p``78.2'']; + item ``{\\it happiness}'' [p''38.1'']; + ...... + +The program will first build a conversion table from idxkeys +(such as ``45.4'') to page references by reading thrugh +``root.idx''. Then it will evaluate all the item and subitem +expressions. The item function produces a line in the +latex file (``index.tex'') using the conversion table. +Thus the above lines may produce + + ........... + \item ``handle'' 46, 57--58, 78 + \item {\it happiness} 38 + ........... + +If insertion of more text in the source files result in +new page splits, then one should manually check that +the item expressions in ``index.ml'' refer to the +right idxkeys. It may be necessary to change some of the +lists in the item expressions and it may be desirable to +insert new \index commands in the source text. However, +if we for simplicity assume that we simply insert new +material corresponding to a new chapter (not affecting +the page splits in other chapters) then one would proceed +as follows: +First add new item expressions in the index.ml file corre- +sponding to new entries in the index (one will have new +\index commands in the new input, of course). Then one +runs latex on ``root.tex'' to produce the ``root.idx'' file. +Then one runs index.ml (enter ML and type use ``index.ml''). +Then one runs latex on root again, this time giving the +correct index. + + + + + diff --git a/rootagfa.tex b/rootagfa.tex new file mode 100644 index 0000000..4bff938 --- /dev/null +++ b/rootagfa.tex @@ -0,0 +1,114 @@ +% this is file `root', the root of the whole semantics +\documentstyle[a4,12pt,twoside]{article} +\title{The Definition of Standard ML\\ Version 3} +\author{Robert Harper \and Robin Milner \and Mads Tofte \\ +Laboratory for Foundations of Computer Science\\ +Department of Computer Science\\ +University of Edinburgh\\ +Edinburgh EH9 3JZ, Scotland} +\date{1 May 1989} +\include{mac} % macros +\makeindex +% +%\includeonly{syncor} +\voffset -12mm +\begin{document} +\pagestyle{empty} +\maketitle +\cleardoublepage +\pagestyle{plain} +\setcounter{page}{3} +\renewcommand{\thepage}{\roman{page}} +\include{preface3} +\include{preface2} +\include{preface1} +\tableofcontents +\cleardoublepage +\pagestyle{headings} +\setcounter{page}{1} +\renewcommand{\thepage}{\arabic{page}} +\include{intro} +\include{syncor} +\include{synmod} +\include{statcor} +\include{statmod} +\include{dyncor} +\include{dynmod} +\include{prog} +\appendix +\include{app1} +\include{app2} +\include{app3} +\include{app4} +\include{app5} +\include{index} +\end{document} + + HOW TO REVISE THE INDEX + +The index is made using partly LaTex and partly an ML progam; +the latter is found on the file ``index.ml''. + +When LaTex is run on input ``root.tex'' it produces a file ``root.idx''. +Each line in this file is of the form + + \indexentry{idxkey}{pageref} + +where idxkey is a key inserted precisely one place in the document +(in the form of a LaTex command \index{idxkey}) +and pageref is the page number of the page LaTex was printing +by the time it encountered the \index{idxkey} command. + +A typical idxkey is 45.1 , which will occur in the TeX file +somewhere near what produces page 45 in the final document. +In fact, when the keys were first inserted in the TeX file, +45.1 would be the first key on page 45, but as the document changes, +one cannot get the pageref from the idxkey simple by taking the +prefix of the idxkey up to the full stop. + +There are many entries in the index that refer to the same +idxkey. Thus the number of idxkeys has been kept relatively +small, typically 2 or 3 pr page. The basic idea, then, is that +there is an ML program (on file ``index.ml'') which +associates entries in the final index with idxkeys by +a sequence of expressions + + ....... + item ``handle'' [p``45.4'',``57.3''to``59.1'',p``78.2'']; + item ``{\\it happiness}'' [p''38.1'']; + ...... + +The program will first build a conversion table from idxkeys +(such as ``45.4'') to page references by reading thrugh +``root.idx''. Then it will evaluate all the item and subitem +expressions. The item function produces a line in the +latex file (``index.tex'') using the conversion table. +Thus the above lines may produce + + ........... + \item ``handle'' 46, 57--58, 78 + \item {\it happiness} 38 + ........... + +If insertion of more text in the source files result in +new page splits, then one should manually check that +the item expressions in ``index.ml'' refer to the +right idxkeys. It may be necessary to change some of the +lists in the item expressions and it may be desirable to +insert new \index commands in the source text. However, +if we for simplicity assume that we simply insert new +material corresponding to a new chapter (not affecting +the page splits in other chapters) then one would proceed +as follows: +First add new item expressions in the index.ml file corre- +sponding to new entries in the index (one will have new +\index commands in the new input, of course). Then one +runs latex on ``root.tex'' to produce the ``root.idx'' file. +Then one runs index.ml (enter ML and type use ``index.ml''). +Then one runs latex on root again, this time giving the +correct index. + + + + + diff --git a/statcor.tex b/statcor.tex new file mode 100644 index 0000000..f826fa1 --- /dev/null +++ b/statcor.tex @@ -0,0 +1,1134 @@ +\section{Static Semantics for the Core} +Our\index{20.1} first task in presenting the semantics -- whether for Core or Modules, +static or dynamic -- is to define the objects concerned. In addition +to the class of {\em syntactic} objects, which we have already defined, +there are classes of so-called {\em semantic} objects used to describe +the meaning of the syntactic objects. Some classes contain {\em simple} +semantic objects; such objects are usually identifiers or names of some +kind. Other classes contain {\em compound} semantic objects, such as +types or environments, which are constructed from component objects. + +\subsection{Simple Objects} +All semantic objects in the static semantics of the entire +language are built from identifiers and two further kinds of simple objects: +type constructor names and structure names. +Type constructor names are the values taken by type constructors; we shall +usually refer to them briefly as type names, but they are to be clearly +distinguished from type variables and type constructors. +Structure names play an active role only in +the Modules semantics; they enter the Core semantics only because +they appear in structure environments, which (in turn) are needed in the Core +semantics only to determine the values of long identifiers. The simple object +classes, and the variables ranging over them, are shown in +Figure~\ref{simple-objects}. We have included $\TyVar$ in the table to +make visible the use of $\alpha$ in the semantics to range over $\TyVar$.\index{20.2} + +\vspace{-7mm} +\begin{figure}[h] +\vspace{2pt} +\begin{displaymath} +\begin{array}{rclr} +\alpha\ {\rm or}\ \tyvar & \in & \TyVar & \mbox{type variables}\\ +\t & \in & \TyNames & \mbox{type names}\\ +\m & \in & \StrNames & \mbox{structure names} +\end{array} +\end{displaymath} +\caption{Simple Semantic Objects} +\label{simple-objects} +%\vspace{3pt} +\end{figure} + +Each\index{20.3} $\alpha \in\TyVar$ possesses a boolean {\sl equality} attribute, +which determines whether or not it {\sl admits equality}, i.e. whether +it is a member of EtyVar (defined on page~\pageref{etyvar-lab}). +%-- in which case we +%also say that it is an {\sl equality} type variable. +%poly +Independently hereof, each $\alpha$ possesses a boolean attribute, +the {\sl imperative} attribute, which determines whether it is imperative, +i.e. whether it is a member of $\ImpTyVar$ (defined on page~\pageref{etyvar-lab}) +or not. + +Each $\t\in\TyNames$ has +an arity $k\geq 0$, and also possesses an equality attribute. +We denote the class of type names with arity $k$ by $\TyNamesk$. + +With\index{20.35} each special constant {\scon} we associate a type +name $\scontype(\scon)$ which is either {\INT}, {\REAL} or {\STRING} +as indicated by Section~\ref{cr:speccon}. + +\subsection{Compound Objects} +When\index{20.4} $A$ and $B$ are sets $\Fin A$ denotes the set of finite subsets of $A$, +and $\finfun{A}{B}$ denotes the set of {\sl finite maps} (partial functions +with finite domain) from $A$ to $B$. +The domain\index{21.1} and range of a finite map, $f$, are denoted $\Dom f$ and +$\Ran f$. +A finite map will often be written explicitly in the form $\kmap{a}{b}, +\ k\geq 0$; +in particular the empty map is $\emptymap$. +We shall use the form $\{x\mapsto e\ ;\ \phi\}$ -- a form of set +comprehension -- to stand for the finite map $f$ whose domain +is the set of values $x$ which satisfy the condition $\phi$, and +whose value on this domain is given by $f(x)=e$. + +When $f$ and $g$ are finite maps the map $\plusmap{f}{g}$, called +$f$ {\sl modified} by $g$, is the finite map with domain +$\Dom f \cup \Dom g$ and values +\[(\plusmap{f}{g})(a) = \mbox{if $a\in\Dom g$ then $g(a)$ else $f(a)$.} +\] + +The compound objects for the static semantics of the Core Language are +shown in Figure~\ref{compound-objects}. +We take $\cup$ to mean disjoint union over +semantic object classes. We also understand all the defined object +classes to be disjoint. + +\begin{figure}[h] +%\vspace{2pt} +\begin{displaymath} +\begin{array}{rcl} + \tau &\in &\Type = \TyVar\cup\RecType\cup\FunType + \cup\ConsType\\ + \longtauk\ {\rm or}\ \tauk + & \in & \Type^k\\ + \longalphak\ {\rm or}\ \alphak + & \in & \TyVar^k\\ + \varrho & \in & \RecType = \finfun{\Lab}{\Type} \\ + \tau\rightarrow\tau' + & \in & \FunType = \Type\times\Type \\ + & & \ConsType = \cup_{k\geq 0}\ConsType^{(k)}\\ + \tauk\t & \in & \ConsType^{(k)} = \Type^k\times\TyNamesk \\ +\typefcn\ {\rm or}\ \typefcnk + & \in & \TypeFcn = \cup_{k\geq 0}\TyVar^k\times\Type\\ +\tych\ {\rm or}\ \longtych + & \in & \TypeScheme = \cup_{k\geq 0}\TyVar^k\times\Type\\ +\S\ {\rm or}\ (\m,\E) + & \in & \Str = \StrNames\times\Env \\ +(\theta,\CE) & \in & \TyStr = \TypeFcn\times\ConEnv\\ +\SE & \in & \StrEnv = \finfun{\StrId}{\Str}\\ +\TE & \in & \TyEnv = \finfun{\TyCon}{\TyStr}\\ +\CE & \in & \ConEnv = \finfun{\Con}{\TypeScheme}\\ +\VE & \in & \VarEnv = \finfun{(\Var\cup\Con\cup\Exn)}{\TypeScheme}\\ +\EE & \in & \ExnEnv = \finfun{\Exn}{\Type}\\ +\E\ {\rm or}\ \longE{} + & \in & \Env = \StrEnv\times\TyEnv\times\VarEnv + \times\ExnEnv\\ +\T & \in & \TyNameSets = \Fin(\TyNames)\\ +\U & \in & \TyVarSet = \Fin(\TyVar)\\ +\C\ or\ \T,\U,\E & \in & \Context = \TyNameSets\times\TyVarSet\times\Env +\end{array} +\end{displaymath} +\caption{Compound Semantic Objects\index{21.2}} +\label{compound-objects} +%\vspace{3pt} +\end{figure} + + +Note that $\Lambda$\index{21.3} and $\forall$ bind type variables. For any semantic object +$A$, $\TyNamesFcn A$ and $\TyVarsFcn A$ denote respectively the set of +type names and the set of type variables occurring free in $A$. +Moreover, $\imptyvars A$ and $\apptyvars A$ denote respectively the set +of imperative type variables and the set of applicative +type variables occurring free in $A$.\index{21.4} +\subsection{Projection, Injection and Modification} +\label{stat-proj}\index{22.1} +{\bf Projection}: We often need to select components of tuples -- for example, +the variable-environment component of a context. In such cases we +rely on variable names to indicate which component +is selected. For instance ``$\of{\VE}{\E}$'' means ``the variable-environment +component +of $\E$'' and ``$\of{\m}{\S}$'' means ``the structure name of $\S$''. + +Moreover, when a tuple contains a finite map we shall ``apply'' the +tuple to an argument, relying on the syntactic class of the argument to +determine the relevant function. For instance $\C(\tycon)$ means +$(\of{\TE}{\C})\tycon$. + +A particular case needs mention: $\C(\con)$ is taken to stand for +$(\of{\VE}{\C})\con$; similarly, $\C(\exn)$ is taken to stand for +$(\of{\VE}{\C})\exn$. + The type scheme of a value constructor is +held in $\VE$ as well as in $\TE$ (where it will be recorded within +a $\CE$); similarly, the type of an exception constructor is held in +$\VE$ as well as in $\EE$. +Thus the re-binding of a constructor of either kind is given proper +effect by accessing it in $\VE$, rather than in $\TE$ or in $\EE$. + +Finally, environments may be applied to long identifiers. +For instance if $\longcon = \strid_1.\cdots.\strid_k.\con$ then +$\E(\longcon)$ means +\[ (\of{\VE} + {(\of{\SE} + {\cdots(\of{\SE} + {(\of{\SE}{\E})\strid_1} + )\strid_2\cdots} + )\strid_k} + )\con. +\] + +{\bf Injection}: Components may be injected into tuple classes; for example,\linebreak +``$\VE\ \In\ \Env$'' means the environment +$(\emptymap,\emptymap,\VE,\emptymap)$. + +{\bf Modification}: The modification of one map $f$ by another map $g$, +written $f+g$, has already been mentioned. It is commonly used for +environment modification, for example $\E+\E'$. Often, empty components +will be left implicit in a modification; for example $\E+\VE$ means +$\E+(\emptymap,\emptymap,\VE,\emptymap)$. For set components, modification +means union, so that $\C+(\T,\VE)$ means +\[ (\ (\of{\T}{\C})\cup\T,\ \of{\U}{\C},\ (\of{\E}{\C})+\VE\ ) \] +Finally, we frequently need to modify a context $\C$ by an environment $\E$ +(or a type environment $\TE$ say), +at the same time extending $\of{\T}{\C}$ to include the type names of $\E$ +(or of $\TE$ say). +We therefore define $\C\oplus\TE$,\index{22.2} for example, to mean +$\C+(\TyNamesFcn\TE,\TE)$. + +\subsection{Types and Type functions} +\label{tyfun-sec} +A type $\tau$ is an {\sl equality type},\index{22.3} or {\sl admits equality}, if it is +of one of the forms +\begin{itemize} +\item $\alpha$, where $\alpha$ admits equality; +\item $\{\lab_1\mapsto\tau_1,\ \cdots,\ \lab_n\mapsto\tau_n\}$, + where each $\tau_i$ admits equality; +\item $\tauk\t$, where $t$ and all members of $\tauk$ admit equality; +\item $(\tau')\REF$.\index{23.1} +\end{itemize} +\label{tyfcn-lab} +A type function $\theta=\Lambda\alphak.\tau$\index{23.2} + has arity $k$; it must be +{\sl closed} -- i.e. +$\TyVarFcn(\tau)\subseteq\alphak$ -- and the bound variables must +be distinct. Two type functions are considered equal +if they only differ in their choice of bound variables (alpha-conversion). +In particular, the equality attribute has no significance in a +bound variable of a type function; for example, $\Lambda\alpha.\alpha\to +\alpha$ and $\Lambda\beta.\beta\to\beta$ are equal type functions +even if $\alpha$ admits equality but $\beta$ does not. +%poly +Similarly, the imperative attribute has no significance +in the bound variable of a type function. +If $t$ has arity $k$, then we write $t$ to mean $\Lambda\alphak.\alphak\t$ +(eta-conversion); thus $\TyNames\subseteq\TypeFcn$. $\theta=\Lambda\alphak.\tau$ +is an {\sl equality} type function, or {\sl admits equality}, if when the +type variables $\alphak$ are chosen to admit equality then $\tau$ also admits +equality. + +We write the application of a type function $\theta$ to a vector +$\tauk$ of types as $\tauk\theta$. +If $\theta=\Lambda\alphak.\tau$ we set $\tauk\theta=\tau\{\tauk/\alphak\}$ +(beta-conversion). + +We write $\tau\{\thetak/\tk\}$ for the result of substituting type +functions $\thetak$ for type names $\tk$ in $\tau$. +We assume that all beta-conversions +are carried out after substitution, so that for example +\[(\tauk\t)\{\Lambda\alphak.\tau/\t\}=\tau\{\tauk/\alphak\}.\] +%poly +\label{imp-ty-lab} +A type is {\sl imperative} if all type variables occurring in it are +imperative. +\subsection{Type Schemes} +\label{type-scheme-sec} +A type scheme $\tych=\forall\alphak.\tau$\index{23.3} + {\sl generalises} a type $\tau'$, +written $\tych \succ\tau'$, +if $\tau'=\tau\{\tauk/\alphak\}$ for some $\tauk$, where each member $\tau_i$ +of $\tauk$ admits equality if $\alpha_i$ does, +%poly +and $\tau_i$ is imperative if $\alpha_i$ is imperative. +If $\tych'=\forall\beta^{(l)}.\tau'$ then $\tych$ {\sl generalises} $\tych'$, +written $\tych\succ\tych'$, if $\tych\succ\tau'$ and $\beta^{(l)}$ contains +no free type variable of $\tych$. +It can be shown that $\tych\succ\tych'$ iff, for all $\tau''$, whenever +$\tych'\succ\tau''$ then also $\tych\succ\tau''$. + +Two type schemes $\tych$ and $\tych'$ are considered equal +if they can be obtained from each other by +renaming and reordering of bound type variables, and deleting type +variables from the prefix which do not occur in the body. +Here, in contrast to the case for type functions, the equality attribute +must be preserved in renaming; for example $\forall\alpha.\alpha\to\alpha$ +and $\forall\beta.\beta\to\beta$ are only equal if either both $\alpha$ +and $\beta$ admit equality, or neither does. +%poly +Similarly, the imperative attribute of a bound type variable of a +type scheme {\sl is} significant. +It can be shown that $\tych=\tych'$ iff $\tych\succ\tych'$ and +$\tych'\succ\tych$. + +We consider a type $\tau$ to be a type scheme, identifying it with +$\forall().\tau$. + +\subsection{Scope of Explicit Type Variables} +\label{scope-sec} + +In\index{23.10} the Core language, a type or datatype binding can +explicitly introduce type variables whose scope is that binding. +In the modules, a description of a value, type, or datatype +may contain explicit type variables whose scope is that +description. However, we\index{23.11} still have to account for the +scope of an explicit type variable occurring in the ``\ml{:} $\ty$'' +of a typed expression or pattern +or in the ``\ml{of} $\ty$'' of an exception binding. For the rest +of this section, we consider such occurrences of type variables only. + +Every occurrence of a value declaration is said to +{\sl scope} a set of explicit type variables determined as follows. + + + +%Every explicit type variable $\alpha$ is {\sl scoped at} a value binding +%which is determined as follows. + +First, an occurrence of $\alpha$ in a value declaration $\valdec$ is said +to be {\sl unguarded} if the occurrence is not part of a smaller value +declaration within $\valbind$. +In this case we say that $\alpha$ {\sl occurs unguarded} in the +value declaration. + +Then we say that $\alpha$ is {\sl scoped at} a particular occurrence +$O$ of $\valdec$ in a program if +(1) $\alpha$ occurs unguarded in this value declaration, and +(2) $\alpha$ does not occur unguarded in any larger value declaration +containing the occurrence $O$.\label{scope-def-lab} + +Hence, associated with every occurrence of a value declaration there is +a set $\U$ of the explicit type variables that are scoped at that +occurrence. One may think of each occurrence of $\VAL$ as being implicitly +decorated with such a set, for instance: + +\vspace*{3mm} +\halign{\indent$#$&$#$&$#$\cr +\mbox{$\VAL_{\{\}}$ \ml{x = }}&\mbox{\ml{(}}& +\mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id1:'a->'a = fn z=>z in Id1 Id1 end,}}\cr +& &\mbox{\ml{let $\VAL_{\{\mbox{\ml{'a}}\}}$ Id2:'a->'a = fn z=>z in Id2 Id2 end)}}\cr +\noalign{\vspace*{3mm}} +\mbox{$\VAL_{\{\mbox{\ml{'a}}\}}$ \ml{x = }}&\mbox{\ml{(}}& +\mbox{\ml{let $\VAL_{\{\}}$ Id:'a->'a = fn z=>z in Id Id end,}}\cr +& &\mbox{\ml{fn z=> z:'a)}}\cr} + +According to the inference rules in Section~\ref{stat-cor-inf-rules} +the first example can be elaborated, but the second cannot since \ml{'a} +is bound at the outer value declaration leaving no possibility of two +different instantiations of the type of \ml{Id} in the application +\ml{Id Id}. + + + +\subsection{Non-expansive Expressions} +\label{expansive-sec} +In\index{23.4} order to treat polymorphic references and exceptions, +the set Exp of expressions is partitioned into two classes, the {\sl +expansive} and the {\sl non-expansive} expressions. Any variable, +constructor and $\FN$ expression, possibly constrained by one or more +type expressions, is non-expansive; all other expressions are said to +be expansive. The idea is that the dynamic evaluation of a +non-expansive expression will neither generate an exception nor extend +the domain of the memory, while the evaluation of an expansive +expression might. + +\subsection{Closure} +\label{closure-sec} +Let\index{24.2} $\tau$ be a type and $A$ a semantic object. Then $\cl{A}{(\tau)}$, +the {\sl closure} of $\tau$ with respect to $A$, is the type scheme +$\forall\alphak.\tau$, where $\alphak=\TyVarFcn(\tau)\setminus\TyVarFcn A$. +Commonly, $A$ will be a context $\C$. +We abbreviate the {\sl total} closure $\cl{\emptymap}{(\tau)}$ to +$\cl{}{(\tau)}$. +If the range of a variable environment $\VE$ contains only types (rather than +arbitrary type schemes) we set +\[\cl{A}{\VE}=\{\id\mapsto\cl{A}{(\tau)}\ ;\ \VE(\id)=\tau\}\] +with a similar definition for $\cl{A}{\CE}$. + +\label{clos-def-lab} +Closing\index{24.3} a variable environment $\VE$ that stems from +the elaboration of a value binding $\valbind$ requires extra +care to ensure type security of references and exceptions and correct +scoping of explicit type variables. +Recall that $\valbind$ is not allowed to bind the +same variable twice. Thus, for each $\var\in\Dom\VE$ +there is a unique \mbox{\pat\ \ml{=} \exp} +in $\valbind$ which binds $\var$. +If $\VE(\var)=\tau$, let +$\cl{\C,\valbind}{\VE(\var)}=\longtych$, where +\[\alphak=\cases{\TyVarFcn\tau\setminus\TyVarFcn\C,&if $\exp$ + is non-expansive;\cr + \apptyvars\tau\setminus\TyVarFcn\C,&if $\exp$ is expansive.} +\] +%(Explicit type variables necessitate a slight strengthening of the requirements +%which a type variable must satisfy in order to be bound: a type variable +%occurring unguarded in $\valbind$ can be admitted among $\alphak$ only +%if it is scoped at the particular occurrence of $\valbind$ at which +%the closure operation is performed.) + +Notice that the form of $\valbind$ does not affect the binding of +applicative type variables, only the binding of imperative +type variables. + +\subsection{Type Structures and Type Environments} +\label{typeenv-wf-sec} +A type\index{24.4} structure $(\theta,\CE)$ is {\sl well-formed} if either +$\CE=\emptymap$, or $\theta$ is a type name $t$. +(The latter case arises, with $\CE\neq\emptymap$, in $\DATATYPE$ +declarations.) +All type structures occurring in elaborations are assumed to +be well-formed. + +A type structure $(\t,\CE)$ is said to +{\sl respect equality} if, whenever $\t$ admits equality, then +either $\t=\REF$ (see Appendix~\ref{init-stat-bas-app}) or, +for each $\CE(\con)$ of the form +$\forall\alphak.(\tau\rightarrow\alphak\t)$, +the type function $\Lambda\alphak.\tau$ also admits equality. +(This ensures that the equality +predicate ~{\tt =}~ will be applicable to a constructed value $(\con,v)$ of +type $\tauk\t$ only when it is applicable to the value $v$ itself, +whose type is $\tau\{\tauk/\alphak\}$.) +A type environment $\TE$ {\sl respects equality} if all its type +structures do so. + +Let $\TE$ be a type environment, and let $T$ be the set of type names +$\t$ such that $(\t,\CE)$ occurs in $\TE$ for some +$\CE\neq\emptymap$. Then $\TE$ is said to {\sl maximise equality} +if (a) $\TE$ respects equality, and also (b) if any larger subset of +$T$ were to admit equality (without any change in the equality +attribute of any type names not in $T$) then $\TE$ would cease to +respect equality. + + +For any $\TE$ of the form +\[\TE=\{\tycon_i\mapsto(t_i,\CE_i)\ ;\ 1\leq i\leq k\},\] +where no $\CE_i$ is the empty map, and for any $\E$ we define +$\Abs(\TE,\E)$ to\index{25.1} be the environment obtained from +$\E$ and $\TE$ as +follows. First, let $\Abs(\TE)$ be the type environment +$\{\tycon_i\mapsto(t_i,\emptymap)\ ;\ 1\leq i\leq k\}$ +in which all constructor +environments $\CE_i$ have been replaced by the empty map. +Let $t_1',\cdots,t_k'$ be new distinct type names none of which +admit equality. Then $\Abs(\TE,\E)$ is the result of simultaneously +substituting +$t_i'$ for $t_i$, $1\leq i\leq k$, throughout $\Abs(\TE)+\E$. +(The effect of the latter substitution is to ensure that the use of +equality on an $\ABSTYPE$ is restricted to the $\WITH$ part.) +\label{abs-lab} +\clearpage + +\subsection{Inference Rules} +\label{stat-cor-inf-rules} +Each rule\index{26.1} of the semantics allows inferences among sentences of the form +\[A\ts{\it phrase}\ra A'\] +where +$A$ is usually an environment or a context, {\it phrase} is a phrase of +the Core, and $A'$ is a semantic object -- usually a type or an +environment. It may be pronounced ``{\it phrase} elaborates to $A'$ in +(context or environment) $A$''. Some rules have extra hypotheses not of +this form; they are called {\sl side conditions}. + +In the presentation of the rules, phrases within single +angle brackets ~$\langle\ \rangle$~ are called {\sl +first options}, and those within double +angle brackets ~$\langle\langle\ \rangle\rangle$~ are called {\sl +second options}. To reduce the number of rules, we have adopted the +following convention: +\begin{quote} In each instance of a rule, the +first options must be either all present or all absent; +similarly the second options must be either all present or all absent. +\end{quote} + +Although not assumed in our definitions, it is intended that every +context $\C=\T,\U,\E$ has the property that $\TyNamesFcn\E\subseteq\T$. +Thus $\T$ may be thought of, loosely, as containing all type names +which ``have been generated''. It is necessary to include $\T$ as a +separate component in a context, since $\TyNamesFcn\E$ may not contain +all the type names which have been generated; one reason is that a +context $\T,\emptyset,\E$ is a projection of the basis +$\B=(\M,\T),\F,\G,\E$ whose other components $\F$ and $\G$ +could contain other such names -- recorded in $\T$ but not present in +$\E$. Of course, remarks about what ``has been generated'' are not +precise in terms of the semantic rules. But the following precise result +may easily be demonstrated: +\begin{quote} +Let S be a sentence +~$\T,\U,\E\ts{\it phrase}\ra A$~ such that +$\TyNamesFcn\E\subseteq\T$, +and let S$'$ be a sentence +~$\T',\U',\E'\ts{\it phrase}'\ra A'$~ +occurring in a proof of S; then also +$\TyNamesFcn\E'\subseteq\T'$. +\end{quote} + + + +% Atomic Expressions +% +\rulesec{Atomic Expressions\index{26.2}}{\C\vdash\atexp\ra\tau} +%\begin{figure}[h] + +\begin{equation} % special constant +\label{sconexp-rule} +\frac{} + {\C\ts\scon\ra\scontype(\scon)}\index{26.3} +\end{equation} + +\begin{equation} % value variable +\label{varexp-rule} +\frac{\C(\longvar)\succ\tau} + {\C\ts\longvar\ra\tau} +\end{equation} + +\begin{equation} % value constructor +\label{conexp-rule} +\frac{\C(\longcon)\succ\tau} + {\C\ts\longcon\ra\tau} +\end{equation} + +\begin{equation} % exception constant +%\label{exconexp-rule} +\frac{\C(\longexn)=\tau} + {\C\ts\longexn\ra\tau} +\end{equation} + +\begin{equation} % record expression +%\label{recexp-rule} +\frac{\langle\C\ts\labexps\ra\varrho\rangle} + {\C\ts\ttlbrace\ \recexp\ \ttrbrace\ra\emptymap\langle +\ \varrho\rangle{\rm\ in\ \Type}}\index{27.0} +\end{equation} + +\begin{equation} % local declaration +\label{let-rule} +\frac{\C\ts\dec\ra\E\qquad\C\oplus\E\ts\exp\ra\tau} + {\C\ts\letexp\ra\tau}\index{27.1} +\end{equation} + +\begin{equation} % paren expression +%\label{parexp-rule} +\frac{\C\ts\exp\ra\tau} + {\C\ts\parexp\ra\tau} +\end{equation} +\comments +\begin{description} +\item{(\ref{varexp-rule}),(\ref{conexp-rule})} +The instantiation of +type schemes allows different occurrences of a single $\longvar$ +or $\longcon$ to assume different types. +\item{(\ref{let-rule})} +The use of $\oplus$, here and elsewhere, ensures that +type names generated by the first sub-phrase are different from +type names generated by the second sub-phrase. +\end{description} + +\rulesec{Expression Rows}{\C\ts\labexps\ra\varrho} +\begin{equation} % expression rows +%\label{labexps-rule} +\frac{\C\ts\exp\ra\tau\qquad\langle\C\ts\labexps\ra\varrho\rangle} + {\C\ts\longlabexps\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{27.2} +\end{equation} +% Expressions +% +\rulesec{Expressions}{\C\ts\exp\ra\tau} +%\vspace{6pt} +%\fbox{$\C\ts\exp\ra\tau$} +\begin{equation} % atomic +\label{atexp-rule} +\frac{\C\ts\atexp\ra\tau} + {\C\ts\atexp\ra\tau}\index{27.3} +\end{equation} + +\begin{equation} % application +%\label{app-rule} +\frac{\C\ts\exp\ra\tau'\rightarrow\tau\qquad\C\ts\atexp\ra\tau'} + {\C\ts\appexp\ra\tau} +\end{equation} + +\begin{equation} % typed +\label{typedexp-rule} +\frac{\C\ts\exp\ra\tau\qquad\C\ts\ty\ra\tau} + {\C\ts\typedexp\ra\tau} +\end{equation} + +\begin{equation} % handle exception +%\label{handlexp-rule} +\frac{\C\ts\exp\ra\tau\qquad\C\ts\match\ra\EXCN\rightarrow\tau} + {\C\ts\handlexp\ra\tau} +\end{equation} + +\begin{equation} % raise exception +\label{raiseexp-rule} +\frac{\C\ts\exp\ra\EXCN} + {\C\ts\raisexp\ra\tau} +\end{equation} + +\begin{equation} % function +%\label{fnexp-rule} +\frac{\C\ts\match\ra\tau} + {\C\ts\fnexp\ra\tau} +\end{equation} +\comments +\begin{description} +\item{(\ref{atexp-rule})} +The relational symbol $\ts$ is overloaded for all syntactic classes (here +atomic expressions and expressions). +\item{(\ref{typedexp-rule})} +Here $\tau$ is determined by $\C$ and $\ty$. Notice that type variables +in $\ty$ cannot be instantiated in obtaining $\tau$; thus the expression +\verb+1:'a+ will not elaborate successfully, nor will the expression +\verb+(fn x=>x):'a->'b+. +The effect of type variables in an explicitly typed expression is +to indicate exactly the degree of polymorphism present in the expression.\index{27.4} +\item{(\ref{raiseexp-rule})} +Note that $\tau$ does not occur in the premise; thus a $\RAISE$ +expression has ``arbitrary'' type. +\end{description} +% Matches +% +\rulesec{Matches}{\C\ts\match\ra\tau} +\begin{equation} % match +%\label{match-rule} +\frac{\C\ts\mrule\ra\tau\qquad\langle\C\ts\match\ra\tau\rangle} + {\C\ts\longmatch\ra\tau}\index{28.1} +\end{equation} +\rulesec{Match Rules}{\C\ts\mrule\ra\tau} +\begin{equation} % mrule +%\label{mrule-rule} +\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C+\VE\ts\exp\ra\tau'} + {\C\ts\longmrule\ \ra\tau\rightarrow\tau'} +\end{equation} +\comment This rule allows new free type variables to enter +the context. These new type variables will be chosen, in effect, during +the elaboration of $\pat$ (i.e., in the inference of the first +hypothesis). In particular, their choice may have to be made to +agree with type variables present in any explicit type expression +occurring within $\exp$ (see rule~\ref{typedexp-rule}). + +% +% Declarations +% +\rulesec{Declarations}{\C\ts\dec\ra\E} +%poly +\begin{equation} % value declaration +\label{valdec-rule} +\frac{\plusmap{\C}{\U}\ts\valbind\ra\VE\qquad + \VE'=\cl{\C,\valbind}{\VE}\qquad + \U\cap\TyVarFcn\VE'=\emptyset} + {\C\ts\valdecS\ra\VE'\ \In\ \Env}\index{28.2} +\end{equation} +%from version 1, without polymorphic refs: +%\begin{equation} % value declaration +%\label{valdec-rule} +%\frac{\C\ts\valbind\ra\VE} +% {\C\ts\valdec\ra\cl{\C}{\VE}\ \In\ \Env} +%\end{equation} + +\begin{equation} % type declaration +%\label{typedec-rule} +\frac{\C\ts\typbind\ra\TE} + {\C\ts\typedec\ra\TE\ \In\ \Env} +\end{equation} + +\begin{equation} % datatype declaration +\label{datatypedec-rule} +\frac{\begin{array}{c} +\C\oplus\TE\ts\datbind\ra\VE,\TE\qquad + \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C}) \\ + \mbox{$\TE$ maximises equality} + \end{array} + } + {\C\ts\datatypedec\ra(\VE,\TE)\ \In\ \Env} +\end{equation} + +\begin{equation} % abstype declaration +\label{abstypedec-rule} +\frac{\begin{array}{rl} + \C\oplus\TE\ts\datbind\ra\VE,\TE\qquad & + \forall(\t,\CE)\in\Ran\TE,\ \t\notin(\of{\T}{\C})\\ + \C\oplus(\VE,\TE)\ts\dec\ra\E\qquad & + \mbox{$\TE$ maximises equality} + \end{array} + } + {\C\ts\abstypedec\ra\Abs(\TE,\E)} +\end{equation} + +\begin{equation} % exception declaration +\label{exceptiondec-rule} +\frac{\C\ts\exnbind\ra\EE\quad\VE=\EE } + {\C\ts\exceptiondec\ra(\VE,\EE)\ \In\ \Env } +\end{equation} + +\begin{equation} % local declaration +%\label{localdec-rule} +\frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2} + {\C\ts\localdec\ra\E_2}\index{28.3} +\end{equation} + +\begin{equation} % open declaration +%\label{open-dec-rule} +\frac{ \C(\longstrid_1)=(\m_1,\E_1) + \quad\cdots\quad + \C(\longstrid_n)=(\m_n,\E_n) } + { \C\ts\openstrdec\ra \E_1 + \cdots + \E_n } +\end{equation} + +\begin{equation} % empty declaration +%\label{emptydec-rule} +\frac{} + {\C\ts\emptydec\ra\emptymap\ \In\ \Env} +\end{equation} + +\begin{equation} % sequential declaration +%\label{seqdec-rule} +\frac{\C\ts\dec_1\ra\E_1\qquad\C\oplus\E_1\ts\dec_2\ra\E_2} + {\C\ts\seqdec\ra\plusmap{E_1}{E_2}} +\end{equation} +\comments +\begin{description} +\item{(\ref{valdec-rule})} +Here $\VE$ will contain types rather than general +type schemes. The closure of $\VE$ is exactly what allows variables to +be used polymorphically, via rule~\ref{varexp-rule}. + +Moreover, $\U$ is the set of explicit type variables scoped at this particular +occurrence of $\valdec$, cf. Section~\ref{scope-sec}, +page~\pageref{scope-def-lab}. The side-condition on $\U$ +ensures that these explicit type variables are bound by the closure operation. +On the other hand, no {\sl other} explicit type variable occurring +free in $\VE$ will become bound, since it must be in $\of{\U}{\C}$, and +is therefore excluded from closure by the definition of the closure operation +(Section~\ref{closure-sec}, page~\pageref{clos-def-lab}) +since $\of{\U}{\C}\subseteq\TyVarFcn\C$. +\item{(\ref{datatypedec-rule}),(\ref{abstypedec-rule})} +The side conditions +express that the elaboration of each datatype binding +generates new type names and that as many of these new names +as possible admit equality. Adding $\TE$ to the context on the left +of the $\ts$ captures the recursive nature of the binding. +%The side condition is +%the formal way of expressing that the elaboration of each datatype binding +%generates new type names. Adding $\TE$ to the context on the left +%of the $\ts$ captures the recursive nature of the binding. Recall that $\TE$ +%is assumed well-formed (as defined in Section~\ref{typeenv-wf-sec}). If +%$\TyNamesFcn(\of{\E}{\C})\subseteq\of{\T}{\C}$ and the side condition is +%satisfied then $\C\oplus\TE$ is well-formed. +\item{(\ref{abstypedec-rule})} +The $\Abs$ operation was defined in Section~\ref{typeenv-wf-sec}, page~\pageref{abs-lab}. +\item{(\ref{exceptiondec-rule})} +No closure operation is used here, since $\EE$ maps exception +names to types rather than to general type schemes. +Note that $\EE$ is also recorded in the {\VarEnv} component of +the resulting environment (see Section~\ref{stat-proj}, page~\pageref{stat-proj}).\index{29.0} +\end{description} + +% Bindings +% +\rulesec{Value Bindings}{\C\ts\valbind\ra\VE} +%\vspace{6pt} +\begin{equation} % value binding +\label{valbind-rule} +\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\exp\ra\tau\qquad + \langle\C\ts\valbind\ra\VE'\rangle } + {\C\ts\longvalbind\ra\VE\ \langle +\ \VE'\rangle}\index{29.1} +\end{equation} + +\begin{equation} % recursive value binding +\label{recvalbind-rule} +\frac{\C+\VE\ts\valbind\ra\VE} + {\C\ts\recvalbind\ra\VE} +\end{equation} +\comments +\begin{description} +\item{(\ref{valbind-rule})} +When the option is present we have $\Dom\VE\cap +\Dom\VE' = \emptyset$ by the syntactic restrictions.\index{29.2} +\item{(\ref{recvalbind-rule})} +Modifying $\C$ by $\VE$ on the left captures the +recursive nature of the binding. From rule~\ref{valbind-rule} we see that any +type scheme occurring in $\VE$ will have to be a type. Thus each use of a +recursive function in its own body must be ascribed the same type. +\end{description} + +\rulesec{Type Bindings}{\C\ts\typbind\ra\TE} +%\fbox{$\C\ts\typbind\ra\TE$} +\begin{equation} % type binding +%\label{typbind-rule} +\frac{\tyvarseq=\alphak\qquad\C\ts\ty\ra\tau\qquad + \langle\C\ts\typbind\ra\TE\rangle} + {\begin{array}{c} + \C\ts\longtypbind\ra\\ + \qquad\qquad\qquad + \{\tycon\mapsto(\typefcnk,\emptymap)\}\ \langle +\ \TE\rangle + \end{array} + }\index{29.3} +\end{equation} +\comment The syntactic restrictions ensure that the type function +$\typefcnk$ satisfies the well-formedness constraints of +Section~\ref{tyfun-sec} and they ensure $tycon\notin\Dom\TE$. + +\rulesec{Data Type Bindings}{\C\ts\datbind\ra\VE,\TE} +%\fbox{$\C\ts\datbind\ra\VE,\TE$} +\begin{equation} % datatype binding +%\label{datbind-rule} +\frac{\begin{array}{c} + \tyvarseq=\alphak\qquad\C,\alphakt\ts\constrs\ra\CE\\ + \langle\C\ts\datbind\ra\VE,\TE\qquad + \forall(\t',\CE)\in\Ran\TE, \t\neq\t'\rangle + \end{array} + } + {\begin{array}{c} + \C\ts\longdatbind\ra\\ + \qquad\qquad\qquad\cl{}{\CE}\langle +\ \VE\rangle,\ + \{\tycon\mapsto(\t,\cl{}{\CE})\}\ \langle +\ \TE\rangle + \end{array} + }\index{30.1} +\end{equation} +\comment The syntactic restrictions ensure $\Dom\VE\cap\Dom\CE = \emptyset$ +and $\tycon\notin\Dom\TE$. + +\rulesec{Constructor Bindings}{\C,\tau\ts\constrs\ra\CE} +%\fbox{$\C,\tau\ts\constrs\ra\CE$} +\begin{equation} % data constructors +%\label{constrs-rule} +\frac{\langle\C\ts\ty\ra\tau'\rangle\qquad + \langle\langle\C,\tau\ts\constrs\ra\CE\rangle\rangle } + {\begin{array}{c} + \C,\tau\ts\longerconstrs\ra\\ + \qquad\qquad\qquad\{\con\mapsto\tau\}\ + \langle +\ \{\con\mapsto\tau'\to\tau\}\ \rangle\ + \langle\langle +\ \CE\rangle\rangle + \end{array} + }\index{30.2} +\end{equation} +\comment By the syntactic restrictions $\con\notin\Dom\CE$. + +\rulesec{Exception Bindings}{\C\ts\exnbind\ra\EE} +%poly with polymorphic exceptions: +\begin{equation} % exception binding +\label{exnbind1-rule} +\frac{\langle\C\ts\ty\ra\tau\quad\mbox{$\tau$ is imperative}\rangle\qquad + \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle } + {\begin{array}{c} + \C\ts\longexnbinda\ra\\ + \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\ + \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\ + \langle\langle +\ \EE\rangle\rangle + \end{array} + }\index{30.3} +\end{equation} + +%with mono typed exceptions: +%\begin{equation} % exception binding +%\label{exnbind1-rule} +%\frac{\langle\C\ts\ty\ra\tau\quad\TyVarFcn(\tau)=\emptyset\rangle\qquad +% \langle\langle\C\ts\exnbind\ra\EE\rangle\rangle } +% {\begin{array}{c} +% \C\ts\longexnbinda\ra\\ +% \qquad\qquad\qquad\{\exn\mapsto\EXCN\}\ +% \langle +\ \{\exn\mapsto\tau\rightarrow\EXCN\}\ \rangle\ +% \langle\langle +\ \EE\rangle\rangle +% \end{array} +% } +%\end{equation} + +\vspace*{4mm} +\begin{equation} % exception binding +\label{exnbind2-rule} +\frac{\C(\longexn)=\tau\qquad + \langle\C\ts\exnbind\ra\EE\rangle } + {\C\ts\longexnbindb\ra\{\exn\mapsto\tau\}\ \langle +\ \EE\rangle} +% {\begin{array}{c} +% \C\ts\longexnbindb\ra\\ +% \qquad\qquad\qquad\{\exn\mapsto\tau\}\ +% \langle +\ \EE\rangle +% \end{array} +% } +\end{equation} +\comments +\begin{description} +\item{(\ref{exnbind1-rule})} Notice that $\tau$ must not contain +any applicative type variables.\index{30.35} +%with monotyped exceptions: +%\item{(\ref{exnbind1-rule})} Notice that $\tau$ must be a monotype +%(see also restriction~\ref{monotypes-res} in +%Section~\ref{further-restrictions-sec}). +\item{(\ref{exnbind1-rule}),(\ref{exnbind2-rule})} +There is a unique $\EE$, for each $\C$ and $\exnbind$, +%No matter which of the options are present, given $\C$ and $\exnbind$ there +%is at most one $\EE$ +such that $\C\ts\exnbind\ra\EE$. +\end{description} + +%\caption{Rules for Bindings} +%\end{figure} + +% Atomic Patterns +% +\rulesec{Atomic Patterns}{\C\ts\atpat\ra(\VE,\tau)} +%\vspace{6pt} +%\fbox{$\C\ts\atpat\ra(\VE,\tau)$} +\begin{equation} % wildcard pattern +%\label{wildcard-rule} +\frac{} + {\C\ts\wildpat\ra (\emptymap,\tau)}\index{30.4} +\end{equation} + +\begin{equation} % special constant in pattern +\frac{} + {\C\ts\scon\ra (\emptymap,\scontype(\scon))}\index{30.5} +\end{equation} + +\begin{equation} % variable pattern +\label{varpat-rule} +\frac{} + {\C\ts\var\ra (\{\var\mapsto\tau\},\tau) } +\end{equation} + +\begin{equation} % constant pattern +%\label{constpat-rule} +\frac{\C(\longcon)\succ\tauk\t } + {\C\ts\longcon\ra (\emptymap,\tauk\t)} +\end{equation} + +\begin{equation} % exception constant +%\label{exconapat-rule} +\frac{\C(\longexn)=\EXCN} + {\C\ts\longexn\ra (\emptymap,\EXCN)} +\end{equation} + + + +\begin{equation} % record pattern +%\label{recpat-rule} +\frac{\langle\C\ts\labpats\ra(\VE,\varrho)\rangle} + {\C\ts\lttbrace\ \recpat\ \rttbrace\ra(\ \emptymap\langle +\ \VE\rangle,\ \emptymap + \langle +\ \varrho\rangle\ \In\ \Type\ ) }\index{31.1} +\end{equation} + +\begin{equation} % parenthesised pattern +%\label{parpat-rule} +\frac{\C\ts\pat\ra(\VE,\tau)} + {\C\ts\parpat\ra(\VE,\tau)} +\end{equation} +\comments +\begin{description} +\item{(\ref{varpat-rule})} +Note that $\var$ can assume a type, not a general type scheme. +\end{description} + +\rulesec{Pattern Rows}{\C\ts\labpats\ra(\VE,\varrho)} +%\fbox{$\C\ts\labpats\ra(\VE,\varrho)$} +\begin{equation} % wildcard record +%\label{wildrec-rule} +\frac{} + {\C\ts\wildrec\ra(\emptymap,\varrho)}\index{31.2} +\end{equation} + +\begin{equation} % record component +\label{longlab-rule} +\frac{\C\ts\pat\ra(\VE,\tau)\qquad + \langle\C\ts\labpats\ra(\VE',\varrho)\qquad\lab\notin\Dom\varrho\rangle +} + {\C\ts\longlabpats\ra + (\VE\langle +\ \VE'\rangle,\ + \{\lab\mapsto\tau\}\langle +\ \varrho\rangle) } +\end{equation} +\comment +\begin{description} +\item{(\ref{longlab-rule})} + By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$. +\end{description} +% Patterns +% +%\begin{figure}[h] +%\label{pat-rules} +\rulesec{Patterns}{\C\ts\pat\ra(\VE,\tau)} +\begin{equation} % atomic pattern +%\label{atpat-rule} +\frac{\C\ts\atpat\ra (\VE,\tau)} + {\C\ts\atpat\ra (\VE,\tau)}\index{31.3} +\end{equation} + +\begin{equation} % construction pattern +%\label{conpat-rule} +\frac{\C(\longcon)\succ\tau'\to\tau\qquad\C\ts\atpat\ra(\VE,\tau')} + {\C\ts\conpat\ra (\VE,\tau)} +\end{equation} + +\begin{equation} % exception construction pattern +%\label{exconpat-rule} +\frac{\C(\longexn)=\tau\rightarrow\EXCN\qquad + \C\ts\atpat\ra(\VE,\tau)} + {\C\ts\exconpat\ra(\VE,\EXCN)} +\end{equation} + +\begin{equation} % typed pattern +%\label{typedpat-rule} +\frac{\C\ts\pat\ra(\VE,\tau)\qquad\C\ts\ty\ra\tau} + {\C\ts\typedpat\ra (\VE,\tau)} +\end{equation} + +\begin{equation} % layered pattern +\label{layeredpat-rule} +\frac{\begin{array}{c} + \C\ts\var\ra(\VE,\tau)\qquad\langle\C\ts\ty\ra\tau\rangle\\ + \C\ts\pat\ra(\VE',\tau) +%\qquad\VE\sim\VE' + \end{array} + } + {\C\ts\layeredpat\ra(\plusmap{\VE}{\VE'},\tau)} +\end{equation} +\comments +\begin{description} +\item{(\ref{layeredpat-rule})} +By the syntactic restrictions, $\Dom\VE\cap\Dom\VE' = \emptyset$. +\end{description} + + +% Type Expressions +\rulesec{Type Expressions}{\C\ts\ty\ra\tau} +\begin{equation} % atype variable +%\label{tyvar-rule} +\frac{\tyvar=\alpha} + {\C\ts\tyvar\ra\alpha}\index{32.1} +\end{equation} + +\begin{equation} % record type +%\label{rectype-rule} +\frac{\langle\C\ts\labtys\ra\varrho\rangle} + {\C\ts\lttbrace\ \rectype\ \rttbrace\ra\emptymap\langle +\ \varrho\rangle\ \In\ \Type} +\end{equation} + +\begin{equation} % constructed type +\label{constype-rule} +\frac{\begin{array}{c} + \tyseq=\ty_1\cdots\ty_k\qquad\C\ts\ty_i\ra\tau_i\ (1\leq i\leq k)\\ + \C(\longtycon)=(\theta,\CE) + \end{array} + } + {\C\ts\constype\ra\tauk\theta} +\end{equation} + +\begin{equation} % function type +%\label{funtype-rule} +\frac{\C\ts\ty\ra\tau\qquad\C\ts\ty'\ra\tau'} + {\C\ts\funtype\ra\tau\to\tau'} +\end{equation} + +\begin{equation} % parenthesised type +%\label{partype-rule} +\frac{\C\ts\ty\ra\tau} + {\C\ts\partype\ra\tau} +\end{equation} +\comments +\begin{tabbing} +(\ref{constype-rule}) \= Recall that for $\tauk\theta$ to be defined, $\theta$ +must have arity $k$. +\end{tabbing} + +\rulesec{Type-expression Rows}{\C\ts\labtys\ra\varrho} +%\fbox{$\C\ts\labtys\ra\varrho$} +\begin{equation} % record type components +%\label{longlabtys-rule} +\frac{\C\ts\ty\ra\tau\qquad\langle\C\ts\labtys\ra\varrho\rangle} + {\C\ts\longlabtys\ra\{\lab\mapsto\tau\}\langle +\ \varrho\rangle}\index{32.15} +\end{equation} +\comment The syntactic constraints ensure $\lab\notin\Dom\varrho$. +%\caption{Rules for Types} +%\end{figure} + +\subsection{Further Restrictions} +\label{further-restrictions-sec} +There\index{32.2} are a few restrictions on programs which should be enforced by a +compiler, but are better expressed apart from the preceding +Inference Rules. They are: +\begin{enumerate} +%poly +%The following restriction has been removed from Version 1 because +%of polymorphic references and exceptions +%\item \label{monotypes-res} +%The reference value constructor ~{\tt ref}~ may occur in patterns +%with polymorphic type, but in an expression it must always elaborate to +%a monotype, i.e. a type containing no type variables. +%Moreover, exception constructors can have monotypes only. +%These restrictions +%will be relaxed in future Versions, but some restrictions will always be +%necessary to ensure soundness of the type discipline. +\item For each occurrence of a record pattern containing a record wildcard, +i.e. of the form +%\begin{quote} +\verb+{+${\it lab}_1$\ml{=}$\pat_1$\ml{,}$\cdots$\ml{,}${\it lab}_m$\ml{=}$\pat_m$\ml{,}\verb+...}+ +%\end{quote} +the program context must determine uniquely the domain +$\{{\it lab}_1,\cdots,{\it lab}_n\}$ +of its record type, where $m\leq n$; thus, the context must +determine the labels $\{{\it lab}_{m+1},\cdots,{\it lab}_n\}$ of the fields +to be matched by the wildcard. For this purpose, an explicit type +constraint may be needed. This restriction is necessary to ensure the +existence of principal type schemes. +\item In a match of the form ${\it pat}_1$ \ml{=>} $\exp_1$ \ml{|}$\;\cdots\;$ +\ml{|} ${\tt pat}_n$ \ml{=>} $\exp_n$ +the pattern sequence $\pat_1,\ldots,\pat_n$ should be {\sl irredundant}; +that is, each $\pat_j$ must match some value +(of the right type) which is not matched by $\pat_i$ for any $i0)\] +of structure names such that, for each $i\ (0\leq i -> # +\end{verbatim} +\vspace*{-6pt} + +\subsection{Special constants} +\label{cr:speccon} +An\index{6.2} {\sl integer constant} +is any non-empty sequence of digits, possibly preceded +by a negation symbol (\verb+~+). +A {\sl real constant} is an integer constant, +possibly followed by a point ({\tt .}) and one or +more digits, possibly followed by an exponent symbol ~{\tt E}~ and an integer +constant; at least one of the optional parts must occur, hence no integer +constant is a real constant. +Examples: ~~{\tt 0.7}~~~{\tt 3.32E5}~~~\verb(3E~7(~~. Non-examples: +%Examples: ~~{\tt 0.7}~~~{\tt +3.32E5}~~~\verb(3E~7(~~. Non-examples: +%Examples: ~~{\tt 0.7}~~~{\tt +3.32E5}~~~{\tt 3E~}~~. Non-examples: +~~{\tt 23}~~~{\tt .3}~~~{\tt 4.E5}~~~{\tt 1E2.0}~~. + +We assume an underlying alphabet of 256 characters +(numbered 0 to 255) such that the characters with numbers +0 to 127 coincide with the ASCII character set. +A {\sl string constant} is a sequence, between quotes ({\tt "}), of zero or +more printable characters (i.e., numbered 33--126), spaces or escape +sequences. +Each escape sequence starts with the +escape character ~\verb+\+~, and stands for a character sequence. The +escape sequences are: +\smallskip + +%\begin{quote} +%\begin{tabular}{ll} +\halign{\indent#\hfil&\quad\parbox[t]{11cm}{\strut#\strut}\cr +\verb+\n+ & A single character interpreted by the system as +end-of-line.\cr +\verb+\t+ & Tab.\cr +\verb+\^+$c$ & The control character $c$, where $c$ may + be any character with number 64--95. The number + of ~{\tt\char'134\char'136}$c$~ is 64 less than the + number of $c$.\cr +\verb+\+$ddd$ & The single character with number $ddd$ (3 decimal digits +denoting an integer in the interval $[0,255]$).\cr +\verb+\"+ & {\tt "}\cr +\verb+\\+ & {\tt\char'134}\cr +\verb+\+$f\cdot\cdot f$\verb+\+ + & This sequence is ignored, + where $f\cdot\cdot f$ stands for a sequence + of one or more formatting characters.\cr +} +%\end{tabular} +%\end{quote} +\smallskip + +The {\sl formatting characters}\index{6.3} are a subset of the non-printable + characters including at least space, tab, newline, formfeed. +The last form allows long strings to be written on more than one line, by + writing ~\verb+\+~ at the end of one line and at the start of the + next.\nopagebreak + +We denote by {\SCon} the class of {\sl special constants}, i.e., the integer, +real, and string constants; we shall use {\scon} +to range over \SCon.\index{6.4} + +\subsection{Comments} +A\index{7.1} {\sl comment} +is any character sequence within comment brackets ~{\tt (* *)}~ +in which +comment brackets are properly nested. An unmatched comment bracket should be +detected by the compiler. + +% +\subsection{Identifiers} +\label{cyn-core-identifiers-sec} +The classes of {\sl identifiers}\index{7.2} for the Core are shown in +Figure~\ref{identifiers}. +\begin{figure} +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&(#)\hfil\tabskip1em&#\hfil\tabskip\@centering\cr +\Var & value variables & long\cr +\Con & value constructors & long\cr +\Exn & exception constructors& long\cr +\TyVar & type variables & \cr +\TyCon & type constructors & long\cr +\Lab & record labels & \cr +\StrId & structure identifiers & long\cr +} +\makeatother +\caption{Identifiers} +\label{identifiers} +\vspace*{-3mm} +\end{figure} +We use $\var$, $\tyvar$ to range over Var, TyVar etc. For each class +X marked ``long'' there is a class longX of {\sl long identifiers}; if +$x$ ranges over X then {\it longx} ranges over longX. The syntax of +these long identifiers is given by the following: +\vspace*{-6pt} +\begin{quote} +\begin{tabular}{rcll} {\it longx} & $::=$ & $x$ & identifier\\ +& &$\strid_1.\cdots.\strid_n.x$ & qualified identifier ($n\geq 1$) +\end{tabular} +\end{quote} +\vspace*{-6pt} +The qualified identifiers constitute a link between the Core and the +Modules. Throughout this document, the term ``identifier'', occurring +without an adjective, refers to non-qualified identifiers only. +%version 2: For each class X marked +%``long'' there is also a class +%\[ {\rm LongX} = \StrId^\ast \times {\rm X} \] +%If $x$ ranges over X, then {\it longx}, or +%$\strid_1.\cdots.\strid_k.x$, $k\geq 0$, ranges over LongX. +%These long identifiers constitute the only link between the Core +%and the language constructs for Modules; by omitting them, and the $\OPEN$ +%declaration, +%we obtain the Core as a complete programming language in +%its own right. (The corresponding adjustment to the Core static and +%dynamic semantics is simply to omit structure environments $\SE$.). + +An identifier is either {\sl alphanumeric}: any sequence of +letters, digits, primes ({\tt '}) and underbars (\wildpat) starting +with a letter or prime, or {\sl symbolic}: any non-empty sequence of the +following {\sl symbols}\index{7.3} +\vspace*{-6pt} +\begin{center} +%\verb(! % & $ + - / : < = > ? (@\verb( \ ~ ` ^ | *( +\verb(! % & $ # + - / : < = > ? @ \ ~ ` ^ | *( +\end{center} +\vspace*{-6pt} +In either case, however, reserved words are excluded. This means that for +example ~\verb+#+~ and ~{\tt |}~ are not identifiers, but ~\verb+##+~ and +~{\tt |=|}~ are identifiers. +The only exception to this rule is that the symbol ~{\tt =}~, which is +a reserved word, is also allowed as an identifier to stand for +the equality predicate. +The identifier ~{\tt =}~ may not be re-bound; +this precludes any syntactic ambiguity. + +A type variable $\tyvar$\index{7.4}\label{etyvar-lab} may be any +alphanumeric identifier starting with a prime; the subclass EtyVar of +TyVar, the {\sl equality} type variables, consists of those which +start with two or more primes. +%poly +The subclass $\ImpTyVar$ of +$\TyVar$, the {\sl imperative} type variables, consists of those which +start with one or two primes followed by an underbar. The complement +$\AppTyVar=\TyVar\setminus\ImpTyVar$\index{8.1} consists of the {\sl +applicative} type variables. The other six classes ({\Var}, {\Con}, +{\Exn}, {\TyCon}, {\Lab} and {\StrId}) are represented by identifiers +not starting with a prime. However,\index{7.5} {\tt *} is excluded from {\TyCon}, +to avoid confusion with the derived form of tuple type (see +Figure~\ref{typ-gram}). The class Lab\index{8.2} is extended to +include the {\em numeric} labels ~{\tt 1}~~{\tt 2}~~{\tt 3}~ $\cdots$, +i.e. any numeral not starting with~{\tt 0}. + +TyVar is therefore disjoint +from the other six classes. Otherwise, the syntax class of an occurrence of +identifier $\id$ in a Core phrase (ignoring derived forms, +Section~\ref{cor-der-form-sec}) is determined thus: +\begin{enumerate} + \item Immediately before ``.'' -- i.e. in a long identifier -- or in an + $\OPEN$ declaration, $\id$ is a structure + identifier. The following rules assume that all occurrences of + structure identifiers have been removed. + \item At the start of a component in a record type, record pattern or record + expression, $\id$ is a record label. + \item Elsewhere in types $\id$ is a type constructor, and must be within the + scope\index{8.3} of the type binding or datatype binding which introduced it. +% \item Elsewhere $\id$ is an exception name if it occurs immediately after +% $\RAISE$, at the start of a handler rule $\hanrule$, or within an +% $\EXCEPTION$ declaration or specification. + \item Elsewhere, $\id$ is an exception constructor if it occurs in + the scope of an exception binding which introduces it as such, + or a value constructor if it occurs in the + scope of a datatype binding which introduced it as such; + otherwise it is a value variable. +\end{enumerate} +It follows from the last rule that no value declaration can make a +``hole'' in the scope of a value or exception constructor +by introducing the same identifier as a variable; this +is because, in the scope of the declaration which introduces $\id$ as a value +or exception constructor, any occurrence of $\id$ in a pattern +is interpreted as the +constructor and not as the binding occurrence of a new variable. + +By means of the above rules a compiler can determine the class to which each +identifier occurrence belongs; for the remainder of this document we shall +therefore assume that the classes are all disjoint. + +\subsection{Lexical analysis} +Each\index{8.4} item of lexical analysis is either a reserved word, a numeric label, a +special constant or a long identifier. +Comments and formatting characters +separate items (except within string constants; see Section~\ref{cr:speccon}) +and are otherwise +ignored. At each stage the longest next item is taken. + +\subsection{Infixed operators} +An\index{8.5} identifier may be given {\sl infix status} by the +~$\INFIX$~ or ~$\INFIXR$~ directive , which may occur as a +declaration; this status only pertains to its use as a $\var$, a +$\con$ or an $\exn$ within the scope (see below) of the directive. +(Note that qualified identifiers never have infix status.) If $\id$ +has infix status, then ``$\exp_1\ \id\ \exp_2$'' (resp. ``$\pat_1\ +\id\ \pat_2$'') may occur -- in parentheses if necessary -- wherever +the application ``$\id$\verb+{+{\tt 1=}$\exp_1$\verb+,+{\tt +2=}$\exp_2$\verb+}+'' or its derived form +``$\id$\verb+(+$\exp_1$\verb+,+$\exp_2$\verb+)+'' (resp +``$\id$\verb+(+$\pat_1$\verb+,+$\pat_2$\verb+)+'') would otherwise +occur. On the other hand, an occurrence of any long identifier (qualified +or not) prefixed by {\OP} is treated as non-infixed. The only required +use of {\OP} is in prefixing a non-infixed occurrence of an +identifier $\id$ which has infix status; elsewhere {\OP}, where +permitted, has no effect.\index{9.1} +%version 2: On the other +%hand, non-infixed occurrences of $\id$ must be prefixed by the reserved word +%~$\OP$~.\index{9.1} +Infix status is cancelled by the ~$\NONFIX$~ +directive. We refer to the three directives collectively as {\sl +fixity directives}. + +The form of the fixity directives is as follows ($n\geq 1$): +\[ \longinfix \] +\[ \longinfixr \] +\[ \longnonfix \] +where $\langle d\rangle$ is an optional decimal digit $d$ indicating +binding precedence. A higher value of $d$ indicates tighter binding; +the default is $0$. ~$\INFIX$~ and ~$\INFIXR$~ dictate left and right +associativity respectively; association is always to the left for different +operators of the same precedence. The precedence of infix operators relative +to other expression and pattern constructions is given in +Appendix~\ref{core-gram-app}. + +The {\sl scope}\index{9.2} of a fixity directive $\dir$ is the ensuing program text, +except that if $\dir$ occurs in a declaration $\dec$ in either of the phrases +\[ \LET\ \dec\ \IN\ \cdots\ \END \] +\[ \LOCAL\ \dec\ \IN\ \cdots\ \END \] +then the scope of $\dir$ does not extend beyond the phrase. Further scope +limitations are imposed for Modules. + +These directives and ~$\OP$~ are omitted from the semantic rules, since they +affect only parsing. + +\subsection{Derived Forms} +\label{cor-der-form-sec} +There\index{9.3} are many standard syntactic forms in ML whose meaning can be expressed +in terms of a smaller number of syntactic forms, called the {\sl bare} language. +These derived forms, and their equivalent forms in the bare language, are +given in +Appendix~\ref{derived-forms-app}. + +%With one exception, these derived forms use no new lexical items. The +%exception is that the symbol \verb+#+ prefixed to an identifier of the +%class Lab constitutes a +%lexical item; \verb+#+{\it lab} denotes a selector function on records, cf. page~\pageref{der-exp}. + +\subsection{Grammar} + +The phrase classes for the Core are shown in Figure~\ref{cor-phr}. +We use the variable $\atexp$ to range over AtExp, etc. + +The grammatical rules for the Core are shown in Figures~\ref{exp-syn} +and \ref{pat-syn}. + +\clearpage +\begin{figure}[t] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&#\hfil\tabskip\@centering\cr +AtExp & atomic expressions \cr +ExpRow & expression rows \cr +Exp & expressions \cr +Match & matches \cr +Mrule & match rules \cr +\noalign{\vspace{2mm}} +%\cr +Dec & declarations \cr +ValBind & value bindings \cr +TypBind & type bindings \cr +DatBind & datatype bindings \cr +ConBind & constructor bindings \cr +%version 1: Constrs & datatype constructions \cr +ExBind & exception bindings \cr +\noalign{\vspace{2mm}} +%\cr +AtPat & atomic patterns \cr +PatRow & pattern rows \cr +Pat & patterns \cr +\noalign{\vspace{2mm}} +%\cr +Ty & type expressions \cr +TyRow & type-expression rows \cr +} +\makeatother +\caption{Core Phrase Classes} +\label{cor-phr} +\end{figure} + +The following\index{10.1} conventions are adopted in presenting the grammatical rules, +and in their interpretation: +\begin{itemize} + \item The brackets\index{10.2} ~$\langle\ \rangle$~ enclose optional phrases. + \item For any syntax class X (over which $x$ ranges) +we define the syntax class Xseq (over which {\it xseq} ranges) as follows: + \begin{quote} + \begin{tabular}{rcll} + {\it xseq} & $::=$ & $x$ & (singleton sequence)\\ + & & & (empty sequence)\\ + & & \ml{(}$x_1$\ml{,}$\cdots$\ml{,}$x_n$\ml{)} + & (sequence,~$n\geq 1$) \\ + \end{tabular} + \end{quote} +(Note that the ``$\cdots$'' used here, meaning syntactic iteration, must not be +confused with ``$\wildrec$'' which is a reserved word of the language.) + \item Alternative forms for each phrase class are in order of decreasing + precedence; this resolves ambiguity in parsing, as explained + in Appendix~\ref{core-gram-app}.\index{10.3} + \item L (resp. R)\index{10.4} means left (resp. right) association. + +\item The syntax of types binds more tightly than that of expressions. + +\item Each\index{10.6} iterated construct (e.g. $\match$, $\cdots$) +extends as far +right as possible; thus, parentheses may be needed around an expression which +terminates with a match, e.g. ``$\FN\ \match$'', if this occurs within a +larger +match. +\end{itemize} + + +\begin{figure}[t] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \atexp& ::= & \scon & special constant\cr + & & \opp\longvar & value variable\cr + & & \opp\longcon & value constructor\cr + & & \opp\longexn & exception constructor\cr + & & \verb+{ +\recexp\verb+ }+ + & record\cr + & & \letexp & local declaration\cr + & & \parexp & \cr +\noalign{\vspace{6pt}} +\labexps& ::= & \longlabexps & expression row\cr +\noalign{\vspace{6pt}} + \exp & ::= & \atexp & atomic\cr + & & \appexp & application (L)\cr + & & \infexp & infixed application\cr + & & \typedexp & typed (L)\cr + & & \handlexp & handle exception\cr + & & \raisexp & raise exception\cr + & & \fnexp & function\cr +\noalign{\vspace{6pt}} +\match & ::= & \longmatch & \cr +\noalign{\vspace{6pt}} +\mrule & ::= & \longmrule & \cr +\noalign{\vspace{6pt}} + \dec & ::= & \valdec & value declaration\cr + & & \typedec & type declaration\cr + & & \datatypedec & datatype declaration\cr + & & \abstypedec & abstype declaration\cr + & & \exceptiondec & exception declaration\cr + & & \localdec & local declaration\cr + & & \openstrdec & open declaration ($n\geq 1$) \cr + & & \emptydec & empty declaration\cr + & & \seqdec & sequential declaration\cr + & & \longinfix & infix (L) directive\cr + & & \longinfixr & infix (R) directive\cr + & & \longnonfix & nonfix directive\cr +\noalign{\vspace{6pt}} +\valbind& ::= & \longvalbind & \cr + & & \recvalbind & \cr +\noalign{\vspace{6pt}} +\typbind& ::= & \longtypbind & \cr +\noalign{\vspace{6pt}} +\datbind& ::= & \longdatbind & \cr +\noalign{\vspace{6pt}} +\constrs& ::= & \opp\longconstrs & \cr +\noalign{\vspace{6pt}} +\exnbind& ::= & \generativeexnbind & \cr + & & \eqexnbind & \cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{-2mm} +\caption{Grammar: Expressions, Matches, Declarations and Bindings\index{11}\index{12.1}} +\label{exp-syn} +\end{figure} +\clearpage % 1 August +\begin{figure}[h] +%\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + \atpat& ::= & \wildpat & wildcard\cr + & & \scon & special constant\cr + & & \opp\var & variable\cr + & & \opp\longcon & constant\cr + & & \opp\longexn & exception constant\cr + & & \verb+{ +\recpat\verb+ }+ + & record\cr + & & \parpat & \cr +\noalign{\vspace{6pt}} +\labpats& ::= & \wildrec & wildcard\cr + & & \longlabpats & pattern row\cr +\noalign{\vspace{6pt}} + \pat & & \atpat & atomic\cr + & & \opp\conpat & value construction\cr + & & \opp\exconpat & exception construction\cr + & & \infpat & infixed value construction\cr + & & \infexpat & infixed exception construction\cr + & & \typedpat & typed\cr + & & \opp\layeredpat & layered\cr +\noalign{\vspace{6pt}} + \ty & ::= & \tyvar & type variable\cr + & & \verb+{ +\rectype\verb+ }+ + & record type expression\cr + & & \constype & type construction\cr + & & \funtype & function type expression (R)\cr + & & \partype & \cr +\noalign{\vspace{6pt}} +\labtys & ::= & \longlabtys & type-expression row\cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{-2mm} +\caption{Grammar: Patterns and Type expressions\index{12.2}\index{13.1}} +\label{pat-syn} +\end{figure} +\nopagebreak[4] +\subsection{Syntactic Restrictions}\index{13.2} +\begin{itemize} +\item No pattern may contain the same $\var$ twice. No expression row, + pattern row or type row may bind the same $\lab$ twice. +\item No binding $\valbind$, $\typbind$, $\datbind$ or $\exnbind$ may bind + the same identifier twice; this applies also to value constructors within + a $\datbind$. +\item In the left side $\tyvarseq\ \tycon$ of any $\typbind$ or $\datbind$, + $\tyvarseq$ must not contain the same $\tyvar$ twice. Any $\tyvar$ + occurring within the right side must occur in $\tyvarseq$. +\item For each value binding \pat\ \ml{=} \exp\ within $\REC$, + $\exp$ must be of the form \fnexp, possibly constrained by one + or more type expressions. The derived form + of function-value binding given in Appendix~\ref{derived-forms-app}, + page~\pageref{der-dec}, necessarily obeys this restriction. +%from version 1: +%\item Every non-local exception binding -- that is, not localised by $\LET$ +% or $\LOCAL$ -- must be explicitly constrained by a type containing +% no type variables. +%not needed, covered by polymorphic references and exceptions: +%\item Any type expression $\ty$ occurring in a non-local +% exception binding -- that is, +% one not localised by $\LET$ or $\LOCAL$ -- must contain no type +% variables. +\end{itemize} diff --git a/synmod.tex b/synmod.tex new file mode 100644 index 0000000..22706d3 --- /dev/null +++ b/synmod.tex @@ -0,0 +1,310 @@ +\section{Syntax of Modules} +\label{syn-mod-sec} +For Modules there are further reserved words, identifier classes and derived +forms. There are no further special constants; +comments and lexical analysis are as for the Core. +The derived forms for modules concern functors and appear in +Appendix~\ref{derived-forms-app}. + +%For Modules there are further keywords and identifier classes, but no +%further special constants and at present no further derived forms. +%Comments and lexical analysis are as for the Core. + +\subsection{Reserved Words} +The\index{14.1} following are the additional reserved words used in Modules. +\begin{verbatim} + eqtype functor include sharing + sig signature struct structure +\end{verbatim} + +\subsection{Identifiers} +\label{syn-mod-identifiers-sec} +The additional syntax classes for Modules are SigId (signature identifiers) +and FunId (functor identifiers); they may be either alphanumeric -- not +starting with a prime -- or symbolic. The class of each identifier occurrence +is determined by the grammatical rules which follow. Henceforth, therefore, +we consider all identifier classes to be disjoint. + +\subsection{Infixed operators} +In addition to the scope rules for fixity directives given for the Core syntax, +there is a further scope limitation: +if $\dir$ occurs in a structure-level declaration $\strdec$ in any of the +phrases +\[ \LET\ \strdec\ \IN\ \cdots\ \END \] +\[ \LOCAL\ \strdec\ \IN\ \cdots\ \END \] +\[ \STRUCT\ \strdec\ \END \] +then the scope of $\dir$ does not extend beyond the phrase. + +One effect of this limitation is that fixity is local to a generative +structure expression -- in particular, to such an expression occurring +as a functor body. A more liberal scheme (which is under consideration) +would allow fixity directives to appear also as specifications, so that +fixity may be dictated by a signature expression; furthermore, it would allow an ~$\OPEN$~ +or ~$\INCLUDE$~ construction to restore the fixity which prevailed +in the structures being opened, or in the signatures being included. +This scheme is not adopted at present. + + +\subsection{Grammar for Modules} +\label{mod-gram-sec} +The\index{14.2} phrase classes for Modules are shown in Figure~\ref{mod-phr}. +We use the variable $\strexp$ to range over StrExp, etc. +The conventions adopted in presenting the grammatical +\pagebreak +\begin{figure}[t] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&#\hfil\tabskip\@centering\cr +StrExp & structure expressions \cr +StrDec & structure-level declarations \cr +StrBind & structure bindings \cr +\cr +SigExp & signature expressions \cr +SigDec & signature declarations \cr +SigBind & signature bindings \cr +\cr +Spec & specifications \cr +ValDesc & value descriptions\cr +TypDesc & type descriptions\cr +DatDesc & datatype descriptions\cr +ConDesc & constructor descriptions\cr +ExDesc & exception descriptions\cr +StrDesc & structure descriptions\cr +SharEq & sharing equations\cr +\cr +FunDec & functor declarations\cr +FunBind & functor bindings\cr +FunSigExp & functor signature expressions\cr +FunSpec & functor specifications\cr +FunDesc & functor descriptions\cr +TopDec & top-level declarations\cr +} +\makeatother +\caption{Modules Phrase Classes\index{15.1}} +\label{mod-phr} +\end{figure} +rules for Modules +are the same as for the Core. +The grammatical rules are shown in Figures~\ref{str-syn}, +\ref{spec-syn} and \ref{prog-syn}. + +It should be noted that functor specifications (FunSpec) cannot +occur in programs; +neither can the associated functor descriptions (FunDesc) +and functor signature expressions (FunSigExp). The purpose of a $\funspec$ +is to specify the static attributes (i.e. functor signature) of one +or more functors. This will be useful, in fact essential, for +separate compilation of functors. If, for example, a functor $g$ +refers to another functor $f$ then --- in order to compile $g$ in +the absence of the declaration of $f$ --- at least the specification +of $f$ (i.e. its functor signature) must be available. At present there is no +special grammatical form for a separately compilable ``chunk'' of text +-- which we may like to call call a {\sl module} -- containing a $\fundec$ +together with a $\funspec$ specifying its global references. However, below in +the semantics for Modules it is defined when a +declared functor matches a functor signature specified for it. This determines +exactly those functor environments (containing declared functors +such as $f$) into which the separately compiled ``chunk'' +containing the declaration of $g$ may be loaded. +\newpage +\begin{figure}[h] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr +\strexp & ::= & \encstrexp & generative\cr + & & \longstrid & structure identifier\cr + & & \funappstr & functor application\cr + & & \letstrexp & local declaration\cr +\noalign{\vspace{6pt}} +% +\strdec & ::= & \dec & declaration \cr + & & \singstrdec & structure \cr + & & \localstrdec & local \cr + & & \emptystrdec & empty \cr + & & \seqstrdec & sequential\cr +\noalign{\vspace{6pt}} +\strbind & ::= & \strbindera \cr +\noalign{\vspace{6pt}} +\sigexp & ::= & \encsigexp & generative\cr + & & \sigid & signature identifier\cr +\noalign{\vspace{6pt}} +\sigdec & ::= & \singsigdec & single\cr + & & \emptysigdec & empty\cr + & & \seqsigdec & sequential\cr +\noalign{\vspace{6pt}} +\sigbind & ::= & \sigbinder \cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Structure and Signature Expressions\index{16.1}} +\label{str-syn} +\end{figure} + +\subsection{Syntactic Restrictions} +\begin{itemize} +\item No\index{16.2} binding $\strbind$, $\sigbind$, or $\funbind$ may bind the + same identifier twice. +\item No description $\valdesc$, $\typdesc$, $\datdesc$, + $\exndesc$, $\strdesc$ or $\fundesc$ may describe the same identifier + twice; this applies also to value constructors within a $\datdesc$. +\end{itemize} +\clearpage %containing figure 'Grammar: Specifications' +\begin{figure}[m] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr +\spec & ::= & \valspec & value\cr + & & \typespec & type\cr + & & \eqtypespec & eqtype\cr + & & \datatypespec & datatype\cr + & & \exceptionspec & exception\cr + & & \structurespec & structure\cr + & & \sharingspec & sharing\cr + & & \localspec & local\cr + & & \openspec & open ($n\geq 1$) \cr + & & \inclspec & include ($n\geq 1$) \cr + & & \emptyspec & empty \cr + & & \seqspec & sequential\cr +\noalign{\vspace{6pt}} +\valdesc & ::= & \valdescription \cr +\noalign{\vspace{6pt}} +\typdesc & ::= & \typdescription \cr +\noalign{\vspace{6pt}} +\datdesc & ::= & \datdescription \cr +\noalign{\vspace{6pt}} +\condesc & ::= & \condescription \cr +\noalign{\vspace{6pt}} +\exndesc & ::= & \exndescription \cr +\noalign{\vspace{6pt}} +\strdesc & ::= & \strdescription \cr +\noalign{\vspace{6pt}} +\shareq & ::= & \strshareq & structure sharing\cr + & & & \qquad ($n\geq 2$) \cr + & & \typshareq & type sharing \cr + & & & \qquad ($n\geq 2$) \cr + & & \multshareq & multiple\cr +\noalign{\vspace{6pt}} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Specifications\index{17}} +\label{spec-syn} +\end{figure} +\clearpage %starting with Figure 'Grammar: Functors and Top-level declarations' +\begin{figure}[t] +\vspace{4pt} +\makeatletter{} +\tabskip\@centering +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr +\fundec & ::= & \singfundec & single\cr + & & \emptyfundec & empty\cr + & & \seqfundec & sequence\cr +\noalign{\vspace{6pt}} +\funbind & ::= & \funstrbinder & functor binding \cr + & & \qquad\qquad\qquad\qquad\optfunbinda \cr} +\vspace*{6pt} +\halign to\textwidth +{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr + +\funsigexp & ::= & \longfunsigexpa & functor signature expression\cr +\noalign{\vspace{6pt}} + \funspec & ::= & \singfunspec & functor specification\cr + & & \emptyfunspec & empty\cr + & & \seqfunspec & sequence\cr + \noalign{\vspace{6pt}} + \fundesc & ::= & \longfundesc\cr + \noalign{\vspace{6pt}} + +\topdec & ::= & \strdec & structure-level declaration\cr + & & \sigdec & signature declaration\cr + & & \fundec & functor declaration\cr +% \noalign{\vspace{6pt}} +%\program & ::= & \longprog & \cr +%from version 1: +%\program & ::= & \strdec & structure-level declaration\cr +% & & \sigdec & signature declaration\cr +% & & \fundec & functor declaration\cr +% & & \seqprog & sequence\cr +\noalign{\vspace{6pt}\parbox{12cm}{{\sl Note:}\/ No $\topdec$ may +contain, as an initial segment, a shorter top-level declaration followed by a semicolon.} +} +} +\makeatother +\vspace{3pt} +\caption{Grammar: Functors and Top-level Declarations\index{18.1}} +\label{prog-syn} +\end{figure} + + +\subsection{Closure Restrictions} +\label{closure-restr-sec} +The\index{18.2} semantics presented in later sections requires no restriction on +reference to non-local identifiers. For example, it allows a signature +expression to refer to external signature identifiers and +(via ~$\SHARING$~ or ~$\OPEN$~) to external structure identifiers; it also +allows a functor to refer to external identifiers of any kind. + +However, implementers who want to provide a simple facility for +separate compilation may want to impose the following restrictions +(ignoring references to identifiers bound in the initial basis +$\B_0$, which may occur anywhere): + +%However, in the present version of the language, +%apart from references to identifiers bound in the initial basis $B_0$ +%(which may occur anywhere), it is required that signatures only refer +%non-locally to signature identifiers and that functors only +%refer non-locally to functor and signature identifiers. +%These restrictions ease separate +%compilation; however, they may be relaxed in a future version of the language. +% +%More precisely, the restrictions are as follows (ignoring reference to +%identifiers bound in $B_0$): +\begin{enumerate} +\item In any signature binding ~$\sigid\ \mbox{{\tt =}}\ \sigexp$~, +the only non-local +references in $\sigexp$ are to signature identifiers. +\item In any functor description ~$\funid\ \longfunsigexpa$~, +the only non-local +references in $\sigexp$ and $\sigexp'$ are to signature identifiers, +except that $\sigexp'$ may refer to $\strid$ and its components. +\item In any functor binding ~$\funstrbinder$~, the only non-local +references in $\sigexp$, $\sigexp'$ and $\strexp$ are to functor and signature +identifiers, +except that both $\sigexp'$ and $\strexp$ may refer to $\strid$ and +its components. +\end{enumerate} +In the last two cases the final qualification allows, for example, sharing +constraints to be specified between functor argument and result. +(For a completely precise definition of these closure restrictions, +see the comments to rules \ref{single-sigdec-rule} +(page~\pageref{single-sigdec-rule}), +\ref{singfunspec-rule} (page~\pageref{singfunspec-rule}) +and \ref{singfundec-rule} (page~\pageref{singfundec-rule}) +in the static semantics of modules, Section~\ref{statmod-sec}.) + +The\index{19.1} +significance of these restrictions is that they may ease separate +compilation; this may be seen as follows. If one takes a {\sl module} +to be a sequence of signature declarations, functor specifications +and functor declarations satisfying the above restrictions then the +elaboration of a module can be made to depend on the initial +static basis alone (in particular, it will not rely on +structures outside the module). Moreover, the elaboration +of a module cannot create new free structure or type names, so +name consistency (as defined in Section~\ref{consistency-sec}, +page \pageref{consistency-sec}) is automatically preserved +across separately compiled modules. On the other hand, +imposing these restrictions may force the programmer to write +many more sharing equations than is needed if functors +and signature expressions can refer to free structures. + + +