Preliminaries

The Typing Relation

  A term t belongs to type T means we can check this statically, instead of depending on some runtime semantics, i.e., \mathtt{if\ true\ then\ true\ else\ 0} is ill-typed, although it will yields the well-typed term at runtime.
  The typeing relation can be formally written as \mathtt{t:T}, meaning "\mathtt t is of type \mathtt T", can be define by a set of inference rules, e.g.:

\mathtt{\cfrac{t_1:Bool\ \ \ t_2:T\ \ \ t_3:T}{if\ t_1\ then\ t_2\ else\ t_3:T}}

The typing relation is the smallest binary relation between terms and types satisfying all the instances of inference rules, a term \mathtt t is said to be typable or well-typed if \mathtt{\exist_{T}(t:T)}

The Inversion Lemma

  The inversion lemma states, given \mathtt{t:T}, if \mathtt t has any type, then \mathtt t has type \mathtt T, this means, for example, if the inference rule states \mathtt{true:Bool}, then you know that if \mathtt{true} has any type at all, it must be of type \mathtt{Bool}.

Under the context of "Simply Typed", Each typable term has only one type, and the type itself has only one derivation tree

Safety of Type Systems

  The safety of typing system build upon two theorems:

  1. Progress: A well-typed term does not stuck(it is either a value or can be derived further more)
  2. Preservation: if \mathtt t is a well-typed term and \mathtt{t\rightarrow t'}, then \mathtt{t'} is also well typed

These two rules can be proven by induction on derivation of \mathtt t, however, the second theorem's is the sufficient condition for a term to be typable, because \mathtt 0 is a well-typed form but the term that can derive it it's not necessary to be typable, e.g., \mathtt{if\ true\ then\ 0\ else\ false}.

Simply Typed Lambda Calculus

  The lambda calculus will involves only \tt Bool type for brevity

Function Types

  Consider that an abstraction in lambda calculus may results in another abstraction, in order to build a soundness type system, we need to keep track of the type for both arguments and return values, we use \tt T\rightarrow R denoting a function(an abstraction) that takes an argument of type \tt T and a return value of type \tt R, the type of new lambda calculus is thus can be defined by the following BNF(our type system contains only one type \tt Bool):

\mathtt{T ::= Bool|T\rightarrow T}

The \rightarrow is called type constructor since it constructs a new type upon the original one, which is right associative, which means, \tt T_1\rightarrow T_2\rightarrow T_3=T_1\rightarrow(T_2\rightarrow T_3)

The Typing Relation

  There are two ways of knowing what type of argument an abstraction would expect:

  1. Implicitly Typed: The type is deduced according the usage of the argument inside the body of the abstraction
  2. Explicitly Typed: Specify the type explicity

  We use \lambda x:\mathtt{T}.t_1 to show that x is expected to be of type \tt T.

  The Typing Context, denoted by \Gamma, is a function from variables to types, it can be represented by a sequence of typing relations separated by commas, and it can be extended by adding a comma and a new binding to the right of it(e.g.: \Gamma,x:\tt T_1 adds a new relation (x:\tt T_1) to the typing context), we use \Gamma\vdash t:\tt T to show that the term t has type \tt T under the set of assumptions \Gamma, \Gamma can be omitted if it equals to \phi. The variables in \Gamma must be distinct, which means you cannot add a variable that is already existed, so variable renaming is required when such thing occurs.

Typing Rules for Lambda Calculus

We can conclude the general rule for typed lambda calculus
:

\begin{gather}
\cfrac{x:\mathtt{T}\in\Gamma}{\Gamma\vdash x:\tt T}\tag{T-Variable}\\
\cfrac{\Gamma,x:\mathtt{T_1}\vdash t:\mathtt{T_2}}{\vdash \lambda x:\mathtt{T_1}.t:\tt T_1\rightarrow T_2}\tag{T-Abstraction}\\
\cfrac{\Gamma\vdash t_1:\mathtt{T_1\rightarrow T_2},t_2:\mathtt{T_1}}{\Gamma\vdash t_1\ t_2:\tt T_2}\tag{T-Application}
\end{gather}

along with the base type \tt Bool

\begin{gather}
\tt true:Bool\tag{T-True}\\
\tt false:Bool\tag{T-False}\\
\cfrac{\Gamma\vdash t_1:\mathtt{Bool},t_2:\mathtt{T},t_3:\mathtt{T}}{\tt \Gamma\vdash if\ \mathnormal{t_1}\ then\ \mathnormal{t_2}\ else\ \mathnormal{t_3}:T}\tag{T-If}
\end{gather}

Specifically, we can consider \Gamma contains the type information of the free variables in t, you can interpret \Gamma\vdash x:\tt T as free variable x is assumed to have type \tt T under context \Gamma

