Meeting 27 - Procedural Abstraction

Bor-Yuh Evan Chang

Tuesday, December 3, 2024

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferrule}[3][]{ \let\and\qquad \begin{array}{@{}l@{}} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Meeting 27 - Procedural Abstraction

What questions does your neighbor have?

Links

In-Class Slides
In-Class Jupyter

Announcements

• Remainder of the Semester
  • HW 5 and Lab 5 before Thanksgiving break
  • Unit 6 (probably one combined assignment) Lab 5 after Thanksgiving break
  • Exam 5-6 in the last week of classes before the Final
• Come see us to make a study plan
  • e.g., via the redo policy
  • see the Final Exam as an opportunity to show growth from mid-semester exams.

Today

• Procedural Abstraction
  • Lazy Evaluation
  • Mutable State
• Triage Your Questions

Questions?

• Review:
  • What is the essence of imperative computation?

Procedures

What are procedures?

When “functions” can be imperative, they are called procedures. Procedures allow reusing code but are very different than mathematical functions.

Assignment

\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& \cdots \mid x \mathrel{\texttt{=}}e_1 \end{array} \]

What if we applied substitution as before?

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} \]

Static Memory

Without procedure call, dynamically-allocated memory addresses seems overkill. \[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[x \mapsto v] \end{array} \]

\[ \inferrule[DoAssignVar]{ }{ \langle x \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[x \mapsto v] \rangle } \]

But what does this form of memory look like?

Procedures: Syntax

\[ \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} \]

Figure 1: Syntax of TypeScripty with number literals, procedure literals, procedure calls, and mutable variable assignment.

Procedures: Semantics

\(\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{)} }\)

Figure 2: Small-step operational semantics of TypeScripty with number literals, procedure literals, procedure calls, and mutable variable assignment.

Procedures: Implementation

defined trait Expr
defined class N
defined class Var
defined class Assign
defined class Deref
defined class A
defined function isValue

defined class Mem
defined object Mem

defined class DoWith
defined object DoWith
import DoWith._

defined function memalloc

defined function substitute

defined function step

Parameter-Passing Modes

Small changes in \(\TirName{DoCall}\).

Call-By-Name Parameters: Syntax

\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{number}\mid\texttt{(}x\texttt{:}\, m\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \\ \text{values} & v& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, m\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& n\mid\texttt{(}x\texttt{:}\, m\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid x \mid e_1\texttt{(}e_2\texttt{)} \mid m\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \\ \text{parameter modes} & m& \mathrel{::=}& \mathbf{const}\mid\mathbf{name} \end{array} \]

Figure 3: Syntax of TypeScripty with number literals, function literals with parameter modes, and variable declarations, and function call expressions.

Call-By-Name Parameters: Semantics

\(\fbox{$e \longrightarrow e'$}\)

\(\inferrule[DoCallByValue]{ }{ (\texttt{(}x\texttt{:}\, \mathbf{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}v_2\texttt{)} \longrightarrow{}[v_2/x]e_1 }\)

\(\inferrule[DoCallByName]{ }{ (\texttt{(}x\texttt{:}\, \mathbf{name}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow{}[e_2/x]e_1 }\)

\(\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{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}e_2\texttt{)} \longrightarrow (\texttt{(}x\texttt{:}\, \mathbf{const}\,\tau \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1)\texttt{(}e_2'\texttt{)} }\)

\(\inferrule[DoConstDecl]{ }{ \mathbf{const}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 \longrightarrow {}[v_1/x]e_2 }\)

\(\inferrule[DoNameDecl]{ }{ \mathbf{name}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow {}[e_1/x]e_2 }\)

\(\inferrule[SearchConstDecl]{ e_1 \longrightarrow e_1' }{ \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow\mathbf{const}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 }\)

Figure 4: Small-step operational semantics of TypeScripty with number literals, function literals with parameter modes, variable declarations, and function call expressions.

Exotic Parameter-Passing Modes

Reference parameters (as in C++ and C#)?

Out parameters (as in C#)?

In-out parameters (as in Ada)?

Pointers

First-class addresses (i.e., when “addresses are values”).

Dynamically-Allocated Mutable Objects: Syntax

\[ \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} \]

Figure 5: Syntax of TypeScripty with number literals and dynamically-allocated mutable objects.

Dynamically-Allocated Mutable Objects: Semantics

\[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ] \end{array} \]

Figure 6: Memories for JavaScripty with dynamically-allocated mutable objects.

Dynamically-Allocated Mutable Objects: Semantics

\(\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 }\)

Figure 7: Small-step operational semantics of JavaScripty with dynamically-allocated mutable objects.

Aliasing

const a = { val: 1 };
const b = a;
b.val = 42;
console.log(a.val)