CSCI3155_Assignment8.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "6a3575958dc77c3cec8d44edb8f99479",
     "grade": false,
     "grade_id": "cell-4dfd42d74736d7f0",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "Before you turn this problem in, make sure everything runs as expected. **Restart the kernel and run all cells** (in the menubar, select Kernel$\\rightarrow$Restart & Run All).\n",
    "\n",
    "Make sure you fill in any place that says `YOUR CODE HERE ???` or \"YOUR ANSWER HERE\". Code cells are autograded, and if the test cells don't run all the way to the line that  prints \"Tests Passed (# points)\", you will not recieve any point for that test."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "9f0556f71d3edaf6ec133d5e0c925321",
     "grade": false,
     "grade_id": "cell-f8e901ca6a64cc4f",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "# CSCI 3155: Assignment 8\n",
    "\n",
    "Goals of this assignment include: \n",
    "- Developing a type system for references\n",
    "- Exercises on type checking and type inference posted on moodle."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Name__: Lucas Laughlin"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "bf52f66cb4ab08d5682cba506b8251ac",
     "grade": false,
     "grade_id": "cell-141cfd4a7d7dcdcf",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "// TEST HELPER\n",
    "def passed(points: Int) {\n",
    "    require(points >=0)\n",
    "    if (points == 1) print(s\"\\n*** Tests Passed (1 point) ***\\n\")\n",
    "    else print(s\"\\n*** Tests Passed ($points points) ***\\n\")\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "9b06fbe985731f09b3bed8270ac88e7a",
     "grade": false,
     "grade_id": "cell-8873b88caab788ec",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "## Problem 1 (25 points)\n",
    "\n",
    "In this problem, we will extend our type system for handling references.  Here is a stripped down version of Lettuce that involves references.\n",
    "\n",
    "$$\\begin{array}{rcl}\n",
    "\\mathbf{Expr} & \\rightarrow & Const(\\mathbf{Double}) \\\\\n",
    "& | & Ident(\\mathbf{Identifier})\\\\\n",
    "& | & Plus(\\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "& | & Div(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    "& | & Geq(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    "& | & And(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    "& | & IfThenElse(\\mathbf{Expr}, \\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "& | & Let(\\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "& | & FunDef(\\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}) \\\\\n",
    "& | & FunCall(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    "& | & \\color{blue}{NewRef(\\mathbf{Expr})} \\\\\n",
    "& | & \\color{blue}{DeRef(\\mathbf{Expr})} \\\\\n",
    "& | & \\color{blue}{AssignRef(\\mathbf{Expr}, \\mathbf{Expr})} \\\\\n",
    "\\end{array}$$\n",
    "\n",
    "We have a type system \n",
    "$$\\begin{array}{rcl}\n",
    "\\mathbf{Type} & \\rightarrow & NumType & \\leftarrow \\text{written as } \\ num \\\\\n",
    "& | & BoolType & \\leftarrow \\text{written as } \\ bool \\\\\n",
    "& | & FunType(\\mathbf{Type} , \\mathbf{Type} ) & \\leftarrow \\text{written as } \\ t_1 \\Rightarrow t_2 \\\\\n",
    "& | & \\color{red}{RefType(\\mathbf{Type})} & \\leftarrow \\text{written as } \\ ref(t_1) \\\\\n",
    "\\end{array}$$\n",
    "\n",
    "\n",
    "### A (5 points)\n",
    "Fill out the missing type annotations labeled type1, type2, and type3 in the program below.\n",
    "\n",
    "~~~\n",
    "let x: type1 = 25 in \n",
    "    let y : type2 = NewRef( - x ) in \n",
    "     let f : type3 = NewRef( function (z: ref(num)) DeRef(z) - x >= 45 ) in \n",
    "          let z : ref(bool) = DeRef(f)(y)\n",
    "~~~"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "checksum": "c9b266006965fd1d2a562c406e672539",
     "grade": true,
     "grade_id": "cell-312b0c7aebe54f39",
     "locked": false,
     "points": 5,
     "schema_version": 1,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "type1: num\n",
    "type2: ref(num)\n",
    "type3: ref(ref(num)=>num)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "25a440393546ca0c57c1df5401cd8724",
     "grade": false,
     "grade_id": "cell-3696a417c6d4ace6",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "### B (10 points): Let us write some inference rules for working with ref types.\n",
    "$$\\newcommand\\typeOf{\\mathbf{typeOf}}$$\n",
    "$$\\newcommand\\semRule[3]{\\begin{array}{c} #1 \\\\ \\hline #2 \\\\ \\end{array}\\;(\\text{#3}) }$$\n",
    "\n",
    "Recall from notes on \"Types and Type Checking\" that $\\typeOf(\\texttt{e}, \\alpha)$ is the type of an \n",
    "expression $\\texttt{e}$ under type environment $\\alpha$. The type environment maps identifiers in the current scope to  their annotated types.\n",
    "\n",
    "\n",
    "Let us write a rule for NewRef.\n",
    "\n",
    "$$\\semRule{ \\typeOf(\\texttt{e}, \\alpha) = t,\\; t \\not= \\mathbf{typeerror} }{\\typeOf(\\texttt{NewRef(e)}, \\alpha) = ref(t) }{newref-ok}$$\n",
    "\n",
    "It says that if $\\texttt{e}$ receives type $t$ under type environment $\\alpha$ and it is not a type error, then $\\texttt{NewRef(e)}$ must receive the type $ref(t)$ under $\\alpha$.\n",
    "\n",
    "\n",
    "\n",
    "(i) Complete the missing terms for the rule for `DeRef` OK rule.\n",
    "$$\\semRule{\\typeOf(\\texttt{e}, \\alpha) = ref(t)}{\\typeOf(\\texttt{DeRef(e)}, \\alpha) = \\color{red}{???_1}}{deref-ok}$$\n",
    "\n",
    "(ii) Complete the missing terms for the rule for `DeRef` error.\n",
    "$$\\semRule{\\typeOf(\\texttt{e}, \\alpha) = t,\\ t \\not= \\color{red}{???_2} }{\\typeOf(\\texttt{DeRef(e)}, \\alpha) = \\mathbf{typeerror}}{deref-nok}$$\n",
    "\n",
    "(iii) Complete the missing terms for `AssignRef` OK rule.\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\color{red}{???_3}, \\typeOf(\\texttt{e2}, \\alpha) = t}{\\typeOf(\\texttt{AssignRef(e1, e2)}, \\alpha) =   \\color{red}{???_4}}{assignref-ok}$$\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "checksum": "d79d258637596aca6c4fa54afff69a5b",
     "grade": true,
     "grade_id": "cell-e1cc8dd790c95fef",
     "locked": false,
     "points": 10,
     "schema_version": 1,
     "solution": true
    }
   },
   "source": [
    "1) t\n",
    "2) ref(t2)\n",
    "3) ref(t)\n",
    "4) t"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "ca1de38bc65cef8c32f7dd2b55933fa9",
     "grade": false,
     "grade_id": "cell-b4ea5d2026431663",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "### C (10 points): Write the type checker with references by filling in the missing code."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "checksum": "423152e04320a79d0629f867894f3c57",
     "grade": false,
     "grade_id": "cell-3b12181f57c0872f",
     "locked": false,
     "schema_version": 1,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "sealed trait Type\n",
    "case object NumType extends Type\n",
    "case object BoolType extends Type\n",
    "case class FunType(t1: Type, t2: Type) extends Type\n",
    "case class RefType(t1: Type) extends Type\n",
    "// TODO: Write a new case class for RefType\n",
    "// YOUR CODE HERE\n",
    "\n",
    "\n",
    "sealed trait Program\n",
    "sealed trait Expr\n",
    "\n",
    "case class Const(f: Double) extends Expr\n",
    "case class Ident(s: String) extends Expr\n",
    "case class Plus(e1: Expr, e2: Expr) extends Expr\n",
    "case class Minus(e1: Expr, e2: Expr) extends Expr\n",
    "case class Geq(e1: Expr, e2: Expr) extends Expr\n",
    "case class IfThenElse(e1: Expr, e2: Expr, e3: Expr) extends Expr\n",
    "case class Let(x: String, xType: Type, e1: Expr, e2: Expr) extends Expr\n",
    "case class FunDef(id: String, idType: Type, e: Expr) extends Expr\n",
    "case class FunCall(calledFun: Expr, argExpr: Expr) extends Expr\n",
    "case class NewRef(e: Expr) extends Expr\n",
    "case class DeRef(e: Expr) extends Expr\n",
    "case class AssignRef(e1: Expr, e2: Expr) extends Expr\n",
    "case class TopLevel(e: Expr) extends Program\n",
    "\n",
    "def typeEquals(t1: Type, t2: Type): Boolean = t1 == t2\n",
    "case class TypeErrorException(s: String) extends Exception\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "checksum": "b45352123979369ec270bea5fc9f16e5",
     "grade": false,
     "grade_id": "cell-e8a060ea96ec6931",
     "locked": false,
     "schema_version": 1,
     "solution": true
    }
   },
   "outputs": [],
   "source": [
    "def typeOf(e: Expr, alpha: Map[String, Type]): Type = {\n",
    "    def checkType(opName: String, e1: Expr, t1: Type, e2: Expr, t2: Type, resType: Type): Type = {\n",
    "        val t1hat = typeOf(e1, alpha)\n",
    "        if (! typeEquals(t1hat, t1)){\n",
    "            throw new TypeErrorException(s\"Type mismatch in arithmetic/comparison/bool op $opName, Expected type $t1, obtained $t1hat\")\n",
    "        }\n",
    "        \n",
    "        val t2hat = typeOf(e2, alpha)\n",
    "        if (! typeEquals(t2hat, t2)){\n",
    "            throw new TypeErrorException(s\"Type mismatch in arithmetic/comparison/bool op $opName, Expected type $t2, obtained $t2hat\")\n",
    "        }\n",
    "        \n",
    "        resType\n",
    "    }\n",
    "    \n",
    "    e match {\n",
    "        case Const(f) => NumType\n",
    "        case Ident(s) => {if (alpha contains s)\n",
    "                             alpha(s)\n",
    "                          else \n",
    "                             throw TypeErrorException(s\"Unknown identifier $s\")}\n",
    "        case Plus(e1, e2) =>  checkType(\"Plus\", e1,  NumType, e2, NumType, NumType)\n",
    "        case Minus(e1, e2) => checkType(\"Minus\",e1,  NumType, e2, NumType, NumType)\n",
    "        case Geq(e1, e2) => checkType(\"Geq\", e1,  NumType, e2, NumType, BoolType)\n",
    "        case IfThenElse(e, e1, e2) => {\n",
    "            val t = typeOf(e, alpha)\n",
    "            if (t == BoolType){\n",
    "                val t1 = typeOf(e1, alpha)\n",
    "                val t2 = typeOf(e2, alpha)\n",
    "                if (typeEquals(t1, t2))\n",
    "                    t1\n",
    "                else \n",
    "                    throw TypeErrorException(s\"If then else returns unequal types $t1 and $t2\")\n",
    "            } else {\n",
    "                throw TypeErrorException(s\"If then else condition expression not boolean $t\")\n",
    "            }\n",
    "        }\n",
    "\n",
    "        case Let(x, t, e1, e2) => {\n",
    "            val t1 = typeOf(e1, alpha)\n",
    "            if (typeEquals(t1, t)){\n",
    "                val newAlpha = alpha + (x -> t)\n",
    "                typeOf(e2, newAlpha)\n",
    "            } else {\n",
    "                throw TypeErrorException(s\"Let binding has type $t whereas it is bound to expression of type $t1\")\n",
    "            }\n",
    "        }\n",
    "\n",
    "        case FunDef(x, t1, e) => {\n",
    "            val newAlpha = alpha + (x -> t1)\n",
    "            val t2 = typeOf(e, newAlpha)\n",
    "            FunType(t1, t2)\n",
    "        }\n",
    "\n",
    "        case FunCall(e1, e2) => {\n",
    "            val ftype = typeOf(e1, alpha)\n",
    "            ftype match {\n",
    "                case FunType(t1, t2) => {\n",
    "                    val argType = typeOf(e2, alpha)\n",
    "                    if (typeEquals(argType, t1)){\n",
    "                        t2\n",
    "                    } else {\n",
    "                        throw TypeErrorException(s\"Call to function with incompatible argument type. Expected $t1, obtained $argType\")\n",
    "                    }\n",
    "                }\n",
    "                case _ => { throw TypeErrorException(s\"Call to function but with a non function type $ftype\")}\n",
    "\n",
    "            }\n",
    "        }\n",
    "\n",
    "        case NewRef(e) => {\n",
    "            val rtype = typeOf(e, alpha)\n",
    "            RefType(rtype)\n",
    "        }\n",
    "        \n",
    "        case AssignRef(e1, e2) => {\n",
    "            val type1 = typeOf(e1, alpha)\n",
    "            val type2 = typeOf(e2, alpha)\n",
    "            type1 match {\n",
    "                case RefType(type2) => type2\n",
    "                case _ => {  throw TypeErrorException(s\"Call to Assign reference but with incorrect reference type $type2 for expression type $type2\")}\n",
    "            }\n",
    "        }\n",
    "        \n",
    "        case DeRef(e) => {\n",
    "            val rtype = typeOf(e, alpha)\n",
    "            rtype match {\n",
    "                case RefType(t1)=>t1\n",
    "                case _ => {  throw TypeErrorException(s\"Call to dereference but with a non reference type $rtype\")}\n",
    "            }\n",
    "        }\n",
    "        \n",
    "    }\n",
    "}\n",
    "\n",
    "def typeOfProgram(p: Program) = p match {\n",
    "    case TopLevel(e) => {\n",
    "            val t = typeOf(e, Map())\n",
    "            println(s\"Program type computed successfully as $t\")\n",
    "            t\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "fea91be69daec9a223c678227f7135f4",
     "grade": true,
     "grade_id": "cell-bc7a12aa7020a075",
     "locked": true,
     "points": 2,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "//BEGIN TEST\n",
    "\n",
    "/* \n",
    "let x : ref(num) = NewRef(10 ) in \n",
    "   let dummy: num = AssignRef(x, 30) in \n",
    "       DeRef(x)\n",
    "       */\n",
    "\n",
    "val p1 = Let(\"x\", RefType(NumType), NewRef(Const(10)), Let(\"dummy\", NumType, AssignRef(Ident(\"x\"), Const(30) ), DeRef(Ident(\"x\"))) )\n",
    "val t1 = typeOfProgram(TopLevel(p1))\n",
    "assert(t1 == NumType, \"Test 1 failed: answer should be NumType\")\n",
    "passed(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "ee086a424f4cd7d89eedffc95fc67e50",
     "grade": true,
     "grade_id": "cell-b0e79cec0732b13b",
     "locked": true,
     "points": 2,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "//BEGIN TEST\n",
    "/* \n",
    "let x : ref(num) = NewRef(function(z: num) z + 10) in \n",
    "   let dummy: num = AssignRef(x, 30) in \n",
    "       DeRef(x)\n",
    "       */\n",
    "val fdef = FunDef(\"z\", NumType, Plus(Ident(\"z\"), Const(10)))\n",
    "val p2 = Let(\"x\", RefType(NumType), NewRef(fdef), Let(\"dummy\", NumType, AssignRef(Ident(\"x\"), Const(30) ), DeRef(Ident(\"x\"))) )\n",
    "val t2 = try {\n",
    "   typeOfProgram(TopLevel(p2))\n",
    "   assert(false, \"The program should not receive a type\")\n",
    "} catch {\n",
    "    case TypeErrorException(msg) => s\"OK -- caught a type error exception: $msg\"\n",
    "    case e => print(e); assert(false, \"Please throw TypeErrorException(message) when a type failure occurs\")\n",
    "}\n",
    "passed(2)\n",
    "//END TEST"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "57bdbd875bb78b4e7976bdd5c21f597d",
     "grade": true,
     "grade_id": "cell-ce1f9c297983715f",
     "locked": true,
     "points": 2,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "//BEGIN TEST\n",
    "/* \n",
    "let x : ref(num => num) = NewRef(function(z: num) z + 10) in \n",
    "   let dummy: num = AssignRef(x, 30) in \n",
    "       DeRef(x)\n",
    "       */\n",
    "val fdef = FunDef(\"z\", NumType, Plus(Ident(\"z\"), Const(10)))\n",
    "val p3 = Let(\"x\", RefType(FunType(NumType, NumType)), NewRef(fdef), Let(\"dummy\", NumType, AssignRef(Ident(\"x\"), Const(30) ), DeRef(Ident(\"x\"))) )\n",
    "val t3 = try {\n",
    "   typeOfProgram(TopLevel(p3))\n",
    "   assert(false, \"The program should not receive a type\")\n",
    "} catch {\n",
    "    case TypeErrorException(msg) => s\"OK -- caught a type error exception: $msg\"\n",
    "    case e => print(e); assert(false, \"Please throw TypeErrorException(message) when a type failure occurs\")\n",
    "}\n",
    "passed(2)\n",
    "//END TEST"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "d117eda272da6ed9de6c800dd6df9aea",
     "grade": true,
     "grade_id": "cell-d0af48c3617e0684",
     "locked": true,
     "points": 2,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "//BEGIN TEST\n",
    "/* \n",
    "let x : ref(num => num) = NewRef(function(z: num) z + 10) in \n",
    "   let dummy: num = AssignRef(NewRef(35), 30) in \n",
    "       DeRef(x)\n",
    "       */\n",
    "val fdef = FunDef(\"z\", NumType, Plus(Ident(\"z\"), Const(10)))\n",
    "val p4 = Let(\"x\", RefType(FunType(NumType, NumType)), NewRef(fdef), Let(\"dummy\", NumType, AssignRef(NewRef(Const(35)), Const(30) ), DeRef(Ident(\"x\"))) )\n",
    "val t4 =  typeOfProgram(TopLevel(p4))\n",
    "assert(t4 == FunType(NumType, NumType), \"Test failed\")\n",
    "passed(2)\n",
    "//END TEST"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "b943060d6926aee5a6675d9c3ea28fe3",
     "grade": true,
     "grade_id": "cell-69076468ac4208e3",
     "locked": true,
     "points": 2,
     "schema_version": 1,
     "solution": false
    }
   },
   "outputs": [],
   "source": [
    "//BEGIN TEST\n",
    "\n",
    "val y = Ident(\"y\")\n",
    "val x = Ident(\"x\")\n",
    "val z = Ident(\"z\")\n",
    "val t1 = RefType(NumType)\n",
    "val t2 = FunType(t1, NumType)\n",
    "val t3 = RefType(t2)\n",
    "\n",
    "val v1 = FunCall(DeRef(y), x)\n",
    "val v2 = Let(\"z\", RefType(BoolType), NewRef(Geq(DeRef(x), Const(25))), v1)\n",
    "val fdef = FunDef(\"z\", RefType(NumType), Plus(DeRef(z), DeRef(x)))\n",
    "val v3 = Let(\"y\", t3, NewRef(fdef), v2)\n",
    "val v4 = Let(\"x\", t1, NewRef(Const(10)), v3)\n",
    "\n",
    "val p5 = TopLevel(v4)\n",
    "assert(typeOfProgram(p5) == NumType, \"Test failed\")\n",
    "passed(2)\n",
    "\n",
    "//END TEST"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "checksum": "9015f1b1dc6a1bc6e6443a9b29239579",
     "grade": false,
     "grade_id": "cell-66368a701542f6cc",
     "locked": true,
     "schema_version": 1,
     "solution": false
    }
   },
   "source": [
    "## Problem 2 (10 points): Attempted Type System for Division by Zero\n",
    "\n",
    "In class, we mentioned that developing a __static type system__ for catching run time errors is much harder. Let us try and see what happens.\n",
    "\n",
    "Let us modify our type grammar to have two different types of numbers: zero and non-zero.\n",
    "\n",
    "$$\\begin{array}{rcl} \n",
    "\\mathbf{Type} & \\rightarrow & NonZeroNumType \\\\\n",
    "& \\rightarrow & ZeroNumType \\\\\n",
    "\\end{array}$$\n",
    "\n",
    "with the following subset of Lettuce just involving arithmetic and let bindings:\n",
    "\n",
    "$$\\begin{array}{rcl}\n",
    "\\mathbf{Expr} & \\rightarrow & Const(\\mathbf{Double}) \\\\\n",
    "& | & Ident(\\mathbf{Identifier})\\\\\n",
    "& | & Plus(\\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "& | & Div(\\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "& | & Let(\\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}, \\mathbf{Expr})\\\\\n",
    "\\end{array}$$\n",
    "\n",
    "__Goal:__ Guarantee that a numeric value that receives type _ZeroNumType_ must be $0$ and a numeric value that receives _NonZeroNumType_ must always be non-zero.\n",
    "\n",
    "__Semantic Rules:__ \n",
    "\n",
    "__Constant:__ The new rule for constants are\n",
    "\n",
    "$$\\semRule{f \\not= 0}{\\typeOf(\\texttt{Const(f)}, \\alpha) = NonZeroNumType}{const-non-zero}$$\n",
    "\n",
    "$$\\semRule{f = 0}{\\typeOf(\\texttt{Const(f)}, \\alpha) = ZeroNumType}{const-zero}$$\n",
    "\n",
    "__Identifiers:__ The rule for identifiers remains unchanged (see notes).\n",
    "\n",
    "__Plus:__ The new rules for plus are\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = ZeroNumType,\\ \\typeOf(e2, \\alpha) = ZeroNumType}{\\typeOf(\\texttt{Plus(e1, e2)}, \\alpha) = ZeroNumType}{plus-zero}$$\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = NonZeroNumType,\\ \\typeOf(e2, \\alpha) = ZeroNumType}{\\typeOf(\\texttt{Plus(e1, e2)}, \\alpha) = NonZeroNumType}{plus-non-zero-1}$$\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = ZeroNumType,\\ \\typeOf(e2, \\alpha) = NonZeroNumType}{\\typeOf(\\texttt{Plus(e1, e2)}, \\alpha) = NonZeroNumType}{plus-non-zero-2}$$\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = NonZeroNumType,\\ \\typeOf(e2, \\alpha) = NonZeroNumType}{\\typeOf(\\texttt{Plus(e1, e2)}, \\alpha) = NonZeroNumType}{plus-non-zero-3}$$\n",
    "\n",
    "\n",
    "__Division:__ The rules for division are\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = ZeroNumType,\\ \\typeOf(e2, \\alpha) = NonZeroNumType}{\\typeOf(\\texttt{Div(e1, e2)}, \\alpha) = ZeroNumType}{div-zero}$$\n",
    "\n",
    "$$\\semRule{\\typeOf(e2, \\alpha) = ZeroNumType}{\\typeOf(\\texttt{Div(e1, e2)}, \\alpha) = \\mathbf{typeerror}}{div-error}$$\n",
    "\n",
    "$$\\semRule{\\typeOf(e1, \\alpha) = NonZeroNumType,\\ \\typeOf(e2, \\alpha) = NonZeroNumType}{\\typeOf(\\texttt{Div(e1, e2)}, \\alpha) = NonZeroNumType}{div-ok}$$\n",
    "\n",
    "__Let Binding:__ Rules are unchanged (see notes).\n",
    "\n",
    "\n",
    "We claim that if a Lettuce program is annotated with the types ZeroNumType and NonZeroNumType, and the type annotations are according to the rules above, then any attempt to divide a number by zero will result in __typeerror__ rather than a runtime exception thrown when evaluating the program using an interpreter.\n",
    "\n",
    "__(A)__ Write a Lettuce program that has the correct type annotations \n",
    "(you should use the concrete syntax for your answer) but results in a division by zero that is not \n",
    "detected as a __typeerror__.\n",
    "\n",
    "\n",
    "__(B)__ Point out which rule among the ones provided is incorrect (techically an incorrect type rule is called unsound).\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": false,
    "nbgrader": {
     "checksum": "008db56b709249835203dfbbf0d16c7d",
     "grade": true,
     "grade_id": "cell-455e0249c2a75e73",
     "locked": false,
     "points": 10,
     "schema_version": 1,
     "solution": true
    }
   },
   "source": [
    "(A) Div(Const(10),Plus(Const(-1),Const(1)))\n",
    "\n",
    "(B)plus-non-zero-3\n",
    "    If two NonZeroNumType numbers add to be 0, the resultant type should be ZeroNumType but this rule would\n",
    "    assign it a NonZeroNumType "
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Scala",
   "language": "scala",
   "name": "scala"
  },
  "language_info": {
   "codemirror_mode": "text/x-scala",
   "file_extension": ".scala",
   "mimetype": "text/x-scala",
   "name": "scala",
   "nbconvert_exporter": "script",
   "version": "2.12.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}