09 - Simply Typed Lambda Calculus.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# TaPL Chapter 9 - Simply Typed Lambda Calculus\n",
    "\n",
    "Chapter 9 of [TaPL](https://www.cis.upenn.edu/~bcpierce/tapl/) describes a\n",
    "simple language consisting of lambda calculus (from chapter 5) plus the boolean\n",
    "expressions `true`, `false`, and `if ... then ... else ...` (from chapters 3 and\n",
    "8).\n",
    "\n",
    "It then shows how that language can by typed. This _Simply Typed Lambda\n",
    "Calculus_ forms the basis of every other typed language in the rest of the book.\n",
    "\n",
    "## 9.1 Function Types\n",
    "\n",
    "We can say that `true` and `false` have the type `Bool`. But what is the type of\n",
    "a function? We could give them a type called `Function`, which we will spell `→`\n",
    "for brevity, but that's not very useful. Too many different functions would be\n",
    "lumped together in the same type. To be useful we need to know the type returned\n",
    "by the function and what type of argument it expects. We will spell that `T₁→T₂`\n",
    "where T₁ is the type of the argument and T₂ the type of the result. So we have\n",
    "the grammar rule:\n",
    "```\n",
    "T ::=\n",
    "      Bool\n",
    "      T → T\n",
    "```\n",
    "\n",
    "With `Bool` as our only base type that gives us an infinite family of function\n",
    "types:\n",
    " - `Bool→Bool`\n",
    " - `(Bool→Bool)→Bool`\n",
    " - `Bool→(Bool→Bool)`\n",
    " - `(Bool→Bool)→(Bool→Bool)`\n",
    " - etc\n",
    "\n",
    "`→` is right associative so `Bool→Bool→Bool` means `Bool→(Bool→Bool)`.\n",
    "\n",
    "## 9.2 The Typing Relation\n",
    "\n",
    "There are two approaches to assigning a type to a function (lambda abstraction)\n",
    "such as:\n",
    "\n",
    "```\n",
    "(λ.x if x then false else true)\n",
    "```\n",
    "\n",
    "The clever way is to analyse the body of the function and deduce that x has to\n",
    "be a Bool. That's covered in Chapter 22.\n",
    "\n",
    "The simpler way - which is the one used in this chapter - is just to annotate\n",
    "the function with the intended type:\n",
    "\n",
    "```\n",
    "(λ.x:Bool if x then false else true)\n",
    "```\n",
    "\n",
    "Chapter 8 introduced the binary typing relation `\":\"` which is used in\n",
    "expressions like `\"t : T\"` and can be read \"term `t` has type `T`\". The\n",
    "introduction of lambda calculus variables complicates things. The type of a term\n",
    "can depend on the types of variables used in that term. That changes the typing\n",
    "relation from a binary one to a ternary one `\"⊢ :\"` which is used in expressions\n",
    "like `\"Γ ⊢ t : T\"` and which can be read \"Given the typing context `Γ` (gamma)\n",
    "we can infer that the term `t` has type `T`\".\n",
    "\n",
    "The typing context `Γ` is sequence of (variable_name, type) pairs. However, it\n",
    "can also be thought of as an associative array (dict, map, hashtable) or a\n",
    "function from the name of a variable to its type. An empty context can be\n",
    "written ∅ or omitted as in `\"⊢ t : T\"`. Contexts can be extended using a comma\n",
    "so `\"Γ, x:T₁\"` is the typing context containing everything in Γ plus the\n",
    "variable x which is of type T₁. Contexts also support set membership so\n",
    " `\"x:T ∈ Γ\"` means \"The type assigned to `x` in `Γ` is `T`\".\n",
    "\n",
    "Given all that we're now in a position to define the typing rules for the\n",
    "simply typed lambda calculus as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "import re\n",
    "import inference\n",
    "from inference import  Rule, Syntax\n",
    "\n",
    "class SimplyTypedLambdaCalculus(inference.Rules):\n",
    "    ## SYNTAX\n",
    "    # This grammar differs slightly from what's in the book. I'm using a\n",
    "    # recursive decent parser so I need to avoid left-recursive productions.\n",
    "    # I do that in term and type by introducing termʹ and typeʹ and doing the\n",
    "    # usual transformations to remove the left-recursion.\n",
    "    rule = Syntax(\n",
    "        '{term} ⟶ {term}',\n",
    "        '{context} ⊢ {term} : {type}',\n",
    "        '{var} : {type} ∈ {context}',\n",
    "    )\n",
    "    term = Syntax(\n",
    "        '( {term} ) {termʹ}',\n",
    "        'true {termʹ}',\n",
    "        'false {termʹ}',\n",
    "        'if {term} then {term} else {term} {termʹ}',\n",
    "        '{var} {termʹ}',\n",
    "        'λ {var} : {type} . {term} {termʹ}',\n",
    "    )\n",
    "    termʹ = Syntax(\n",
    "        '{term} {termʹ}',\n",
    "        '',\n",
    "    )\n",
    "    var = Syntax(\n",
    "        re.compile(r\"[a-z]('+|\\b)\")\n",
    "    )\n",
    "    type = Syntax(\n",
    "        '( {type} ) {typeʹ}',\n",
    "        '{base_type} {typeʹ}',\n",
    "    )\n",
    "    typeʹ = Syntax(\n",
    "        '→ {type} {typeʹ}',\n",
    "        '',\n",
    "    )\n",
    "    base_type = Syntax(\n",
    "        'Bool',\n",
    "    )\n",
    "    context = Syntax(\n",
    "        '( {context} )',\n",
    "        '∅',\n",
    "        '{var} : {type} , {context}'\n",
    "    )\n",
    "\n",
    "    ## Lambda Calculus Typing\n",
    "    T_VAR = Rule('{Γ} ⊢ {x}:{T}', given=[\n",
    "        '{x}:{T} ∈ {Γ}'\n",
    "    ])\n",
    "    T_ABS = Rule('{Γ} ⊢ λ{x}:{T1}.{t2} : {T1}→{T2}', given=[\n",
    "        '{x}:{T1},{Γ} ⊢ {t2} : {T2}',\n",
    "    ])\n",
    "    T_APP = Rule('{Γ} ⊢ {t1} {t2} : {T12}', given=[\n",
    "        '{Γ} ⊢ {t1} : {T11}→{T12}',\n",
    "        '{Γ} ⊢ {t2} : {T11}',\n",
    "    ])\n",
    "\n",
    "    ## Boolean Typing\n",
    "    T_TRUE = Rule('{Γ} ⊢ true : Bool')\n",
    "    T_FALSE = Rule('{Γ} ⊢ false : Bool')\n",
    "    T_IF = Rule('{Γ} ⊢ if {t1} then {t2} else {t3} : {T}', given=[\n",
    "        '{Γ} ⊢ {t1} : Bool',\n",
    "        '{Γ} ⊢ {t2} : {T}',\n",
    "        '{Γ} ⊢ {t3} : {T}',\n",
    "    ])\n",
    "\n",
    "    ## List Membership\n",
    "    M_HEAD = Rule('{x}:{T} ∈ {x}:{T}, {Γ}')\n",
    "    M_TAIL = Rule('{x}:{T} ∈ {y}:{T1}, {Γ}', given=[\n",
    "        '{x}:{T} ∈ {Γ}',\n",
    "    ])\n",
    "\n",
    "    @classmethod\n",
    "    def infer_type(cls, expression, context='∅'):\n",
    "        goal = f'{context} ⊢ {expression} : {{__result__}}'\n",
    "        return cls.solve(goal)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "We're now in the position that we can infer the types of expressions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(Bool)"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SimplyTypedLambdaCalculus.infer_type('(λx:Bool.x) true')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "We can also draw the derivation trees of those proofs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<style>\n",
       "table.inference_proof {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "}\n",
       "\n",
       "table.inference_proof table {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "  margin: 0 auto !important;\n",
       "}\n",
       "\n",
       "table.inference_proof td {\n",
       "  border-width: 0 20px 0 0;\n",
       "  padding: 2px 0;\n",
       "  border-style: solid;\n",
       "  border-color: black rgba(0,0,0,0);\n",
       "  vertical-align: bottom;\n",
       "  text-align: center;\n",
       "  white-space: nowrap\n",
       "}\n",
       "\n",
       "table.inference_proof td:last-child {\n",
       "  border-width: 0 !important;\n",
       "}\n",
       "\n",
       "table.inference_proof tr {\n",
       "  border-width: 0;\n",
       "}\n",
       "\n",
       "table.inference_proof tr:last-child td {\n",
       "  border-width: 1px 0 0 0 !important;\n",
       "}\n",
       "</style>\n",
       "<table class=\"inference_proof\"><tr><td><table><tr><td><table><tr><td><table><tr><td colspan=1><span title=\"M_HEAD\">x : Bool ∈ (x : Bool , ∅)</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"T_VAR\">(x : Bool , ∅) ⊢ x : Bool</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"T_ABS\">∅ ⊢ (λ x : Bool . x) : (Bool → Bool)</span></td></tr></table></td><td><table><tr><td colspan=1><span title=\"T_TRUE\">∅ ⊢ true : Bool</span></td></tr></table></td></tr><tr><td colspan=2><span title=\"T_APP\">∅ ⊢ ((λ x : Bool . x) true) : Bool</span></td></tr></table>"
      ],
      "text/plain": [
       "---------------------------  <<M_HEAD>>                                         \n",
       "(x : Bool ∈ (x : Bool , ∅))                                                     \n",
       "---------------------------  <<T_VAR>>                                          \n",
       "((x : Bool , ∅) ⊢ x : Bool)                                                     \n",
       "--------------------------------------  <<T_ABS>>  -----------------  <<T_TRUE>>\n",
       "(∅ ⊢ (λ x : Bool . x) : (Bool → Bool))             (∅ ⊢ true : Bool)            \n",
       "--------------------------------------------------------------------  <<T_APP>>\n",
       "(∅ ⊢ ((λ x : Bool . x) true) : Bool)"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SimplyTypedLambdaCalculus.infer_type('(λx:Bool.x) true').proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "### Exercise 9.2.1\n",
    "\n",
    "The _pure_ simply typed lambda calculus is the simply typed lambda calculus\n",
    "without anything related to the boolean base type. That's a useful thing to have\n",
    "as a base to build on, but in itself it is _degenerate_, meaning that it has no\n",
    "well-typed terms at all. The reason for that is that types in the pure simply\n",
    "typed lambda calculus have the form:\n",
    "\n",
    "```\n",
    "T = T→T\n",
    "```\n",
    "\n",
    "But with no base types to \"prime the pumps\" that results in there being no types\n",
    "in the language at all."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "#### Exercise 9.2.2.1\n",
    "\n",
    "_Draw a derivation tree for `\"f:(Bool→Bool) ⊢ f (if false then true else false) : Bool\"`_"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<style>\n",
       "table.inference_proof {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "}\n",
       "\n",
       "table.inference_proof table {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "  margin: 0 auto !important;\n",
       "}\n",
       "\n",
       "table.inference_proof td {\n",
       "  border-width: 0 20px 0 0;\n",
       "  padding: 2px 0;\n",
       "  border-style: solid;\n",
       "  border-color: black rgba(0,0,0,0);\n",
       "  vertical-align: bottom;\n",
       "  text-align: center;\n",
       "  white-space: nowrap\n",
       "}\n",
       "\n",
       "table.inference_proof td:last-child {\n",
       "  border-width: 0 !important;\n",
       "}\n",
       "\n",
       "table.inference_proof tr {\n",
       "  border-width: 0;\n",
       "}\n",
       "\n",
       "table.inference_proof tr:last-child td {\n",
       "  border-width: 1px 0 0 0 !important;\n",
       "}\n",
       "</style>\n",
       "<table class=\"inference_proof\"><tr><td><table><tr><td><table><tr><td colspan=1><span title=\"M_HEAD\">f : (Bool → Bool) ∈ (f : (Bool → Bool) , ∅)</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"T_VAR\">(f : (Bool → Bool) , ∅) ⊢ f : (Bool → Bool)</span></td></tr></table></td><td><table><tr><td><table><tr><td colspan=1><span title=\"T_FALSE\">(f : (Bool → Bool) , ∅) ⊢ false : Bool</span></td></tr></table></td><td><table><tr><td colspan=1><span title=\"T_TRUE\">(f : (Bool → Bool) , ∅) ⊢ true : Bool</span></td></tr></table></td><td><table><tr><td colspan=1><span title=\"T_FALSE\">(f : (Bool → Bool) , ∅) ⊢ false : Bool</span></td></tr></table></td></tr><tr><td colspan=3><span title=\"T_IF\">(f : (Bool → Bool) , ∅) ⊢ (if false then true else false) : Bool</span></td></tr></table></td></tr><tr><td colspan=2><span title=\"T_APP\">(f : (Bool → Bool) , ∅) ⊢ (f (if false then true else false)) : Bool</span></td></tr></table>"
      ],
      "text/plain": [
       "---------------------------------------------  <<M_HEAD>>  ----------------------------------------  <<T_FALSE>>  ---------------------------------------  <<T_TRUE>>  ----------------------------------------  <<T_FALSE>>\n",
       "(f : (Bool → Bool) ∈ (f : (Bool → Bool) , ∅))              ((f : (Bool → Bool) , ∅) ⊢ false : Bool)               ((f : (Bool → Bool) , ∅) ⊢ true : Bool)              ((f : (Bool → Bool) , ∅) ⊢ false : Bool)             \n",
       "---------------------------------------------  <<T_VAR>>   ----------------------------------------------------------------------------------------------------------------------------------------------------  <<T_IF>>   \n",
       "((f : (Bool → Bool) , ∅) ⊢ f : (Bool → Bool))              ((f : (Bool → Bool) , ∅) ⊢ (if false then true else false) : Bool)                                                                                               \n",
       "---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------  <<T_APP>>\n",
       "((f : (Bool → Bool) , ∅) ⊢ (f (if false then true else false)) : Bool)"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expression = 'f (if false then true else false)'\n",
    "context = 'f:(Bool→Bool), ∅'\n",
    "T = SimplyTypedLambdaCalculus.infer_type(expression, context=context)\n",
    "assert T == ('Bool',)\n",
    "T.proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "#### Exercise 9.2.2.2\n",
    "\n",
    "_Draw a derivation tree for `\"f:(Bool→Bool) ⊢ λx:Bool. f(if false then true else false) : Bool→Bool\"`_"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<style>\n",
       "table.inference_proof {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "}\n",
       "\n",
       "table.inference_proof table {\n",
       "  border: none;\n",
       "  border-collapse: collapse;\n",
       "  margin: 0 auto !important;\n",
       "}\n",
       "\n",
       "table.inference_proof td {\n",
       "  border-width: 0 20px 0 0;\n",
       "  padding: 2px 0;\n",
       "  border-style: solid;\n",
       "  border-color: black rgba(0,0,0,0);\n",
       "  vertical-align: bottom;\n",
       "  text-align: center;\n",
       "  white-space: nowrap\n",
       "}\n",
       "\n",
       "table.inference_proof td:last-child {\n",
       "  border-width: 0 !important;\n",
       "}\n",
       "\n",
       "table.inference_proof tr {\n",
       "  border-width: 0;\n",
       "}\n",
       "\n",
       "table.inference_proof tr:last-child td {\n",
       "  border-width: 1px 0 0 0 !important;\n",
       "}\n",
       "</style>\n",
       "<table class=\"inference_proof\"><tr><td><table><tr><td><table><tr><td><table><tr><td><table><tr><td colspan=1><span title=\"M_HEAD\">f : (Bool → Bool) ∈ (f : (Bool → Bool) , ∅)</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"M_TAIL\">f : (Bool → Bool) ∈ (x : Bool , (f : (Bool → Bool) , ∅))</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"T_VAR\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ f : (Bool → Bool)</span></td></tr></table></td><td><table><tr><td><table><tr><td colspan=1><span title=\"T_FALSE\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ false : Bool</span></td></tr></table></td><td><table><tr><td colspan=1><span title=\"T_TRUE\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ true : Bool</span></td></tr></table></td><td><table><tr><td colspan=1><span title=\"T_FALSE\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ false : Bool</span></td></tr></table></td></tr><tr><td colspan=3><span title=\"T_IF\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ (if false then true else false) : Bool</span></td></tr></table></td></tr><tr><td colspan=2><span title=\"T_APP\">(x : Bool , (f : (Bool → Bool) , ∅)) ⊢ (f (if false then true else false)) : Bool</span></td></tr></table></td></tr><tr><td colspan=1><span title=\"T_ABS\">(f : (Bool → Bool) , ∅) ⊢ (λ x : Bool . (f (if false then true else false))) : (Bool → Bool)</span></td></tr></table>"
      ],
      "text/plain": [
       "---------------------------------------------  <<M_HEAD>>                                                                                                                                                                                                                       \n",
       "(f : (Bool → Bool) ∈ (f : (Bool → Bool) , ∅))                                                                                                                                                                                                                                   \n",
       "----------------------------------------------------------  <<M_TAIL>>  -----------------------------------------------------  <<T_FALSE>>  ----------------------------------------------------  <<T_TRUE>>  -----------------------------------------------------  <<T_FALSE>>\n",
       "(f : (Bool → Bool) ∈ (x : Bool , (f : (Bool → Bool) , ∅)))              ((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ false : Bool)               ((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ true : Bool)              ((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ false : Bool)             \n",
       "----------------------------------------------------------  <<T_VAR>>   -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------  <<T_IF>>   \n",
       "((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ f : (Bool → Bool))              ((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ (if false then true else false) : Bool)                                                                                                                         \n",
       "-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------  <<T_APP>>  \n",
       "((x : Bool , (f : (Bool → Bool) , ∅)) ⊢ (f (if false then true else false)) : Bool)                                                                                                                                                                                             \n",
       "-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------  <<T_ABS>>\n",
       "((f : (Bool → Bool) , ∅) ⊢ (λ x : Bool . (f (if false then true else false))) : (Bool → Bool))"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expression = 'λx:Bool. f(if false then true else false)'\n",
    "context = 'f:(Bool→Bool), ∅'\n",
    "T = SimplyTypedLambdaCalculus.infer_type(expression, context=context)\n",
    "assert T == ('Bool','→', 'Bool')\n",
    "T.proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "source": [
    "### Exercise 9.2.3\n",
    "\n",
    "_Find a context Γ under which the term `\"f x y\"` has the type Bool._\n",
    "\n",
    "It would be lovely if we could show this by running:\n",
    "```\n",
    "SimplyTypedLambdaCalculus.solve('{context} ⊢ (f x y) : Bool')\n",
    "```\n",
    "and seeing what pops out. Unfortunately that doesn't work. Turns out that a few\n",
    "dozen lines of hastily written code for drawing derivation trees !=  Prolog.\n",
    "Who knew?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "source": [
    "## 9.3 Properties of Typing\n",
    "\n",
    "This is where TaPL proves that the Simply Typed Lambda Calculus is Type Safe.\n",
    "The proof follows the same lines as chapter 8. i.e.\n",
    "\n",
    "**Safety = Progress + Preservation**.\n",
    "\n",
    " - **Progress**: If `\"⊢ t : T\"` then either `t` is a value or there is some `tʹ`\n",
    "   where `t ⟶ tʹ`\n",
    " - **Preservation**: If `\"Γ ⊢ t : T\"` and `t ⟶ tʹ` then `\"Γ ⊢ tʹ : T\"`\n",
    "\n",
    "Or in english:\n",
    "\n",
    " - **Progress**: Any well-typed term is either a value (i.e. it has finished\n",
    "   evaluating) or it can be evaluated another step. \n",
    " - **Preservation**: If you can evaluate a well-typed term, the result will be\n",
    "   another well-typed term with the same type.\n",
    "\n",
    "I'm not going to reproduce the proofs here. They are can mostly be summarised as\n",
    "\"sprinkle some induction on it\". For more details, go read the book."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "source": [
    "### Exercise 9.3.2\n",
    "\n",
    "_Can we construct a `Γ` and `T` such that `\"Γ ⊢ x x : T\"`?_\n",
    "\n",
    "No, not with our current type system. The `T-ABS` rule is the one which would\n",
    "apply to that term. It says that the first `x` has type `T₁→T₂` and the second\n",
    "`x` has type `T₁`. But since both `x`s are the same its need to have both of\n",
    "those types at the same time. Theres no way to unify `T₁→T₂` with `T₁` to make\n",
    "that true."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "### Exercise 9.3.10\n",
    "\n",
    "_Does \"subject expansion\" hold for the functional part of the calculus?_\n",
    "\n",
    "That is, Do `\"t ⟶ tʹ\"` and `\"Γ ⊢ tʹ : T\"` together imply `\"Γ ⊢ t : T\"` for\n",
    "terms t which don't include conditional expressions?\n",
    "\n",
    "No. There exist untyped terms which evaluate to typed terms. For example.\n",
    "```\n",
    "(λx:Bool. λy.Bool. y)(true true)\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx:Bool. λy:Bool. y)(true true) is not well-typed\n",
      "(λx:Bool. λy:Bool. y)(true true) evaluates to (λy:Bool. y)\n",
      "The type of (λy:Bool. y) is Bool → Bool\n"
     ]
    }
   ],
   "source": [
    "expression1 = '(λx:Bool. λy:Bool. y)(true true)'\n",
    "try:\n",
    "    T = SimplyTypedLambdaCalculus.infer_type(expression1)\n",
    "    print(f'The type of {expression1} is {T}')\n",
    "except inference.NoProofFoundError:\n",
    "    print(f'{expression1} is not well-typed')\n",
    "\n",
    "expression2 = '(λy:Bool. y)'\n",
    "\n",
    "print(f'{expression1} evaluates to {expression2}')\n",
    "try:\n",
    "    SimplyTypedLambdaCalculus.infer_type(expression2)\n",
    "    print(f'The type of {expression2} is {T}')\n",
    "except inference.NoProofFoundError:\n",
    "    print(f'{expression2} is not well-typed')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "## 9.4 The Curry Howard Correspondence \n",
    "\n",
    "We skipped this because time was short and it seemed like an aside.\n",
    "\n",
    "There were a couple of related talks recommended on slack before the meeting:\n",
    "\n",
    "[\"Propositions as Types\" - Philip Wadler](https://www.youtube.com/watch?v=IOiZatlZtGU)\n",
    "\n",
    "[\"The Hitchhiker's Guide to the Curry-Howard Correspondence\" - Chris Ford](https://vimeo.com/100976695)\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "## 9.5 Erasure and Typability\n",
    "\n",
    "Even though we can define evaluation rules on typed terms, the type annotations\n",
    "play no role in the evaluation at runtime. They are carried along but are\n",
    "redundant.\n",
    "\n",
    "**Erasure** is a function which maps simply typed terms to the equivalent terms\n",
    "in the untyped lambda calculus.\n",
    "\n",
    "It can be proved that the following two approaches to evaluation are exactly\n",
    "equivalent:\n",
    " - evaluating a typed term according to the typed evaluation rules and then\n",
    "   erasing types from the result.\n",
    " - erasing types from a typed term and then evaluating that using the untyped\n",
    "   evaluation rules.\n",
    "\n",
    "**Typability** is in some ways the opposite of erasure. An untyped term `m` is\n",
    "said to be typable is there is some typed term `t`, type `T` and context `Γ`\n",
    "such that\n",
    "\n",
    "```\n",
    "Γ ⊢ t : T and erase(t) = m\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "## 9.6 Curry-Style vs. Church-Style\n",
    "\n",
    "There are two ways of discussing the semantics of a typed language:\n",
    "\n",
    " - Curry-style: Start by defining terms, then the semantics of terms, then add a\n",
    "   type system which rejects some terms which have undesirable behaviour.\n",
    " - Church-style: Start by defining which terms, then the type-system. Finally\n",
    "   assign semantic meaning only to well-typed terms.\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}