{ "cells": [ { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "# TaPL Chapter 10 - An ML Implementation of Simple Types\n", "\n", "Chapter 10 of [TaPL](https://www.cis.upenn.edu/~bcpierce/tapl/) is all about \n", "implementing the Simply Typed Lambda Calculus described in [chapter\n", "9](09 - Simply Typed Lambda Calculus.ipynb).\n", "\n", "My Python implementation based on the\n", "[`inference`](https://github.com/richardcooper/inference) library can be found\n", "[here](tapl/chapter_09_simply_typed_lambda_calculus.py). _(Warning: Mojibake if\n", "viewed via jupyter or nbview. Github renders it correctly.)_" ] }, { "cell_type": "code", "execution_count": 1, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [], "source": [ "from tapl import SimplyTypedLambdaCalculus" ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "## QuickCheck Terms\n", "\n", "For this chapter, Leo wrote a [Haskell QuickCheck\n", "generator](https://github.com/leocassarani/types-and-programming-languages/blob/master/09-simply-typed-lambda-calculus/Generator.hs)\n", "which creates random terms with a given type.\n", "\n", "Here is a quick test of my code against some of those terms which he shared on\n", "Slack." ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "### 1" ] }, { "cell_type": "code", "execution_count": 2, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "
(s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) , ∅) ⊢ false : Bool
∅ ⊢ (λ s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) . false) : ((((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) → Bool)
v : ((Bool → Bool) → (Bool → Bool)) ∈ (v : ((Bool → Bool) → (Bool → Bool)) , ∅)
v : ((Bool → Bool) → (Bool → Bool)) ∈ (j : Bool , (v : ((Bool → Bool) → (Bool → Bool)) , ∅))
(j : Bool , (v : ((Bool → Bool) → (Bool → Bool)) , ∅)) ⊢ v : ((Bool → Bool) → (Bool → Bool))
(v : ((Bool → Bool) → (Bool → Bool)) , ∅) ⊢ (λ j : Bool . v) : (Bool → ((Bool → Bool) → (Bool → Bool)))
∅ ⊢ (λ v : ((Bool → Bool) → (Bool → Bool)) . (λ j : Bool . v)) : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool))))
∅ ⊢ ((λ s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) . false) (λ v : ((Bool → Bool) → (Bool → Bool)) . (λ j : Bool . v))) : Bool
" ], "text/plain": [ " --------------------------------------------------------------------------------- <> \n", " (v : ((Bool → Bool) → (Bool → Bool)) ∈ (v : ((Bool → Bool) → (Bool → Bool)) , ∅)) \n", " ---------------------------------------------------------------------------------------------- <> \n", " (v : ((Bool → Bool) → (Bool → Bool)) ∈ (j : Bool , (v : ((Bool → Bool) → (Bool → Bool)) , ∅))) \n", " ---------------------------------------------------------------------------------------------- <> \n", " ((j : Bool , (v : ((Bool → Bool) → (Bool → Bool)) , ∅)) ⊢ v : ((Bool → Bool) → (Bool → Bool))) \n", "------------------------------------------------------------------------------------------------------- <> --------------------------------------------------------------------------------------------------------- <> \n", "((s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) , ∅) ⊢ false : Bool) ((v : ((Bool → Bool) → (Bool → Bool)) , ∅) ⊢ (λ j : Bool . v) : (Bool → ((Bool → Bool) → (Bool → Bool)))) \n", "------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ <> ----------------------------------------------------------------------------------------------------------------------------------------------- <>\n", "(∅ ⊢ (λ s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) . false) : ((((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) → Bool)) (∅ ⊢ (λ v : ((Bool → Bool) → (Bool → Bool)) . (λ j : Bool . v)) : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool))))) \n", "------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ <>\n", "(∅ ⊢ ((λ s : (((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))) . false) (λ v : ((Bool → Bool) → (Bool → Bool)) . (λ j : Bool . v))) : Bool)" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "random_term_1 = \"\"\"\n", " (\n", " (λs:(((Bool → Bool) → (Bool → Bool)) → (Bool → ((Bool → Bool) → (Bool → Bool)))). false)\n", " (λv:((Bool → Bool) → (Bool → Bool)). (λj:Bool. v))\n", " )\n", "\"\"\"\n", "type_1 = SimplyTypedLambdaCalculus.infer_type(random_term_1)\n", "assert type_1 == ('Bool',)\n", "type_1.proof" ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "### 2" ] }, { "cell_type": "code", "execution_count": 3, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "
∅ ⊢ true : Bool
∅ ⊢ false : Bool
∅ ⊢ false : Bool
∅ ⊢ true : Bool
∅ ⊢ false : Bool
∅ ⊢ false : Bool
∅ ⊢ false : Bool
∅ ⊢ (if false then false else false) : Bool
∅ ⊢ (if false then true else (if false then false else false)) : Bool
∅ ⊢ (if true then false else (if false then true else (if false then false else false))) : Bool
∅ ⊢ true : Bool
∅ ⊢ true : Bool
∅ ⊢ (if (if true then false else (if false then true else (if false then false else false))) then true else true) : Bool
" ], "text/plain": [ " ------------------ <> ------------------ <> ------------------ <> \n", " (∅ ⊢ false : Bool) (∅ ⊢ false : Bool) (∅ ⊢ false : Bool) \n", " ------------------ <> ----------------- <> ------------------------------------------------------------------------------------ <> \n", " (∅ ⊢ false : Bool) (∅ ⊢ true : Bool) (∅ ⊢ (if false then false else false) : Bool) \n", "----------------- <> ------------------ <> ---------------------------------------------------------------------------------------------------------------------------------------------------- <> \n", "(∅ ⊢ true : Bool) (∅ ⊢ false : Bool) (∅ ⊢ (if false then true else (if false then false else false)) : Bool) \n", "-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <> ----------------- <> ----------------- <>\n", "(∅ ⊢ (if true then false else (if false then true else (if false then false else false))) : Bool) (∅ ⊢ true : Bool) (∅ ⊢ true : Bool) \n", "----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <>\n", "(∅ ⊢ (if (if true then false else (if false then true else (if false then false else false))) then true else true) : Bool)" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "random_term_2 = \"\"\"\n", " (if (if true then false else (if false then true else (if false then false else false))) then true else true)\n", "\"\"\"\n", "type_2 = SimplyTypedLambdaCalculus.infer_type(random_term_2)\n", "assert type_2 == ('Bool',)\n", "type_2.proof" ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "### 3" ] }, { "cell_type": "code", "execution_count": 4, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "
∅ ⊢ false : Bool
t : Bool ∈ (t : Bool , ∅)
t : Bool ∈ (n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅))
(n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅)) ⊢ t : Bool
(t : Bool , ∅) ⊢ (λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) : ((((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) → Bool)
t : Bool ∈ (t : Bool , ∅)
t : Bool ∈ (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))
t : Bool ∈ (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))
t : Bool ∈ (j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))))
(j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))) ⊢ t : Bool
(y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))) ⊢ (λ j : (Bool → Bool) . t) : ((Bool → Bool) → Bool)
(t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)) ⊢ (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)) : ((Bool → Bool) → ((Bool → Bool) → Bool))
(t : Bool , ∅) ⊢ (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))) : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool)))
(t : Bool , ∅) ⊢ ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)))) : Bool
∅ ⊢ (λ t : Bool . ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))))) : (Bool → Bool)
c : Bool ∈ (c : Bool , ∅)
(c : Bool , ∅) ⊢ c : Bool
∅ ⊢ (λ c : Bool . c) : (Bool → Bool)
∅ ⊢ (if false then (λ t : Bool . ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))))) else (λ c : Bool . c)) : (Bool → Bool)
" ], "text/plain": [ " --------------------------- <> \n", " (t : Bool ∈ (t : Bool , ∅)) \n", " -------------------------------------------------------------------- <> \n", " (t : Bool ∈ (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))) \n", " ------------------------------------------------------------------------------------------ <> \n", " (t : Bool ∈ (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))) \n", " ---------------------------------------------------------------------------------------------------------------- <> \n", " (t : Bool ∈ (j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))))) \n", " --------------------------- <> ---------------------------------------------------------------------------------------------------------------- <> \n", " (t : Bool ∈ (t : Bool , ∅)) ((j : (Bool → Bool) , (y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)))) ⊢ t : Bool) \n", " ---------------------------------------------------------------------------------------------------------------- <> ------------------------------------------------------------------------------------------------------------------------------------ <> \n", " (t : Bool ∈ (n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅))) ((y : (Bool → Bool) , (t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅))) ⊢ (λ j : (Bool → Bool) . t) : ((Bool → Bool) → Bool)) \n", " ---------------------------------------------------------------------------------------------------------------- <> -------------------------------------------------------------------------------------------------------------------------------------------------------- <> \n", " ((n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) , (t : Bool , ∅)) ⊢ t : Bool) ((t' : ((Bool → Bool) → (Bool → Bool)) , (t : Bool , ∅)) ⊢ (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)) : ((Bool → Bool) → ((Bool → Bool) → Bool))) \n", " --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <> ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <> --------------------------- <> \n", " ((t : Bool , ∅) ⊢ (λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) : ((((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) → Bool)) ((t : Bool , ∅) ⊢ (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))) : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool)))) (c : Bool ∈ (c : Bool , ∅)) \n", " -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <> --------------------------- <> \n", " ((t : Bool , ∅) ⊢ ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t)))) : Bool) ((c : Bool , ∅) ⊢ c : Bool) \n", "------------------ <> -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <> -------------------------------------- <>\n", "(∅ ⊢ false : Bool) (∅ ⊢ (λ t : Bool . ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))))) : (Bool → Bool)) (∅ ⊢ (λ c : Bool . c) : (Bool → Bool)) \n", "-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- <>\n", "(∅ ⊢ (if false then (λ t : Bool . ((λ n : (((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))) . t) (λ t' : ((Bool → Bool) → (Bool → Bool)) . (λ y : (Bool → Bool) . (λ j : (Bool → Bool) . t))))) else (λ c : Bool . c)) : (Bool → Bool))" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "random_term_3 = \"\"\"\n", " (\n", " if false then \n", " (λt:Bool. (\n", " (λn:(((Bool → Bool) → (Bool → Bool)) → ((Bool → Bool) → ((Bool → Bool) → Bool))). t)\n", " (λt':((Bool → Bool) → (Bool → Bool)). (λy:(Bool → Bool). (λj:(Bool → Bool). t)))\n", " ))\n", " else\n", " (λc:Bool. c)\n", " )\n", "\"\"\"\n", "type_3 = SimplyTypedLambdaCalculus.infer_type(random_term_3)\n", "assert type_3 == ('Bool','→','Bool')\n", "type_3.proof" ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "### 4\n", "\n", "The forth term is over 18K characters long. So we'll load it from a file." ] }, { "cell_type": "code", "execution_count": 5, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Characters in term: 18048\n", "CPU times: user 32.1 s, sys: 78.7 ms, total: 32.2 s\n", "Wall time: 32.2 s\n" ] } ], "source": [ "%%time\n", "random_term_4 = open(\"data/large_lambda_term.txt\").read()\n", "type_4 = SimplyTypedLambdaCalculus.infer_type(random_term_4)\n", "assert type_4 == ('Bool','→','Bool')\n", "print('Characters in term:', len(random_term_4))" ] }, { "cell_type": "markdown", "metadata": { "deletable": true, "editable": true }, "source": [ "Rendering the proof would be silly given its size. Lets looks at some stats instead." ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "data": { "text/plain": [ "'Proof size = 1338, depth = 50, width = 328'" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f'Proof size = {type_4.proof.size}, depth = {type_4.proof.depth}, width = {type_4.proof.width}'" ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "collapsed": false, "deletable": true, "editable": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "M_HEAD 143\n", "M_TAIL 295\n", "T_ABS 374\n", "T_APP 69\n", "T_FALSE 82\n", "T_IF 129\n", "T_TRUE 103\n", "T_VAR 143\n" ] } ], "source": [ "from collections import defaultdict\n", "def count_rules_used_in_proof(proof):\n", " result = defaultdict(int)\n", " result[proof.rule.name] = 1\n", " for p in proof.premises:\n", " for (name, count) in count_rules_used_in_proof(p).items():\n", " result[name] += count\n", " return result\n", "\n", "for name, count in sorted(count_rules_used_in_proof(type_4.proof).items()):\n", " print(f'{name:8} {count}')" ] } ], "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 }