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