# test ();;
[Infinite loop, need to control c out]
We can use functions that take arguments of type unit to control
execution. In Scheme parlance, functions on the unit type are called
*thunks* (which I've always assumed was a blend of "think" and "chunk").
Curry-Howard, take 1
--------------------
We will return to the Curry-Howard correspondence a number of times
during this course. It expresses a deep connection between logic,
types, and computation. Today we'll discuss how the simply-typed
lambda calculus corresponds to intuitionistic logic. This naturally
give rise to the question of what sort of computation classical logic
corresponds to---as we'll see later, the answer involves continuations.
So at this point we have the simply-typed lambda calculus: a set of
ground types, a set of functional types, and some typing rules, given
roughly as follows:
If a variable `x` has type σ and term `M` has type τ, then
the abstract `\xM` has type σ `-->` τ.
If a term `M` has type σ `-->` τ, and a term `N` has type
σ, then the application `MN` has type τ.
These rules are clearly obverses of one another: the functional types
that abstract builds up are taken apart by application.
The next step in making sense out of the Curry-Howard corresponence is
to present a logic. It will be a part of intuitionistic logic. We'll
start with the implicational fragment (that is, the part of
intuitionistic logic that only involves axioms and implications):
Axiom: ---------
A |- A
Structural Rules:
Γ, A, B, Δ |- C
Exchange: ---------------------------
Γ, B, A, Δ |- C
Γ, A, A |- B
Contraction: -------------------
Γ, A |- B
Γ |- B
Weakening: -----------------
Γ, A |- B
Logical Rules:
Γ, A |- B
--> I: -------------------
Γ |- A --> B
Γ |- A --> B Γ |- A
--> E: -----------------------------------
Γ |- B

`A`, `B`, etc. are variables over formulas.
Γ, Δ, etc. are variables over (possibly empty) sequences
of formulas. Γ `|- A` is a sequent, and is interpreted as
claiming that if each of the formulas in Γ is true, then `A`
must also be true.
This logic allows derivations of theorems like the following:
------- Id
A |- A
---------- Weak
A, B |- A
------------- --> I
A |- B --> A
----------------- --> I
|- A --> B --> A

Should remind you of simple types. (What was `A --> B --> A` the type
of again?)
The easy way to grasp the Curry-Howard correspondence is to *label*
the proofs. Since we wish to establish a correspondence between this
logic and the lambda calculus, the labels will all be terms from the
simply-typed lambda calculus. Here are the labeling rules:
Axiom: -----------
x:A |- x:A
Structural Rules:
Γ, x:A, y:B, Δ |- R:C
Exchange: -------------------------------
Γ, y:B, x:A, Δ |- R:C
Γ, x:A, x:A |- R:B
Contraction: --------------------------
Γ, x:A |- R:B
Γ |- R:B
Weakening: ---------------------
Γ, x:A |- R:B [x chosen fresh]
Logical Rules:
Γ, x:A |- R:B
--> I: -------------------------
Γ |- \xM:A --> B
Γ |- f:(A --> B) Γ |- x:A
--> E: -------------------------------------
Γ |- (fx):B

In these labeling rules, if a sequence Γ in a premise contains
labeled formulas, those labels remain unchanged in the conclusion.
What is means for a variable `x` to be chosen *fresh* is that
`x` must be distinct from any other variable in any of the labels
used in the proof.
Using these labeling rules, we can label the proof
just given:
------------ Id
x:A |- x:A
---------------- Weak
x:A, y:B |- x:A
------------------------- --> I
x:A |- (\y.x):(B --> A)
---------------------------- --> I
|- (\x y. x):A --> B --> A

We have derived the *K* combinator, and typed it at the same time!
Need a proof that involves application, and a proof with cut that will
show beta reduction, so "normal" proof.
[To do: add pairs and destructors; unit and negation...]
Excercise: construct a proof whose labeling is the combinator S.