| 1 | \documentclass[draft]{article} |
| 2 | \usepackage{fullpage} |
| 3 | \usepackage{amsmath} |
| 4 | \usepackage{amssymb} |
| 5 | |
| 6 | \include{macros} |
| 7 | |
| 8 | % math fonts |
| 9 | \newcommand{\mbb}[1]{\mathbb{#1}} |
| 10 | \newcommand{\mbf}[1]{\mathbf{#1}} |
| 11 | \renewcommand{\mit}[1]{\mathit{#1}} |
| 12 | \newcommand{\mrm}[1]{\mathrm{#1}} |
| 13 | \newcommand{\mtt}[1]{\mathtt{#1}} |
| 14 | \newcommand{\mcal}[1]{\mathcal{#1}} |
| 15 | \newcommand{\msf}[1]{\mathsf{#1}} |
| 16 | |
| 17 | % text fonts |
| 18 | \newcommand{\ttt}[1]{\texttt{#1}} |
| 19 | |
| 20 | % formatting |
| 21 | \newenvironment{stackAux}[2]{% |
| 22 | \setlength{\arraycolsep}{0pt} |
| 23 | \begin{array}[#1]{#2}}{ |
| 24 | \end{array}} |
| 25 | \newenvironment{stackCC}{ |
| 26 | \begin{stackAux}{c}{c}}{\end{stackAux}} |
| 27 | \newenvironment{stackCL}{ |
| 28 | \begin{stackAux}{c}{l}}{\end{stackAux}} |
| 29 | \newenvironment{stackTL}{ |
| 30 | \begin{stackAux}{t}{l}}{\end{stackAux}} |
| 31 | \newenvironment{stackTR}{ |
| 32 | \begin{stackAux}{t}{r}}{\end{stackAux}} |
| 33 | \newenvironment{stackBC}{ |
| 34 | \begin{stackAux}{b}{c}}{\end{stackAux}} |
| 35 | \newenvironment{stackBL}{ |
| 36 | \begin{stackAux}{b}{l}}{\end{stackAux}} |
| 37 | |
| 38 | \newcommand{\stagger}[2]{% |
| 39 | \begin{array}{ccc}% |
| 40 | \multicolumn{2}{l}{#1}&\\% |
| 41 | &\multicolumn{2}{r}{#2}% |
| 42 | \end{array}} |
| 43 | |
| 44 | \newcommand{\axiom}[1]{{\displaystyle\strut{#1}}} |
| 45 | \newcommand{\infrule}[2]{{\frac{\displaystyle\strut{#1}}{\displaystyle\strut{#2}}}} |
| 46 | \newcommand{\judge}[2]{\infrule{#1}{#2}} |
| 47 | |
| 48 | \begin{document} |
| 49 | |
| 50 | \title{Formal Specification of the ML Basis system} |
| 51 | \author{Copyright \copyright\ 2004\\ |
| 52 | Henry Cejtin, Matthew Fluet, Suresh Jagannathan, and Stephen Weeks} |
| 53 | \date{\today} |
| 54 | \maketitle |
| 55 | % |
| 56 | This document formally specifies the ML Basis system (MLB) in {\mlton} |
| 57 | used to program in the large. The system has been designed to be a |
| 58 | natural extension of Standard ML, and the specification is given in |
| 59 | the style of The Definition of Standard ML~\cite{MTHM97} (henceforeth, |
| 60 | the Definition). This section adopts (often silently) abbreviations, |
| 61 | conventions, definitions, and notation from the Definition. |
| 62 | % |
| 63 | \section{Syntax of MLB} |
| 64 | For MLB there are further reserved words, identifier classes and |
| 65 | derived forms. There are no further special constants; comments and |
| 66 | lexical analysis are as for the Core and Modules. The derived forms |
| 67 | appear in Appendix~\ref{sec:mlb:DerivedForms}. |
| 68 | % |
| 69 | \subsection{Reserved Words} |
| 70 | The following are the additional reserved words used in MLB. |
| 71 | \begin{displaymath} |
| 72 | \mtt{bas} \quad\quad \mtt{basis} |
| 73 | \end{displaymath} |
| 74 | Note that many of the reserved words from the Core and Modules are not |
| 75 | used by the grammar of MLB. However, as the grammar includes |
| 76 | identifiers from the grammars of the Core and Modules, it is useful to |
| 77 | consider the reserved words from the Core and Modules to be reserved |
| 78 | in MLB as well. |
| 79 | % |
| 80 | \subsection{Identifiers} |
| 81 | The additional identifier class for MLB are $\mrm{BasId}$ (basis |
| 82 | identifiers). Basis identifiers must be alphanumeric, not starting |
| 83 | with a prime. The class of each identifier occurence is determined by |
| 84 | the grammatical rules which follow. Henceforth, therefore, we |
| 85 | consider all identifier classes to be disjoint. |
| 86 | % |
| 87 | \subsection{Infixed operators} |
| 88 | The grammar of MLB does not directly admit fixity directives. |
| 89 | However, the static and dynamic semantics for MLB will import source |
| 90 | files that must be parsed in the scope of fixity directives and that |
| 91 | may introduce additional fixity directives into scope. |
| 92 | Figure~\ref{fig:mlb:S:FixityEnv} formalizes the Definition's notion of |
| 93 | \emph{infix status} as a \emph{fixity environment}. |
| 94 | \begin{figure}[h] |
| 95 | \begin{displaymath} |
| 96 | \begin{array}{rcl} |
| 97 | & & \mrm{InfixStatus} = \{\mtt{nonfix}\} \cup \bigcup_{d \in \{0,\ldots,9\}} \{\mtt{infix}~d, \mtt{infixr}~d\} \\ |
| 98 | \mit{FE} & \in & \mrm{FixEnv} = \mrm{VId} \xrightarrow{\mrm{fin}} \mrm{InfixStatus} \end{array} |
| 99 | \end{displaymath} |
| 100 | \caption{Fixity Environment}\label{fig:mlb:S:FixityEnv} |
| 101 | \end{figure} |
| 102 | % |
| 103 | \subsection{Grammar for MLB} |
| 104 | The phrase classes for MLB are shown in |
| 105 | Figure~\ref{fig:mlb:S:PhraseClasses}. |
| 106 | \begin{figure}[h] |
| 107 | \begin{displaymath} |
| 108 | \begin{array}{ll} |
| 109 | \mrm{BasExp} & \mbox{basis expressions} \\ |
| 110 | \mrm{BasDec} & \mbox{basis-level declaration} \\ |
| 111 | \mrm{BasBind} & \mbox{basis bindings} \\ |
| 112 | \mrm{BStrBind} & \mbox{(basis) structure bindings} \\ |
| 113 | \mrm{BSigBind} & \mbox{(basis) signature bindings} \\ |
| 114 | \mrm{BFunBind} & \mbox{(basis) functor bindings} |
| 115 | \end{array} |
| 116 | \end{displaymath} |
| 117 | \caption{MLB Phrase Classes}\label{fig:mlb:S:PhraseClasses} |
| 118 | \end{figure} |
| 119 | We use the variable $\mit{basexp}$ to range over $\mrm{BasExp}$, etc. |
| 120 | The conventions adopted in presenting the grammatical rules for MLB |
| 121 | are the same as for the Core and Modules. The grammatical rules are |
| 122 | shown in Figure~\ref{fig:mlb:S:GrammaticalRules}. |
| 123 | \begin{figure}[h] |
| 124 | \begin{displaymath} |
| 125 | \begin{array}{rcll} |
| 126 | \mit{basexp} & ::= & |
| 127 | \mtt{bas}~ \mit{basdec} ~\mtt{end} |
| 128 | & \mbox{basic} \\&& |
| 129 | \mit{basid} |
| 130 | & \mbox{basis identifier} \\&& |
| 131 | \mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end} |
| 132 | & \mbox{local declaration} \\ |
| 133 | |
| 134 | \mit{basdec} & ::= & |
| 135 | \mtt{basis}~ \mit{basbind} |
| 136 | & \mbox{basis} \\&& |
| 137 | \mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end} |
| 138 | & \mbox{local} \\&& |
| 139 | \mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n |
| 140 | & \mbox{open ($n \geq 1$)} \\&& |
| 141 | \mtt{structure}~ \mit{bstrbind} |
| 142 | & \mbox{(basis) structure binding} \\&& |
| 143 | \mtt{signature}~ \mit{bsigbind} |
| 144 | & \mbox{(basis) signature binding} \\&& |
| 145 | \mtt{functor}~ \mit{bfunbind} |
| 146 | & \mbox{(basis) functor binding} \\&& |
| 147 | \quad |
| 148 | & \mbox{empty} \\&& |
| 149 | \mit{basdec}_1~\langle\mtt{;}\rangle~\mit{basdec}_2 |
| 150 | & \mbox{sequential} \\&& |
| 151 | \msf{path.mlb} & |
| 152 | \mbox{import ML basis} \\&& |
| 153 | \msf{path.sml} |
| 154 | & \mbox{import source} \\ |
| 155 | |
| 156 | \mit{basbind} & ::= & |
| 157 | \mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~ \mit{basbind}\rangle \\ |
| 158 | \mit{bstrbind} & ::= & |
| 159 | \mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~ \mit{bstrbind}\rangle \\ |
| 160 | \mit{bsigbind} & ::= & |
| 161 | \mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~ \mit{bsigbind}\rangle \\ |
| 162 | \mit{bfunbind} & ::= & |
| 163 | \mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~ \mit{bfunbind}\rangle |
| 164 | \end{array} |
| 165 | \end{displaymath} |
| 166 | \caption{Grammar: Basis Expressions, Declarations, and Bindings}\label{fig:mlb:S:GrammaticalRules} |
| 167 | \end{figure} |
| 168 | % |
| 169 | \subsection{Syntactic Restrictions} |
| 170 | \begin{itemize} |
| 171 | \item No binding $\mit{basbind}$ may bind the same identifier twice. |
| 172 | \item No binding $\mit{bstrbind}$, $\mit{bsigbind}$ or $\mit{bfunbind}$ may bind the same identifier twice. |
| 173 | \item MLB may not be cyclic; i.e., successively replacing |
| 174 | $\msf{path.mlb}$ with its parsed $\mrm{BasDec}$ must terminate. |
| 175 | \end{itemize} |
| 176 | % |
| 177 | \subsection{Parsing} |
| 178 | The static and dynamic semantics for MLB will interpret |
| 179 | $\msf{path.sml}$ as a parsed $\mrm{TopDec}$ and |
| 180 | $\msf{path.mlb}$ as a parsed $\mrm{BasDec}$. Parsing a $\mrm{TopDec}$ |
| 181 | takes a fixity environment as input and returns a fixity environment |
| 182 | as output; the output fixity environment corresponds to fixity |
| 183 | directives introduced by and whose scope is not limited by the parsed |
| 184 | $\mrm{TopDec}$. |
| 185 | |
| 186 | Paths and parsers are given in Figure~\ref{fig:mlb:S:PathsParser}. A |
| 187 | (fixed) $\mrm{Parser}$ $\mcal{P}$ provides the interpretation of |
| 188 | $\msf{path.sml}$ and $\msf{path.mlb}$ imports. |
| 189 | \begin{figure}[h] |
| 190 | \begin{displaymath} |
| 191 | \begin{array}{c} |
| 192 | \begin{array}{rcl} |
| 193 | \msf{path.sml} & \in & \mrm{SourcePath} \\ |
| 194 | \msf{path.mlb} & \in & \mrm{MLBasisPath} |
| 195 | \end{array} \\ |
| 196 | \begin{array}{rcl} |
| 197 | \mcal{P} & \in & \mrm{Parser} = |
| 198 | ((\mrm{FixEnv} \times \mrm{SourcePath}) |
| 199 | \xrightarrow{\mrm{fin}} (\mrm{FixEnv} \times \mrm{TopDec})) |
| 200 | \times |
| 201 | (\mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{BasDec}) |
| 202 | \end{array} |
| 203 | \end{array} |
| 204 | \end{displaymath} |
| 205 | \caption{Parser}\label{fig:mlb:S:PathsParser} |
| 206 | \end{figure} |
| 207 | % |
| 208 | For a file extension $\msf{.ext}$, $\msf{path.ext}$ denotes either an |
| 209 | absolute path or a relative path (relative to the $\mrm{BasDec}$ being |
| 210 | parsed) to a file in the underlying file system. Paths that denote the same |
| 211 | file in the underlying file system are considered equal, though they may |
| 212 | have distinct textual representations. An implementation |
| 213 | may allow additional extensions (e.g., $\mtt{.ML}$, $\mtt{.fun}$, |
| 214 | $\mtt{.sig}$) in elements of $\mrm{SourcePath}$. An implementation |
| 215 | may additionally allow path variables to appear in |
| 216 | paths. $\mrm{Parser}$ could be refined by a \emph{current working |
| 217 | directory}, to formally specify the interpretation of relative paths, |
| 218 | and an \emph{path map}, to formally specify the |
| 219 | interpretation of path variables, but the above suffices |
| 220 | for the development in the following sections. |
| 221 | % |
| 222 | \section{Static Semantics for MLB} |
| 223 | % |
| 224 | \subsection{Semantic Objects} |
| 225 | The simple objects for the MLB static semantics are exactly as for |
| 226 | Modules. The compound objects are those for Modules, augmented by |
| 227 | those in Figure~\ref{fig:mlb:SS:CompoundObjects}. |
| 228 | \begin{figure}[h] |
| 229 | \begin{displaymath} |
| 230 | \begin{array}{rcl} |
| 231 | \mit{BE} & \in & \mrm{BasEnv} = \mrm{BasId} \xrightarrow{\mrm{fin}} \mrm{MBasis} \\ |
| 232 | \mit{M} ~\mrm{or}~ \mit{FE},\mit{BE},\mit{B} & \in & |
| 233 | \mrm{MBasis} = \mrm{FixEnv} \times \mrm{BasEnv} \times \mrm{Basis} \\ |
| 234 | \Psi & \in & \mrm{BasCache} = \mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{MBasis} |
| 235 | \end{array} |
| 236 | \end{displaymath} |
| 237 | \caption{Compound Semantic Objects}\label{fig:mlb:SS:CompoundObjects} |
| 238 | \end{figure} |
| 239 | The operations of projection, injection and modification are as for |
| 240 | Modules. |
| 241 | % |
| 242 | \subsection{Inference Rules} |
| 243 | As for the Core and for Modules, the rules for MLB static semantics |
| 244 | allow sentences of the form |
| 245 | \begin{displaymath} |
| 246 | A \vdash \mit{phrase} \longrightarrow A' |
| 247 | \end{displaymath} |
| 248 | to be inferred. Some hypotheses in rules are not of this form; they |
| 249 | are called \emph{side-conditions}. The convention for options is as |
| 250 | in the Core and Modules semantics. |
| 251 | |
| 252 | \vspace{2\parsep} |
| 253 | {\large\noindent |
| 254 | \textbf{Basis Expressions} \hfill |
| 255 | \fbox{$\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi'$} |
| 256 | }\nopagebreak |
| 257 | |
| 258 | \begin{equation} |
| 259 | \judge{ |
| 260 | \mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' |
| 261 | }{ |
| 262 | \mit{M}, \Psi \vdash \mtt{bas}~ \mit{basdec} ~\mtt{end} \longrightarrow \mit{M}', \Psi' |
| 263 | } |
| 264 | \end{equation} |
| 265 | |
| 266 | \begin{equation} |
| 267 | \judge{ |
| 268 | \mit{M}(\mit{basid}) = \mit{M}' |
| 269 | }{ |
| 270 | \mit{M}, \Psi \vdash \mit{basid} \longrightarrow \mit{M}', \Psi |
| 271 | } |
| 272 | \end{equation} |
| 273 | |
| 274 | \begin{equation} |
| 275 | \label{eqn:mlb:SS:localDeclaration} |
| 276 | \judge{ |
| 277 | \mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 278 | \mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basexp} \longrightarrow \mit{M}_2, \Psi_2 |
| 279 | }{ |
| 280 | \mit{M}, \Psi \vdash \mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2 |
| 281 | } |
| 282 | \end{equation} |
| 283 | |
| 284 | \begin{samepage} |
| 285 | \noindent |
| 286 | \textit{Comments}: |
| 287 | \begin{itemize} |
| 288 | \item[(\ref{eqn:mlb:SS:localDeclaration})] The use of $\oplus$, here |
| 289 | and elsewhere, ensures that the type names generated by the first |
| 290 | sub-phrase are distinct from the names generated by the second sub-phrase. |
| 291 | \end{itemize} |
| 292 | \end{samepage} |
| 293 | |
| 294 | \vspace{2\parsep} |
| 295 | {\large\noindent |
| 296 | \textbf{Basis-level Declarations} \hfill |
| 297 | \fbox{$\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'$} |
| 298 | }\nopagebreak |
| 299 | |
| 300 | \begin{equation} |
| 301 | \judge{ |
| 302 | \mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi' |
| 303 | }{ |
| 304 | \mit{M}, \Psi \vdash \msf{basis}~ \mit{basbind} \longrightarrow \mit{BE}' ~\mrm{in}~ \mrm{MBasis}, \Psi' |
| 305 | } |
| 306 | \end{equation} |
| 307 | |
| 308 | \begin{equation} |
| 309 | \judge{ |
| 310 | \mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 311 | \mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 \quad |
| 312 | }{ |
| 313 | \mit{M}, \Psi \vdash \mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2 |
| 314 | } |
| 315 | \end{equation} |
| 316 | |
| 317 | \begin{equation} |
| 318 | \judge{ |
| 319 | \mit{M}(\mit{basid}_1) = \mit{M}_1 \quad \cdots \quad |
| 320 | \mit{M}(\mit{basid}_n) = \mit{M}_n |
| 321 | }{ |
| 322 | \mit{M}, \Psi \vdash \mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n \longrightarrow \mit{M}_1 \oplus \cdots \oplus \mit{M}_n, \Psi |
| 323 | } |
| 324 | \end{equation} |
| 325 | |
| 326 | \begin{equation} |
| 327 | \judge{ |
| 328 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{bstrbind} \longrightarrow SE |
| 329 | }{ |
| 330 | \mit{M}, \Psi \vdash \mtt{structure}~ \mit{bstrbind} |
| 331 | \longrightarrow \mit{SE} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 332 | } |
| 333 | \end{equation} |
| 334 | |
| 335 | \begin{equation} |
| 336 | \judge{ |
| 337 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{bsigbind} \longrightarrow G |
| 338 | }{ |
| 339 | \mit{M}, \Psi \vdash \mtt{signature}~ \mit{bsigbind} |
| 340 | \longrightarrow \mit{G } ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 341 | } |
| 342 | \end{equation} |
| 343 | |
| 344 | \begin{equation} |
| 345 | \judge{ |
| 346 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{bfunbind} \longrightarrow F |
| 347 | }{ |
| 348 | \mit{M}, \Psi \vdash \mtt{functor}~ \mit{bfunbind} |
| 349 | \longrightarrow \mit{F} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 350 | } |
| 351 | \end{equation} |
| 352 | |
| 353 | \begin{equation} |
| 354 | \judge{ |
| 355 | }{ |
| 356 | \mit{M}, \Psi \vdash \quad \longrightarrow \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 357 | } |
| 358 | \end{equation} |
| 359 | |
| 360 | \begin{equation} |
| 361 | \judge{ |
| 362 | \mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 363 | \mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 |
| 364 | }{ |
| 365 | \mit{M}, \Psi \vdash \mit{basdec}_1 ~\langle\mtt{;}\rangle~ \mit{basdec}_2 \longrightarrow \mit{M}_1 \oplus \mit{M}_2, \Psi_2 |
| 366 | } |
| 367 | \end{equation} |
| 368 | |
| 369 | \begin{equation} |
| 370 | \label{eqn:mlb:SS:path.sml} |
| 371 | \judge{ |
| 372 | \mcal{P}(\mit{FE}~\mrm{of}~\mit{M}, \msf{path.sml}) = (\mit{FE}', \mit{topdec}) \quad |
| 373 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{topdec} \Rightarrow \mit{B}' |
| 374 | }{ |
| 375 | \mit{M}, \Psi \vdash \msf{path.sml} \longrightarrow (\mit{FE}',\{\},\mit{B}'), \Psi |
| 376 | } |
| 377 | \end{equation} |
| 378 | |
| 379 | \begin{equation} |
| 380 | \judge{ |
| 381 | \Psi(\msf{path.mlb}) = \mit{M}' |
| 382 | }{ |
| 383 | \mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi |
| 384 | } |
| 385 | \end{equation} |
| 386 | |
| 387 | \begin{equation} |
| 388 | \judge{ |
| 389 | \msf{path.mlb} \notin \mrm{Dom}~\Psi \quad |
| 390 | \mcal{P}(\msf{path.mlb}) = \mit{basdec} \quad |
| 391 | \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' |
| 392 | }{ |
| 393 | \mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi' + \{\msf{path.mlb} \mapsto \mit{M}'\} |
| 394 | } |
| 395 | \end{equation} |
| 396 | |
| 397 | \begin{samepage} |
| 398 | \noindent |
| 399 | \textit{Comments}: |
| 400 | \begin{itemize} |
| 401 | \item[(\ref{eqn:mlb:SS:path.sml})] |
| 402 | Note the use of the Definition's |
| 403 | $\mit{B} \vdash \mit{topdec} \Rightarrow \mit{B}'$. |
| 404 | \end{itemize} |
| 405 | \end{samepage} |
| 406 | |
| 407 | \vspace{2\parsep} |
| 408 | {\large\noindent |
| 409 | \textbf{Basis Bindings} \hfill |
| 410 | \fbox{$\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi'$} |
| 411 | }\nopagebreak |
| 412 | |
| 413 | \begin{equation} |
| 414 | \judge{ |
| 415 | \mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' \quad |
| 416 | \langle\mit{M} + \mrm{tynames}~\mit{M}', \Psi' \vdash \mit{basbind} \longrightarrow \mit{BE}'', \Psi''\rangle |
| 417 | }{ |
| 418 | \mit{M}, \Psi \vdash \mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~\mit{basbind}\rangle \longrightarrow |
| 419 | \{\mit{basid} \mapsto \mit{M}'\} \langle+ \mit{BE}''\rangle, \Psi'\langle'\rangle |
| 420 | } |
| 421 | \end{equation} |
| 422 | |
| 423 | \vspace{2\parsep} |
| 424 | {\large\noindent |
| 425 | \textbf{(Basis) Structure Bindings} \hfill |
| 426 | \fbox{$\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}$} |
| 427 | }\nopagebreak |
| 428 | |
| 429 | \begin{equation} |
| 430 | \label{eqn:mlb:SS:bstrbind} |
| 431 | \judge{ |
| 432 | \mit{B}(\mit{strid}_2) = E \quad |
| 433 | \langle\mit{B} + \mrm{tynames}~\mit{E} \vdash \mit{bstrbind} \longrightarrow \mit{SE}\rangle |
| 434 | }{ |
| 435 | \mit{B} \vdash \mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~\mit{bstrbind}\rangle \longrightarrow |
| 436 | \{\mit{strid}_1 \mapsto \mit{E}\} \langle+ \mit{SE}\rangle |
| 437 | } |
| 438 | \end{equation} |
| 439 | |
| 440 | \begin{samepage} |
| 441 | \noindent |
| 442 | \textit{Comments}: |
| 443 | \begin{itemize} |
| 444 | \item[(\ref{eqn:mlb:SS:bstrbind})] Note that $\mit{bstrbind} \subset |
| 445 | \mit{strbind}$. Hence, this rule can be derived from the |
| 446 | Definition's $\mit{B} \vdash \mit{strbind} \Rightarrow \mit{SE}$. |
| 447 | \end{itemize} |
| 448 | \end{samepage} |
| 449 | |
| 450 | \vspace{2\parsep} |
| 451 | {\large\noindent |
| 452 | \textbf{(Basis) Signature Bindings} \hfill |
| 453 | \fbox{$\mit{B} \vdash \mit{bsigbind} \longrightarrow \mit{G}$} |
| 454 | }\nopagebreak |
| 455 | |
| 456 | \begin{equation} |
| 457 | \label{eqn:mlb:SS:bsigbind} |
| 458 | \judge{ |
| 459 | \begin{stackCC} |
| 460 | \mit{B}(\mit{sigid}_2) = \Sigma \quad \Sigma = (\mit{T})\mit{E} \quad |
| 461 | \mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset \\ |
| 462 | \mit{T} = \mrm{tynames}~\mit{E} \setminus (\mit{T}~\mrm{of}~\mit{B}) \quad |
| 463 | \langle\mit{B} \vdash \mit{bsigbind} \longrightarrow \mit{G}\rangle |
| 464 | \end{stackCC} |
| 465 | }{ |
| 466 | \mit{B} \vdash \mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~\mit{bsigbind}\rangle \longrightarrow |
| 467 | \{\mit{sigid}_1 \mapsto \Sigma\} \langle+ \mit{G}\rangle |
| 468 | } |
| 469 | \end{equation} |
| 470 | |
| 471 | \begin{samepage} |
| 472 | \noindent |
| 473 | \textit{Comments}: |
| 474 | \begin{itemize} |
| 475 | \item[(\ref{eqn:mlb:SS:bsigbind})] Note that $\mit{bsigbind} \subset |
| 476 | \mit{sigbind}$. Hence, this rule can be derived from the |
| 477 | Definition's $\mit{B} \vdash \mit{sigbind} \Rightarrow \mit{G}$. As such, the |
| 478 | following comment from the Definition applies: |
| 479 | \begin{quote} |
| 480 | The bound names of $\mit{B}(\mit{sigid}_2)$ can always be renamed to |
| 481 | satisfy $\mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset$, if necessary. |
| 482 | \end{quote} |
| 483 | \end{itemize} |
| 484 | \end{samepage} |
| 485 | |
| 486 | \vspace{2\parsep} |
| 487 | {\large\noindent |
| 488 | \textbf{(Basis) Functor Bindings} \hfill |
| 489 | \fbox{$\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}$} |
| 490 | }\nopagebreak |
| 491 | |
| 492 | \begin{equation} |
| 493 | \judge{ |
| 494 | \begin{stackCC} |
| 495 | \mit{B}(\mit{funid}_2) = \Phi \quad \Phi = (\mit{T})(\mit{E},(\mit{T}')\mit{E}') \quad |
| 496 | \mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset \\ |
| 497 | \mit{T}' = \mrm{tynames}~\mit{E}' \setminus ((\mit{T}~\mrm{of}~\mit{B}) \cup \mit{T}) \quad |
| 498 | \langle\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}\rangle |
| 499 | \end{stackCC} |
| 500 | }{ |
| 501 | \mit{B} \vdash \mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~\mit{bfunbind}\rangle \longrightarrow |
| 502 | \{\mit{funid}_1 \mapsto \Phi\} \langle+ \mit{F}\rangle |
| 503 | } |
| 504 | \end{equation} |
| 505 | % |
| 506 | \section{Dynamic Semantics for MLB} |
| 507 | % |
| 508 | \subsection{Reduced Syntax} |
| 509 | The syntax of MLB is unchanged for the purposes of the dynamic |
| 510 | semantics for MLB. However, the $\mrm{Parser}$ $\mcal{P}$ returns a |
| 511 | $\mit{topdec}$ in the reduced syntax of Modules. |
| 512 | % |
| 513 | \subsection{Compound Objects} |
| 514 | The compound objects for the MLB dynamic semantics, extra to those |
| 515 | for the Modules dynamic semantics, are shown in Figure~\ref{fig:mlb:DS:CompoundObjects}. |
| 516 | \begin{figure}[h] |
| 517 | \begin{displaymath} |
| 518 | \begin{array}{rcl} |
| 519 | \mit{BE} & \in & \mrm{BasEnv} = \mrm{BasId} \xrightarrow{\mrm{fin}} \mrm{MBasis} \\ |
| 520 | \mit{M} ~\mrm{or}~ \mit{FE},\mit{BE},\mit{B} & \in & \mrm{MBasis} = |
| 521 | \mrm{FixEnv} \times \mrm{BasEnv} \times \mrm{Basis} \\ |
| 522 | \Psi & \in & \mrm{BasCache} = \mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{MBasis} |
| 523 | \end{array} |
| 524 | \end{displaymath} |
| 525 | \caption{Compound Semantic Objects}\label{fig:mlb:DS:CompoundObjects} |
| 526 | \end{figure} |
| 527 | % |
| 528 | \subsection{Inference Rules} |
| 529 | The semantic rules allow sentences of the form |
| 530 | \begin{displaymath} |
| 531 | s, A \vdash \mit{phrase} \longrightarrow A', s' |
| 532 | \end{displaymath} |
| 533 | to be inferred, where $s$, $s'$ are the states before and after the |
| 534 | evaluation represented by the sentence. Some hypotheses in rules are |
| 535 | not of this form; they are called \emph{side-conditions}. The |
| 536 | convention for options is as in the Core and Modules semantics. |
| 537 | |
| 538 | The state and exception conventions are adopted as in the Core and |
| 539 | Modules dynamic semantics. However, it can be shown that the only |
| 540 | MLB phrases whose evaluation may cause a side-effect or generate an |
| 541 | exception packet are of the form $\mit{basexp}$, $\mit{basdec}$ or |
| 542 | $\mit{basbind}$. |
| 543 | |
| 544 | \vspace{2\parsep} |
| 545 | {\large\noindent |
| 546 | \textbf{Basis Expressions} \hfill |
| 547 | \fbox{$\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' / p$} |
| 548 | }\nopagebreak |
| 549 | |
| 550 | \begin{equation} |
| 551 | \judge{ |
| 552 | \mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' |
| 553 | }{ |
| 554 | \mit{M}, \Psi \vdash \mtt{bas}~ \mit{basdec} ~\mtt{end} \longrightarrow \mit{M}', \Psi' |
| 555 | } |
| 556 | \end{equation} |
| 557 | |
| 558 | \begin{equation} |
| 559 | \judge{ |
| 560 | \mit{M}(\mit{basid}) = \mit{M}' |
| 561 | }{ |
| 562 | \mit{M}, \Psi \vdash \mit{basid} \longrightarrow \mit{M}', \Psi |
| 563 | } |
| 564 | \end{equation} |
| 565 | |
| 566 | \begin{equation} |
| 567 | \judge{ |
| 568 | \mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 569 | \mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basexp} \longrightarrow \mit{M}_2, \Psi_2 |
| 570 | }{ |
| 571 | \mit{M}, \Psi \vdash \mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2 |
| 572 | } |
| 573 | \end{equation} |
| 574 | |
| 575 | \vspace{2\parsep} |
| 576 | {\large\noindent |
| 577 | \textbf{Basis-level Declarations} \hfill |
| 578 | \fbox{$\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' / p$} |
| 579 | }\nopagebreak |
| 580 | |
| 581 | \begin{equation} |
| 582 | \judge{ |
| 583 | \mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi' |
| 584 | }{ |
| 585 | \mit{M}, \Psi \vdash \msf{basis}~ \mit{basbind} \longrightarrow \mit{BE}' ~\mrm{in}~ \mrm{MBasis}, \Psi' |
| 586 | } |
| 587 | \end{equation} |
| 588 | |
| 589 | \begin{equation} |
| 590 | \judge{ |
| 591 | \mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 592 | \mit{M} + \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 \quad |
| 593 | }{ |
| 594 | \mit{M}, \Psi \vdash \mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2 |
| 595 | } |
| 596 | \end{equation} |
| 597 | |
| 598 | \begin{equation} |
| 599 | \judge{ |
| 600 | \mit{M}(\mit{basid}_1) = \mit{M}_1 \quad \cdots \quad |
| 601 | \mit{M}(\mit{basid}_n) = \mit{M}_n |
| 602 | }{ |
| 603 | \mit{M}, \Psi \vdash \mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n \longrightarrow \mit{M}_1 + \cdots + \mit{M}_n, \Psi |
| 604 | } |
| 605 | \end{equation} |
| 606 | |
| 607 | \begin{equation} |
| 608 | \judge{ |
| 609 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{bstrbind} \longrightarrow SE |
| 610 | }{ |
| 611 | \mit{M}, \Psi \vdash \mtt{structure}~ \mit{bstrbind} |
| 612 | \longrightarrow \mit{SE} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 613 | } |
| 614 | \end{equation} |
| 615 | |
| 616 | \begin{equation} |
| 617 | \judge{ |
| 618 | \mrm{Inter}~(\mit{B}~\mrm{of}~\mit{M}) \vdash \mit{bsigbind} \longrightarrow G |
| 619 | }{ |
| 620 | \mit{M}, \Psi \vdash \mtt{signature}~ \mit{bsigbind} |
| 621 | \longrightarrow \mit{G } ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 622 | } |
| 623 | \end{equation} |
| 624 | |
| 625 | \begin{equation} |
| 626 | \judge{ |
| 627 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{bfunbind} \longrightarrow F |
| 628 | }{ |
| 629 | \mit{M}, \Psi \vdash \mtt{functor}~ \mit{bfunbind} |
| 630 | \longrightarrow \mit{F} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 631 | } |
| 632 | \end{equation} |
| 633 | |
| 634 | \begin{equation} |
| 635 | \judge{ |
| 636 | }{ |
| 637 | \mit{M}, \Psi \vdash \quad \longrightarrow \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi |
| 638 | } |
| 639 | \end{equation} |
| 640 | |
| 641 | \begin{equation} |
| 642 | \judge{ |
| 643 | \mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad |
| 644 | \mit{M} + \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 |
| 645 | }{ |
| 646 | \mit{M}, \Psi \vdash \mit{basdec}_1 ~\langle\mtt{;}\rangle~ \mit{basdec}_2 \longrightarrow \mit{M}_1 \oplus \mit{M}_2, \Psi_2 |
| 647 | } |
| 648 | \end{equation} |
| 649 | |
| 650 | \begin{equation} |
| 651 | \label{eqn:mlb:DS:path.sml} |
| 652 | \judge{ |
| 653 | \mcal{P}(\mit{FE}~\mrm{of}~\mit{M}, \msf{path.sml}) = (\mit{FE}', \mit{topdec}) \quad |
| 654 | \mit{B}~\mrm{of}~\mit{M} \vdash \mit{topdec} \Rightarrow \mit{B}' |
| 655 | }{ |
| 656 | \mit{M}, \Psi \vdash \msf{path.sml} \longrightarrow (\mit{FE}',\{\},\mit{B}'), \Psi |
| 657 | } |
| 658 | \end{equation} |
| 659 | |
| 660 | \begin{equation} |
| 661 | \judge{ |
| 662 | \Psi(\msf{path.mlb}) = \mit{M}' |
| 663 | }{ |
| 664 | \mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi |
| 665 | } |
| 666 | \end{equation} |
| 667 | |
| 668 | \begin{equation} |
| 669 | \judge{ |
| 670 | \msf{path.mlb} \notin \mrm{Dom}~\Psi \quad |
| 671 | \mcal{P}(\msf{path.mlb}) = \mit{basdec} \quad |
| 672 | \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' |
| 673 | }{ |
| 674 | \mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi' + \{\msf{path.mlb} \mapsto \mit{M}'\} |
| 675 | } |
| 676 | \end{equation} |
| 677 | |
| 678 | \begin{samepage} |
| 679 | \noindent |
| 680 | \textit{Comments}: |
| 681 | \begin{itemize} |
| 682 | \item[(\ref{eqn:mlb:DS:path.sml})] |
| 683 | Note the use of the Definition's |
| 684 | $\mit{B} \vdash \mit{topdec} \Rightarrow \mit{B}'$. |
| 685 | \end{itemize} |
| 686 | \end{samepage} |
| 687 | |
| 688 | \vspace{2\parsep} |
| 689 | {\large\noindent |
| 690 | \textbf{Basis Bindings} \hfill |
| 691 | \fbox{$\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi' / p$} |
| 692 | }\nopagebreak |
| 693 | |
| 694 | \begin{equation} |
| 695 | \judge{ |
| 696 | \mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' \quad |
| 697 | \langle\mit{M}, \Psi' \vdash \mit{basbind} \longrightarrow \mit{BE}'', \Psi''\rangle |
| 698 | }{ |
| 699 | \mit{M}, \Psi \vdash \mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~\mit{basbind}\rangle \longrightarrow |
| 700 | \{\mit{basid} \mapsto \mit{M}'\} \langle+ \mit{BE}''\rangle, \Psi'\langle'\rangle |
| 701 | } |
| 702 | \end{equation} |
| 703 | |
| 704 | \vspace{2\parsep} |
| 705 | {\large\noindent |
| 706 | \textbf{(Basis) Structure Bindings} \hfill |
| 707 | \fbox{$\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}$} |
| 708 | }\nopagebreak |
| 709 | |
| 710 | \begin{equation} |
| 711 | \label{eqn:mlb:DS:bstrbind} |
| 712 | \judge{ |
| 713 | \mit{B}(\mit{strid}_2) = E \quad |
| 714 | \langle\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}\rangle |
| 715 | }{ |
| 716 | \mit{B} \vdash \mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~\mit{bstrbind}\rangle \longrightarrow |
| 717 | \{\mit{strid}_1 \mapsto \mit{E}\} \langle+ \mit{SE}\rangle |
| 718 | } |
| 719 | \end{equation} |
| 720 | |
| 721 | \begin{samepage} |
| 722 | \noindent |
| 723 | \textit{Comments}: |
| 724 | \begin{itemize} |
| 725 | \item[(\ref{eqn:mlb:DS:bstrbind})] Note that $\mit{bstrbind} \subset |
| 726 | \mit{strbind}$. Hence, this rule can be derived from the |
| 727 | Definition's $\mit{B} \vdash \mit{strbind} \Rightarrow \mit{SE} / p$, noting that |
| 728 | the derivation may neither cause a side-effect nor generate an |
| 729 | exception packet. |
| 730 | \end{itemize} |
| 731 | \end{samepage} |
| 732 | |
| 733 | \vspace{2\parsep} |
| 734 | {\large\noindent |
| 735 | \textbf{(Basis) Signature Bindings} \hfill |
| 736 | \fbox{$\mit{IB} \vdash \mit{bsigbind} \longrightarrow \mit{G}$} |
| 737 | }\nopagebreak |
| 738 | |
| 739 | \begin{equation} |
| 740 | \label{eqn:mlb:DS:bsigbind} |
| 741 | \judge{ |
| 742 | \mit{IB}(\mit{sigid}_2) = I \quad |
| 743 | \langle\mit{IB} \vdash \mit{bsigbind} \longrightarrow \mit{G}\rangle |
| 744 | }{ |
| 745 | \mit{IB} \vdash \mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~\mit{bsigbind}\rangle \longrightarrow |
| 746 | \{\mit{sigid}_1 \mapsto I\} \langle+ \mit{G}\rangle |
| 747 | } |
| 748 | \end{equation} |
| 749 | |
| 750 | \begin{samepage} |
| 751 | \noindent |
| 752 | \textit{Comments}: |
| 753 | \begin{itemize} |
| 754 | \item[(\ref{eqn:mlb:DS:bsigbind})] Note that $\mit{bsigbind} \subset |
| 755 | \mit{sigbind}$. Hence, this rule can be derived from the |
| 756 | Definition's $\mit{IB} \vdash \mit{sigbind} \Rightarrow \mit{G}$, noting that |
| 757 | the derivation may neither cause a side-effect nor generate an |
| 758 | exception packet. |
| 759 | \end{itemize} |
| 760 | \end{samepage} |
| 761 | |
| 762 | \vspace{2\parsep} |
| 763 | {\large\noindent |
| 764 | \textbf{(Basis) Functor Bindings} \hfill |
| 765 | \fbox{$\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}$} |
| 766 | }\nopagebreak |
| 767 | |
| 768 | \begin{equation} |
| 769 | \judge{ |
| 770 | \mit{B}(\mit{funid}_2) = (\mit{strid}:\mit{I},\mit{strexp},\mit{B}) \quad |
| 771 | \langle\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}\rangle |
| 772 | }{ |
| 773 | \mit{B} \vdash \mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~\mit{bfunbind}\rangle \longrightarrow |
| 774 | \{\mit{funid}_1 \mapsto (\mit{strid}:\mit{I},\mit{strexp},\mit{B})\} \langle+ \mit{F}\rangle |
| 775 | } |
| 776 | \end{equation} |
| 777 | |
| 778 | \appendix |
| 779 | \section{Derived Forms} |
| 780 | \label{sec:mlb:DerivedForms} |
| 781 | Figure~\ref{fig:mlb:DF:bindings} shows derived forms for structure, |
| 782 | signature, and functor bindings in MLB. These derived forms are |
| 783 | a useful shorthand for specifying import and export filters. |
| 784 | |
| 785 | \begin{figure}[h] |
| 786 | \begin{center} |
| 787 | \begin{tabular}{|l|l|} |
| 788 | \multicolumn{1}{c}{Derived Form} & |
| 789 | \multicolumn{1}{c}{Equivalent Form} \\ |
| 790 | \multicolumn{2}{c}{} \\ |
| 791 | \multicolumn{2}{l}{\textbf{(Basis) Structure Bindings} $\mit{bstrbind}$} \\ |
| 792 | \hline |
| 793 | $\mit{strid} ~\langle\mtt{and}~ \mit{bstrbind}\rangle$ & |
| 794 | $\mit{strid} ~\mtt{=}~ \mit{strid} ~\langle\mtt{and}~ \mit{bstrbind}\rangle$ \\ |
| 795 | \hline |
| 796 | \multicolumn{2}{c}{} \\ |
| 797 | \multicolumn{2}{l}{\textbf{(Basis) Signature Bindings} $\mit{bsigbind}$} \\ |
| 798 | \hline |
| 799 | $\mit{sigid} ~\langle\mtt{and}~ \mit{bsigbind}\rangle$ & |
| 800 | $\mit{sigid} ~\mtt{=}~ \mit{sigid} ~\langle\mtt{and}~ \mit{bsigbind}\rangle$ \\ |
| 801 | \hline |
| 802 | \multicolumn{2}{c}{} \\ |
| 803 | \multicolumn{2}{l}{\textbf{(Basis) Functor Bindings} $\mit{bfunbind}$} \\ |
| 804 | \hline |
| 805 | $\mit{funid} ~\langle\mtt{and}~ \mit{bfunbind}\rangle$ & |
| 806 | $\mit{funid} ~\mtt{=}~ \mit{funid} ~\langle\mtt{and}~ \mit{bfunbind}\rangle$ \\ |
| 807 | \hline |
| 808 | \end{tabular} |
| 809 | \end{center} |
| 810 | \caption{Derived forms of (Basis) Structure, Signature, and Functor Bindings}\label{fig:mlb:DF:bindings} |
| 811 | \end{figure} |
| 812 | |
| 813 | \bibliographystyle{alpha} |
| 814 | \bibliography{bib} |
| 815 | |
| 816 | \end{document} |