Skip to content

Commit

Permalink
Update textbook
Browse files Browse the repository at this point in the history
  • Loading branch information
clarksmr committed Aug 17, 2024
1 parent cb6adfb commit 4f97500
Show file tree
Hide file tree
Showing 158 changed files with 3,867 additions and 13,071 deletions.
124 changes: 21 additions & 103 deletions _sources/chapters/adv/curry-howard.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "markdown",
"id": "755efc53",
"id": "b1e40fc1",
"metadata": {},
"source": [
"# The Curry-Howard Correspondence\n",
Expand Down Expand Up @@ -59,28 +59,17 @@
},
{
"cell_type": "code",
"execution_count": 1,
"id": "c20a27bb",
"execution_count": null,
"id": "fca2564e",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type empty = |\n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"outputs": [],
"source": [
"type empty = |"
]
},
{
"cell_type": "markdown",
"id": "8928e524",
"id": "48b65255",
"metadata": {},
"source": [
"We could have called that type anything we wanted instead of `empty`; the\n",
Expand All @@ -98,41 +87,10 @@
},
{
"cell_type": "code",
"execution_count": 2,
"id": "12fc0f06",
"execution_count": null,
"id": "78f24a7c",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val pair : 'a -> 'b -> 'a * 'b = <fun>\n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val fst : 'a * 'b -> 'a = <fun>\n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val snd : 'a * 'b -> 'b = <fun>\n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"outputs": [],
"source": [
"let pair x y = (x, y)\n",
"let fst (x, y) = x\n",
Expand All @@ -141,7 +99,7 @@
},
{
"cell_type": "markdown",
"id": "99fd003c",
"id": "168b30a5",
"metadata": {},
"source": [
"We could think of `pair` as a function that takes in evidence for `'a` and\n",
Expand Down Expand Up @@ -289,28 +247,17 @@
},
{
"cell_type": "code",
"execution_count": 3,
"id": "b1535f8c",
"execution_count": null,
"id": "f7f24442",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type ('a, 'b) disj = Left of 'a | Right of 'b\n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"outputs": [],
"source": [
"type ('a, 'b) disj = Left of 'a | Right of 'b"
]
},
{
"cell_type": "markdown",
"id": "f00d9469",
"id": "e2990bd8",
"metadata": {},
"source": [
"A value `v` of that type is either `Left a`, where `a : 'a`; or `Right b`, where\n",
Expand Down Expand Up @@ -343,28 +290,17 @@
},
{
"cell_type": "code",
"execution_count": 4,
"id": "5d0a6c6c",
"execution_count": null,
"id": "bd857ed2",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val loop : 'a -> 'b = <fun>\n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"outputs": [],
"source": [
"let rec loop x = loop x"
]
},
{
"cell_type": "markdown",
"id": "f92b32ea",
"id": "bc81402b",
"metadata": {},
"source": [
"Now if you enter this code in utop you will get no response:\n",
Expand All @@ -382,30 +318,21 @@
},
{
"cell_type": "code",
"execution_count": 5,
"id": "ae895059",
"execution_count": null,
"id": "6ef93d5a",
"metadata": {
"tags": [
"raises-exception"
]
},
"outputs": [
{
"ename": "error",
"evalue": "runtime_error",
"output_type": "error",
"traceback": [
"\u001b[31mException: Failure \"\".\nRaised at Stdlib.failwith in file \"stdlib.ml\", line 29, characters 17-33\nCalled from unknown location\nCalled from Stdlib__Fun.protect in file \"fun.ml\", line 33, characters 8-15\nRe-raised at Stdlib__Fun.protect in file \"fun.ml\", line 38, characters 6-52\nCalled from Topeval.load_lambda in file \"toplevel/byte/topeval.ml\", line 89, characters 4-150\n\u001b[0m"
]
}
],
"outputs": [],
"source": [
"let e : empty = failwith \"\""
]
},
{
"cell_type": "markdown",
"id": "9ff26b31",
"id": "ab4e8281",
"metadata": {},
"source": [
"Again, the expression type checks, but it never produces an actual value of type\n",
Expand Down Expand Up @@ -775,15 +702,6 @@
"language": "OCaml",
"name": "ocaml-jupyter"
},
"language_info": {
"codemirror_mode": "text/x-ocaml",
"file_extension": ".ml",
"mimetype": "text/x-ocaml",
"name": "OCaml",
"nbconverter_exporter": null,
"pygments_lexer": "OCaml",
"version": "4.14.0"
},
"source_map": [
14,
67,
Expand Down
11 changes: 1 addition & 10 deletions _sources/chapters/basics/debugging.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "markdown",
"id": "0426b7ba",
"id": "731372f5",
"metadata": {},
"source": [
"# Debugging\n",
Expand Down Expand Up @@ -251,15 +251,6 @@
"language": "OCaml",
"name": "ocaml-jupyter"
},
"language_info": {
"codemirror_mode": "text/x-ocaml",
"file_extension": ".ml",
"mimetype": "text/x-ocaml",
"name": "OCaml",
"nbconverter_exporter": null,
"pygments_lexer": "OCaml",
"version": "4.14.0"
},
"source_map": [
14
]
Expand Down
Loading

0 comments on commit 4f97500

Please sign in to comment.