aboutsummaryrefslogtreecommitdiff
path: root/lab5/imperative-computation-lab.ipynb
diff options
context:
space:
mode:
Diffstat (limited to 'lab5/imperative-computation-lab.ipynb')
-rw-r--r--lab5/imperative-computation-lab.ipynb1522
1 files changed, 1522 insertions, 0 deletions
diff --git a/lab5/imperative-computation-lab.ipynb b/lab5/imperative-computation-lab.ipynb
new file mode 100644
index 0000000..b26fe3b
--- /dev/null
+++ b/lab5/imperative-computation-lab.ipynb
@@ -0,0 +1,1522 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "8e3502cc",
+ "metadata": {},
+ "source": [
+ "Before you turn this problem in, make sure everything runs as expected. First, **restart the kernel** (in the menubar, select Kernel $\\rightarrow$ Restart) and then **run all cells** (in the menubar, select Cell $\\rightarrow$ Run All).\n",
+ "\n",
+ "Make sure you fill in any place that says `???`, `YOUR CODE HERE`, \"???\", \"YOUR ANSWER HERE\", as well as your name and collaborators below:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "a71e0446",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "val NAME = \"\"\n",
+ "val COLLABORATORS = \"\""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ac39c01f",
+ "metadata": {},
+ "source": [
+ "---"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d2d5fb3c-8d64-445f-9f8c-52390c9ce652",
+ "metadata": {},
+ "source": [
+ "$\\newcommand{\\TirName}[1]{\\text{#1}}\n",
+ "\\newcommand{\\inferrule}[3][]{\n",
+ " \\let\\and\\qquad\n",
+ " \\begin{array}{@{}l@{}}\n",
+ " \\TirName{#1}\n",
+ " \\\\\n",
+ " \\displaystyle\n",
+ " \\frac{#2}{#3}\n",
+ " \\end{array}\n",
+ "}\n",
+ "\\newcommand{\\infer}[3][]{\\inferrule[#1]{#2}{#3}}\n",
+ "$\n",
+ "\n",
+ "# Lab: Imperative Computation\n",
+ "\n",
+ "<!-- 3 Expressions -->\n",
+ "\n",
+ "<!-- 4 Binding and Scope -->\n",
+ "\n",
+ "<!-- 8 Recursion -->\n",
+ "\n",
+ "<!-- 9 Inductive Data Types -->\n",
+ "\n",
+ "<!-- 11 Concrete Syntax -->\n",
+ "\n",
+ "<!-- 12 Abstract Syntax and Parsing -->\n",
+ "\n",
+ "<!-- 13 Exercise: Syntax -->\n",
+ "\n",
+ "<!-- 14 Static Scoping -->\n",
+ "\n",
+ "<!-- 15 Judgments -->\n",
+ "\n",
+ "<!-- 16 Variables, Basic Values, and Judgments Lab -->\n",
+ "\n",
+ "<!-- 18 Operational Semantics -->\n",
+ "\n",
+ "<!-- 19 Functions and Dynamic Scoping -->\n",
+ "\n",
+ "<!-- 20 Big-Step Exercise -->\n",
+ "\n",
+ "<!-- 21 Evaluation Order -->\n",
+ "\n",
+ "<!-- 26 Static Type Checking -->\n",
+ "\n",
+ "<!-- 27 Lazy Evaluation -->\n",
+ "\n",
+ "<!-- 28 Objects -->\n",
+ "\n",
+ "<!-- 28 Static Type Checking Lab -->\n",
+ "\n",
+ "<!-- 30 Mutable State -->\n",
+ "\n",
+ "<!-- Encapsulating Effects Exercise -->\n",
+ "\n",
+ "<!-- Imperative Lab -->\n",
+ "\n",
+ "### Learning Goals\n",
+ "\n",
+ "The primary goals of this lab are to understand the following:\n",
+ "\n",
+ "- imperative computation;\n",
+ "- mutation and aliasing;\n",
+ "- programming with encapsulated effects.\n",
+ "\n",
+ "Functional Programming Skills \n",
+ "Encapsulating computation in a data structure library.\n",
+ "\n",
+ "Programming Language Ideas \n",
+ "Imperative computation (e.g., memory, addresses, aliasing).\n",
+ "\n",
+ "### Instructions\n",
+ "\n",
+ "A version of project files for this lab resides in the public\n",
+ "[pppl-lab5](https://github.com/csci3155/pppl-lab5) repository. Please\n",
+ "follow separate instructions to get a private clone of this repository\n",
+ "for your work.\n",
+ "\n",
+ "You will be replacing `???` or `case _ => ???` in the `Lab5.scala` file\n",
+ "with solutions to the coding exercises described below.\n",
+ "\n",
+ "**Your lab will not be graded if it does not compile**. You may check\n",
+ "compilation with your IDE, `sbt compile`, or with the “sbt compile”\n",
+ "GitHub Action provided for you. Comment out any code that does not\n",
+ "compile or causes a failing assert. Put in `???` as needed to get\n",
+ "something that compiles without error.\n",
+ "\n",
+ "You may add additional tests to the `Lab5Spec.scala` file. In the\n",
+ "`Lab5Spec.scala`, there is empty test class `Lab5StudentSpec` that you\n",
+ "can use to separate your tests from the given tests in the `Lab5Spec`\n",
+ "class. You are also likely to edit `Lab5.worksheet.sc` for any scratch\n",
+ "work. You can also use `Lab5.worksheet.ts` to write and experiment in a\n",
+ "JavaScript file that you can then parse into a TypeScripty AST (see\n",
+ "`Lab5.worksheet.sc`).\n",
+ "\n",
+ "If you like, you may use this notebook for experimentation. However,\n",
+ "**please make sure your code is in `Lab5.scala`; code in this notebook\n",
+ "will not graded.**\n",
+ "\n",
+ "## TypeScripty: Mutable Variables and Objects\n",
+ "\n",
+ "#### Imperative Computation\n",
+ "\n",
+ "In this lab, we build on all of the techniques throughout the course to\n",
+ "explore imperative computation. We consider the imperative core of\n",
+ "JavaScript that has mutable variables and dynamically-allocated mutable\n",
+ "objects.\n",
+ "\n",
+ "Concretely, we will see that supporting imperative programming language\n",
+ "features forces a global refactoring of our interpreter. To minimize the\n",
+ "impact of this refactoring, we will be use the functional programming\n",
+ "idea of encapsulating effects in a data type (known as a monad).\n",
+ "\n",
+ "Additionally, we consider parameter passing modes to illustrate\n",
+ "different possible language design decisions and how design decisions\n",
+ "manifest in the operational semantics. Call-by-value with pointer values\n",
+ "and call-by-reference are often confused, but with the operational\n",
+ "semantics, we can see clearly the distinction. JavaScript, like most\n",
+ "languages, fixes one parameter passing mode—all parameters are allocated\n",
+ "as mutable variables and arguments are passed by value. Other parameter\n",
+ "passing modes can be reasonably simulated with other language features,\n",
+ "so having different parameter passing modes can be seen as somewhat\n",
+ "exotic.\n",
+ "\n",
+ "#### Assignment\n",
+ "\n",
+ "We introduce an assignment expression\n",
+ "\n",
+ "$$\n",
+ "e_1 \\mathrel{\\texttt{=}}e_2\n",
+ "$$\n",
+ "\n",
+ "that writes the value of $e_2$ to a memory location named by expression\n",
+ "$e_1$. Note that we use the C and JavaScript-style assignment operator\n",
+ "$\\texttt{=}$, which unfortunately looks like mathematical equality but\n",
+ "is very different.\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{expressions} & e& \\mathrel{::=}& e_1 \\mathrel{\\texttt{=}}e_2\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 1: Abstract syntax of JavaScripty with assignment."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "f42708b7",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "trait Expr // e\n",
+ "case class Assign(e1: Expr, e2: Expr) extends Expr // e ::= e1 = e2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "069961b2-918c-4338-9aa3-801953140900",
+ "metadata": {},
+ "source": [
+ "For the dynamic semantics, we define an auxiliary judgment form\n",
+ "$e\\;\\mathsf{location}$ to specify expression forms that specify memory\n",
+ "locations (i.e., *locations* or *l-values*)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "18302934",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def isLValue(e: Expr): Boolean = ???"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "75b1e7b2-21c7-4ebe-86ed-67a97f26c488",
+ "metadata": {},
+ "source": [
+ "#### Mutable Variable Allocation\n",
+ "\n",
+ "We introduce *mutable variables* declared as follows:\n",
+ "\n",
+ "$$\n",
+ "\\mathbf{var}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2\n",
+ "$$\n",
+ "\n",
+ "A $\\mathbf{var}$ declaration allocates a new mutable variable $x$,\n",
+ "assigns it an initial value from evaluating $e_1$, and whose scope is\n",
+ "$e_2$.\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{expressions} & e& \\mathrel{::=}&\n",
+ "d\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2\n",
+ "\\mid x\n",
+ "\\\\\n",
+ "\\text{parameter modes} & d& \\mathrel{::=}& \\mathbf{const}\\mid\\mathbf{var}\n",
+ "\\\\\n",
+ "\\text{variables} & x\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 2: Abstract syntax of JavaScripty with $\\mathbf{const}$- and\n",
+ "$\\mathbf{var}$-variable declarations.\n",
+ "\n",
+ "Note that the concrete syntax of JavaScript has two mutable variable\n",
+ "declaration forms with `var` and `let` that differ in the scope of the\n",
+ "declared variable.\n",
+ "\n",
+ "For simplicity and uniformity, we consider a single abstract syntax form\n",
+ "for variable declarations $d\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2$ whose\n",
+ "scope is given as $e_2$. The $d$ may be $\\mathbf{const}$-mode that binds\n",
+ "the value of $e_1$ to variable $x$ for use in $e_2$ as before or now may\n",
+ "be $\\mathbf{var}$-mode that allocates a new mutable variable initialized\n",
+ "to the value of $e_1$ for use in $e_2$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "73823007",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "case class Decl(d: Mode, x: String, e1: Expr, e2: Expr) extends Expr // e ::= d x = e1; e2\n",
+ "case class Var(x: String) extends Expr // e ::= x\n",
+ "\n",
+ "trait Mode // d\n",
+ "case object MConst extends Mode // d ::= const\n",
+ "case object MVar extends Mode // d ::= var"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "731e2bbc-c582-4d97-b581-0479ee0ac4c7",
+ "metadata": {},
+ "source": [
+ "We can think of a mutable variable as a box that can be filled with a\n",
+ "value, and then the value can be updated by filling the box with a new\n",
+ "value. A memory cell $[a \\mapsto v]$ is such a box that has an address\n",
+ "$a$ to reference that box. A memory $m$ is then a finite set of such\n",
+ "memory cells:\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{memories} & m& \\mathrel{::=}& \\cdot\\mid m[a \\mapsto v]\n",
+ "\\\\\n",
+ "\\text{addresses} & a\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 3: Memories for JavaScripty with mutable variables.\n",
+ "\n",
+ "We add addresses $a$, as well as an address dereference operator\n",
+ "$\\mathord{\\texttt{*}}e_1$, to the expression language to use as\n",
+ "intermediate expressions during reduction:\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{expressions} & e& \\mathrel{::=}&\n",
+ "a\n",
+ "\\mid\\mathop{\\mathit{uop}} e_1\n",
+ "\\\\\n",
+ "\\text{unary operators} & \\mathit{uop}& \\mathrel{::=}& \\texttt{*}\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 4: Abstract syntax of JavaScripty with addresses and an address\n",
+ "dereference operator."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "7350e1c0",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "case class A(a: Int) extends Expr // e ::= a\n",
+ "case class Unary(uop: Uop, e1: Expr) extends Expr // e ::= uop e1\n",
+ "\n",
+ "trait Uop // uop\n",
+ "case object Deref extends Uop // uop ::= *"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "19ba9db1-c21e-47f9-abcb-3cef3957c7d9",
+ "metadata": {},
+ "source": [
+ "To formalize mutable variables in JavaScript, the address dereference\n",
+ "expression $\\mathord{\\texttt{*}}e_1$ is not strictly necessary, but it\n",
+ "helps us conceptually distinguish between the address $a$ from its use\n",
+ "in naming the memory cell $[a \\mapsto v]$. The $\\mathord{\\texttt{*}}e_1$\n",
+ "expression corresponds to the pointer-dereference expression in the C\n",
+ "and C++ languages.\n",
+ "\n",
+ "We state the $\\mathord{\\texttt{*}}a$ names a memory location for a\n",
+ "mutable variable (i.e., is an l-value):\n",
+ "\n",
+ "$\\fbox{$e\\;\\mathsf{location}$}$\n",
+ "\n",
+ "$\\inferrule[VarLocation]{\n",
+ "}{\n",
+ " \\mathord{\\texttt{*}}a \\;\\mathsf{location}\n",
+ "}$\n",
+ "\n",
+ "Figure 5: Location values for JavaScripty with mutable variables."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "c548d3bc",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def isLValue(e: Expr): Boolean = e match {\n",
+ " case Unary(Deref, A(_)) => true\n",
+ " case _ => false\n",
+ "}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "04ed0f94-c328-4d37-8f08-13fc46c80227",
+ "metadata": {},
+ "source": [
+ "#### Dynamically-Allocated Mutable Objects\n",
+ "\n",
+ "We consider the expression syntax of objects but now implement them as\n",
+ "dynamically-allocated mutable objects as in JavaScript:\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ " \\text{types} & \\tau& \\mathrel{::=}&\n",
+ " \\texttt{\\{} \\overline{ f\\texttt{:}\\,\\tau } \\texttt{\\}} \n",
+ " \\\\\n",
+ " \\text{values} & v& \\mathrel{::=}& a\n",
+ " \\\\[1ex]\n",
+ " \\text{expressions} & e& \\mathrel{::=}& \n",
+ " \\texttt{\\{} \\overline{ f\\texttt{:}\\,e } \\texttt{\\}} \n",
+ " \\mid e_1\\texttt{.}f\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 6: Abstract syntax of JavaScripty with pointers and objects."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "81a59003",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "trait Typ\n",
+ "case class TObj(fts: Map[String, Typ]) extends Typ // t ::= { fts }\n",
+ "\n",
+ "case class Obj(fes: Map[String,Expr]) extends Expr // e ::= { fes }\n",
+ "case class GetField(e1: Expr, f: String) extends Expr // e ::= e1.f"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a571e116-507e-4a4a-9e20-d60b3c857fae",
+ "metadata": {},
+ "source": [
+ "The value of an object expression\n",
+ "$\\texttt{\\{} \\overline{ f\\texttt{:}\\,e } \\texttt{\\}}$ is address $a$ at\n",
+ "which the object is stored in memory (i.e., a *pointer* to the object is\n",
+ "its value).\n",
+ "\n",
+ "Memories for dynamically-allocated mutable objects store objects at\n",
+ "addresses:\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{memories} & m& \\mathrel{::=}& \\cdot \\mid m[a \\mapsto \\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}} ]\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 7: Memories for JavaScripty with dynamically-allocated mutable\n",
+ "objects.\n",
+ "\n",
+ "A field of an object is an assignable memory location:\n",
+ "\n",
+ "$\\fbox{$e\\;\\mathsf{location}$}$\n",
+ "\n",
+ "$\\inferrule[FieldLocation]{\n",
+ "}{\n",
+ " a\\texttt{.}f \\;\\mathsf{location}\n",
+ "}$\n",
+ "\n",
+ "Figure 8: Location values for JavaScripty with dynamically-allocated\n",
+ "mutable objects."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "7e650a31",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def isLValue(e: Expr): Boolean = e match {\n",
+ " case Unary(Deref, A(_)) | GetField(A(_), _) => true\n",
+ " case _ => false\n",
+ "}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "51d3ccbf-96c6-430e-8196-374cf7b88bb3",
+ "metadata": {},
+ "source": [
+ "With both mutable variables and mutable objects, we have two kinds of\n",
+ "memory cells and two forms of l-values.\n",
+ "\n",
+ "#### Location References\n",
+ "\n",
+ "Call-by-value with pointer values and call-by-reference are often\n",
+ "confused, so we formalize the notion of location *references*, that is,\n",
+ "sharing a memory location with a variable alias. *Aliasing* refers to\n",
+ "the concept that the same memory location may be referenced using two\n",
+ "different program expressions.\n",
+ "\n",
+ "In particular, on a procedure call, we may want a parameter of the\n",
+ "callee to alias a previously allocated memory location (i.e., a\n",
+ "call-by-reference parameter).\n",
+ "\n",
+ "$$\n",
+ "\\begin{array}{rrrl}\n",
+ "\\text{parameter modes} & d& \\mathrel{::=}& \\mathbf{ref}\n",
+ "\\\\[1ex]\n",
+ " \\text{types} & \\tau& \\mathrel{::=}& \\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau'\n",
+ " \\\\\n",
+ " \\text{values} & v& \\mathrel{::=}& x^{?}\\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)}\\tau^{?} \\mathrel{\\texttt{=}\\!\\texttt{>}} e_1\n",
+ " \\\\\n",
+ " \\text{expressions} & e& \\mathrel{::=}& \n",
+ " d\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2\n",
+ " \\mid x\n",
+ " \\mid x^{?}\\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)}\\tau^{?} \\mathrel{\\texttt{=}\\!\\texttt{>}} e_1\n",
+ " \\mid e_0\\texttt{(} \\overline{e} \\texttt{)}\n",
+ "\\\\\n",
+ "\\text{variables} & x\n",
+ "\\\\\n",
+ "\\text{optional variables} & x^{?}& \\mathrel{::=}& x\\mid\\varepsilon\n",
+ "\\\\\n",
+ "\\text{optional type annotations} & \\tau^{?}& \\mathrel{::=}& \\texttt{:}\\,\\tau \\mid\\varepsilon\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Figure 9: Abstract syntax of JavaScripty with $\\mathbf{ref}$-parameters."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "30c21c0c",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "case object MRef extends Mode // mode ::= ref"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "852f5962",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "case class MTyp(d: Mode, t: Typ) // d t\n",
+ "case class TFun(ydts: List[(String,MTyp)], tret: Typ) extends Typ // t ::= (ydts) => tret\n",
+ "\n",
+ "trait Expr // e\n",
+ "case class Fun(xopt: Option[String], ydts: List[(String,MTyp)], tretopt: Option[Typ], e1: Expr) extends Expr // e ::= xopt(ydts)tretopt => e1\n",
+ "case class Call(e0: Expr, es: List[Expr]) extends Expr // e ::= e0(es)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "016279fe-8a81-414c-9cb4-9cebe054a79a",
+ "metadata": {},
+ "source": [
+ "We extend parameter modes $d$ with $\\mathbf{ref}$ parameters. Note that\n",
+ "procedure parameters now have a mode annotation in the abstract syntax.\n",
+ "\n",
+ "We do not introduce first-class references (i.e., we do not have\n",
+ "reference values or reference types as in C++ or Rust).\n",
+ "\n",
+ "Note that in low-level languages, pointers and references both\n",
+ "correspond to memory addresses in implementation, so one source of\n",
+ "confusion may be that pointers are sometimes called references.\n",
+ "\n",
+ "## Interpreter Implementation\n",
+ "\n",
+ "We break our interpreter implementation into evaluation and type\n",
+ "checking.\n",
+ "\n",
+ "#### Small-Step Reduction\n",
+ "\n",
+ "For evaluation, we continue with implementing a small-step operational\n",
+ "semantics with a `step` that implements a single reduction step\n",
+ "\n",
+ "$$\n",
+ " \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle \n",
+ "$$\n",
+ "\n",
+ "on closed expressions that says informally, “Expression $e$ with memory\n",
+ "$m$ steps to a new configuration with expression $e'$ and memory $m'$.”\n",
+ "The memory $m$ is a map from addresses $a$ to contents, which can be\n",
+ "values $v$ or objects $\\texttt{\\{}\\overline{f\\texttt{:}\\,v}\\texttt{\\}}$.\n",
+ "The presence of a memory $m$ that gets updated during evaluation is the\n",
+ "hallmark of *imperative computation*.\n",
+ "\n",
+ "To simplify the implementation (and minimize bugs), we implement `step`\n",
+ "using the following type signature:\n",
+ "\n",
+ "``` scala\n",
+ "def step(e: Expr): DoWith[Mem, Expr] = ???\n",
+ "```\n",
+ "\n",
+ "where `DoWith[Mem, Expr]` is a data type that encapsulates a function of\n",
+ "type `Mem => (Mem, Expr)`, which we can see corresponds to $m$, $m'$,\n",
+ "and $e'$, respectively, in the judgment form\n",
+ "$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $. The\n",
+ "main advantage of using the encapsulated computation type\n",
+ "`DoWith[Mem,Expr]` is that we can put this common-case threading into\n",
+ "the `DoWith` library.\n",
+ "\n",
+ "##### Memory\n",
+ "\n",
+ "We define `Mem` as an abstract data type to represent memories $m$ as a\n",
+ "wrapper around a Scala `Map[A, Expr]` (cf. the Mutable State chapter\n",
+ "(**?@sec-implementation-memories**)).\n",
+ "\n",
+ "Some rules require allocating fresh addresses. In the implementation,\n",
+ "call `memalloc(k)` to get a fresh address with the memory cell\n",
+ "initialized to contents `k`:\n",
+ "\n",
+ "``` scala\n",
+ "def memalloc(k: Expr): DoWith[Mem, A]\n",
+ "```\n",
+ "\n",
+ "#### Static Type Checking\n",
+ "\n",
+ "As before, we define the judgment form $\\Gamma \\vdash e : \\tau$, which\n",
+ "says, “In type environment $\\Gamma$, expression $e$ has type $\\tau$.”\n",
+ "\n",
+ "Because we need to distinguish between assignable expressions that\n",
+ "specify memory locations (e.g., $x$ declared as $\\mathbf{var}$) versus\n",
+ "non-assignable expressions (e.g., $n$), type environments now map\n",
+ "variables $x$ to their mode $d$ and type $\\tau$: $$\n",
+ "\\begin{array}{rrrl}\n",
+ " \\text{type environments} & \\Gamma& \\mathrel{::=}& \\cdot\\mid\\Gamma, x : d\\,\\tau\n",
+ "\\end{array}\n",
+ "$$\n",
+ "\n",
+ "Note that it would be arguably cleaner to define type environments to\n",
+ "carry just the needed assumptions (i.e., “assignability” and type). For\n",
+ "our purposes, the mode $d$ is a placeholder for “assignability.”\n",
+ "\n",
+ "We then implement a function `hastype`:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "2e04c495",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def hastype(tenv: Map[String, MTyp], e: Expr): Typ = ???"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5b2e9eff-3747-42ed-ba9b-d043dca3f445",
+ "metadata": {},
+ "source": [
+ "that corresponds directly to this judgment form. It takes as input a\n",
+ "type environment `tenv: Map[String, MTyp]` ($\\Gamma$) and an expression\n",
+ "`e: Expr` ($e$) to return a type `Typ` ($\\tau$).\n",
+ "\n",
+ "#### Notes\n",
+ "\n",
+ "- Note that the provided tests are minimal. **You will want to add\n",
+ " your own tests to cover most language features.**\n",
+ "- As before, we recommend “incrementally grow the language” by going\n",
+ " language-feature by-language-feature rather than\n",
+ " function-by-function in your implementation. In the subsequent\n",
+ " steps, we describe the small-step operational semantics and the\n",
+ " static typing semantics together incrementally by language feature.\n",
+ "\n",
+ "## Base TypeScripty\n",
+ "\n",
+ "### Small-Step Reduction\n",
+ "\n",
+ "We consider the base TypeScripty that has numbers with arithmetic\n",
+ "expressions, booleans with logic and comparison expressions, strings\n",
+ "with concatenation, $\\mathbf{undefined}$ with printing, and\n",
+ "$\\mathbf{const}$-variable declarations.\n",
+ "\n",
+ "$\\fbox{$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $}$\n",
+ "\n",
+ "$\\inferrule[DoNeg]{\n",
+ " n' = - n_1\n",
+ "}{\n",
+ " \\langle \\mathop{\\texttt{-}} n_1, m \\rangle \\longrightarrow \\langle n', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoArith]{\n",
+ " n' = n_1 \\mathbin{\\mathit{bop}}n_2\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{+}, \\texttt{-}, \\texttt{*}, \\texttt{/} \\right\\}\n",
+ "}{\n",
+ " \\langle n_1 \\mathbin{\\mathit{bop}}n_2, m \\rangle \\longrightarrow \\langle n', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoPlusString]{\n",
+ " \\mathit{str}' = \\mathit{str}_1 \\mathit{str}_2\n",
+ "}{\n",
+ " \\langle \\mathit{str}_1 \\mathbin{\\texttt{+}} \\mathit{str}_2, m \\rangle \\longrightarrow \\langle \\mathit{str}', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoInequalityNumber]{\n",
+ " b' = n_1 \\mathbin{\\mathit{bop}}n_2\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{<}, \\texttt{<=}, \\texttt{>}, \\texttt{>=} \\right\\}\n",
+ "}{\n",
+ " \\langle n_1 \\mathbin{\\mathit{bop}}n_2, m \\rangle \\longrightarrow \\langle b', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoInequalityString]{\n",
+ " b' = \\mathit{str}_1 \\mathbin{\\mathit{bop}}\\mathit{str}_2\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{<}, \\texttt{<=}, \\texttt{>}, \\texttt{>=} \\right\\}\n",
+ "}{\n",
+ " \\langle \\mathit{str}_1 \\mathbin{\\mathit{bop}}\\mathit{str}_2, m \\rangle \\longrightarrow \\langle b', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoEquality]{\n",
+ " b' = (v_1 \\mathbin{\\mathit{bop}}v_2)\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{===}, \\texttt{!==} \\right\\}\n",
+ "}{\n",
+ " \\langle v_1 \\mathbin{\\mathit{bop}}v_2, m \\rangle \\longrightarrow \\langle b', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoNot]{\n",
+ " b' = \\neg b_1\n",
+ "}{\n",
+ " \\langle \\mathop{\\texttt{!}} b_1, m \\rangle \\longrightarrow \\langle b', m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoAndTrue]{\n",
+ "}{\n",
+ " \\langle \\mathbf{true} \\mathbin{\\texttt{\\&\\&}} e_2, m \\rangle \\longrightarrow \\langle e_2, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoAndFalse]{\n",
+ "}{\n",
+ " \\langle \\mathbf{false} \\mathbin{\\texttt{\\&\\&}} e_2, m \\rangle \\longrightarrow \\langle v_1, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoOrTrue]{\n",
+ "}{\n",
+ " \\langle \\mathbf{true} \\mathbin{\\texttt{||}} e_2, m \\rangle \\longrightarrow \\langle v_1, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoOrFalse]{\n",
+ "}{\n",
+ " \\langle \\mathbf{false} \\mathbin{\\texttt{||}} e_2, m \\rangle \\longrightarrow \\langle e_2, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoIfTrue]{\n",
+ "}{\n",
+ " \\langle \\mathbf{true}\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3, m \\rangle \\longrightarrow \\langle e_2, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoIfFalse]{\n",
+ "}{\n",
+ " \\langle \\mathbf{false}\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3, m \\rangle \\longrightarrow \\langle e_3, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoSeq]{\n",
+ "}{\n",
+ " \\langle v_1 \\mathbin{\\texttt{,}} e_2, m \\rangle \\longrightarrow \\langle e_2, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoPrint]{\n",
+ " \\text{$v_1$ printed}\n",
+ "}{\n",
+ " \\langle \\texttt{console}\\texttt{.}\\texttt{log}\\texttt{(}v_1\\texttt{)}, m \\rangle \\longrightarrow \\langle \\mathbf{undefined}, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoConstDecl]{\n",
+ "}{\n",
+ " \\langle \\mathbf{const}\\;x\\;\\texttt{=}\\;v_1\\texttt{;}\\;e_2, m \\rangle \\longrightarrow \\langle [v_1/x]e_2, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchUnary]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\langle \\mathop{\\mathit{uop}}e_1, m \\rangle \\longrightarrow \\langle \\mathop{\\mathit{uop}}e_1', m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchBinary1]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\langle e_1 \\mathbin{\\mathit{bop}}e_2, m \\rangle \\longrightarrow \\langle e_1' \\mathbin{\\mathit{bop}}e_2, m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchBinary2]{\n",
+ " \\langle e_2, m \\rangle \\longrightarrow \\langle e_2', m' \\rangle \n",
+ "}{\n",
+ " \\langle v_1 \\mathbin{\\mathit{bop}}e_2, m \\rangle \\longrightarrow \\langle v_1 \\mathbin{\\mathit{bop}}e_2', m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchIf]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\langle e_1\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3, m \\rangle \\longrightarrow \\langle e_1'\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3, m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchPrint]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchConstDecl]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "Figure 10: Small-step operational semantics of base TypeScripty,\n",
+ "including numbers with arithmetic expressions, booleans with logic and\n",
+ "comparison expressions, strings with concatenation, $\\mathbf{undefined}$\n",
+ "with printing, and $\\mathbf{const}$-variable declarations.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 1 (Small-Step Reduction for Base\n",
+ "TypeScripty)**</span> Implement `step` for base TypeScripty following\n",
+ "the small-step operational semantics in\n",
+ "<a href=\"#fig-typescripty-basemem-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 10</a> defining the reduction-step judgment\n",
+ "form $ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $.\n",
+ "\n",
+ "Note that your task here is essentially refactoring a `step` function\n",
+ "for the pure language features that do not use memory `Mem` to thread\n",
+ "it. Because we are implementing `step` with type\n",
+ "`Expr => DoWith[Mem, Expr]`, the code changes here is minimal and\n",
+ "type-directed.\n",
+ "\n",
+ "### Static Type Checking\n",
+ "\n",
+ "We define static typing with the judgment form $\\Gamma \\vdash e : \\tau$\n",
+ "of base TypeScripty that has numbers with arithmetic expressions,\n",
+ "booleans with logic and comparison expressions, strings with\n",
+ "concatenation, $\\mathbf{undefined}$ with printing, and\n",
+ "$\\mathbf{const}$-variable as before:\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e : \\tau$}$\n",
+ "\n",
+ "$\\inferrule[TypeNumber]{\n",
+ "}{\n",
+ " \\Gamma \\vdash n : \\texttt{number}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeString]{\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathit{str} : \\texttt{string}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeNeg]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{number}\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathop{\\texttt{-}} e_1 : \\texttt{number}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeArith]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{number}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\texttt{number}\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{+}, \\texttt{-}, \\texttt{*}, \\texttt{/} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\mathit{bop}}e_2 : \\texttt{number}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypePlusString]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{string}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\texttt{string}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\texttt{+}} e_2 : \\texttt{string}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeInequalityNumber]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{number}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\texttt{number}\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{<}, \\texttt{<=}, \\texttt{>}, \\texttt{>=} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\mathit{bop}}e_2 : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeInequalityString]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{string}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\texttt{string}\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{<}, \\texttt{<=}, \\texttt{>}, \\texttt{>=} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\mathit{bop}}e_2 : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeEquality]{\n",
+ " \\Gamma \\vdash e_1 : \\tau\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\tau\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{===}, \\texttt{!==} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\mathit{bop}}e_2 : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeBool]{\n",
+ "}{\n",
+ " \\Gamma \\vdash b : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeNot]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{bool}\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathop{\\texttt{!}} e_1 : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeAndOr]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{bool}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\texttt{bool}\n",
+ " \\and\n",
+ " \\mathit{bop}\\in \\left\\{ \\texttt{\\&\\&}, \\texttt{||} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\mathit{bop}}e_2 : \\texttt{bool}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeIf]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{bool}\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\tau\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_3 : \\tau\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3 : \\tau\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeUndefined]{\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathbf{undefined} : \\texttt{Undefined}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeSeq]{\n",
+ " \\Gamma \\vdash e_1 : \\tau_1\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\tau_2\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathbin{\\texttt{,}} e_2 : \\tau_2\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypePrint]{\n",
+ " \\Gamma \\vdash e_1 : \\tau_1\n",
+ "}{\n",
+ " \\Gamma \\vdash \\texttt{console}\\texttt{.}\\texttt{log}\\texttt{(}e_1\\texttt{)} : \\texttt{Undefined}\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeConstDecl]{\n",
+ " \\Gamma \\vdash e_1 : \\tau_1\n",
+ " \\and\n",
+ " \\Gamma, x : \\mathbf{const}\\,\\tau_1 \\vdash e_2 : \\tau_2\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathbf{const}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 : \\tau_2\n",
+ "}$\n",
+ "\n",
+ "Figure 11: Typing of base TypeScripty, including numbers with arithmetic\n",
+ "expressions, booleans with logic and comparison expressions, strings\n",
+ "with concatenation, $\\mathbf{undefined}$ with printing, and\n",
+ "$\\mathbf{const}$-varable declarations.\n",
+ "\n",
+ "We will maintain the invariant that a variable use $x$ corresponds to\n",
+ "its assumed type, regardless of its mode $d$, so we may generalize the\n",
+ "typing of all variable uses and declarations:\n",
+ "\n",
+ "$\\inferrule[TypeVar]{\n",
+ " x : d\\,\\tau \\in \\Gamma\n",
+ "}{\n",
+ " \\Gamma \\vdash x : \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 12: Typing of variable uses.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 2 (Static Type Checking for Base\n",
+ "TypeScripty)**</span> Implement a function `hastype` for base TypeScript\n",
+ "following the static typing semantics in\n",
+ "<a href=\"#fig-typescripty-basemem-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 11</a> and\n",
+ "<a href=\"#fig-typescripty-declmem-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 12</a> defining the typing judgment form\n",
+ "$\\Gamma \\vdash e : \\tau$.\n",
+ "\n",
+ "## Mutable Variables\n",
+ "\n",
+ "### Small-Step Reduction\n",
+ "\n",
+ "A location value $\\mathord{\\texttt{*}}a$ specifies a memory cell\n",
+ "$[a \\mapsto v]$ corresponding to a mutable variable $x$. Observe that\n",
+ "$\\TirName{DoDeref}$ corresponds to reading a mutable variable,\n",
+ "$\\TirName{DoAssignVar}$ to assigning to a mutable variable, and\n",
+ "$\\TirName{DoVarDecl}$ to allocating a new mutable variable. See the\n",
+ "Mutable State chapter (**?@sec-javascripty-variables-smallstep**) for a\n",
+ "more in-depth discussion.\n",
+ "\n",
+ "$\\fbox{$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $}$\n",
+ "\n",
+ "$\\inferrule[DoDeref]{\n",
+ "}{\n",
+ " \\langle \\mathord{\\texttt{*}}a , m \\rangle \\longrightarrow \\langle m(a) , m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoAssignVar]{\n",
+ "}{\n",
+ " \\langle \\mathord{\\texttt{*}}a \\mathrel{\\texttt{=}} v , m \\rangle \\longrightarrow \\langle v, m[a \\mapsto v] \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchAssign2Var]{\n",
+ " \\langle e_2, m \\rangle \\longrightarrow \\langle e_2', m' \\rangle \n",
+ "}{\n",
+ " \\langle \\mathord{\\texttt{*}}a \\mathrel{\\texttt{=}} e_2 , m \\rangle \\longrightarrow \\langle \\mathord{\\texttt{*}}a \\mathrel{\\texttt{=}} e_2' , m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoVarDecl]{\n",
+ " a\\notin \\operatorname{dom}(m)\n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchVarDecl]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "Figure 13: Small-step operational semantics with mutable variables.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 3 (Small-Step Reduction for\n",
+ "Mutable Variables)**</span> Implement the cases in `step` for reducing\n",
+ "mutable variables using the rules given in\n",
+ "<a href=\"#fig-typescripty-mutable-variables-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 13</a> for the reduction-step judgment form\n",
+ "$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $.\n",
+ "\n",
+ "### Static Type Checking\n",
+ "\n",
+ "We check that the left-hand–side of assignment is an assignable, mutable\n",
+ "variable:\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e : \\tau$}$\n",
+ "\n",
+ "$\\inferrule[TypeAssignVar]{\n",
+ " x : \\mathbf{var}\\,\\tau \\in \\Gamma\n",
+ " \\and\n",
+ " \\Gamma \\vdash e : \\tau\n",
+ "}{\n",
+ " \\Gamma \\vdash x \\mathrel{\\texttt{=}}e : \\tau\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeVarDecl]{\n",
+ " \\Gamma \\vdash e_1 : \\tau_1\n",
+ " \\and\n",
+ " \\Gamma, x : \\mathbf{var}\\,\\tau_1 \\vdash e_2 : \\tau_2\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathbf{var}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 : \\tau_2\n",
+ "}$\n",
+ "\n",
+ "Figure 14: Typing of assignment to and declaration of mutable variables.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 4 (Static Type Checking for\n",
+ "Mutable Variables)**</span> Implement the cases in `hastype` for typing\n",
+ "mutable variable expressions using the rules given in\n",
+ "<a href=\"#fig-typescripty-mutable-variables-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 14</a> defining the typing judgment form\n",
+ "$\\Gamma \\vdash e : \\tau$.\n",
+ "\n",
+ "## Dynamically-Allocated Mutable Objects\n",
+ "\n",
+ "### Small-Step Reduction\n",
+ "\n",
+ "The $\\TirName{DoObject}$ rule states that an object\n",
+ "$\\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}}$ is not a value and\n",
+ "steps an address (i.e., a pointer). In particular, it allocates a memory\n",
+ "address $a$, stores the object at that memory location\n",
+ "$[a \\mapsto \\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}} ]$, and\n",
+ "returns the pointer $a$ to the object\n",
+ "$\\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}}$ as its value. See\n",
+ "the section on Pointers (**?@sec-javascripty-pointers-smallstep**) for\n",
+ "further discussion.\n",
+ "\n",
+ "$\\fbox{$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $}$\n",
+ "\n",
+ "$\\inferrule[DoObject]{\n",
+ " a\\notin \\operatorname{dom}(m)\n",
+ "}{\n",
+ " \\langle \\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}} , m \\rangle \\longrightarrow \\langle a, m[a \\mapsto \\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}} ] \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoGetField]{\n",
+ " m(a) = \n",
+ " \\texttt{\\{} \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,v\\texttt{,}\n",
+ " \\ldots\n",
+ " \\texttt{\\}}\n",
+ "}{\n",
+ " \\langle a\\texttt{.}f , m \\rangle \\longrightarrow \\langle v, m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchObject]{\n",
+ " \\langle e_i, m \\rangle \\longrightarrow \\langle e_i', m' \\rangle \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchGetField]{\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\langle e_1\\texttt{.}f , m \\rangle \\longrightarrow \\langle e_1'\\texttt{.}f , m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "Figure 15: Small-step operational semantics of allocating and reading\n",
+ "from dynamically-allocated mutable objects.\n",
+ "\n",
+ "The $\\TirName{DoAssignField}$ rule is as expected—replacing the value of\n",
+ "an object field given by a location value $a\\texttt{.}f$:\n",
+ "\n",
+ "$\\inferrule[DoAssignField]{\n",
+ " m(a) = \n",
+ " \\texttt{\\{} \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,v\\texttt{,}\n",
+ " \\ldots\n",
+ " \\texttt{\\}}\n",
+ "}{\n",
+ " \\langle a\\texttt{.}f \\mathrel{\\texttt{=}} v' , m \\rangle \\longrightarrow \\langle v' , m[a \\mapsto \\texttt{\\{} \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,v'\\texttt{,}\n",
+ " \\ldots\n",
+ " \\texttt{\\}} ] \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchAssign2]{\n",
+ " e_1\\;\\mathsf{location}\n",
+ " \\and\n",
+ " \\langle e_2, m \\rangle \\longrightarrow \\langle e_2', m' \\rangle \n",
+ "}{\n",
+ " \\langle e_1 \\mathrel{\\texttt{=}} e_2 , m \\rangle \\longrightarrow \\langle e_1 \\mathrel{\\texttt{=}} e_2' , m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchAssign1]{\n",
+ " \\nvdash e_1\\;\\mathsf{location}\n",
+ " \\and\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\langle e_1 \\mathrel{\\texttt{=}} e_2 , m \\rangle \\longrightarrow \\langle e_1' \\mathrel{\\texttt{=}} e_2 , m' \\rangle \n",
+ "}$\n",
+ "\n",
+ "Figure 16: Small-step operational semantics of assigning to object\n",
+ "fields.\n",
+ "\n",
+ "However, now its possible that the left-hand–side of assignment needs to\n",
+ "be reduced to a location value. With mutable variables, we knew and\n",
+ "assumed that the left-hand–side would immediately by its location value\n",
+ "by substitution. We generalize the search rules for the assignment\n",
+ "expression $e_1 \\mathrel{\\texttt{=}}e_2$ to reduce $e_1$ to a location\n",
+ "value (i.e., satisfies $e_1\\;\\mathsf{location}$) with rule\n",
+ "$\\TirName{SearchAssign1}$. We write $\\nvdash e_1\\;\\mathsf{location}$ for\n",
+ "when $e_1$ is not a location value. The $\\TirName{SearchAssign2}$ rule\n",
+ "generalizes $\\TirName{SearchAssign2Var}$ above for reducing the\n",
+ "right-hand–side of assignment to a value.\n",
+ "\n",
+ "In implementation, the judgment form $e_1\\;\\mathsf{location}$ is\n",
+ "specified by the `isLValue` function.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 5 (Small-Step Reduction for\n",
+ "Mutable Objects)**</span> Implement the cases in `step` for reducing\n",
+ "dynamically-allocated mutable objects using the rules given in\n",
+ "<a href=\"#fig-typescripty-mutable-objects-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 15</a> and\n",
+ "<a href=\"#fig-typescripty-field-assignment-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 16</a> for the reduction-step judgment form\n",
+ "$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $.\n",
+ "\n",
+ "### Static Type Checking\n",
+ "\n",
+ "Typing of object literals and reading from a field is unchanged because\n",
+ "allocation and reading from memory is a run-time consideration:\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e : \\tau$}$\n",
+ "\n",
+ "$\\inferrule[TypeObject]{\n",
+ " \\Gamma \\vdash e_i : \\tau_i\n",
+ " \\and\n",
+ " \\text{for all $i$}\n",
+ "}{\n",
+ " \\Gamma \\vdash \\texttt{\\{}\n",
+ " \\ldots\\texttt{,}\n",
+ " f_i\\texttt{:}\\,e_i\\texttt{,}\n",
+ " \\ldots \\texttt{\\}}\n",
+ " : \\texttt{\\{}\n",
+ " \\ldots\\texttt{,}\n",
+ " f_i\\texttt{:}\\,\\tau_i\\texttt{,}\n",
+ " \\ldots \\texttt{\\}} \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeGetField]{\n",
+ " \\Gamma \\vdash e : \\texttt{\\{}\n",
+ " \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,\\tau\\texttt{,}\n",
+ " \\ldots \\texttt{\\}} \n",
+ "}{\n",
+ " \\Gamma \\vdash \n",
+ " e\\texttt{.}f\n",
+ " : \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 17: Typing of object literals and field read.\n",
+ "\n",
+ "We also need to check that the left-hand–side of assignment could be an\n",
+ "assignable field:\n",
+ "\n",
+ "$\\inferrule[TypeAssignField]{\n",
+ " \\Gamma \\vdash e_1 : \\texttt{\\{}\n",
+ " \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,\\tau\\texttt{,}\n",
+ " \\ldots \\texttt{\\}} \n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\tau\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1\\texttt{.}f \\mathrel{\\texttt{=}}e_2 : \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 18: Typing of assignment to object fields.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 6 (Static Type Checking for\n",
+ "Mutable Objects)**</span> Implement the cases in `hastype` for typing\n",
+ "dynamically-allocated mutable object expressions using the rules given\n",
+ "in <a href=\"#fig-typescripty-mutable-objects-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 17</a> and\n",
+ "<a href=\"#fig-typescripty-field-assignment-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 18</a> defining the typing judgment form\n",
+ "$\\Gamma \\vdash e : \\tau$.\n",
+ "\n",
+ "## Location References\n",
+ "\n",
+ "### Small-Step Reduction\n",
+ "\n",
+ "A reference variable is one that uses a previously-allocated location:\n",
+ "\n",
+ "$\\fbox{$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $}$\n",
+ "\n",
+ "$\\inferrule[DoRefDecl]{\n",
+ " e_1\\;\\mathsf{location}\n",
+ "}{\n",
+ " \\langle \\mathbf{ref}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 , m \\rangle \\longrightarrow \\langle {}[ e_1 /x]e_2 , m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchRefDecl]{\n",
+ " \\nvdash e_1\\;\\mathsf{location}\n",
+ " \\and\n",
+ " \\langle e_1, m \\rangle \\longrightarrow \\langle e_1', m' \\rangle \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "Figure 19: Small-step operational semantics of location references.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 7 (Small-Step Reduction for\n",
+ "Location References)**</span> Implement the cases in `step` for reducing\n",
+ "location references using the rules given in\n",
+ "<a href=\"#fig-typescripty-locref-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 19</a> for the reduction-step judgment form\n",
+ "$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $.\n",
+ "\n",
+ "### Static Type Checking\n",
+ "\n",
+ "Examining the $\\TirName{DoRefDecl}$ rule in the operational semantics,\n",
+ "we see that we need to ensure that statically the binding expression\n",
+ "$e_1$ refers to a location (i.e., either a mutable variable or field).\n",
+ "We considered this case-by-case, but let us define a judgment form that\n",
+ "captures this concept:\n",
+ "\n",
+ "$$\n",
+ "\\Gamma \\vdash e \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau\n",
+ "$$\n",
+ "\n",
+ "says informally, “In typing environment $\\Gamma$, expression $e$ is a\n",
+ "location expression whose contents have type $\\tau$.” This judgment form\n",
+ "is the static analogue of the run-time judgment form\n",
+ "$e\\;\\mathsf{location}$.\n",
+ "\n",
+ "We implement this judgment form with the following Scala function:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "52d5e674",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def hasloctype(tenv: Map[String, MTyp], e: Expr): Option[Typ] = ???"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "8c4b3445-2ab4-4f3e-bb69-5c53938352a5",
+ "metadata": {},
+ "source": [
+ "$\\fbox{$\\Gamma \\vdash e : \\tau$}$\n",
+ "\n",
+ "$\\inferrule[TypeRefDecl]{\n",
+ " \\Gamma \\vdash e_1 \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau_1\n",
+ " \\and\n",
+ " \\Gamma, x : \\mathbf{ref}\\,\\tau_1 \\vdash e_2 : \\tau_2\n",
+ "}{\n",
+ " \\Gamma \\vdash \\mathbf{ref}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 : \\tau_2\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeAssign]{\n",
+ " \\Gamma \\vdash e_1 \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau\n",
+ " \\and\n",
+ " \\Gamma \\vdash e_2 : \\tau\n",
+ "}{\n",
+ " \\Gamma \\vdash e_1 \\mathrel{\\texttt{=}}e_2 : \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 20: Typing of declaration of location references and assignment.\n",
+ "\n",
+ "With this location-typing judgment form, we can replace\n",
+ "$\\TirName{TypeAssignVar}$ and $\\TirName{TypeAssignField}$ with the\n",
+ "$\\TirName{TypeAssign}$ rule given above. And we see that the\n",
+ "location-typing judgment form specifies that mutable variables or fields\n",
+ "are location expressions, which we had previously inlined:\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau$}$\n",
+ "\n",
+ "$\\inferrule[LocTypeVar]{\n",
+ " x : d\\,\\tau \\in \\Gamma\n",
+ " \\and\n",
+ " d\\in \\left\\{ \\mathbf{var}, \\mathbf{ref} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash x \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[LocTypeGetField]{\n",
+ " \\Gamma \\vdash e : \\texttt{\\{}\n",
+ " \\ldots\\texttt{,}\n",
+ " f\\texttt{:}\\,\\tau\\texttt{,}\n",
+ " \\ldots \\texttt{\\}} \n",
+ "}{\n",
+ " \\Gamma \\vdash e\\texttt{.}f \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 21: Location typing of mutable variables and object fields.\n",
+ "\n",
+ "We see here in the $\\TirName{LocTypeVar}$ rule that it would arguably be\n",
+ "clearer for the typing environment to carry location assumptions, rather\n",
+ "than the varable mode $d$ directly.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 8 (Static Type Checking for\n",
+ "Mutable Variables)**</span> Implement the cases in `hastype` for typing\n",
+ "location reference expressions using the rules given in\n",
+ "<a href=\"#fig-typescripty-locref-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 20</a> defining the typing judgment form\n",
+ "$\\Gamma \\vdash e : \\tau$ and `hasloctype` for the location typing\n",
+ "judgment form $\\Gamma \\vdash e \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau$\n",
+ "using the rules given in <a href=\"#fig-typescripty-loctyping-lab\"\n",
+ "class=\"quarto-xref\">Figure 21</a>.\n",
+ "\n",
+ "## Multi-Parameter Procedures with Parameter-Passing Modes (Extra Credit)\n",
+ "\n",
+ "For procedures, we want to support an arbitrary number of parameters\n",
+ "that may be individually declared with any parameter-passing mode. To\n",
+ "avoid re-encoding the case analysis of the $\\TirName{DoConstDecl}$,\n",
+ "$\\TirName{SearchConstDecl}$, $\\TirName{DoVarDecl}$,\n",
+ "$\\TirName{SearchVarDecl}$, and $\\TirName{DoRefDecl}$, and\n",
+ "$\\TirName{SearchRefDecl}$ rules, we define the $\\TirName{DoCall}$ and\n",
+ "$\\TirName{DoCallRec}$ rules to transform the parameter binding to a\n",
+ "variable binding expression $e'$.\n",
+ "\n",
+ "$\\fbox{$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $}$\n",
+ "\n",
+ "$\\inferrule[DoCall]{\n",
+ " e' =\n",
+ " d_1\\;y_1\\;\\texttt{=}\\;e_1\\texttt{;}\\; \\cdots\\texttt{;}d_n\\;y_n\\;\\texttt{=}\\;e_n\\texttt{;}\\; e \n",
+ "}{\n",
+ " \\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 \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[DoCallRec]{\n",
+ " 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)\n",
+ " \\and\n",
+ " e' =\n",
+ " d_1\\;y_1\\;\\texttt{=}\\;e_1\\texttt{;}\\; \\cdots\\texttt{;}d_n\\;y_n\\;\\texttt{=}\\;e_n\\texttt{;}\\; e \n",
+ "}{\n",
+ " \\langle v\\texttt{(} e_1\\texttt{,}\\ldots\\texttt{,}e_n \\texttt{)} , m \\rangle \\longrightarrow \\langle {}[v/x]e' , m \\rangle \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[SearchCall1]{\n",
+ " e\\longrightarrow e'\n",
+ "}{\n",
+ " e\\texttt{(}e_1, \\ldots, e_n\\texttt{)}\n",
+ " \\longrightarrow\n",
+ " e'\\texttt{(}e_1, \\ldots, e_n\\texttt{)}\n",
+ "}$\n",
+ "\n",
+ "Figure 22: Small-step operational semantics for multi-parameter\n",
+ "recursive procedures with parameter-passing modes.\n",
+ "\n",
+ "Observe that there is no $\\TirName{SearchCall2}$ rule that reduces the\n",
+ "arguments, as the appropriate reduction of those arguments happens via\n",
+ "the $\\TirName{SearchConstDecl}$, $\\TirName{SearchVarDecl}$, and\n",
+ "$\\TirName{SearchRefDecl}$ rules.\n",
+ "\n",
+ "### Small-Step Reduction\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 9 (Small-Step Reduction for\n",
+ "Parameter-Passing Modes)**</span> Implement the cases in `step` for\n",
+ "reducing procedures with parameter passing modes using the rules given\n",
+ "in <a href=\"#fig-typescripty-procedures-smallstep-lab\"\n",
+ "class=\"quarto-xref\">Figure 22</a> for the reduction-step judgment form\n",
+ "$ \\langle e, m \\rangle \\longrightarrow \\langle e', m' \\rangle $.\n",
+ "\n",
+ "### Static Type Checking\n",
+ "\n",
+ "For typing, we similarly want to avoid re-encoding the case analysis of\n",
+ "the $\\TirName{TypeConstDecl}$, $\\TirName{TypeVarDecl}$, and\n",
+ "$\\TirName{TypeRefDecl}$. Let us define a judgment form that combines the\n",
+ "cases to state state when an expression is well-typed for a given mode:\n",
+ "\n",
+ "$$\n",
+ "\\Gamma \\vdash e : d\\,\\tau\n",
+ "$$\n",
+ "\n",
+ "saying, “In type environment $\\Gamma$, expression $e$ has type $\\tau$\n",
+ "and can be bound to a variable with mode $d$.”\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e : d\\,\\tau$}$\n",
+ "\n",
+ "$\\inferrule[ValBindable]{\n",
+ " \\Gamma \\vdash e : \\tau\n",
+ " \\and\n",
+ " d\\in \\left\\{ \\mathbf{const}, \\mathbf{var} \\right\\}\n",
+ "}{\n",
+ " \\Gamma \\vdash e : d\\,\\tau\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[RefBindable]{\n",
+ " \\Gamma \\vdash e \\mathrel{\\mathord{:}\\mathord{\\&}} \\tau\n",
+ "}{\n",
+ " \\Gamma \\vdash e : \\mathbf{ref}\\,\\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 23: Typing with bindablity to a given variable mode.\n",
+ "\n",
+ "We implement this judgment form with the following Scala function:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "9df9c747",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def hasmodetype(tenv: Map[String, MTyp], e: Expr, d: Mode): Option[Typ] = ???"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ffabb1e9-bb0e-47d7-b365-167451899166",
+ "metadata": {},
+ "source": [
+ "We can then define the $\\TirName{TypeDecl}$ and $\\TirName{TypeCall}$\n",
+ "rules as follows:\n",
+ "\n",
+ "$\\fbox{$\\Gamma \\vdash e : \\tau$}$\n",
+ "\n",
+ "$\\inferrule[TypeDecl]{\n",
+ " \\Gamma \\vdash e_1 : d\\,\\tau_1\n",
+ " \\and\n",
+ " \\Gamma, x : d\\,\\tau_1 \\vdash e_2 : \\tau_2\n",
+ "}{\n",
+ " \\Gamma \\vdash d\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 : \\tau_2\n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeCall]{\n",
+ " \\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 \n",
+ " \\and\n",
+ " \\Gamma \\vdash e_1 : d_1\\,\\tau_1\n",
+ " \\quad\\cdots\\quad\n",
+ " \\Gamma \\vdash e_n : d_n\\,\\tau_n\n",
+ "}{\n",
+ " \\Gamma \\vdash e\\texttt{(}e_1, \\ldots, e_n\\texttt{)} : \\tau\n",
+ "}$\n",
+ "\n",
+ "Figure 24: Typing of variable declarations and call with\n",
+ "parameter-passing modes.\n",
+ "\n",
+ "Note that we can use the $\\TirName{TypeDecl}$ rule to replace the\n",
+ "$\\TirName{TypeConstDecl}$, $\\TirName{TypeVarDecl}$, and\n",
+ "$\\TirName{TypeRefDecl}$ rules. You may optionally refactor your\n",
+ "implementation to use $\\TirName{TypeDecl}$.\n",
+ "\n",
+ "Typing of function literals remains essentially the same, except that\n",
+ "declared modes are also assumed in the typing environment:\n",
+ "\n",
+ "$\\inferrule[TypeFunction]{\n",
+ " \\Gamma, y_1 : d_1\\,\\tau_1, \\cdots , y_n : d_n\\,\\tau_n \\vdash e' : \\tau'\n",
+ "}{\n",
+ " \\Gamma \\vdash \\texttt{(} \\overline{y\\texttt{:}\\, d\\,\\tau } \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} e' : \\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau' \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeFunctionAnn]{\n",
+ " \\Gamma, y_1 : d_1\\,\\tau_1, \\cdots, , y_n : d_n\\,\\tau_n \\vdash e' : \\tau'\n",
+ "}{\n",
+ " \\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' \n",
+ "}$\n",
+ "\n",
+ "$\\inferrule[TypeFunctionRec]{\n",
+ " \\Gamma, x : \\tau_x , y_1 : d_1\\,\\tau_1, \\cdots, , y_n : d_n\\,\\tau_n \\vdash e' : \\tau'\n",
+ " \\and\n",
+ " \\tau_x = \\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau' \n",
+ "}{\n",
+ " \\Gamma \\vdash x\\texttt{(} \\overline{y\\texttt{:}\\,d\\,\\tau} \\texttt{)} \\texttt{:}\\,\\tau' \\mathrel{\\texttt{=}\\!\\texttt{>}} e' : \\tau_x \n",
+ "}$\n",
+ "\n",
+ "Figure 25: Typing of multi-parameter recursive functions.\n",
+ "\n",
+ "<span class=\"theorem-title\">**Exercise 10 (Static Type Checking for\n",
+ "Parameter-Passing Modes)**</span> Implement the cases in `hastype` for\n",
+ "typing procedures with parameter-passing modes using the rules given in\n",
+ "<a href=\"#fig-typescripty-modedecl-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 24</a> and\n",
+ "<a href=\"#fig-typescripty-procedures-typing-lab\"\n",
+ "class=\"quarto-xref\">Figure 25</a> defining the typing judgment form\n",
+ "$\\Gamma \\vdash e : \\tau$ and `hasmodetype` for typing with bindablity to\n",
+ "a given variable mode in <a href=\"#fig-typescripty-mode-bindable-lab\"\n",
+ "class=\"quarto-xref\">Figure 23</a>."
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Scala",
+ "language": "scala",
+ "name": "scala",
+ "path": "/Users/bec/Library/Jupyter/kernels/scala"
+ },
+ "language_info": {
+ "codemirror_mode": "text/x-scala",
+ "file_extension": ".sc",
+ "mimetype": "text/x-scala",
+ "name": "scala",
+ "nbconvert_exporter": "script",
+ "version": "2.13.4"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}