\lambda_{\rightarrow} can be used to represent the simply typed lambda calculus

It is clear that \lambda_{\rightarrow} will degenerate to untyped without a base type (in this case, \tt Bool) because no type can be actually applied.

Typing Properties

The Inversion Lemma

  The inversion lemma for \lambda_{\rightarrow} is essentially the reverse of its definitions:

\begin{align*}
\Gamma\vdash x:\tt T&\implies x:\mathtt{T}\in\Gamma\tag{I-Var}\\
\vdash \lambda x:\mathtt{T_1}.t:\tt R&\implies \exists_{\mathtt{T_2}}(\mathtt{R=T_1\rightarrow T_2}\land (\Gamma,x:\mathtt{T_1}\vdash t:\mathtt{T_2}))\tag{I-Abs}\\
\Gamma\vdash t_1\ t_2:\tt T_2&\implies \exist_{\mathtt{T_1}}(\Gamma\vdash t_1:\mathtt{T_1\rightarrow T_2}\land\Gamma\vdash t_2:\mathtt{T_1})\tag{I-App}
\end{align*}

with the cases for base type, in this case, \tt Bool

\begin{align*}
\Gamma\vdash\tt true:T&\implies \tt T=Bool\tag{I-IF-True}\\
\Gamma\vdash\tt false:T&\implies \tt T=Bool\tag{I-IF-False}\\
\Gamma\vdash \tt if\ \mathnormal{t_1}\ then\ \mathnormal{t_2}\ else\ \mathnormal{t_3}:T&\implies \Gamma\vdash\tt \mathnormal{t_1}:Bool\land\Gamma\vdash \mathnormal{t_2,t_3}:T\tag{I-IF}
\end{align*}

Uniqueness

  Given typing context \Gamma, a term t can have at most one type, and at most one derivation, i.e., both type and type derivation is unique.

Canonical Forms

  The lemma of canonical forms states the shape of the values (normal forms) of the \lambda_{\rightarrow}

  1. If t is a value of type \tt Bool, then t=\mathtt{true}\lor t=\mathtt{false}
  2. If t is a value of type \tt T_1\rightarrow T_2, then t=\lambda x:\mathtt{T_1}:t_2

Preservation

  The Progress Theorem is omitted since it's nothing more than a straightforwared induction on derivations, here only shows the proof for Preservation

Permutation Lemma

  If \Gamma\vdash t:\tt T and \Delta is a permutation of \Gamma, then \Delta\vdash t:\tt T, the latter derivation would have the same depth as the former

Weakening Lemma

  If \Gamma\vdash t:\mathtt{T}\land x\notin dom(\Gamma), then \Gamma,x:\mathtt{S}\vdash t:\tt T. Weakening Lemma basically says if a judgment holds for a set of hypotheses, then it will holds for the augmented hypotheses

Preservation of Types Under Substitution Lemma

  If \Gamma,x:\mathtt{S}\vdash t:\mathtt{T}\land\Gamma\vdash s:\tt S, then \Gamma\vdash[x\mapsto s]t:\tt T
  The substitution lemma basically says if you replace a free variable in a term with another one with the same type, then the type of the term is preserved, these two free variables may stand for different meanings, but we are focusing only on the type now.
  The proof for this lemma is written here due to its complexity
Proof:
  The proof will based on the induction on the derivation of \Gamma,x:\mathtt{S}\vdash t:\tt T, which means we will assume that the lemma holds for all subderivations of \Gamma,x:\mathtt{S}\vdash t:\tt T upon several cases:

Case T-Variable

  If the last inference rule used in derivation is \text{T-Variable}, by the substitution rule, we know that [x\mapsto s]t will result in s or t depends on whether t=x, if it results in s the desired result is immediate because t=x\land\Gamma\vdash t:\mathtt{T},s:\mathtt{S}\implies \tt T=S, since the variables in typing context is unique, and if it results in t the answer is also immediate since original term t stays intact

\tag*{◃}
Case T-Abstraction

  If the last inference rule used in derivation is \text{T-Abstraction}, the proof can be witnessed by the following inference tree

\tag*{◃}
Case T-Application

  If the last inference rule used is \text{T-Application}, which means it has form t_1\ t_2, then by induction hypothesis we know \Gamma\vdash [x\mapsto s]t_1:\tt T_1\rightarrow T and \Gamma\vdash [x\mapsto s]t_2:\tt T_1, thus by \text{T-Application}, we have \Gamma\vdash [x\mapsto s]t_1\ [x\mapsto s]t_2:\tt T, therefore, \Gamma\vdash [x\mapsto s](t_1\ t_2):\tt T

\tag*{◃}
Case T-True

  \Gamma\vdash[x\mapsto s]\tt true:T is trivial and immediate

