What needs to have a type?

Values
Reduxes

We will define a type T->T where the first T is the domain and the second T is the range. The -> acts as a type constructor.

T1->T2 says if given a type T1 a function will return a type T2

T ::= T->T

The problem with this is that there are no base cases. So we need base types. Base types are concrete types.

Here we add Bool

T ::= T->T | Bool

We can now type a lambda as following:

$(λ x : B o o l . x) : B o o l \to B o o l$

It can also be applied for App:

$(((λ x : B o o l . x) : B o o l \to B o o l) t r u e) : B o o l$

Type Ascription

In general it is impossible to figure out a $λ$ 's input type from its output type. Function application "removes" information.

Type Rules

\frac{t_{1} : T_{1} \to T_{2} t_{2} : T_{1}}{(t_{1} t_{2}) : T_{2}} TApp

Note

The context of a term is a list of all the bound variables and their types.

A type rule for variables is as follows

\frac{(x \to T) \in Γ}{Γ ⊢ x : T} TVar

Syntax

$t ::= λ x : T . t | (t t) | x$
$v ::= λ x : T . t$
$T ::= T \to T$

Type Safety

Proof of Progress

if $Γ ⊢ t : T$ then $t$ is a value or $t \to t^{'}, \exists t^{'}$

Proof.

$x$ - Assume combinators (no free variables), thus $x$ is not a term to consider as it it not bound and therefor not a combinator.
$Γ ⊢ λ x : T . t \to R$ - Lambdas are values and the theorem holds true.
$Γ ⊢ (t_{1} t_{2}) : T$ - Assume progress for $t_{1}$ and $t_{2}$
- Case 1: $t_{1}$ is not a value because it is not lambda. Then $t_{1} \to t_{2}^{'}$ (inductive hypothesis) and EApp1 applies.
- Case 2: $t_{1}$ is not a value because it is not lambda. Then $t_{1} \to t_{2}^{'}$ (inductive hypothesis) and EApp2 applies.
- Case 3: $t_{1}$ and $t_{2}$ are both values, then BetaReduction applies.

Proof of Preservation

This involves the use of a few other lemmas.

Permutation Lemma

If $Γ ⊢ t : t$ and $Δ$ is a permutation of $Γ$ , then $d e l t a ⊢ t : T$ .

This says that the ordering of $Γ$ doesn't matter. This is not always true.

In order to prevent this we prevent shadowing meaning a variable can't be used more than once. Languages like Haskell get around this by mangling variables and renaming them to be unique, this is called alpha reduction.

Proof.

By induction on terms:

Case 1: $x$

$Γ ⊢ x : T$ implies $(x \to T) \in Γ$ by type inversion. By definition of permutation $(x \to T) \in Δ$ so $Δ ⊢ x : T$ by TVar.

Case 2: $(λ x : T_{1} . t_{2})$

$Γ ⊢ (λ x : T_{1} . t_{2}) : T_{1} \to T_{2}$ by type inversion. The induction hypothesis says permutation holds for $(x \to T_{1})$ , $Δ ⊢ t_{2} : T_{2}$ . Thus $Δ ⊢ (λ x : T_{1} . t 2) : T_{1} \to T_{2}$ holds by TLambda

Case 3: $(t_{1} t_{2})$

$Γ ⊢ (t_{1} t_{2}) : T_{2}$ implies there exists some $Γ ⊢ t_{1} : T_{1} \to T_{2}$ and $Γ ⊢ t_{2} : T_{1}$ by type inversion. Induction hypothesis says permutation holds $Δ ⊢ t_{1} : T_{1} \to T_{2}$ . Thus $Δ ⊢ (t_{1} t_{2}) : T_{2}$ holds by TApp.

Weakening Lemma

If $Γ ⊢ t : T$ and $x \notin d o m (T)$ then $(x \to S), Γ ⊢ t : T$

This essentially says typing is invariant if unique variables are added to the context.

Preservation of Types Under Substitution

If $(x \to S), Γ ⊢ t : T$ and $Γ ⊢ s : S$ then $Γ ⊢ . . .$

This essentially says typing is invariant with respect to replacing a well-typed variable with a well-typed term of the same type.

Proof.

TVar
- t = z=>z:T
- $(z \to T) \in (x \to S), Γ$ by type inversion
- Case 1 $z = x$ : $[x \to s] z = s$ Since we know z:T and x:S then T=S and s:T
- Case 2 $x \neq z$ : $[x \to s] z = z$ and s:T
TLambda
- t = λy: T2.t1
- T = T2 -> T1
- $(y \to T_{2}) (x \to S), Γ ⊢ t_{1} : T_{1}$
- $(y \to T_{2}) a, Γ ⊢ [x \to s] t_{1} : T_{1}$ by S=T2
- $Γ ⊢ [x \to s] t_{1} : T_{1}$ by induction hypothesis

The Proof

uhhh...

Simple Extensions

There are three ways to enrich a language:

Extension - Add new syntax, new values, new types and associated inference rules
Derived Forms - Add new syntax and new types defined in terms of existing constructs
Libraries - Add new functionality by using the language to define new resuable constructs

Prefer 2 over 3

Base Types

Extend the definition of $T$ to include arbitrary uninterpretable base types.

$T ::= . . . | A | T \to T$

Unit and ;

Unit is a type with a single value.

Syntax:

$t ::= . . . | u n i t$
$v ::= . . . | u n i t$
$T ::= . . . | U n i t$

Type Rules:

$Γ ⊢ unit : Unit$

Conservative Extensions

A conservative extension is an extension to a language that does not reference any other bits of the language. It does not affect how the language works.

Unit in this case is a conservative extension.

Derived Form:

$t_{1}; t_{2} \equiv (λ x : Unit . t_{2}) t_{1}, where x \notin F V (t_{2})$

Note

This assumes call by value evaluation semantics.

This is defining sequencing (;) such that $t_{1}$ is evaluated before $t_{2}$ . The where condition also requires that $x$ doesn't appear in $t_{2}$ so that it does not affect the evaluation of t_2.

Derived forms are evaluated by expanding the syntax with their definition

Inference Rules:

\frac{t_{1} \to t_{1}^{'}}{t_{1}; t_{2} \to t_{1}^{'}; t_{2}} ESeqFirst

The above rule requires $t_{1}$ to be evaluated first.

\frac{}{unit; t_{2} \to t_{2}} ESeqUnit

This rule takes the unit production of the first rule and removes it to evaluate $t_{2}$

Type Rules:

\frac{Γ ⊢ t_{2} : Unit Γ ⊢ t_{2} : T}{Γ ⊢ t_{1}; t_{2} : T}

Let Binding

Syntax

$t ::= . . . | let x = t in t$

Evaluation Rules

\frac{}{let x = t in t_{2} \to [x \to v_{1}] t_{2}}

\frac{}{let x = t_{1} in t_{2} \to let x = t_{1}^{'} in t_{2}}

Type Rules

\frac{Γ ⊢ t_{1} : T_{1} (x \to T_{1}), Γ ⊢ t_{2} : T_{2}}{Γ ⊢ let x = t_{1} in t_{2} : T_{2}}

Derived Forms

let $x = t_{1}$ in $t_{2} \equiv ((λ x : T . t_{1}) t_{2})$

Some Proofs

Define $e$

$e x \equiv x$
$e (λ x . t) \equiv λ x . e t$
$e (t_{1} t_{2}) \equiv ((e t_{1}) (e t_{2}))$
$e let x = t_{1} in t_{2}$

Pairs

Syntax

$t ::= . . . | {t, t} | t .1 | t .2$
$v :: . . . | v, v$
$T ::= . . . | T_{1} \cross T_{2}$

Evaluation Rules

\frac{}{{v_{1}, v_{2}} .1 \to v_{1}} E P r o j 1

\frac{}{{v_{1}, v_{2}} .2 \to v_{2}} E P r o j 2

\frac{t \to t^{'}}{t .1 \to t^{'} .1} E P a i r 2

\frac{t \to t^{'}}{t .2 \to t^{'} .2} E P a i r 2

\frac{t_{1} \to t_{1}^{'}}{{t_{1}, t_{2}} \to {t_{1}^{'}, t_{2}}}

\frac{t_{2} \to t_{2}^{'}}{{v_{1}, t_{2}} \to {v_{1}, t_{2}^{'}}}

Type Rules

\frac{Γ ⊢ t_{1} : T_{1} Γ ⊢ t_{1} : T_{2}}{Γ ⊢ {t_{1}, t_{2}} : T_{2} \times T_{2}} T P a i r

\frac{Γ ⊢ t : T_{1} \times T_{2}}{Γ ⊢ t .1 : T_{1}} T P r o j 1

\frac{Γ ⊢ t : T_{1} \times T_{2}}{Γ ⊢ t .2 : T_{2}} T P r o j 2

Type Ascription

Type Rules

Syntax

Type Safety

Proof of Progress

Proof of Preservation

Permutation Lemma

Weakening Lemma

Preservation of Types Under Substitution

The Proof

Simple Extensions

Base Types

Let Binding

Syntax

Evaluation Rules

Type Rules

Derived Forms

Some Proofs

Pairs

Syntax

Evaluation Rules

Type Rules

Sums and Products

Recursion and `letrec`

Type Ascription

Type Rules

Syntax

Type Safety

Proof of Progress

Proof of Preservation

Permutation Lemma

Weakening Lemma

Preservation of Types Under Substitution

The Proof

Simple Extensions

Base Types

Let Binding

Syntax

Evaluation Rules

Type Rules

Derived Forms

Some Proofs

Pairs

Syntax

Evaluation Rules

Type Rules

Sums and Products

Recursion and letrec

Recursion and `letrec`