33 Procedural Abstraction
In introducing mutable state in the previous chapter (Section 32.1), we left out functions. When “functions” can be imperative, they are called procedures. Procedures allow reusing code but are very different than mathematical functions.
Naively applying substitution for function call does not make any sense: \[ \begin{array}{rrl} (\texttt{(} \texttt{i} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \texttt{i} \mathrel{\texttt{=}} \texttt{1} \texttt{,}\,\texttt{console}\texttt{.}\texttt{log}\texttt{(} \texttt{i} \texttt{)} ) \texttt{(} \texttt{2} \texttt{)} & \longrightarrow& {}[ \texttt{2} / \texttt{i} ] ( \texttt{i} \mathrel{\texttt{=}} \texttt{1} \texttt{,}\,\texttt{console}\texttt{.}\texttt{log}\texttt{(} \texttt{i} \texttt{)} ) \\ & = & { ( \texttt{2} \mathrel{\texttt{=}} \texttt{1} \texttt{,}\,\texttt{console}\texttt{.}\texttt{log}\texttt{(} \texttt{2} \texttt{)} ) } \end{array} \]
33.1 Static Memory
The formalization of mutable variables in the previous chapter (Chapter 32) effectively considered each variable corresponding to dynamically-allocated memory cell upon executing a \(\mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2\) declaration. Memories \(m\) had the following form: \[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[a \mapsto v] \end{array} \]
where addresses \(a\) were dynamically allocated.
This might have felt overkill, as without procedures, the number of mutable cells needed can be statically determined. A formalization where memories look like “updatable environments”
\[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[x \mapsto v] \end{array} \]
would seem sufficient. However, we know from previous discussion that naively extending such a formalization to procedures would result in dynamic scoping (cf. Chapter 19).
We shall see that introducing addresses, along with distinguishing between values and memory locations is essential for procedural abstraction.
33.2 TypeScripty: Procedures
Let us consider imperative TypeScripty with procedures.
33.2.1 Syntax
Let us consider the abstract syntax of TypeScripty with procedures. We consider parameters to be mutable variables, which we make explicit here with the \(\mathbf{var}\) parameter mode annotation (cf. Figure 27.1 from Section 27.1). In JavaScript/TypeScript, all parameters are in essence declared as mutable variables \(\mathbf{var}\).
\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{number}\mid\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \\ \text{values} & v& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid x \mid e_1\texttt{(}e_2\texttt{)} \mid x \mathrel{\texttt{=}}e_1 \mid\mathord{\texttt{*}}a \end{array} \]
33.2.2 Small-Step Operational Semantics
Let us consider the small-step operational semantics of TypeScripty with procedures:
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoDeref]{ }{ \langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle m(a) , m \rangle }\)
\(\inferrule[DoAssignVar]{ }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle }\)
\(\inferrule[DoCall]{ a\notin \operatorname{dom}(m) }{ \langle (\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(} v_2 \texttt{)} , m \rangle \longrightarrow \langle {}[ \mathord{\texttt{*}}a /x]e_1 , m[a \mapsto v_2] \rangle }\)
\(\inferrule[SearchAssign2]{ \langle e_2', m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} e_2' , m' \rangle }\)
\(\inferrule[SearchCall1]{ e_1 \longrightarrow e_1' }{ e_1\texttt{(}e_2\texttt{)} \longrightarrow e_1'\texttt{(}e_2\texttt{)} }\)
\(\inferrule[SearchCall2]{ e_2 \longrightarrow e_2' }{ (\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow (\texttt{(}x\texttt{:}\, \mathbf{var}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1)\texttt{(}e_2'\texttt{)} }\)
In rule \(\TirName{DoCall}\), we use substitution to implement static scoping with call-by-value semantics (cf. Figure 27.2 from Section 27.1.2). The dereference expression \(\mathord{\texttt{*}}a\) emphasizes that we distinguish between the memory location named by \(a\) and the content at that location \(m(a)\), as we see in rules \(\TirName{DoDeref}\) and \(\TirName{DoAssignVar}\).
Compare rule \(\TirName{DoCall}\) to rule \(\TirName{DoVarDecl}\) in Figure 32.4 from Section 32.1.2.
33.3 JavaScripty: Pointers
In JavaScript, objects are mutable and dynamically-allocated. Their memory addresses are their values. That is, JavaScript does have a form of pointers.
33.3.1 Syntax
Let us consider the abstract syntax of JavaScripty with pointers.
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& n \mid\texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}} \mid e_1 \mathrel{\texttt{=}}e_2 \mid e_1\texttt{.}f \mid x \mid\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \\ \text{values} & v& \mathrel{::=}& n\mid a \\ \text{location values} & l& \mathrel{::=}& a\texttt{.}f \\ \text{addresses} & a \end{array} \]
We include constant-variable declarations to emphasize that object fields may be mutable, while the pointer values are themselves may be bound to immutable variables.
33.3.2 Small-Step Operational Semantics
A memory cell \([a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ]\) holds an object \(\texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}}\):
\[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ] \end{array} \]
The small-step operational semantics with dynamically-allocated, mutable objects is thus as follows:
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoObject]{ a\notin \operatorname{dom}(m) }{ \langle \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} , m \rangle \longrightarrow \langle a, m[a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ] \rangle }\)
\(\inferrule[DoGetField]{ m(a) = \texttt{\{} \ldots\texttt{,} f\texttt{:}\,v\texttt{,} \ldots \texttt{\}} }{ \langle a\texttt{.}f , m \rangle \longrightarrow \langle v, m \rangle }\)
\(\inferrule[DoAssignField]{ m(a) = \texttt{\{} \ldots\texttt{,} f\texttt{:}\,v\texttt{,} \ldots \texttt{\}} }{ \langle a\texttt{.}f \mathrel{\texttt{=}} v' , m \rangle \longrightarrow \langle v' , m[a \mapsto \texttt{\{} \ldots\texttt{,} f\texttt{:}\,v'\texttt{,} \ldots \texttt{\}} ] \rangle }\)
\(\inferrule[SearchObject]{ \langle e_i, m \rangle \longrightarrow \langle e_i', m' \rangle }{ \langle \texttt{\{} \ldots\texttt{,}f_i\texttt{:}\,e_i\texttt{,}\ldots \texttt{\}} , m \rangle \longrightarrow \langle \texttt{\{} \ldots\texttt{,}f_i\texttt{:}\,e_i'\texttt{,}\ldots \texttt{\}} , m' \rangle }\)
\(\inferrule[SearchGetField]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle e_1\texttt{.}f , m \rangle \longrightarrow \langle e_1'\texttt{.}f , m' \rangle }\)
\(\inferrule[SearchAssign2]{ \langle e_2', m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle a\texttt{.}f \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle a\texttt{.}f \mathrel{\texttt{=}} e_2' , m' \rangle }\)
\(\inferrule[DoConstDecl]{ }{ \langle \mathbf{const}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle {}[v_1/x]e_2 , m \rangle }\)
\(\inferrule[SearchConstDecl]{ \langle e_1', m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle \mathbf{const}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 , m' \rangle }\)
There is a \(\TirName{DoObject}\) rule that allocates a memory address \(a\), stores the object at that memory location \([a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ]\), and returns the pointer \(a\) to the object \(\texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}}\) as its value.