trait Expr // e
case class Assign(e1: Expr, e2: Expr) extends Expr // e ::= e1 = e2defined trait Expr defined class Assign
34 Lab: Imperative Computation
Learning Goals
The primary goals of this lab are to understand the following:
- imperative computation;
- mutation and aliasing;
- programming with encapsulated effects.
- Functional Programming Skills
- Encapsulating computation in a data structure library.
- Programming Language Ideas
- Imperative computation (e.g., memory, addresses, aliasing).
Instructions
A version of project files for this lab resides in the public pppl-lab5 repository. Please follow separate instructions to get a private clone of this repository for your work.
You will be replacing ??? or case _ => ??? in the Lab5.scala file with solutions to the coding exercises described below.
Your lab will not be graded if it does not compile. You may check compilation with your IDE, sbt compile, or with the “sbt compile” GitHub Action provided for you. Comment out any code that does not compile or causes a failing assert. Put in ??? as needed to get something that compiles without error.
You may add additional tests to the Lab5Spec.scala file. In the Lab5Spec.scala, there is empty test class Lab5StudentSpec that you can use to separate your tests from the given tests in the Lab5Spec class. You are also likely to edit Lab5.worksheet.sc for any scratch work. You can also use Lab5.worksheet.ts to write and experiment in a JavaScript file that you can then parse into a TypeScripty AST (see Lab5.worksheet.sc).
If you like, you may use this notebook for experimentation. However, please make sure your code is in Lab5.scala; code in this notebook will not graded.
34.1 TypeScripty: Mutable Variables and Objects
34.1.0.1 Imperative Computation
In this lab, we build on all of the techniques throughout the course to explore imperative computation. We consider the imperative core of JavaScript that has mutable variables and dynamically-allocated mutable objects.
Concretely, we will see that supporting imperative programming language features forces a global refactoring of our interpreter. To minimize the impact of this refactoring, we will be use the functional programming idea of encapsulating effects in a data type (known as a monad).
Additionally, we consider parameter passing modes to illustrate different possible language design decisions and how design decisions manifest in the operational semantics. Call-by-value with pointer values and call-by-reference are often confused, but with the operational semantics, we can see clearly the distinction. JavaScript, like most languages, fixes one parameter passing mode—all parameters are allocated as mutable variables and arguments are passed by value. Other parameter passing modes can be reasonably simulated with other language features, so having different parameter passing modes can be seen as somewhat exotic.
34.1.0.2 Assignment
We introduce an assignment expression
\[ e_1 \mathrel{\texttt{=}}e_2 \]
that writes the value of \(e_2\) to a memory location named by expression \(e_1\). Note that we use the C and JavaScript-style assignment operator \(\texttt{=}\), which unfortunately looks like mathematical equality but is very different.
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& e_1 \mathrel{\texttt{=}}e_2 \end{array} \]
For the dynamic semantics, we define an auxiliary judgment form \(e\;\mathsf{location}\) to specify expression forms that specify memory locations (i.e., locations or l-values).
def isLValue(e: Expr): Boolean = ???defined function isLValue
34.1.0.3 Mutable Variable Allocation
We introduce mutable variables declared as follows:
\[ \mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \]
A \(\mathbf{var}\) declaration allocates a new mutable variable \(x\), assigns it an initial value from evaluating \(e_1\), and whose scope is \(e_2\).
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid x \\ \text{parameter modes} & d& \mathrel{::=}& \mathbf{const}\mid\mathbf{var} \\ \text{variables} & x \end{array} \]
Note that the concrete syntax of JavaScript has two mutable variable declaration forms with var and let that differ in the scope of the declared variable.
For simplicity and uniformity, we consider a single abstract syntax form for variable declarations \(d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2\) whose scope is given as \(e_2\). The \(d\) may be \(\mathbf{const}\)-mode that binds the value of \(e_1\) to variable \(x\) for use in \(e_2\) as before or now may be \(\mathbf{var}\)-mode that allocates a new mutable variable initialized to the value of \(e_1\) for use in \(e_2\).
case class Decl(d: Mode, x: String, e1: Expr, e2: Expr) extends Expr // e ::= d x = e1; e2
case class Var(x: String) extends Expr // e ::= x
trait Mode // d
case object MConst extends Mode // d ::= const
case object MVar extends Mode // d ::= vardefined class Decl defined class Var defined trait Mode defined object MConst defined object MVar
We can think of a mutable variable as a box that can be filled with a value, and then the value can be updated by filling the box with a new value. A memory cell \([a \mapsto v]\) is such a box that has an address \(a\) to reference that box. A memory \(m\) is then a finite set of such memory cells:
\[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot\mid m[a \mapsto v] \\ \text{addresses} & a \end{array} \]
We add addresses \(a\), as well as an address dereference operator \(\mathord{\texttt{*}}e_1\), to the expression language to use as intermediate expressions during reduction:
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& a \mid\mathop{\mathit{uop}} e_1 \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{*} \end{array} \]
case class A(a: Int) extends Expr // e ::= a
case class Unary(uop: Uop, e1: Expr) extends Expr // e ::= uop e1
trait Uop // uop
case object Deref extends Uop // uop ::= *defined class A defined class Unary defined trait Uop defined object Deref
To formalize mutable variables in JavaScript, the address dereference expression \(\mathord{\texttt{*}}e_1\) is not strictly necessary, but it helps us conceptually distinguish between the address \(a\) from its use in naming the memory cell \([a \mapsto v]\). The \(\mathord{\texttt{*}}e_1\) expression corresponds to the pointer-dereference expression in the C and C++ languages.
We state the \(\mathord{\texttt{*}}a\) names a memory location for a mutable variable (i.e., is an l-value):
\(\fbox{$e\;\mathsf{location}$}\)
\(\inferrule[VarLocation]{ }{ \mathord{\texttt{*}}a \;\mathsf{location} }\)
def isLValue(e: Expr): Boolean = e match {
case Unary(Deref, A(_)) => true
case _ => false
}defined function isLValue
34.1.0.4 Dynamically-Allocated Mutable Objects
We consider the expression syntax of objects but now implement them as dynamically-allocated mutable objects as in JavaScript:
\[ \begin{array}{rrrl} \text{types} & \tau& \mathrel{::=}& \texttt{\{} \overline{ f\texttt{:}\,\tau } \texttt{\}} \\ \text{values} & v& \mathrel{::=}& a \\[1ex] \text{expressions} & e& \mathrel{::=}& \texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}} \mid e_1\texttt{.}f \end{array} \]
trait Typ
case class TObj(fts: Map[String, Typ]) extends Typ // t ::= { fts }
case class Obj(fes: Map[String,Expr]) extends Expr // e ::= { fes }
case class GetField(e1: Expr, f: String) extends Expr // e ::= e1.fdefined trait Typ defined class TObj defined class Obj defined class GetField
The value of an object expression \(\texttt{\{} \overline{ f\texttt{:}\,e } \texttt{\}}\) is address \(a\) at which the object is stored in memory (i.e., a pointer to the object is its value).
Memories for dynamically-allocated mutable objects store objects at addresses:
\[ \begin{array}{rrrl} \text{memories} & m& \mathrel{::=}& \cdot \mid m[a \mapsto \texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}} ] \end{array} \]
A field of an object is an assignable memory location:
\(\fbox{$e\;\mathsf{location}$}\)
\(\inferrule[FieldLocation]{ }{ a\texttt{.}f \;\mathsf{location} }\)
def isLValue(e: Expr): Boolean = e match {
case Unary(Deref, A(_)) | GetField(A(_), _) => true
case _ => false
}defined function isLValue
With both mutable variables and mutable objects, we have two kinds of memory cells and two forms of l-values.
34.1.0.5 Location References
Call-by-value with pointer values and call-by-reference are often confused, so we formalize the notion of location references, that is, sharing a memory location with a variable alias. Aliasing refers to the concept that the same memory location may be referenced using two different program expressions.
In particular, on a procedure call, we may want a parameter of the callee to alias a previously allocated memory location (i.e., a call-by-reference parameter).
\[ \begin{array}{rrrl} \text{parameter modes} & d& \mathrel{::=}& \mathbf{ref} \\[1ex] \text{types} & \tau& \mathrel{::=}& \texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' \\ \text{values} & v& \mathrel{::=}& x^{?}\texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid x \mid x^{?}\texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e_1 \mid e_0\texttt{(} \overline{e} \texttt{)} \\ \text{variables} & x \\ \text{optional variables} & x^{?}& \mathrel{::=}& x\mid\varepsilon \\ \text{optional type annotations} & \tau^{?}& \mathrel{::=}& \texttt{:}\,\tau \mid\varepsilon \end{array} \]
case object MRef extends Mode // mode ::= refdefined object MRef
case class MTyp(d: Mode, t: Typ) // d t
case class TFun(ydts: List[(String,MTyp)], tret: Typ) extends Typ // t ::= (ydts) => tret
trait Expr // e
case class Fun(xopt: Option[String], ydts: List[(String,MTyp)], tretopt: Option[Typ], e1: Expr) extends Expr // e ::= xopt(ydts)tretopt => e1
case class Call(e0: Expr, es: List[Expr]) extends Expr // e ::= e0(es)defined class MTyp defined class TFun defined trait Expr defined class Fun defined class Call
We extend parameter modes \(d\) with \(\mathbf{ref}\) parameters. Note that procedure parameters now have a mode annotation in the abstract syntax.
We do not introduce first-class references (i.e., we do not have reference values or reference types as in C++ or Rust).
Note that in low-level languages, pointers and references both correspond to memory addresses in implementation, so one source of confusion may be that pointers are sometimes called references.
34.2 Interpreter Implementation
We break our interpreter implementation into evaluation and type checking.
34.2.0.1 Small-Step Reduction
For evaluation, we continue with implementing a small-step operational semantics with a step that implements a single reduction step
\[ \langle e, m \rangle \longrightarrow \langle e', m' \rangle \]
on closed expressions that says informally, “Expression \(e\) with memory \(m\) steps to a new configuration with expression \(e'\) and memory \(m'\).” The memory \(m\) is a map from addresses \(a\) to contents, which can be values \(v\) or objects \(\texttt{\{}\overline{f\texttt{:}\,v}\texttt{\}}\). The presence of a memory \(m\) that gets updated during evaluation is the hallmark of imperative computation.
To simplify the implementation (and minimize bugs), we implement step using the following type signature:
def step(e: Expr): DoWith[Mem, Expr] = ???where DoWith[Mem, Expr] is a data type that encapsulates a function of type Mem => (Mem, Expr), which we can see corresponds to \(m\), \(m'\), and \(e'\), respectively, in the judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \). The main advantage of using the encapsulated computation type DoWith[Mem,Expr] is that we can put this common-case threading into the DoWith library.
34.2.0.1.1 Memory
We define Mem as an abstract data type to represent memories \(m\) as a wrapper around a Scala Map[A, Expr] (cf. the Mutable State chapter (?sec-implementation-memories)).
Some rules require allocating fresh addresses. In the implementation, call memalloc(k) to get a fresh address with the memory cell initialized to contents k:
def memalloc(k: Expr): DoWith[Mem, A]34.2.0.2 Static Type Checking
As before, we define the judgment form \(\Gamma \vdash e : \tau\), which says, “In type environment \(\Gamma\), expression \(e\) has type \(\tau\).”
Because we need to distinguish between assignable expressions that specify memory locations (e.g., \(x\) declared as \(\mathbf{var}\)) versus non-assignable expressions (e.g., \(n\)), type environments now map variables \(x\) to their mode \(d\) and type \(\tau\): \[ \begin{array}{rrrl} \text{type environments} & \Gamma& \mathrel{::=}& \cdot\mid\Gamma, x : d\,\tau \end{array} \]
Note that it would be arguably cleaner to define type environments to carry just the needed assumptions (i.e., “assignability” and type). For our purposes, the mode \(d\) is a placeholder for “assignability.”
We then implement a function hastype:
def hastype(tenv: Map[String, MTyp], e: Expr): Typ = ???defined function hastype
that corresponds directly to this judgment form. It takes as input a type environment tenv: Map[String, MTyp] (\(\Gamma\)) and an expression e: Expr (\(e\)) to return a type Typ (\(\tau\)).
Notes
- Note that the provided tests are minimal. You will want to add your own tests to cover most language features.
- As before, we recommend “incrementally grow the language” by going language-feature by-language-feature rather than function-by-function in your implementation. In the subsequent steps, we describe the small-step operational semantics and the static typing semantics together incrementally by language feature.
34.3 Base TypeScripty
34.3.1 Small-Step Reduction
We consider the base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, \(\mathbf{undefined}\) with printing, and \(\mathbf{const}\)-variable declarations.
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoNeg]{ n' = - n_1 }{ \langle \mathop{\texttt{-}} n_1, m \rangle \longrightarrow \langle n', m \rangle }\)
\(\inferrule[DoArith]{ n' = n_1 \mathbin{\mathit{bop}}n_2 \and \mathit{bop}\in \left\{ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/} \right\} }{ \langle n_1 \mathbin{\mathit{bop}}n_2, m \rangle \longrightarrow \langle n', m \rangle }\)
\(\inferrule[DoPlusString]{ \mathit{str}' = \mathit{str}_1 \mathit{str}_2 }{ \langle \mathit{str}_1 \mathbin{\texttt{+}} \mathit{str}_2, m \rangle \longrightarrow \langle \mathit{str}', m \rangle }\)
\(\inferrule[DoInequalityNumber]{ b' = n_1 \mathbin{\mathit{bop}}n_2 \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \langle n_1 \mathbin{\mathit{bop}}n_2, m \rangle \longrightarrow \langle b', m \rangle }\)
\(\inferrule[DoInequalityString]{ b' = \mathit{str}_1 \mathbin{\mathit{bop}}\mathit{str}_2 \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \langle \mathit{str}_1 \mathbin{\mathit{bop}}\mathit{str}_2, m \rangle \longrightarrow \langle b', m \rangle }\)
\(\inferrule[DoEquality]{ b' = (v_1 \mathbin{\mathit{bop}}v_2) \and \mathit{bop}\in \left\{ \texttt{===}, \texttt{!==} \right\} }{ \langle v_1 \mathbin{\mathit{bop}}v_2, m \rangle \longrightarrow \langle b', m \rangle }\)
\(\inferrule[DoNot]{ b' = \neg b_1 }{ \langle \mathop{\texttt{!}} b_1, m \rangle \longrightarrow \langle b', m \rangle }\)
\(\inferrule[DoAndTrue]{ }{ \langle \mathbf{true} \mathbin{\texttt{\&\&}} e_2, m \rangle \longrightarrow \langle e_2, m \rangle }\)
\(\inferrule[DoAndFalse]{ }{ \langle \mathbf{false} \mathbin{\texttt{\&\&}} e_2, m \rangle \longrightarrow \langle v_1, m \rangle }\)
\(\inferrule[DoOrTrue]{ }{ \langle \mathbf{true} \mathbin{\texttt{||}} e_2, m \rangle \longrightarrow \langle v_1, m \rangle }\)
\(\inferrule[DoOrFalse]{ }{ \langle \mathbf{false} \mathbin{\texttt{||}} e_2, m \rangle \longrightarrow \langle e_2, m \rangle }\)
\(\inferrule[DoIfTrue]{ }{ \langle \mathbf{true}\;\texttt{?}\;e_2\;\texttt{:}\;e_3, m \rangle \longrightarrow \langle e_2, m \rangle }\)
\(\inferrule[DoIfFalse]{ }{ \langle \mathbf{false}\;\texttt{?}\;e_2\;\texttt{:}\;e_3, m \rangle \longrightarrow \langle e_3, m \rangle }\)
\(\inferrule[DoSeq]{ }{ \langle v_1 \mathbin{\texttt{,}} e_2, m \rangle \longrightarrow \langle e_2, m \rangle }\)
\(\inferrule[DoPrint]{ \text{$v_1$ printed} }{ \langle \texttt{console}\texttt{.}\texttt{log}\texttt{(}v_1\texttt{)}, m \rangle \longrightarrow \langle \mathbf{undefined}, 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[SearchUnary]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathop{\mathit{uop}}e_1, m \rangle \longrightarrow \langle \mathop{\mathit{uop}}e_1', m' \rangle }\)
\(\inferrule[SearchBinary1]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle e_1 \mathbin{\mathit{bop}}e_2, m \rangle \longrightarrow \langle e_1' \mathbin{\mathit{bop}}e_2, m' \rangle }\)
\(\inferrule[SearchBinary2]{ \langle e_2, m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle v_1 \mathbin{\mathit{bop}}e_2, m \rangle \longrightarrow \langle v_1 \mathbin{\mathit{bop}}e_2', m' \rangle }\)
\(\inferrule[SearchIf]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3, m \rangle \longrightarrow \langle e_1'\;\texttt{?}\;e_2\;\texttt{:}\;e_3, m' \rangle }\)
\(\inferrule[SearchPrint]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1\texttt{)}, m \rangle \longrightarrow \langle \texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1'\texttt{)}, 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 }\)
Exercise 34.1 (Small-Step Reduction for Base TypeScripty) Implement step for base TypeScripty following the small-step operational semantics in Figure 34.10 defining the reduction-step judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \).
Note that your task here is essentially refactoring a step function for the pure language features that do not use memory Mem to thread it. Because we are implementing step with type Expr => DoWith[Mem, Expr], the code changes here is minimal and type-directed.
34.3.2 Static Type Checking
We define static typing with the judgment form \(\Gamma \vdash e : \tau\) of base TypeScripty that has numbers with arithmetic expressions, booleans with logic and comparison expressions, strings with concatenation, \(\mathbf{undefined}\) with printing, and \(\mathbf{const}\)-variable as before:
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeNumber]{ }{ \Gamma \vdash n : \texttt{number} }\)
\(\inferrule[TypeString]{ }{ \Gamma \vdash \mathit{str} : \texttt{string} }\)
\(\inferrule[TypeNeg]{ \Gamma \vdash e_1 : \texttt{number} }{ \Gamma \vdash \mathop{\texttt{-}} e_1 : \texttt{number} }\)
\(\inferrule[TypeArith]{ \Gamma \vdash e_1 : \texttt{number} \and \Gamma \vdash e_2 : \texttt{number} \and \mathit{bop}\in \left\{ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{number} }\)
\(\inferrule[TypePlusString]{ \Gamma \vdash e_1 : \texttt{string} \and \Gamma \vdash e_2 : \texttt{string} }{ \Gamma \vdash e_1 \mathbin{\texttt{+}} e_2 : \texttt{string} }\)
\(\inferrule[TypeInequalityNumber]{ \Gamma \vdash e_1 : \texttt{number} \and \Gamma \vdash e_2 : \texttt{number} \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeInequalityString]{ \Gamma \vdash e_1 : \texttt{string} \and \Gamma \vdash e_2 : \texttt{string} \and \mathit{bop}\in \left\{ \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeEquality]{ \Gamma \vdash e_1 : \tau \and \Gamma \vdash e_2 : \tau \and \mathit{bop}\in \left\{ \texttt{===}, \texttt{!==} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeBool]{ }{ \Gamma \vdash b : \texttt{bool} }\)
\(\inferrule[TypeNot]{ \Gamma \vdash e_1 : \texttt{bool} }{ \Gamma \vdash \mathop{\texttt{!}} e_1 : \texttt{bool} }\)
\(\inferrule[TypeAndOr]{ \Gamma \vdash e_1 : \texttt{bool} \and \Gamma \vdash e_2 : \texttt{bool} \and \mathit{bop}\in \left\{ \texttt{\&\&}, \texttt{||} \right\} }{ \Gamma \vdash e_1 \mathbin{\mathit{bop}}e_2 : \texttt{bool} }\)
\(\inferrule[TypeIf]{ \Gamma \vdash e_1 : \texttt{bool} \and \Gamma \vdash e_2 : \tau \and \Gamma \vdash e_3 : \tau }{ \Gamma \vdash e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 : \tau }\)
\(\inferrule[TypeUndefined]{ }{ \Gamma \vdash \mathbf{undefined} : \texttt{Undefined} }\)
\(\inferrule[TypeSeq]{ \Gamma \vdash e_1 : \tau_1 \and \Gamma \vdash e_2 : \tau_2 }{ \Gamma \vdash e_1 \mathbin{\texttt{,}} e_2 : \tau_2 }\)
\(\inferrule[TypePrint]{ \Gamma \vdash e_1 : \tau_1 }{ \Gamma \vdash \texttt{console}\texttt{.}\texttt{log}\texttt{(}e_1\texttt{)} : \texttt{Undefined} }\)
\(\inferrule[TypeConstDecl]{ \Gamma \vdash e_1 : \tau_1 \and \Gamma, x : \mathbf{const}\,\tau_1 \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 : \tau_2 }\)
We will maintain the invariant that a variable use \(x\) corresponds to its assumed type, regardless of its mode \(d\), so we may generalize the typing of all variable uses and declarations:
\(\inferrule[TypeVar]{ x : d\,\tau \in \Gamma }{ \Gamma \vdash x : \tau }\)
Exercise 34.2 (Static Type Checking for Base TypeScripty) Implement a function hastype for base TypeScript following the static typing semantics in Figure 34.11 and Figure 34.12 defining the typing judgment form \(\Gamma \vdash e : \tau\).
34.4 Mutable Variables
34.4.1 Small-Step Reduction
A location value \(\mathord{\texttt{*}}a\) specifies a memory cell \([a \mapsto v]\) corresponding to a mutable variable \(x\). Observe that \(\TirName{DoDeref}\) corresponds to reading a mutable variable, \(\TirName{DoAssignVar}\) to assigning to a mutable variable, and \(\TirName{DoVarDecl}\) to allocating a new mutable variable. See the Mutable State chapter (?sec-javascripty-variables-smallstep) for a more in-depth discussion.
\(\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[SearchAssign2Var]{ \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[DoVarDecl]{ a\notin \operatorname{dom}(m) }{ \langle \mathbf{var}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle {}[ \mathord{\texttt{*}}a /x]e_2 , m[a \mapsto v_1] \rangle }\)
\(\inferrule[SearchVarDecl]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle \mathbf{var}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 , m' \rangle }\)
Exercise 34.3 (Small-Step Reduction for Mutable Variables) Implement the cases in step for reducing mutable variables using the rules given in Figure 34.13 for the reduction-step judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \).
34.4.2 Static Type Checking
We check that the left-hand–side of assignment is an assignable, mutable variable:
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeAssignVar]{ x : \mathbf{var}\,\tau \in \Gamma \and \Gamma \vdash e : \tau }{ \Gamma \vdash x \mathrel{\texttt{=}}e : \tau }\)
\(\inferrule[TypeVarDecl]{ \Gamma \vdash e_1 : \tau_1 \and \Gamma, x : \mathbf{var}\,\tau_1 \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 : \tau_2 }\)
Exercise 34.4 (Static Type Checking for Mutable Variables) Implement the cases in hastype for typing mutable variable expressions using the rules given in Figure 34.14 defining the typing judgment form \(\Gamma \vdash e : \tau\).
34.5 Dynamically-Allocated Mutable Objects
34.5.1 Small-Step Reduction
The \(\TirName{DoObject}\) rule states that an object \(\texttt{\{} \overline{ f\texttt{:}\,v } \texttt{\}}\) is not a value and steps an address (i.e., a pointer). In particular, it 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. See the section on Pointers (Section 33.3.2) for further discussion.
\(\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[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 }\)
The \(\TirName{DoAssignField}\) rule is as expected—replacing the value of an object field given by a location value \(a\texttt{.}f\):
\(\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[SearchAssign2]{ e_1\;\mathsf{location} \and \langle e_2, m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle e_1 \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle e_1 \mathrel{\texttt{=}} e_2' , m' \rangle }\)
\(\inferrule[SearchAssign1]{ \nvdash e_1\;\mathsf{location} \and \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle e_1 \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle e_1' \mathrel{\texttt{=}} e_2 , m' \rangle }\)
However, now its possible that the left-hand–side of assignment needs to be reduced to a location value. With mutable variables, we knew and assumed that the left-hand–side would immediately by its location value by substitution. We generalize the search rules for the assignment expression \(e_1 \mathrel{\texttt{=}}e_2\) to reduce \(e_1\) to a location value (i.e., satisfies \(e_1\;\mathsf{location}\)) with rule \(\TirName{SearchAssign1}\). We write \(\nvdash e_1\;\mathsf{location}\) for when \(e_1\) is not a location value. The \(\TirName{SearchAssign2}\) rule generalizes \(\TirName{SearchAssign2Var}\) above for reducing the right-hand–side of assignment to a value.
In implementation, the judgment form \(e_1\;\mathsf{location}\) is specified by the isLValue function.
Exercise 34.5 (Small-Step Reduction for Mutable Objects) Implement the cases in step for reducing dynamically-allocated mutable objects using the rules given in Figure 34.15 and Figure 34.16 for the reduction-step judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \).
34.5.2 Static Type Checking
Typing of object literals and reading from a field is unchanged because allocation and reading from memory is a run-time consideration:
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeObject]{ \Gamma \vdash e_i : \tau_i \and \text{for all $i$} }{ \Gamma \vdash \texttt{\{} \ldots\texttt{,} f_i\texttt{:}\,e_i\texttt{,} \ldots \texttt{\}} : \texttt{\{} \ldots\texttt{,} f_i\texttt{:}\,\tau_i\texttt{,} \ldots \texttt{\}} }\)
\(\inferrule[TypeGetField]{ \Gamma \vdash e : \texttt{\{} \ldots\texttt{,} f\texttt{:}\,\tau\texttt{,} \ldots \texttt{\}} }{ \Gamma \vdash e\texttt{.}f : \tau }\)
We also need to check that the left-hand–side of assignment could be an assignable field:
\(\inferrule[TypeAssignField]{ \Gamma \vdash e_1 : \texttt{\{} \ldots\texttt{,} f\texttt{:}\,\tau\texttt{,} \ldots \texttt{\}} \and \Gamma \vdash e_2 : \tau }{ \Gamma \vdash e_1\texttt{.}f \mathrel{\texttt{=}}e_2 : \tau }\)
Exercise 34.6 (Static Type Checking for Mutable Objects) Implement the cases in hastype for typing dynamically-allocated mutable object expressions using the rules given in Figure 34.17 and Figure 34.18 defining the typing judgment form \(\Gamma \vdash e : \tau\).
34.6 Location References
34.6.1 Small-Step Reduction
A reference variable is one that uses a previously-allocated location:
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoRefDecl]{ e_1\;\mathsf{location} }{ \langle \mathbf{ref}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle {}[ e_1 /x]e_2 , m \rangle }\)
\(\inferrule[SearchRefDecl]{ \nvdash e_1\;\mathsf{location} \and \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathbf{ref}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle \mathbf{ref}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 , m' \rangle }\)
Exercise 34.7 (Small-Step Reduction for Location References) Implement the cases in step for reducing location references using the rules given in Figure 34.19 for the reduction-step judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \).
34.6.2 Static Type Checking
Examining the \(\TirName{DoRefDecl}\) rule in the operational semantics, we see that we need to ensure that statically the binding expression \(e_1\) refers to a location (i.e., either a mutable variable or field). We considered this case-by-case, but let us define a judgment form that captures this concept:
\[ \Gamma \vdash e \mathrel{\mathord{:}\mathord{\&}} \tau \]
says informally, “In typing environment \(\Gamma\), expression \(e\) is a location expression whose contents have type \(\tau\).” This judgment form is the static analogue of the run-time judgment form \(e\;\mathsf{location}\).
We implement this judgment form with the following Scala function:
def hasloctype(tenv: Map[String, MTyp], e: Expr): Option[Typ] = ???defined function hasloctype
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeRefDecl]{ \Gamma \vdash e_1 \mathrel{\mathord{:}\mathord{\&}} \tau_1 \and \Gamma, x : \mathbf{ref}\,\tau_1 \vdash e_2 : \tau_2 }{ \Gamma \vdash \mathbf{ref}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 : \tau_2 }\)
\(\inferrule[TypeAssign]{ \Gamma \vdash e_1 \mathrel{\mathord{:}\mathord{\&}} \tau \and \Gamma \vdash e_2 : \tau }{ \Gamma \vdash e_1 \mathrel{\texttt{=}}e_2 : \tau }\)
With this location-typing judgment form, we can replace \(\TirName{TypeAssignVar}\) and \(\TirName{TypeAssignField}\) with the \(\TirName{TypeAssign}\) rule given above. And we see that the location-typing judgment form specifies that mutable variables or fields are location expressions, which we had previously inlined:
\(\fbox{$\Gamma \vdash e \mathrel{\mathord{:}\mathord{\&}} \tau$}\)
\(\inferrule[LocTypeVar]{ x : d\,\tau \in \Gamma \and d\in \left\{ \mathbf{var}, \mathbf{ref} \right\} }{ \Gamma \vdash x \mathrel{\mathord{:}\mathord{\&}} \tau }\)
\(\inferrule[LocTypeGetField]{ \Gamma \vdash e : \texttt{\{} \ldots\texttt{,} f\texttt{:}\,\tau\texttt{,} \ldots \texttt{\}} }{ \Gamma \vdash e\texttt{.}f \mathrel{\mathord{:}\mathord{\&}} \tau }\)
We see here in the \(\TirName{LocTypeVar}\) rule that it would arguably be clearer for the typing environment to carry location assumptions, rather than the varable mode \(d\) directly.
Exercise 34.8 (Static Type Checking for Mutable Variables) Implement the cases in hastype for typing location reference expressions using the rules given in Figure 34.20 defining the typing judgment form \(\Gamma \vdash e : \tau\) and hasloctype for the location typing judgment form \(\Gamma \vdash e \mathrel{\mathord{:}\mathord{\&}} \tau\) using the rules given in Figure 34.21.
34.7 Multi-Parameter Procedures with Parameter-Passing Modes (Extra Credit)
For procedures, we want to support an arbitrary number of parameters that may be individually declared with any parameter-passing mode. To avoid re-encoding the case analysis of the \(\TirName{DoConstDecl}\), \(\TirName{SearchConstDecl}\), \(\TirName{DoVarDecl}\), \(\TirName{SearchVarDecl}\), and \(\TirName{DoRefDecl}\), and \(\TirName{SearchRefDecl}\) rules, we define the \(\TirName{DoCall}\) and \(\TirName{DoCallRec}\) rules to transform the parameter binding to a variable binding expression \(e'\).
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoCall]{ e' = d_1\;y_1\;\texttt{=}\;e_1\texttt{;}\; \cdots\texttt{;}d_n\;y_n\;\texttt{=}\;e_n\texttt{;}\; e }{ \langle (\texttt{(} y_1\texttt{:}\, d_1\,\tau_1 \texttt{,}\ldots\texttt{,}y_n\texttt{:}\, d_n\,\tau_n \texttt{)}\tau^{?} \mathrel{\texttt{=}\!\texttt{>}} e) \texttt{(}e_1\texttt{,}\ldots\texttt{,}e_n\texttt{)} , m \rangle \longrightarrow \langle e' , m \rangle }\)
\(\inferrule[DoCallRec]{ v= (x\texttt{(} y_1\texttt{:}\, d_1\,\tau_1 \texttt{,}\ldots\texttt{,}y_n\texttt{:}\, d_n\,\tau_n \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e) \and e' = d_1\;y_1\;\texttt{=}\;e_1\texttt{;}\; \cdots\texttt{;}d_n\;y_n\;\texttt{=}\;e_n\texttt{;}\; e }{ \langle v\texttt{(} e_1\texttt{,}\ldots\texttt{,}e_n \texttt{)} , m \rangle \longrightarrow \langle {}[v/x]e' , m \rangle }\)
\(\inferrule[SearchCall1]{ e\longrightarrow e' }{ e\texttt{(}e_1, \ldots, e_n\texttt{)} \longrightarrow e'\texttt{(}e_1, \ldots, e_n\texttt{)} }\)
Observe that there is no \(\TirName{SearchCall2}\) rule that reduces the arguments, as the appropriate reduction of those arguments happens via the \(\TirName{SearchConstDecl}\), \(\TirName{SearchVarDecl}\), and \(\TirName{SearchRefDecl}\) rules.
34.7.1 Small-Step Reduction
Exercise 34.9 (Small-Step Reduction for Parameter-Passing Modes) Implement the cases in step for reducing procedures with parameter passing modes using the rules given in Figure 34.22 for the reduction-step judgment form \( \langle e, m \rangle \longrightarrow \langle e', m' \rangle \).
34.7.2 Static Type Checking
For typing, we similarly want to avoid re-encoding the case analysis of the \(\TirName{TypeConstDecl}\), \(\TirName{TypeVarDecl}\), and \(\TirName{TypeRefDecl}\). Let us define a judgment form that combines the cases to state state when an expression is well-typed for a given mode:
\[ \Gamma \vdash e : d\,\tau \]
saying, “In type environment \(\Gamma\), expression \(e\) has type \(\tau\) and can be bound to a variable with mode \(d\).”
\(\fbox{$\Gamma \vdash e : d\,\tau$}\)
\(\inferrule[ValBindable]{ \Gamma \vdash e : \tau \and d\in \left\{ \mathbf{const}, \mathbf{var} \right\} }{ \Gamma \vdash e : d\,\tau }\)
\(\inferrule[RefBindable]{ \Gamma \vdash e \mathrel{\mathord{:}\mathord{\&}} \tau }{ \Gamma \vdash e : \mathbf{ref}\,\tau }\)
We implement this judgment form with the following Scala function:
def hasmodetype(tenv: Map[String, MTyp], e: Expr, d: Mode): Option[Typ] = ???defined function hasmodetype
We can then define the \(\TirName{TypeDecl}\) and \(\TirName{TypeCall}\) rules as follows:
\(\fbox{$\Gamma \vdash e : \tau$}\)
\(\inferrule[TypeDecl]{ \Gamma \vdash e_1 : d\,\tau_1 \and \Gamma, x : d\,\tau_1 \vdash e_2 : \tau_2 }{ \Gamma \vdash d\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 : \tau_2 }\)
\(\inferrule[TypeCall]{ \Gamma \vdash e : \texttt{(} y_1\texttt{:}\,d_1\,\tau_1\texttt{,}\ldots\texttt{,}y_n\texttt{:}\,d_n\,\tau_n \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau \and \Gamma \vdash e_1 : d_1\,\tau_1 \quad\cdots\quad \Gamma \vdash e_n : d_n\,\tau_n }{ \Gamma \vdash e\texttt{(}e_1, \ldots, e_n\texttt{)} : \tau }\)
Note that we can use the \(\TirName{TypeDecl}\) rule to replace the \(\TirName{TypeConstDecl}\), \(\TirName{TypeVarDecl}\), and \(\TirName{TypeRefDecl}\) rules. You may optionally refactor your implementation to use \(\TirName{TypeDecl}\).
Typing of function literals remains essentially the same, except that declared modes are also assumed in the typing environment:
\(\inferrule[TypeFunction]{ \Gamma, y_1 : d_1\,\tau_1, \cdots , y_n : d_n\,\tau_n \vdash e' : \tau' }{ \Gamma \vdash \texttt{(} \overline{y\texttt{:}\, d\,\tau } \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e' : \texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }\)
\(\inferrule[TypeFunctionAnn]{ \Gamma, y_1 : d_1\,\tau_1, \cdots, , y_n : d_n\,\tau_n \vdash e' : \tau' }{ \Gamma \vdash \texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e' : \texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }\)
\(\inferrule[TypeFunctionRec]{ \Gamma, x : \mathbf{const}\,\tau_x , y_1 : d_1\,\tau_1, \cdots, , y_n : d_n\,\tau_n \vdash e' : \tau' \and \tau_x = \texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \mathrel{\texttt{=}\!\texttt{>}} \tau' }{ \Gamma \vdash x\texttt{(} \overline{y\texttt{:}\,d\,\tau} \texttt{)} \texttt{:}\,\tau' \mathrel{\texttt{=}\!\texttt{>}} e' : \tau_x }\)
Exercise 34.10 (Static Type Checking for Parameter-Passing Modes) Implement the cases in hastype for typing procedures with parameter-passing modes using the rules given in Figure 34.24 and Figure 34.25 defining the typing judgment form \(\Gamma \vdash e : \tau\) and hasmodetype for typing with bindablity to a given variable mode in Figure 34.23.