\tag*{◃}
Case T-False

  \Gamma\vdash[x\mapsto s]\tt false:T is trivial and immediate

\tag*{◃}
Case If

  If the last inference rule used in the derivation is \text{T-If}, which means it has form \tt if\ \mathnormal{t_1}\ then\ \mathnormal{t_2}\ else\ \mathnormal{t_3}, by induction hypothesis we have:

\begin{aligned}
&\Gamma\vdash[x\mapsto s]t_1:\tt Bool\\
&\Gamma\vdash[x\mapsto s]t_2:\tt T\\
&\Gamma\vdash[x\mapsto s]t_3:\tt T
\end{aligned}

therefore by \text{T-If} we have:

\Gamma\vdash\tt if\ \mathnormal{[x\mapsto s]t_1}\ then\ \mathnormal{[x\mapsto s]t_2}\ else\ \mathnormal{[x\mapsto s]t_3}:T

which is

\begin{aligned}
\Gamma\vdash\tt \mathnormal{[x\mapsto s]}(if\ \mathnormal{t_1}\ then\ \mathnormal{t_2}\ else\ \mathnormal{t_3}):T\\\\
\tag*{◃}
\end{aligned}

The proof is thereby completed.

\begin{aligned}
\tag*{∎}
\end{aligned}

From the lemmas' above, we can prove the preservation of the \lambda_{\rightarrow}, by induction on the last derivation rule used by a term t, since both \text{T-Variable} and \text{T-Abstration} is already in normal form, the only thing that needs to be considered is \text{T-Application}, following the evaluation rules stated in Untyped Lambda Calculus, we can prove each of them individually, specifically, when proving the last rule(\beta-reduction), use the substitution lemma we've just proved above.

\begin{aligned}
\tag*{∎}
\end{aligned}

Curry-Howard Correspondence

  In typed lambda calculus, more specifically, the type constructor \rightarrow, contains two kinds:

  1. Introduction rules, which is the \text{T-Abstraction}, they described how elements of the type can be constructed
  2. Elimination rules, which is the \text{T-Application}, they described how elements of the type can be used.

The Curry-Howard Correspondence stated the correlation between type theory and constructive logic, generally speaking, there is a one-to-one correspondence between logic statements and types, it can be concluded in the table below1:

\begin{array}{|c|c|}
\hline
Logic & Type\\ \hline
Propositions & Types \\
P\implies Q & \tt P\rightarrow Q\\
P\land Q & \tt P\times Q\\
\text{Proof of }P & t:\tt P\\
P\text{ is provable} & \exist_{t}(t:\tt P)\\
\hline
\end{array}

2

Erasure

  In \lambda_{\rightarrow}, the type does not preserve to the evaluation, it can be witnessed from the fact that the evaluation rule of \lambda_{\rightarrow} is the same as the untyped one, thus, a term of \lambda_{\rightarrow} can actually degenerates to a term of untyped lambda calculus, called type erasure, defined inductively:

\begin{aligned}
erase(x)&=x\\
erase(\lambda x:\mathtt{T}.t)&=\lambda x.\ erase(t)\\
erase(t_1\ t_2)&=erase(t_1)\ erase(t_2)
\end{aligned}

  And since types don't matter during the evaluation, there are some simple correspondence between evaluate typed terms directly and evaluate terms after their types have been erased:

\begin{aligned}
t\rightarrow t'&\implies erase(t)\rightarrow erase(t')\\
t\in\lambda_{\rightarrow}\land erase(t)\rightarrow m'&\implies\exist_{t'\in\lambda_{\rightarrow}}(t\rightarrow t'\land erase(t')=m')
\end{aligned}

The second rule here basically tells "it doesn't matter whether to evaluate before or after the erasure"

Typability

  A term m in untyped lambda calculus is said to be typable in \lambda_{\rightarrow} if there are some typed term t, type \tt T, and context \Gamma such that erase(t)=m\land\Gamma\vdash t:\tt T3

Church-Style and Curry-Style

  Church-Style and Curry-Style are two ways to define a language, until now we're using the Curry-Style, which is define the syntax first, then define semantics (evaluation rules), and define its type system at last to reject the ill-formed terms.
  Church-Style, on the other hand, takes a difference approach, it first define all the terms, then give a type system to identify those typable terms, and give semantics only on those.
  From a historical perspective, the Church-Style is mostly used in explicitly typed systems, while Curry-Style is prefered to be used in implicitly typed systems.


  1. This table is incomplete, more of the rows will be added during the learning of type theory ↩︎
  2. The product type is not learnt yet ↩︎
  3. Related topic is type reconstruction, haven't learnt yet, however, languages like ML use such method to infer type automatically ↩︎

We Choose to Go to the Moon