{
"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",
" | | | | | | | ∅ ⊢ (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 |
| | |
∅ ⊢ (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",
" | 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
}