imperative-computation-lab.ipynb

{
 "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
}