static-type-checking-lab.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f37a2723",
   "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": "79519ef5",
   "metadata": {},
   "outputs": [],
   "source": [
    "val NAME = \"\"\n",
    "val COLLABORATORS = \"\""
   ]
  },
  {
   "cell_type": "markdown",
   "id": "630bdcba",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2485cb19-a0d3-4305-b6e0-a5c61282d0b3",
   "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: Static Type Checking\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",
    "<!-- 25 Static Type Checking -->\n",
    "\n",
    "<!-- 26 Objects -->\n",
    "\n",
    "<!-- 27 Static Type Checking Lab -->\n",
    "\n",
    "### Learning Goals\n",
    "\n",
    "The primary goals of this lab are:\n",
    "\n",
    "-   Programming with higher-order functions.\n",
    "-   Static type checking and understanding the interplay between type\n",
    "    checking and evaluation.\n",
    "\n",
    "Functional Programming Skills  \n",
    "Higher-order functions with collections and callbacks.\n",
    "\n",
    "Programming Language Ideas  \n",
    "Static type checking and type safety. Records.\n",
    "\n",
    "### Instructions\n",
    "\n",
    "A version of project files for this lab resides in the public\n",
    "[pppl-lab4](https://github.com/csci3155/pppl-lab4) 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 `Lab4.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 `Lab4Spec.scala` file. In the\n",
    "`Lab4Spec.scala`, there is empty test class `Lab4StudentSpec` that you\n",
    "can use to separate your tests from the given tests in the `Lab4Spec`\n",
    "class. You are also likely to edit `Lab4.worksheet.sc` for any scratch\n",
    "work. You can also use `Lab4.worksheet.ts` to write and experiment in a\n",
    "JavaScript file that you can then parse into a TypeScripty AST (see\n",
    "`Lab4.worksheet.sc`).\n",
    "\n",
    "If you like, you may use this notebook for experimentation. However,\n",
    "**please make sure your code is in `Lab4.scala`; code in this notebook\n",
    "will not graded.**\n",
    "\n",
    "## Static Typing: TypeScripty: Functions and Objects\n",
    "\n",
    "#### Static Typing\n",
    "\n",
    "As we have seen in the prior labs, dealing with coercions and checking\n",
    "for dynamic type errors complicate the interpreter implementation (i.e.,\n",
    "`step`). Some languages restrict the possible programs that it will\n",
    "execute to ones that it can guarantee will not result in a dynamic type\n",
    "error. This restriction of programs is enforced with an analysis phase\n",
    "after parsing but before evalation known as *type checking*. Such\n",
    "languages are called *statically-typed*. In this lab, we implement a\n",
    "statically-typed version of JavaScripty that we affectionately call\n",
    "TypeScripty. We will not permit *any* type coercions and simultaneously\n",
    "guarantee the absence of dynamic type errors.\n",
    "\n",
    "#### Multi-Parameter Recursive Functions\n",
    "\n",
    "Using our skills working with higher-order functions on collections from\n",
    "previous assignments, we now consider functions with zero-or-more\n",
    "parameters (instead of exactly one):\n",
    "\n",
    "$$\n",
    "\\begin{array}{rrrl}\n",
    "  \\text{types} & \\tau& \\mathrel{::=}& \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau'\n",
    "  \\\\\n",
    "  \\text{values} & v& \\mathrel{::=}& x^{?}\\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)}\\tau^{?} \\mathrel{\\texttt{=}\\!\\texttt{>}} e_1\n",
    "  \\\\\n",
    "  \\text{expressions} & e& \\mathrel{::=}& \n",
    "  x^{?}\\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)}\\tau^{?} \\mathrel{\\texttt{=}\\!\\texttt{>}} e_1\n",
    "  \\mid e_1\\texttt{(}e_2\\texttt{)}\n",
    "  \\\\\n",
    "  \\text{optional variables} & x^{?}& \\mathrel{::=}& x\\mid\\varepsilon \\\\\n",
    "  \\text{optional type annotations} & \\tau^{?}& \\mathrel{::=}& \\texttt{:}\\,\\tau \\mid\\varepsilon\n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "We write a sequence of things using either an overbar or dots (e.g.,\n",
    "$\\overline{y}$ or $y_1, \\ldots, y_n$ for a sequence of variables).\n",
    "Functions can now take any number of parameters\n",
    "$\\overline{y\\texttt{:}\\,\\tau}$. We have a language of types $\\tau$ and\n",
    "function parameters $\\overline{y}$ are annotated with types\n",
    "$\\overline{\\tau}$.\n",
    "\n",
    "Functions can be named or unnamed $x^{?}$ and can be annotated with a\n",
    "return type or unannotated $\\tau^{?}$. To define recursive functions,\n",
    "the function needs to be named *and* annotated with a return type.\n",
    "\n",
    "To represent an arbitrary number of function parameters or function call\n",
    "arguments in Scala, we use an appropriate `List`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f5304f2a",
   "metadata": {},
   "outputs": [],
   "source": [
    "trait Typ  // t\n",
    "case class TFun(yts: List[(String,Typ)], tret: Typ) extends Typ // t ::= (yts) => tret\n",
    "\n",
    "trait Expr // e\n",
    "case class Fun(xopt: Option[String], yts: List[(String,Typ)], tretopt: Option[Typ], e1: Expr) extends Expr // e ::= xopt(yts)tretopt => e1\n",
    "case class Call(e0: Expr, es: List[Expr]) extends Expr                                                     // e ::= e0(es)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "75c5ea82-615b-49d1-8c09-53c06ef581a6",
   "metadata": {},
   "source": [
    "#### Immutable Objects (Records)\n",
    "\n",
    "Similarly, we now consider immutable objects that can have an arbitrary\n",
    "number of fields: $$\n",
    "\\begin{array}{rrrl}\n",
    "  \\text{types} & \\tau& \\mathrel{::=}&\n",
    "  \\texttt{\\{} \\overline{ f\\texttt{:}\\,\\tau } \\texttt{\\}} \n",
    "  \\\\\n",
    "  \\text{values} & v& \\mathrel{::=}&\n",
    "  \\texttt{\\{} \\overline{ f\\texttt{:}\\,v } \\texttt{\\}} \n",
    "  \\\\\n",
    "  \\text{expressions} & e& \\mathrel{::=}& \n",
    "  \\texttt{\\{} \\overline{ f\\texttt{:}\\,e } \\texttt{\\}} \n",
    "  \\mid e_1\\texttt{.}f\n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "An object literal expression $$\n",
    "\\texttt{\\{}\n",
    "  f_1\\texttt{:}\\,e_1\\texttt{,}\n",
    "  \\ldots\\texttt{,}\n",
    "  f_n\\texttt{:}\\,e_n\n",
    "\\texttt{\\}}\n",
    "$$ is a comma-separated sequence of field names with initialization\n",
    "expressions surrounded by braces. Objects here are more like records in\n",
    "other programming languages compared to actual JavaScript objects, as we\n",
    "do not have any form of mutation or dynamic extension. Fields here\n",
    "correspond to what JavaScript calls properties but which can be\n",
    "dynamically added or removed from objects. We use the term fields to\n",
    "emphasize that they are fixed based on their type: $$\n",
    "\\texttt{\\{}\n",
    "  f_1\\texttt{:}\\,e_1\\texttt{,}\n",
    "  \\ldots\\texttt{,}\n",
    "  f_n\\texttt{:}\\,e_n\n",
    "\\texttt{\\}}\n",
    "\\quad:\\quad\n",
    "\\texttt{\\{}\n",
    "  f_1\\texttt{:}\\,\\tau_1\\texttt{,}\n",
    "  \\ldots\\texttt{,}\n",
    "  f_n\\texttt{:}\\,\\tau_n\n",
    "\\texttt{\\}}\n",
    "$$\n",
    "\n",
    "Note that an object value is an object literal expression where each\n",
    "field is a value:\n",
    "\n",
    "$$\n",
    "\\texttt{\\{}\n",
    "  f_1\\texttt{:}\\,v_1\\texttt{,}\n",
    "  \\ldots\\texttt{,}\n",
    "  f_n\\texttt{:}\\,v_n\n",
    "\\texttt{\\}}\n",
    "$$\n",
    "\n",
    "The field read expression $e_1\\texttt{.}f$ evaluates $e_1$ to an object\n",
    "value and then looks up the field named $f$.\n",
    "\n",
    "To represent object types and object literal expressions in Scala, we\n",
    "use an appropriate `Map`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "86680ee5",
   "metadata": {},
   "outputs": [],
   "source": [
    "case class TObj(fts: Map[String, Typ]) extends Typ    // t ::= { fts }\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": "bf3c7de8-bf8d-484a-a711-f072c8a00266",
   "metadata": {},
   "source": [
    "Otherwise, we consider our base JavaScripty language that has numbers\n",
    "with arithmetic expressions, booleans with logic and comparison\n",
    "expressions, strings with concatenation, $\\mathbf{undefined}$ with\n",
    "printing, and $\\mathbf{const}$-variable declarations. In summary, the\n",
    "type language $\\tau$ includes base types for numbers, booleans, strings,\n",
    "and $\\mathbf{undefined}$, as well as constructed types for functions and\n",
    "objects described above:\n",
    "\n",
    "$$\n",
    "\\begin{array}{rrrl}\n",
    "  \\text{types} & \\tau& \\mathrel{::=}&\n",
    "  \\texttt{number}\n",
    "  \\mid\\texttt{bool}\n",
    "  \\mid\\texttt{string}\n",
    "  \\mid\\texttt{Undefined}\n",
    "  \\\\\n",
    "  & & \\mid&\n",
    "  \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau'\n",
    "  \\mid\\texttt{\\{} \\overline{ f\\texttt{:}\\,\\tau } \\texttt{\\}} \n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "As an aside, we have chosen a concrete syntax that is compatible with\n",
    "the TypeScript language that adds typing to JavaScript. TypeScript is a\n",
    "proper superset of JavaScript, so it is not as strictly typed as\n",
    "TypeScripty is here in this lab.\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",
    "$e \\longrightarrow e'$ on closed expressions. Because of the static type\n",
    "checking, the reduction-step cases can be greatly simplified: we\n",
    "eliminate performing all coercions, and what’s cool is that we no longer\n",
    "need to represent the possibility of a dynamic $\\mathsf{typeerror}$\n",
    "(e.g., with a `Either[DynamicTypeError,Expr]`).\n",
    "\n",
    "We can use the more basic type signature for `step`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d2d56168",
   "metadata": {},
   "outputs": [],
   "source": [
    "def step(e: Expr): Expr = ???"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3a30f916-aa9c-4099-92ed-997b0ffa2257",
   "metadata": {},
   "source": [
    "corresponding to the more basic judgment form $e \\longrightarrow e'$\n",
    "(given in the subsequent sections).\n",
    "\n",
    "To make easier to identify implementation bugs, we introduce another\n",
    "Scala exception type to throw when there is no possible next step."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "beefdd74",
   "metadata": {},
   "outputs": [],
   "source": [
    "case class StuckError(e: Expr) extends Exception"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ebecfd73-18ee-452c-aeff-1ba82e8042bc",
   "metadata": {},
   "source": [
    "However, the intent of this exception is that it should get thrown at\n",
    "run-time! If it does get thrown, that signals a bug in our interpreter\n",
    "implementation rather than an error in the TypeScripty test input.\n",
    "\n",
    "In particular, if the TypeScripty expression `e` passed into `step` is\n",
    "closed and well-typed (i.e., `inferType(e)` does not throw\n",
    "`StaticTypeError`), then `step` should never throw a `StuckError`. This\n",
    "property is *type safety*.\n",
    "\n",
    "Recall that to implement `step`, we need to implement a substitution\n",
    "function `substitute` corresponding to ${}[v/x]e$ that we use to eagerly\n",
    "apply variable bindings:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "79fd9c7b",
   "metadata": {},
   "outputs": [],
   "source": [
    "def substitute(v: Expr, x: String, e: Expr) = ???"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dda62743-2c2a-456d-af69-18870ec54198",
   "metadata": {},
   "source": [
    "#### Static Type Checking\n",
    "\n",
    "We implement a static type checker that up front rules out programs that\n",
    "would get stuck in taking reduction steps. This type checker is very\n",
    "similar to a big-step interpreter. Instead of computing the value of an\n",
    "expression by recursively computing the value of each sub-expression, we\n",
    "infer the type of an expression, by recursively inferring the type of\n",
    "each sub-expression. An expression is *well-typed* if we can infer a\n",
    "type for it.\n",
    "\n",
    "Given its similarity to big-step evaluation, we formalize a type\n",
    "inference algorithm in a similar way. That is, we define the judgment\n",
    "form $\\Gamma \\vdash e : \\tau$, which says, “In type environment\n",
    "$\\Gamma$, expression $e$ has type $\\tau$.” We then implement a function\n",
    "`hastype`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1d81aea1",
   "metadata": {},
   "outputs": [],
   "source": [
    "type TEnv = Map[String, Typ]\n",
    "def hastype(tenv: TEnv, e: Expr): Typ = ???"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c387e9c0-734d-4f96-bf23-adb03d0f6159",
   "metadata": {},
   "source": [
    "that corresponds directly to this judgment form. It takes as input a\n",
    "type environment `tenv: TEnv` ($\\Gamma$) and an expression `e: Expr`\n",
    "($e$) to return a type `Typ` ($\\tau$). It is informative to compare the\n",
    "rules defining typing with a big-step operational semantics.\n",
    "\n",
    "To signal a type error, we will use a Scala exception"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "68e6db00",
   "metadata": {},
   "outputs": [],
   "source": [
    "case class StaticTypeError(tbad: Typ, esub: Expr, e: Expr) extends Exception"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "81f3fb8b-7772-41a0-91fb-5e284e7a46d3",
   "metadata": {},
   "source": [
    "where `tbad` is the type that is inferred sub-expression `esub` of input\n",
    "expression `e`. These arguments are used to construct a useful error\n",
    "message. We also provide a helper function `err` to simplify throwing\n",
    "this exception.\n",
    "\n",
    "While it is possible to implement iterative reduction via `step` and\n",
    "type inference via`hastype` independently, it is generally easier to\n",
    "“incrementally grow the language” by going language-feature\n",
    "by-language-feature for all functions rather than function-by-function.\n",
    "In the subsequent steps, we describe the small-step operational\n",
    "semantics and the static typing semantics together incrementally by\n",
    "language feature.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "For testing your implementation, there are some interface functions\n",
    "defined that calls your `step` and `hastype` implementations with some\n",
    "debugging information:\n",
    "\n",
    "-   The `iterateStep: Expr => Expr` function repeatedly calls your\n",
    "    `step` implementation until reaching a value.\n",
    "-   The `inferType: Expr => Typ` function calls your `hastype` function\n",
    "    with an empty type environment.\n",
    "\n",
    "Note that the provided tests are minimal. **You will want to add your\n",
    "own tests to cover most language features.**\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 from previous assignments and\n",
    "remove all coercions.\n",
    "\n",
    "$\\fbox{$e \\longrightarrow e'$}$\n",
    "\n",
    "$\\inferrule[DoNeg]{\n",
    "  n' = - n_1\n",
    "}{\n",
    "  \\mathop{\\texttt{-}} n_1 \\longrightarrow n'\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",
    "  n_1 \\mathbin{\\mathit{bop}}n_2 \\longrightarrow n'\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoPlusString]{\n",
    "  \\mathit{str}' = \\mathit{str}_1 \\mathit{str}_2\n",
    "}{\n",
    "  \\mathit{str}_1 \\mathbin{\\texttt{+}} \\mathit{str}_2 \\longrightarrow\\mathit{str}'\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",
    "  n_1 \\mathbin{\\mathit{bop}}n_2 \\longrightarrow b'\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",
    "  \\mathit{str}_1 \\mathbin{\\mathit{bop}}\\mathit{str}_2 \\longrightarrow b'\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",
    "  v_1 \\mathbin{\\mathit{bop}}v_2 \\longrightarrow b'\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoNot]{\n",
    "  b' = \\neg b_1\n",
    "}{\n",
    "  \\mathop{\\texttt{!}} b_1 \\longrightarrow b'\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoAndTrue]{\n",
    "}{\n",
    "  \\mathbf{true} \\mathbin{\\texttt{\\&\\&}} e_2 \\longrightarrow e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoAndFalse]{\n",
    "}{\n",
    "  \\mathbf{false} \\mathbin{\\texttt{\\&\\&}} e_2 \\longrightarrow v_1\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoOrTrue]{\n",
    "}{\n",
    "  \\mathbf{true} \\mathbin{\\texttt{||}} e_2 \\longrightarrow v_1\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoOrFalse]{\n",
    "}{\n",
    "  \\mathbf{false} \\mathbin{\\texttt{||}} e_2 \\longrightarrow e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoIfTrue]{\n",
    "}{\n",
    "  \\mathbf{true}\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3 \\longrightarrow e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoIfFalse]{\n",
    "}{\n",
    "  \\mathbf{false}\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3 \\longrightarrow e_3\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoSeq]{\n",
    "}{\n",
    "  v_1 \\mathbin{\\texttt{,}} e_2 \\longrightarrow e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoPrint]{\n",
    "  \\text{$v_1$ printed}\n",
    "}{\n",
    "  \\texttt{console}\\texttt{.}\\texttt{log}\\texttt{(}v_1\\texttt{)} \\longrightarrow\\mathbf{undefined}\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoConst]{\n",
    "}{\n",
    "  \\mathbf{const}\\;x\\;\\texttt{=}\\;v_1\\texttt{;}\\;e_2 \\longrightarrow[v_1/x]e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchUnary]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  \\mathop{\\mathit{uop}}e_1 \\longrightarrow\\mathop{\\mathit{uop}}e_1'\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchBinary1]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  e_1 \\mathbin{\\mathit{bop}}e_2 \\longrightarrow e_1' \\mathbin{\\mathit{bop}}e_2\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchBinary2]{\n",
    "  e_2 \\longrightarrow e_2'\n",
    "}{\n",
    "  v_1 \\mathbin{\\mathit{bop}}e_2 \\longrightarrow v_1 \\mathbin{\\mathit{bop}}e_2'\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchIf]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  e_1\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3 \\longrightarrow e_1'\\;\\texttt{?}\\;e_2\\;\\texttt{:}\\;e_3\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchPrint]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  \\texttt{console}\\texttt{.}\\texttt{log}\\texttt{(}e_1\\texttt{)} \\longrightarrow\\texttt{console}\\texttt{.}\\texttt{log}\\texttt{(}e_1'\\texttt{)}\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchConst]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  \\mathbf{const}\\;x\\;\\texttt{=}\\;e_1\\texttt{;}\\;e_2 \\longrightarrow\\mathbf{const}\\;x\\;\\texttt{=}\\;e_1'\\texttt{;}\\;e_2  \n",
    "}$\n",
    "\n",
    "Figure 1: 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-lab-base-smallstep\"\n",
    "class=\"quarto-xref\">Figure 1</a> defining the reduction-step judgment\n",
    "form $e \\longrightarrow e'$.\n",
    "\n",
    "Note that your task here is simpler than what you have done before in\n",
    "previous assignments. There are no judgment forms or rules defining\n",
    "coercions (e.g., `toBoolean`) or stepping to a $\\mathsf{typeerror}$\n",
    "result (e.g., `Left(DynamicTypeError(e))`).\n",
    "\n",
    "You will need to implement a helper function `substitute` for base\n",
    "TypeScripty to perform scope-respecting substitution ${}[v/x]e$ as in\n",
    "previous assignments.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "-   You may use (or ignore) the provided helper function `doInequality`\n",
    "    to implement the $\\TirName{DoInequalityNumber}$ and\n",
    "    $\\TirName{DoInequalityString}$ rules.\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 declarations.\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[TypeVar]{\n",
    "}{\n",
    "  \\Gamma \\vdash x : \\Gamma(x)\n",
    "}$\n",
    "\n",
    "$\\inferrule[TypeConstDecl]{\n",
    "  \\Gamma \\vdash e_1 : \\tau_1\n",
    "  \\and\n",
    "  \\Gamma, x : \\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 2: 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}$-variable declarations.\n",
    "\n",
    "Observe how closely the $\\TirName{Type}$ rules align with the\n",
    "$\\TirName{Do}$ rules in <a href=\"#fig-typescripty-lab-base-smallstep\"\n",
    "class=\"quarto-xref\">Figure 1</a>, except for having a big-step\n",
    "evaluation structure with types.\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-lab-base-typing\"\n",
    "class=\"quarto-xref\">Figure 2</a> defining the typing judgment form\n",
    "$\\Gamma \\vdash e : \\tau$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ff9b4265",
   "metadata": {},
   "outputs": [],
   "source": [
    "type TEnv = Map[String, Typ]\n",
    "def hastype(tenv: TEnv, e: Expr): Typ = ???"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5a767128-f0b7-4693-bd1a-03770652f972",
   "metadata": {},
   "source": [
    "## Immutable Objects (Records)\n",
    "\n",
    "Next, we extend our interpreter implementation for immutable objects. We\n",
    "consider the implementation for immutable objects next, as it is a bit\n",
    "simpler than that for multi-parameter functions.\n",
    "\n",
    "### Small-Step Reduction\n",
    "\n",
    "We extend the reduction-step judgment form $e \\longrightarrow e'$ for\n",
    "immutable objects:\n",
    "\n",
    "$\\fbox{$e \\longrightarrow e'$}$\n",
    "\n",
    "$\\inferrule[DoGetField]{\n",
    "}{\n",
    "   \\texttt{\\{}\n",
    "      f_1\\texttt{:}\\,v_1\\texttt{,}\n",
    "      \\ldots\\texttt{,}\n",
    "      f_i\\texttt{:}\\,v_i\\texttt{,}\n",
    "      \\ldots\\texttt{,}\n",
    "      f_n\\texttt{:}\\,v_n \\texttt{\\}}\n",
    "  \\texttt{.}f_i\n",
    "  \\longrightarrow\n",
    "  v_i\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchObject]{\n",
    "  e_i \\longrightarrow e_i'\n",
    "  \\and\n",
    "  e_j = v_j\n",
    "  \\and\n",
    "  \\text{for all $j < i$}\n",
    "}{\n",
    "    \\texttt{\\{}\n",
    "      f_1\\texttt{:}\\,e_1\\texttt{,}\n",
    "      \\ldots\\texttt{,}\n",
    "      f_i\\texttt{:}\\,e_i\\texttt{,}\n",
    "      \\ldots\n",
    "    \\texttt{\\}}\n",
    "  \\longrightarrow\n",
    "    \\texttt{\\{}\n",
    "      f_1\\texttt{:}\\,e_1\\texttt{,}\n",
    "      \\ldots\\texttt{,}\n",
    "      f_i \\mathbin{\\texttt{:}} e_i'\\texttt{,}\n",
    "      \\ldots\n",
    "    \\texttt{\\}}\n",
    "}$\n",
    "\n",
    "$\\inferrule[SearchGetField]{\n",
    "  e_1 \\longrightarrow e_1'\n",
    "}{\n",
    "  e_1\\texttt{.}f\n",
    "  \\longrightarrow\n",
    "  e_1'\\texttt{.}f\n",
    "}$\n",
    "\n",
    "Figure 3: Small-step operational semantics of TypeScripty with immutable\n",
    "objects.\n",
    "\n",
    "<span class=\"theorem-title\">**Exercise 3 (Small-Step Reduction for\n",
    "Immutable Objects)**</span> Implement the cases in `step` for reducing\n",
    "immutable object expressions using the rules given in\n",
    "<a href=\"#fig-typescripty-lab-objects-smallstep\"\n",
    "class=\"quarto-xref\">Figure 3</a> for the reduction-step judgment form\n",
    "$e \\longrightarrow e'$.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "-   Field names $f$ are different than variable names $x$, even though\n",
    "    they are both represented in Scala with a `String`. Object\n",
    "    expressions are not variable binding constructs—what does that mean\n",
    "    about `substitute` for them?\n",
    "\n",
    "-   For $\\TirName{SearchObject}$, you should make the reduction step\n",
    "    apply to the first non-value as given by the left-to-right iteration\n",
    "    of the collection using the `find` method on `Map`s:\n",
    "\n",
    "    ``` scala\n",
    "    (m: Map[K,V]).find(f: ((K,V)) => Boolean): Option[(K,V)]\n",
    "    ```\n",
    "\n",
    "-   Other helpful Scala library methods not previously mentioned to use\n",
    "    here include the following:\n",
    "\n",
    "    ``` scala\n",
    "    (m: Map[K,V]).get(k: K): Option[V]\n",
    "    ```\n",
    "\n",
    "### Static Type Checking\n",
    "\n",
    "We extend the static typing judgment form $\\Gamma \\vdash e : \\tau$ for\n",
    "immutable objects:\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 4: Typing of TypeScripty with immutable objects.\n",
    "\n",
    "<span class=\"theorem-title\">**Exercise 4 (Static Type Checking for\n",
    "Immutable Objects)**</span> Implement the cases in `hastype` for typing\n",
    "immutable object expressions using the rules given in\n",
    "<a href=\"#fig-typescripty-lab-objects-typing\"\n",
    "class=\"quarto-xref\">Figure 4</a> defining the typing judgment form\n",
    "$\\Gamma \\vdash e : \\tau$.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "-   Other helpful Scala library methods not previously mentioned to use\n",
    "    here include the following:\n",
    "\n",
    "    ``` scala\n",
    "    (m: Map[K,V]).map(f: ((K,V)) => (J,U)): Map[J,U]\n",
    "    ```\n",
    "\n",
    "## Multi-Parameter Recursive Functions\n",
    "\n",
    "Finally, we extend our interpreter implementation for multi-parameter\n",
    "recursive functions.\n",
    "\n",
    "### Small-Step Reduction\n",
    "\n",
    "We extend the reduction-step judgment form $e \\longrightarrow e'$ for\n",
    "multi-paramter recursive functions:\n",
    "\n",
    "$\\fbox{$e \\longrightarrow e'$}\n",
    "\\quad$\n",
    "\n",
    "$\\inferrule[DoCall]{\n",
    "}{  (\\texttt{(} y_1\\texttt{:}\\,\\tau_1\\texttt{,}\\ldots\\texttt{,}y_n\\texttt{:}\\,\\tau_n   \\texttt{)}\\tau^{?} \\mathrel{\\texttt{=}\\!\\texttt{>}} e)\n",
    "  \\texttt{(}v_1, \\ldots v_n\\texttt{)}\n",
    "  \\longrightarrow\n",
    "  [v_n/y_n]\\cdots[v_1/y_1]e\n",
    "}$\n",
    "\n",
    "$\\inferrule[DoCallRec]{\n",
    "  v=     (x\\texttt{(} y_1\\texttt{:}\\,\\tau_1\\texttt{,}\\ldots\\texttt{,}y_n\\texttt{:}\\,\\tau_n   \\texttt{)} \\texttt{:}\\,\\tau'  \\mathrel{\\texttt{=}\\!\\texttt{>}} e)\n",
    "}{\n",
    "  v\\texttt{(}v_1, \\ldots v_n\\texttt{)}\n",
    "  \\longrightarrow\n",
    "  [v/x][v_n/y_n]\\cdots[v_1/y_1]e\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",
    "$\\inferrule[SearchCall2]{\n",
    "  e_i \\longrightarrow e_i'\n",
    "  \\and\n",
    "  e_j = v_j\n",
    "  \\and\n",
    "  \\text{for all $j < i$}\n",
    "}{\n",
    "  v\\texttt{(}e_1, \\ldots, e_i, \\ldots, e_n\\texttt{)}\n",
    "  \\longrightarrow\n",
    "  v\\texttt{(}e_1, \\ldots, e_i', \\ldots, e_n\\texttt{)}\n",
    "}$\n",
    "\n",
    "Figure 5: Small-step operational semantics for TypeScripty with\n",
    "multi-parameter recursive functions.\n",
    "\n",
    "<span class=\"theorem-title\">**Exercise 5 (Small-Step Reduction for\n",
    "Multi-Parameter Recursive Functions)**</span> Implement the cases in\n",
    "`step` for reducing multi-parameter recursive functions using the rules\n",
    "given in <a href=\"#fig-typescripty-lab-functions-smallstep\"\n",
    "class=\"quarto-xref\">Figure 5</a> for the reduction-step judgment form\n",
    "$e \\longrightarrow e'$.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "-   Other helpful Scala library methods not previously mentioned to use\n",
    "    here include the following:\n",
    "\n",
    "    ``` scala\n",
    "    (l: List[A]).map(f: A => B): List[B]\n",
    "    (l: List[A]).exists(f: A => Boolean): Boolean\n",
    "    (la: List[A]).zip(lb: List[B]): List[(A,B)]\n",
    "    (l: List[A]).forall(f: A => Boolean): Boolean\n",
    "    (l: List[A]).foldRight(f: (A,B) => B): B\n",
    "    ```\n",
    "\n",
    "    -   You may want to use the `zip` method for the $\\TirName{DoCall}$\n",
    "        and $\\TirName{DoCallRec}$ cases to match up formal parameters\n",
    "        and actual arguments.\n",
    "\n",
    "-   You might want to use your `mapFirst` function from Homework 4 here.\n",
    "\n",
    "### Static Type Checking\n",
    "\n",
    "We extend the static typing judgment form $\\Gamma \\vdash e : \\tau$ for\n",
    "multi-parameter recursive functions:\n",
    "\n",
    "$\\inferrule[TypeCall]{\n",
    "  \\Gamma \\vdash e :  \\texttt{(} y_1\\texttt{:}\\,\\tau_1\\texttt{,}\\ldots\\texttt{,}y_n\\texttt{:}\\,\\tau_n \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau  \n",
    "  \\and\n",
    "  \\Gamma \\vdash e_1 : \\tau_1\n",
    "  \\quad\\cdots\\quad\n",
    "  \\Gamma \\vdash e_n : \\tau_n\n",
    "}{\n",
    "  \\Gamma \\vdash e\\texttt{(}e_1, \\ldots, e_n\\texttt{)} : \\tau\n",
    "}$\n",
    "\n",
    "$\\inferrule[TypeFunction]{\n",
    "  \\Gamma, y_1 : \\tau_1, \\cdots, , y_n : \\tau_n \\vdash e' : \\tau'\n",
    "}{\n",
    "  \\Gamma \\vdash  \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} e'  :  \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau' \n",
    "}$\n",
    "\n",
    "$\\inferrule[TypeFunctionAnn]{\n",
    "  \\Gamma, y_1 : \\tau_1, \\cdots, , y_n : \\tau_n \\vdash e' : \\tau'\n",
    "}{\n",
    "  \\Gamma \\vdash  \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\texttt{:}\\,\\tau'  \\mathrel{\\texttt{=}\\!\\texttt{>}} e'  :  \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau' \n",
    "}$\n",
    "\n",
    "$\\inferrule[TypeFunctionRec]{\n",
    "  \\Gamma, x :  \\tau_x , y_1 : \\tau_1, \\cdots, , y_n : \\tau_n \\vdash e' : \\tau'\n",
    "  \\and\n",
    "  \\tau_x = \\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\mathrel{\\texttt{=}\\!\\texttt{>}} \\tau' \n",
    "}{\n",
    "  \\Gamma \\vdash  x\\texttt{(} \\overline{y\\texttt{:}\\,\\tau} \\texttt{)} \\texttt{:}\\,\\tau'  \\mathrel{\\texttt{=}\\!\\texttt{>}} e'  :  \\tau_x \n",
    "}$\n",
    "\n",
    "Figure 6: Typing of TypeScripty with multi-parameter recursive\n",
    "functions.\n",
    "\n",
    "<span class=\"theorem-title\">**Exercise 6 (Static Type Checking for\n",
    "Immutable Objects)**</span> Implement the cases in `hastype` for typing\n",
    "multi-parameter recursive function expressions using the rules given in\n",
    "<a href=\"#fig-typescripty-lab-functions-typing\"\n",
    "class=\"quarto-xref\">Figure 6</a> defining the typing judgment form\n",
    "$\\Gamma \\vdash e : \\tau$.\n",
    "\n",
    "#### Notes\n",
    "\n",
    "-   Other helpful Scala library methods not previously mentioned to use\n",
    "    here include the following:\n",
    "\n",
    "    ``` scala\n",
    "    (l: List[A]).foldLeft(f: (B,A) => B): B\n",
    "    (l: List[A]).foreach(f: A => Unit): Unit\n",
    "    (l: List[A]).length: Int\n",
    "    (m1: Map[K,V]).++(m2: Map[K,V]): Map[K,V]\n",
    "    ```\n",
    "\n",
    "    -   The `++` method on `Map`s appends two `Map`s together."
   ]
  }
 ],
 "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
}