TypesAndTypeCheckingInLettuce.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Types and Their Usefulness\n",
    "\n",
    "We must all be familiar with types. They are fundamental to most of the programming languages that we have\n",
    "seen thus far. Let us take a language such as Java.  Whenever we write a class, function definition or declare\n",
    "a variable, we need to tell Java its type, even if obvious to us.\n",
    "\n",
    "~~~\n",
    "class Hello {\n",
    "  public int y;\n",
    "  public Hello (Hello h){\n",
    "     ... constructor code ...\n",
    "  }\n",
    "  \n",
    "  public String foo( int x) {\n",
    "     .. code must return a String .. \n",
    "  \n",
    "  }\n",
    "~~~\n",
    "\n",
    "You see that every declaration introduces the type of the thing that has been declared. `y` is declared to be an `int`. `h` the argument in the constructor of class `Hello` has type `Hello`. The return type of function `foo` is a `String` and its argument `x` has type `int`. \n",
    "\n",
    "\n",
    "What about other languages such as Python?\n",
    "\n",
    "~~~\n",
    ">>> x = 10\n",
    ">>> print(type(x))\n",
    "<class 'int'>\n",
    ">>> y = {\"x\":10, \"y\": 35, \"z\":50}\n",
    ">>> print(type(y))\n",
    "<class 'dict'>\n",
    "~~~\n",
    "\n",
    "Even though we do not write types, it is clear that the Python interpreter has the notion of types. Furthermore, it checks during runtime if operations make sense depending on the type of the argument.\n",
    "\n",
    "~~~\n",
    ">>> x = 10\n",
    ">>> y = \"hello\"\n",
    ">>> z = y * x\n",
    ">>> w = x ^ y\n",
    "TypeError: unsupported operand type(s) for ^: 'int' and 'str'\n",
    "~~~\n",
    "\n",
    "## Benefits of static typing\n",
    "\n",
    "Types can be checked at compile time (e.g. Java) or at run time (e.g. Python). If the former, the language is said to be *statically typed*; if the latter, the language is said to be *dynamically typed*.\n",
    "\n",
    "A major benefit of static typing is that you can rule out many errors *before* running your program. Consider the following Python program, which asks for the user's name and greets them in reponse. Can you find the bug?\n",
    "\n",
    "```python\n",
    "def get_first_name(full_name):\n",
    "    return full_name.split(\" \")[0]\n",
    "\n",
    "fallback_name = {\n",
    "    \"first_name\": \"UserFirstName\",\n",
    "    \"last_name\": \"UserLastName\"\n",
    "}\n",
    "\n",
    "raw_name = input(\"Please enter your name: \")\n",
    "first_name = get_first_name(raw_name)\n",
    "\n",
    "# If the user didn't type anything in, use the fallback name\n",
    "if not first_name:\n",
    "    first_name = get_first_name(fallback_name)\n",
    "\n",
    "print(f\"Hi, {first_name}!\")\n",
    "```\n",
    "\n",
    "This bug only manifests at run time and on a specific input -- finding and debugging such an error takes time and effort. A static type system would rule out such an error automatically without having to run your program. Recognizing this, Python 3.6 added support for type hints, which serve as a makeshift static type system for Python.\n",
    "\n",
    "```python\n",
    "from typing import Dict\n",
    "\n",
    "def get_first_name(full_name: str) -> str:\n",
    "    return full_name.split(\" \")[0]\n",
    "\n",
    "fallback_name: Dict[str, str] = {\n",
    "    \"first_name\": \"UserFirstName\",\n",
    "    \"last_name\": \"UserLastName\"\n",
    "}\n",
    "\n",
    "raw_name: str = input(\"Please enter your name: \")\n",
    "first_name: str = get_first_name(raw_name)\n",
    "\n",
    "# If the user didn't type anything in, use the fallback name\n",
    "if not first_name:\n",
    "    first_name = get_first_name(fallback_name)\n",
    "\n",
    "print(f\"Hi, {first_name}!\")\n",
    "```\n",
    "This enables the type checker to catch the bug before running the code. In a language-aware IDE such as PyCharm, you can even catch type errors as you write the code, just as a spell-checker catches spelling mistakes on the fly.\n",
    "\n",
    "![ide-type-error](https://cdn-images-1.medium.com/max/1200/1*0K13YjrBJYUlJHcNiJiV6g.png)\n",
    "\n",
    "Credit: https://medium.com/@ageitgey/learn-how-to-use-static-type-checking-in-python-3-6-in-10-minutes-12c86d72677b"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Type Checked Lettuce\n",
    "\n",
    "In this lecture, we will study types and endow Lettuce with a static type system. Static type checking allows us to ensure that a variety of runtime errors will never happen when we execute the program.\n",
    "\n",
    "- When we evaluate an identifier, we would like it to be defined (or bound) in the environment.\n",
    "- Whenever we evaluate arithmetic expressions involving Plus, Minus, Mult, Div, ... we would like  to guarantee that the arguments evaluate to numbers.\n",
    "- Whenever we evaluate comparisons like Geq, Eq, .., both arguments evaluate to numbers.\n",
    "- Whenever we evaluate Boolean operators such as And, Or, Not, we would like its arguments to be booleans.\n",
    "- If then else expressions must have a Boolean type condition and the then/else parts must be the same expressions.\n",
    "- Whenever we call a function, the called expression must evaluate to a closure. The argument must evaluate to an appropriate type for the function.\n",
    "\n",
    "## Lettuce Language\n",
    "\n",
    "Let us consider Lettuce with numerical (double precision), Boolean, Closures, and __error__.  We will\n",
    "not consider references yet. But include the _recursive function calls_. The grammar is shown below for your reference: \n",
    "\n",
    "\n",
    "\n",
    "$$\\begin{array}{rcll}\n",
    "\\mathbf{Program} & \\rightarrow & TopLevel(\\mathbf{Expr}) \\\\[5pt]\n",
    "\\mathbf{Expr} & \\rightarrow & Const(\\mathbf{Number}) \\\\\n",
    " & | & Ident(\\mathbf{Identifier}) \\\\\n",
    " & | & Plus(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Mult(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Div(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Eq(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Geq (\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & IfThenElse(\\mathbf{Expr}, \\mathbf{Expr}, \\mathbf{Expr}) & \\text{if (expr) then expr else expr} \\\\\n",
    " & | & Let( \\mathbf{Identifier}, \\mathbf{Expr}, \\mathbf{Expr}) & \\text{let identifier = expr in expr} \\\\\n",
    " & | & FunDef( \\mathbf{Identifier}, \\mathbf{Expr}) & \\text{function (identifier-formal-parameter) expr } \\\\ \n",
    " & | & FunCall(\\mathbf{Expr}, \\mathbf{Expr}) & \\text{function call - expr(expr)} \\\\\n",
    " & | & LetRec(\\mathbf{Identifier}, \\mathbf{Identifier}, \\mathbf{Expr}, \\mathbf{Expr})  & \\text{argument 1 - function name, argument 2 - parameter}\\\\\n",
    " &&& \\text{argument 3 - function definition expression, argument 4 - body expr} \\\\[5pt]\n",
    "\\end{array}$$\n",
    "\n",
    "## Examples of Welltyped vs. Mistyped Expressions. \n",
    "\n",
    "To motivate our study, let us start with various examples of welltyped vs. mistyped expressions (programs).\n",
    "\n",
    "### 1. Mistyped Program \n",
    "~~~\n",
    "let x = 10 in \n",
    "   if (x) then True else False\n",
    "~~~\n",
    "\n",
    "This is mistyped because x is used as a Boolean in the `if-then-else` statement.\n",
    "\n",
    "### 2. Welltyped Program \n",
    "\n",
    "~~~\n",
    "let x = 10 in \n",
    "   if (x >= 9) then 1 else 2\n",
    "~~~\n",
    "\n",
    "The type of the program as a whole is __num__ since it returns a numerical value.\n",
    "\n",
    "### 3. Mistyped Program\n",
    "\n",
    "~~~\n",
    "let f =  function (x) \n",
    "    if (x >= 10) \n",
    "    then 9\n",
    "    else false\n",
    " in ...\n",
    "~~~\n",
    "\n",
    "The program is considered mistyped since the function `f` does not have a definite return type: it returns a number or a boolean depending on the value of `x`. \n",
    "\n",
    "Note that such functions were perfectly OK thus far. So the decision to call them mistyped can be considered controversial. \n",
    "\n",
    "### 4. Mistyped Program\n",
    "\n",
    "~~~\n",
    "let f = 10 in \n",
    "   f (20) \n",
    "~~~\n",
    "\n",
    "Although f is used as a called function in `f (20)`, note that it is not a function.\n",
    "\n",
    "### 5. Welltyped Program\n",
    "\n",
    "~~~\n",
    "let rec f = function (x) f (x - 1) in \n",
    "   f(36)\n",
    "~~~\n",
    "\n",
    "We will accept this program as valid typed even the recursive call never terminates. Why do we make this decision? It is somewhat pragmatic. It will turn out that proving termination/non-termination is very hard problem\n",
    "for computers (this is called the halting problem). \n",
    "\n",
    "So if we said  that only terminating program can be well  typed: checking whether a program is well typed will become equivalent to solving the halting problem, which is not easy. Therefore, we will side step this issue for now. The situation is not as dire as one may think. It is certainly possible to design systems in which only terminating recursions can be defined. However, this is outside the scope of our studies in this class.\n",
    "\n",
    "\n",
    "### 6. Mistyped Program\n",
    "\n",
    "~~~\n",
    "let x = 10 in \n",
    "  let y = true in \n",
    "      x - y\n",
    "~~~\n",
    "\n",
    "Subtracting a boolean from a number.\n",
    "\n",
    "### 7. Mistyped program\n",
    "\n",
    "~~~\n",
    "let x = y + 10 in \n",
    "   x\n",
    "~~~\n",
    "\n",
    "`y` is not defined in the very first line of the program.\n",
    "\n",
    "\n",
    "\n",
    "## Basic Types \n",
    "\n",
    "Let us study the problem of checking if a program is well typed by starting with the definition of all possible types. \n",
    "\n",
    "- __num__ is the type of all expressions that yield a numerical value in $\\mathbb{R}$.\n",
    "- __bool__ is the type of all expressions that yield a Boolean value in $\\mathbb{B}$.\n",
    "- __t1 => t2__ denotes a function type, wherein t1 and t2 are types.\n",
    "\n",
    "We will skip a type for __error__. It is a value that will only be encountered at runtime and we will never\n",
    "intentionally create __error__ in our language. So it will make no sense to have it as a valid type in our type system.\n",
    "\n",
    "Let us take some examples:\n",
    "\n",
    "- `Const(10.0)` has type __num__\n",
    "- `Const(True)` has type __bool__\n",
    "- `Plus(Const(10), Const(5))` has type __num__\n",
    "- `Minus(Const(10), Const(True))` has no type in our system since it is a mistyped epression.\n",
    "- `And( Geq(Const(10.0), Const(5.0)), Eq(Const(True), Const(False)) )` has type __bool__\n",
    "- `Let(\"x\", Const(15.0), Plus(Ident(\"x\"), Const(20)))` has type __num__. \n",
    "- `FunDef(\"x\", Plus(Ident(\"x\"), Const(10)))` has type __num => num__  or is mistyped, depending on the type of the identifier \"x\".  \n",
    "\n",
    "The last example already shows us the main issue. We cannot really talk about the type of an expression unless, we know the type of identifiers. \n",
    "\n",
    "In the first version of Lettuce, we will use type annotations."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Lettuce with Type Annotations\n",
    "\n",
    "Type annotations are common in many languages such as Java, C/C++, and Scala. For instance, consider the program below:\n",
    "\n",
    "~~~\n",
    "int foo(int y){\n",
    "  int x = 200;\n",
    "  return y + x \n",
    "  }\n",
    "~~~\n",
    "\n",
    "The type annotations tell us to expect that \n",
    "- y is an integer\n",
    "- x is an integer\n",
    "- The function foo takes one integer argument and returns an integer.\n",
    "\n",
    "This does not mean that the function is well typed. However, having declared the types, the compiler can\n",
    "more easily check the function and make sure that the declared types match with what the program does.\n",
    "\n",
    "Similar type annotations are used in Scala programs.\n",
    "\n",
    "~~~\n",
    "def f(y: Int): Int = {\n",
    "    val x : Int = 200\n",
    "    y + x\n",
    "}\n",
    "~~~\n",
    "\n",
    "We will do the same with Lettuce with type annotations. The syntax is different but the idea is the same.\n",
    "\n",
    "\n",
    "## Where should type annotations be added?\n",
    "\n",
    "Let us consider the basic problem of where type annotations should be added in a Lettuce program. \n",
    "One way of doing this is to make sure that every identifier that is introduced also has a type annotations.\n",
    "\n",
    "There are two places where new identifiers are introduced:\n",
    "\n",
    "- Let bindings: `let x = .... in ...`. We should put in a type annotation for x.\n",
    "- Ditto for Let rec bindings.\n",
    "- Function call parameters: ` function (x) ... `.  We should put in a type annotation for x.\n",
    "\n",
    "Therefore, we will modify Lettuce syntax to allow type annotations at the site of let bindings, let rec bindings and function call definitions.\n",
    "\n",
    "## Grammar of Types\n",
    "\n",
    "We will first start with a grammar for the types that can be annotated.\n",
    "\n",
    "$$\\begin{array}{rcl}\n",
    "\\mathbf{Type} & \\rightarrow & NumType \\\\\n",
    "& | & BoolType \\\\\n",
    "& | & FunType(\\mathbf{Type}, \\mathbf{Type}) \\\\\n",
    "\\end{array} $$\n",
    "\n",
    "The grammar is simple enough: we have types for numbers `NumType`, booleans `BoolType`,  and\n",
    "functions `FunType(t1, t2)`.\n",
    "\n",
    "A complex type such as __ num => ( (num => bool) => bool) __ is expressed as `FunType(NumType, FunType( FunType(NumType, BoolType), BoolType))`.\n",
    "\n",
    "## Lettuce Grammar with Type Annotations\n",
    "\n",
    "We will first explain the concrete syntax with type annotations.\n",
    "\n",
    "- Let bindings with type annotations will have the form \n",
    "   ~~~ \n",
    "   let x: type = expr in expr \n",
    "   ~~~\n",
    "\n",
    "- Function definition expressions will have the form\n",
    "   ~~~\n",
    "   function (x: type) ... expr ... \n",
    "   ~~~\n",
    "   \n",
    "- Letrec bindings with type annotations will have the form\n",
    "   ~~~\n",
    "    let rec f: type = function (x: type) expr in expr\n",
    "   ~~~\n",
    "   \n",
    "\n",
    "$$\\begin{array}{rcll}\n",
    "\\mathbf{Program} & \\rightarrow & TopLevel(\\mathbf{Expr}) \\\\[5pt]\n",
    "\\mathbf{Expr} & \\rightarrow & Const(\\mathbf{Number}) \\\\\n",
    " & | & Ident(\\mathbf{Identifier}) \\\\\n",
    " & | & Plus(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Mult(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Eq(\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & Geq (\\mathbf{Expr}, \\mathbf{Expr}) \\\\\n",
    " & | & IfThenElse(\\mathbf{Expr}, \\mathbf{Expr}, \\mathbf{Expr}) & \\text{if (expr) then expr else expr} \\\\\n",
    " & | & Let( \\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}, \\mathbf{Expr}) & \\text{let identifier = expr in expr} \\\\\n",
    " & | & FunDef( \\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}) & \\text{function (identifier-formal-parameter) expr } \\\\ \n",
    " & | & FunCall(\\mathbf{Expr}, \\mathbf{Expr}) & \\text{function call - expr(expr)} \\\\\n",
    " & | & LetRec(\\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Identifier}, \\color{red}{\\mathbf{Type}}, \\mathbf{Expr}, \\mathbf{Expr})  & \\text{}\\\\\n",
    " &&& \\text{} \\\\[5pt]\n",
    "\\end{array}$$\n",
    "\n",
    "\n",
    "### Examples of type annotated programs\n",
    "\n",
    "__Example 1:__  The concrete syntax is \n",
    "~~~\n",
    "let x : num = 25 in \n",
    "    x + 30\n",
    "~~~\n",
    "The abstract syntax is \n",
    "~~~\n",
    "Let(\"x\", NumType, Const(25), Plus(Ident(\"x\"), Const(30)) )\n",
    "~~~\n",
    "\n",
    "__Example 2:__ Concrete syntax\n",
    "~~~\n",
    "let y : num = 15 in \n",
    " let x : bool = 25 >= y in \n",
    "     x and (30 >= y)\n",
    "~~~\n",
    "\n",
    "Abstract syntax\n",
    "~~~\n",
    "Let (\"y\", NumType, Const(15), \n",
    "        Let (\"x\", BoolType, Geq (Const(25), Ident(\"y\")), \n",
    "              And( Ident(\"x\"), Geq(Const(30), Ident(\"y\")) )\n",
    "             )\n",
    "    )\n",
    "~~~\n",
    "\n",
    "__Example 3:__ Concrete Syntax\n",
    "\n",
    "~~~\n",
    "let f : (num => num) => num = function (g: num => num) g(20) in \n",
    "    let g : num => num = function (x: num) x in \n",
    "        f (g) \n",
    "~~~\n",
    "\n",
    "Abstract Syntax\n",
    "~~~\n",
    "Let (\"f\", FunType( FunType(NumType, NumType), NumType ), \n",
    "          FunDef(\"g\", FunType(NumType, NumType), FunCall( Ident(\"g\"), Const(20) ), \n",
    "          Let (\"g\", FunType(NumType, NumType), FunDef(\"x\", Num, Ident(\"x\")), \n",
    "              FunCall(Ident(\"f\"), Ident(\"g\"))\n",
    "~~~\n",
    "\n",
    "We are ready to add the AST to scala in the usual manner."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mtrait\u001b[39m \u001b[36mType\u001b[39m\n",
       "defined \u001b[32mobject\u001b[39m \u001b[36mNumType\u001b[39m\n",
       "defined \u001b[32mobject\u001b[39m \u001b[36mBoolType\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mFunType\u001b[39m\n",
       "defined \u001b[32mtrait\u001b[39m \u001b[36mProgram\u001b[39m\n",
       "defined \u001b[32mtrait\u001b[39m \u001b[36mExpr\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mConst\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mIdent\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mMinus\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mPlus\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mMult\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mDiv\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mEq\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mGeq\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mIfThenElse\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mLet\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mFunDef\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mFunCall\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mLetRec\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mTopLevel\u001b[39m"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "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",
    "\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 Minus(e1: Expr, e2: Expr) extends Expr\n",
    "case class Plus(e1: Expr, e2: Expr) extends Expr\n",
    "case class Mult(e1: Expr, e2: Expr) extends Expr\n",
    "case class Div(e1: Expr, e2: Expr) extends Expr\n",
    "case class Eq(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 LetRec(funName: String, funType: Type, param: String, paramType: Type, funExpr: Expr, bodyExpr: Expr) extends Expr\n",
    "\n",
    "case class TopLevel(e: Expr) extends Program\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Checking\n",
    "\n",
    "Given a type annotated lettuce program, is the type annotation correct? To do so, we are going to implement a type checker that uses and checks the type annotation. Thus, we should be able to say things like this:\n",
    "\n",
    "### Example 1\n",
    "\n",
    "The program \n",
    "~~~\n",
    "let x: num = true in \n",
    "   x + 10\n",
    "~~~\n",
    "is mistyped.\n",
    "\n",
    "The program \n",
    "~~~\n",
    "let x: num = 25 in \n",
    "   x + 10\n",
    "~~~\n",
    "is welltyped and has type `num`.\n",
    "\n",
    "### Example 2\n",
    "\n",
    "The program \n",
    "~~~\n",
    "let rec f: num => num = function (x: num) if (x <= 0) then 1 else x * f(x-1) in \n",
    "  f(30)\n",
    "~~~\n",
    "is welltyped and has type `num`.\n",
    "\n",
    "The program \n",
    "~~~\n",
    "let rec f: num => num = function (x: num) if (x <= 0) then true else x >= f(x-1) in \n",
    "  f(30)\n",
    "~~~\n",
    "is mistyped.\n",
    "\n",
    "The goal of a type checker is to take in an annotated lettuce program and compute its type. If the program's type is successfully computed, we also conclude that it is well typed and in doing so, we calculate the type of each expression. Therefore, we will define a recursive type checker that calculates the type of an expression:\n",
    "`typeOf(expr, type-environment)` much like an interpreter implements a function `eval(expr, environment)`.\n",
    "\n",
    "- We will need to clarify what a `type-environment` is in contrast to the environments we are familar with.\n",
    "- `typeOf` is either successful and provides a type for the expression or computes a __type-error__ that signifies a mistyped expression.\n",
    "\n",
    "### Errors that a type checker will not catch.\n",
    "\n",
    "As mentioned earlier, there are runtime errors that a type checker can catch before we run the program. On the other hand, there are errors that we cannot catch using a type checker. Let us clearly mention what these are:\n",
    "- Nontermination -- we can have programs that may not terminate. We cannot catch these errors.\n",
    "- Divide by zero, log on negative values, etc.. These kinds of errors are not type errors. When we write a program: \n",
    "~~~ \n",
    "let x : num = 0 in \n",
    "  let f : num => num = function (y: num) y/x in \n",
    "      f(220)\n",
    "~~~\n",
    "\n",
    "The program is typed correctly. However, the fact that it divides by zero is not part of our type system and we will note that it is in general undecidable. We will call these runtime errors.\n",
    "\n",
    "\n",
    "### Types and Values\n",
    "\n",
    "\n",
    "First we will denote for each type in our system, a set of values that belong to that type:\n",
    "- __num__ corresponds to all values in $\\mathbb{R}$.\n",
    "- __bool__ corresponds to all values in $\\mathbb{B}$.\n",
    "- __t1 => t2__ corresponds to all closures in $\\mathbb{C}$ that have a formal argument that takes in value `t1` and returns a value of type `t2`.\n",
    "\n",
    "### Type Environments\n",
    "\n",
    "Just like we have environments $\\sigma$ that map identifiers to values, we need to have type environments $\\alpha$ that map identifiers to types.\n",
    "\n",
    "Example: \n",
    "\n",
    "- Enviromnent : $\\sigma: \\{ \"x\" \\mapsto 2, \"y\" \\mapsto true, \"f\" \\mapsto Closure(\"x\", Plus(\"x\", Const(10))) \\}$.\n",
    "- Type Environment: $\\alpha: \\{ \"x\" \\mapsto \\mathbf{num},\\ \"y\" \\mapsto \\mathbf{bool},\\ \"f\" \\mapsto \\mathbf{num} => \\mathbf{num} \\}$.\n",
    "\n",
    "We say that an environment $\\sigma$ is \\emph{compatible} with a type environment $\\alpha$ if and only if \n",
    "- $\\mathbf{domain}(\\sigma) \\subseteq \\mathbf{domain}(\\alpha)$ - everything defined in $\\sigma$ must be typed in $\\alpha$.\n",
    "- $\\sigma(x)$ is a value of type $\\alpha(x)$ for every $x \\in \\mathbf{domain}(\\sigma)$. If $v$ is the value of $x$ in $\\sigma$, the type in $\\alpha$ must be the type of value $v$.\n",
    "\n",
    "**Definition** An expression `e` in a program has a type `t`  under type environment $\\tau$ if and only if \n",
    "- for any environment $\\sigma$ that is _compatible_ with $\\alpha$, \n",
    "- evaluating the expression $e$ under $\\sigma$ must yield one of the following possibilities:\n",
    "   - A value of type $t$, \n",
    "   - Nonterminating execution, or\n",
    "   - A runtime error due to division by zero.\n",
    "   \n",
    "   \n",
    "We will use a special type value __typeerror__ to signify that an expression is mistyped. In practice, our type checker will simply throw an exception under type errors."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Checking for Lettuce With Recursion\n",
    "\n",
    "$$\\newcommand\\typeOf{\\mathbf{typeOf}}$$\n",
    "Let us first look at a type checker without recursion. We will write proof rules for the \n",
    "function $\\typeOf(\\texttt{e}, \\alpha)$, the type of an expression under environment $\\alpha$.\n",
    "\n",
    "## Const Rule\n",
    "\n",
    "$$\\newcommand\\semRule[3]{\\begin{array}{c} #1 \\\\ \\hline #2 \\\\ \\end{array}\\;(\\text{#3}) }$$\n",
    "\n",
    "$$\\semRule{}{\\typeOf(\\texttt{Const(f)}, \\alpha) = \\mathbf{num}}{Const}$$\n",
    "\n",
    "## Identifier Rule\n",
    "\n",
    "$$\\semRule{x \\in \\mathbf{domain}(\\alpha)}{ \\typeOf(\\texttt{Ident(x)}, \\alpha)  = \\alpha(x)}{ident-ok}$$\n",
    "$$\\semRule{x \\not\\in \\mathbf{domain}(\\alpha)}{ \\typeOf(\\texttt{Ident(x)}, \\alpha)  = \\mathbf{typeerror}}{ident-nok}$$\n",
    "\n",
    "The first rule is straightforward. The second rule says that an undefined variable leads to a __typeerror__\n",
    "\n",
    "## Arithmetic Rule\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\mathbf{num},\\ \\typeOf(\\texttt{e2}, \\alpha) = \\mathbf{num}, T \\in \\{ Plus, Minus, Mult, Div \\} }{\\typeOf(\\texttt{T(e1, e2)}, \\alpha) = \\mathbf{num}}{arith-ok} $$\n",
    "\n",
    "Note that we do not check if `Div` leads to a division by zero in our type checking rule. This is a difference between the interpreter and type checker.\n",
    "\n",
    "Short circuit semantics for type error: \n",
    "\n",
    "$$\\semRule{\\color{red}{\\typeOf(\\texttt{e1}, \\alpha) \\not= \\mathbf{num}},\\ T \\in \\{ Plus, Minus, Mult, Div \\} }{\\typeOf(\\texttt{T(e1, e2)}, \\alpha) = \\mathbf{typeerror}}{arith-nok-1} $$\n",
    "\n",
    "Note that if `e1` leads to a result that is not a number, we simply shortcut.\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\mathbf{num},\\ \\color{red}{\\typeOf(\\texttt{e2}, \\alpha) \\not= \\mathbf{num}},\\ T \\in \\{ Plus, Minus, Mult, Div \\} }{\\typeOf(\\texttt{T(e1, e2)}, \\alpha) = \\mathbf{typeerror}}{arith-nok-2} $$\n",
    "\n",
    "## Comparison Operator Rule\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\mathbf{num},\\ \\typeOf(\\texttt{e2}, \\alpha) = \\mathbf{num}, T \\in \\{ Geq\\} }{\\typeOf(\\texttt{T(e1, e2)}, \\alpha) = \\mathbf{bool}}{geq-ok} $$\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\typeOf(\\texttt{e2}, \\alpha) }{\\typeOf(\\texttt{Eq(e1, e2)}, \\alpha) = \\mathbf{bool}}{eq-ok} $$\n",
    "\n",
    "Notice how the equality operator is unlike the Geq operator. We are allowed to compare any two types using the equality operator in our language.\n",
    "\n",
    "__Exercise__ Write down the type error rules for comparsion operators.\n",
    "\n",
    "## Boolean Operator Rule\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{e1}, \\alpha) = \\mathbf{bool},\\ \\typeOf(\\texttt{e2}, \\alpha) = \\mathbf{bool}, T \\in \\{ And, Or\\} }{\\typeOf(\\texttt{T(e1, e2)}, \\alpha) = \\mathbf{bool}}{boolop-ok} $$\n",
    "\n",
    "Note that unlike the rule for interpreter, the type checker does not __short circuit__ boolean operators. This is because, we cannot know in advance if the value of `e1` is true for an `Or` or false for an `And`.\n",
    "\n",
    "__Exercise__ Write down the type error rules for boolean operators.\n",
    "\n",
    "\n",
    "## If Then Else Rule\n",
    "\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{condExpr}, \\alpha) = \\mathbf{bool}\\\\ \\typeOf(\\texttt{thenExpr}, \\alpha) = \\typeOf(\\texttt{elseExpr}, \\alpha) = t,\\ t \\not= \\mathbf{typeerror} }{\\typeOf(\\texttt{If(condExpr, thenExpr, elseExpr)}, \\alpha) = t}{ite-ok} $$\n",
    "\n",
    "$$\\semRule{\\color{red}{\\typeOf(\\texttt{condExpr}, \\alpha) \\not= \\mathbf{bool}} }{\\typeOf(\\texttt{If(condExpr, thenExpr, elseExpr)}, \\alpha) = \\mathbf{typeerror} }{ite-nok-1} $$\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{condExpr}, \\alpha) = \\mathbf{bool}\\\\ \\color{red}{\\typeOf(\\texttt{thenExpr}, \\alpha) \\not= \\typeOf(\\texttt{elseExpr}, \\alpha)}}{\\typeOf(\\texttt{If(condExpr, thenExpr, elseExpr)}, \\alpha) = \\mathbf{typeerror}}{ite-nok-2} $$\n",
    "\n",
    "## Let bindings\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{xExpr}, \\alpha) = \\texttt{xType} \\\\\n",
    "\\typeOf(\\texttt{body}, \\alpha[\\texttt{x} \\mapsto \\texttt{xType}]) = t}{ \\typeOf(\\texttt{Let(x, xType, xExpr, body)}, \\alpha) =  t}{let-ok}$$\n",
    "\n",
    "The rule has couple of things to note:\n",
    "- Note how we check that `xExpr` must have type `xType`, the same type as the annotation for `x`.\n",
    "- When type checking `body`, we add the mapping $x \\mapsto \\texttt{xType}$ to the type environment.\n",
    "\n",
    "A type error results when `xExpr` does not match the type annotation for `x` in the binding.\n",
    "\n",
    "$$\\semRule{\\color{red}{\\typeOf(\\texttt{xExpr}, \\alpha) \\not= \\texttt{xType}}}{ \\typeOf(\\texttt{Let(x, xType, xExpr, body)}, \\alpha) = \\mathbf{typeerror}}{let-nok-1}$$\n",
    "\n",
    "Similarly, a type error results when `body` leads to a type error.\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{xExpr}, \\alpha) = \\texttt{xType}\\\\\n",
    "\\color{red}{\\typeOf(\\texttt{body}, \\alpha[x \\mapsto \\texttt{xType}]) = \\mathbf{typeerror}}}{ \\typeOf(\\texttt{Let(x, xType, xExpr, body)}, \\alpha) = \\mathbf{typeerror} }{let-nok-2}$$\n",
    "\n",
    "Note that having written down this rule, we are going to get the same effect from the let-ok rule already.\n",
    "\n",
    "## Function Definitions\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{body}, \\alpha[\\texttt{arg} \\mapsto \\texttt{argType}]) = \\texttt{returnType},\\ \\texttt{returnType} \\not= \\mathbf{typeerror}}{\n",
    "\\typeOf(\\texttt{FunDef(arg, argType, body)}) = (\\texttt{argType} => \\texttt{returnType})}{fun-ok}$$\n",
    "\n",
    "\n",
    "$$\\semRule{\\color{red}{\\typeOf(\\texttt{body}, \\alpha[\\texttt{arg} \\mapsto \\texttt{argType}]) =  \\mathbf{typeerror}}}{\n",
    "\\typeOf(\\texttt{FunDef(arg, argType, body)} = \\mathbf{typeerror} }{fun-nok}$$\n",
    "\n",
    "## Function Calls\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{argExpr}, \\alpha) = \\texttt{t1} \\\\ \\typeOf(\\texttt{funcExpr}, \\alpha) = \\texttt{t1} => \\texttt{t2}}{\\typeOf(\\texttt{FunCall(funcExpr, argExpr)}, \\alpha) = \\texttt{t2}}{funcall-ok}$$\n",
    "\n",
    "Note that technically in our type system when we have a function type `t1 => t2`, we know for a fact\n",
    "that `t1` and `t2` cannot be a type error. This makes it redundant to say `t1 != typeerror` or `t2 != typeerror` in the rule.\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{argExpr}, \\alpha) = \\texttt{t1}\\\\ \\color{red}{\\typeOf(\\texttt{funcExpr}, \\alpha) \\not= \\texttt{t1} => \\texttt{t2}}}{\\typeOf(\\texttt{FunCall(funcExpr, argExpr)}, \\alpha) = \\mathbf{typeerror}}{funcall-nok}$$\n",
    "\n",
    "__Exercise__ Write rules when evaluating `funcExpr` or `argExpr` leads to a typeerror.\n",
    "\n",
    "## Handling Recursion \n",
    "\n",
    "The rule for recursion is actually much easier than the corresponding rule when we wrote an interpreter to support it.\n",
    "\n",
    "$$\\semRule{\\typeOf(\\texttt{funcBody}, \\alpha[arg \\mapsto \\texttt{argType}, f \\mapsto \\texttt{argType => returnType}]) = \\texttt{t2}\\\\\n",
    "\\typeOf(\\texttt{letBody}, \\alpha[f \\mapsto \\texttt{argType => returnType}]) = t}{\n",
    "\\typeOf(\\texttt{LetRec(f, argType => returnType, arg, argType, funcBody, letBody)},\\alpha) = t}{rec-ok}$$\n",
    "\n",
    "The idea behind the rule is as follows. Take a let rec definition:\n",
    "\n",
    "~~~\n",
    "let f: argType => returnType = function (x: argType) funcBody\n",
    "   in letBody\n",
    "~~~\n",
    "\n",
    "- We check that if `f` were typed as `argType => returnType` and `arg` were typed as `argType`, does `funcBody` have a type of `returnType`?\n",
    "- If yes to the question above, then we evaluate the type of `letBody` with `f` now receiving the type `argType => returnType`.\n",
    "\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mtypeEquals\u001b[39m\n",
       "defined \u001b[32mclass\u001b[39m \u001b[36mTypeErrorException\u001b[39m"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def typeEquals(t1: Type, t2: Type): Boolean = t1 == t2\n",
    "\n",
    "\n",
    "case class TypeErrorException(s: String) extends Exception\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mtypeOf\u001b[39m\n",
       "defined \u001b[32mfunction\u001b[39m \u001b[36mtypeOfProgram\u001b[39m"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "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 Mult(e1, e2) => checkType(\"Mult\",e1,  NumType, e2, NumType, NumType)\n",
    "        case Div(e1, e2) => checkType(\"Div\", e1,  NumType, e2, NumType, NumType)\n",
    "        case Geq(e1, e2) => checkType(\"Geq\", e1,  NumType, e2, NumType, BoolType)\n",
    "        case Eq(e1, e2) => {\n",
    "            val t1 = typeOf(e1, alpha)\n",
    "            val t2 = typeOf(e2, alpha)\n",
    "            if (typeEquals(t1, t2))\n",
    "                BoolType\n",
    "            else \n",
    "                throw TypeErrorException(s\"Equality operator compares unequal types $t1 with $t2\")\n",
    "        }\n",
    "\n",
    "        //case And(e1, e2) => checkType(e1, BoolType, e2, BoolType, BoolType)\n",
    "        //case Or(e1, e2) => checkType(e1, BoolType, e2, BoolType, 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 LetRec(f, fType, x, argType, e1, e2 ) => {\n",
    "            fType match {\n",
    "                case FunType(t1, t2) => {\n",
    "                    if (typeEquals(argType, t1)){\n",
    "                        val newAlpha = alpha +(f -> fType, x -> argType)\n",
    "                        val retType = typeOf(e1, newAlpha)\n",
    "                        if (typeEquals(retType, t2)){\n",
    "                            typeOf(e2, alpha + (f -> fType))\n",
    "                        } else {\n",
    "                            throw TypeErrorException(s\"Rec. function call expression evaluates to type $retType. Expected type: $t2\")\n",
    "                        }\n",
    "                    } else {\n",
    "                        throw TypeErrorException(s\"Recursive function: function type $fType incompatible with declared type of argument: $argType\")\n",
    "                    }\n",
    "                }\n",
    "                case _ => {throw TypeErrorException(s\"Recursive function is annotated with non function type: $fType\")}\n",
    "            }\n",
    "        }\n",
    "    }\n",
    "}\n",
    "\n",
    "def typeOfProgram(p: Program) = p match {\n",
    "    case TopLevel(e) => {\n",
    "        try {\n",
    "            val t = typeOf(e, Map())\n",
    "            println(s\"Program type computed successfully as $t\")\n",
    "        } catch {\n",
    "            case TypeErrorException(s) => println(s\"Type error found: $s\")\n",
    "        }\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Program type computed successfully as NumType\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "\u001b[36mp1\u001b[39m: \u001b[32mTopLevel\u001b[39m = TopLevel(Let(x,NumType,Const(20.0),Plus(Ident(x),Const(30.0))))"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val p1 = TopLevel(Let(\"x\", NumType, Const(20), Plus(Ident(\"x\"), Const(30)) ))\n",
    "typeOfProgram(p1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Type error found: Type mismatch in arithmetic/comparison/bool op Geq, Expected type NumType, obtained BoolType\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "\u001b[36mp2\u001b[39m: \u001b[32mTopLevel\u001b[39m = TopLevel(Let(y,NumType,Const(15.0),Let(x,BoolType,Geq(Const(25.0),Ident(y)),Geq(Ident(x),Geq(Const(30.0),Ident(y))))))"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "/* let y = 15 in \n",
    "      let x = 25 >= y in \n",
    "          x >= (30 >= y)\n",
    "          */\n",
    "val p2 = TopLevel(Let (\"y\", NumType, Const(15), \n",
    "        Let (\"x\", BoolType, Geq (Const(25), Ident(\"y\")), \n",
    "              Geq( Ident(\"x\"), Geq(Const(30), Ident(\"y\")) )\n",
    "             )\n",
    "    ))\n",
    "typeOfProgram(p2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Program type computed successfully as NumType\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "\u001b[36mp\u001b[39m: \u001b[32mTopLevel\u001b[39m = TopLevel(Let(f,FunType(FunType(NumType,NumType),NumType),FunDef(g,FunType(NumType,NumType),FunCall(Ident(g),Const(20.0))),Let(g,FunType(NumType,NumType),FunDef(x,NumType,Ident(x)),FunCall(Ident(f),Ident(g)))))"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val p = TopLevel(Let (\"f\", FunType( FunType(NumType, NumType), NumType ), \n",
    "          FunDef(\"g\", FunType(NumType, NumType), FunCall( Ident(\"g\"), Const(20) )), \n",
    "          Let (\"g\", FunType(NumType, NumType), FunDef(\"x\", NumType, Ident(\"x\")), \n",
    "              FunCall(Ident(\"f\"), Ident(\"g\")))))\n",
    "typeOfProgram(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Program type computed successfully as NumType\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "\u001b[36mp\u001b[39m: \u001b[32mTopLevel\u001b[39m = TopLevel(LetRec(f,FunType(NumType,NumType),z,NumType,IfThenElse(Geq(Const(0.0),Ident(z)),Const(1.0),Plus(Const(1.0),FunCall(Ident(f),Minus(Ident(z),Const(1.0))))),FunCall(Ident(f),Const(10.0))))"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "/*\n",
    "let rec f: Num => Num = function (z: Num) if (z <= 0) then 1 else 1 + f(z -1) in f(10)\n",
    "*/\n",
    "\n",
    "val p = TopLevel(\n",
    "    LetRec(\"f\", FunType(NumType, NumType), \"z\", NumType, \n",
    "          IfThenElse( \n",
    "                         Geq(Const(0), Ident(\"z\")),\n",
    "                         Const(1),\n",
    "                         Plus(Const(1), FunCall(Ident(\"f\"), Minus(Ident(\"z\"), Const(1))))\n",
    "                         ), \n",
    "                  FunCall(Ident(\"f\"), Const(10))\n",
    "          )\n",
    "\n",
    ")\n",
    "typeOfProgram(p)"
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "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
}