Intro to Type System

$$\renewcommand{\t}{\tau} \renewcommand{\proves}{\vdash} \renewcommand{\T}{\textsf{T}} \renewcommand{\tt}{\mathbb 1} \renewcommand{\bt}{\mathbb 0} \renewcommand{\Int}{\textsf{int}} \renewcommand{\Bool}{\textsf{bool}} \renewcommand{\Proj}{\textsf{proj}} \renewcommand{\Unit}{\textsf{unit}} \renewcommand{\List}{\textsf{list}} \renewcommand{\Fold}{\textsf{fold}} \renewcommand{\Unfold}{\textsf{unfold}} \renewcommand{\Lab}{\textbf{Lab}} \renewcommand{\Unif}{\textsf{Unif}} \renewcommand{\Id}{\textsf{Id}} \renewcommand{\FV}{\textsf{FV}} \renewcommand{\st}{<:} \renewcommand{\Void}{\textsf{void}} \renewcommand{\Var}{\textbf{Var}} \renewcommand{\Type}{\textbf{Type}} \renewcommand{\Nat}{\mathbb N} \renewcommand{\Succ}{\textsf{succ}} \renewcommand{\Add}{\textsf{add}}$$

1. Simple Typed $\lambda$-calculus

1.1. Syntax

Recall that the syntax of pure $\lambda$-calculus formally defined as follows

$$e:= x\mid \lambda x. e\mid e_1\ e_2$$

Definition. Basic on this, we can define simple typed lambda calculus (STLC). The biggest difference is that we now have two inductively defined expressions: terms and types.

$$\begin{aligned} &\text{Types}& &\tau:=\Unit \mid \tau_1\to\tau_2\\ &\text{Terms}& &e:=()\mid x\mid \lambda x:\t\ e\mid e_1\ e_2 \end{aligned}$$

where

• $():\Unit$
• $\lambda x:\tau. e$ is a function that takes one input of type $\tau$ and evaluates $e$.

By convention, the function arrow is right-associative, so $\t_1\to\t_2\to\t_3$ is the same as $\t_1\to(\t_2\to\t_3)$. This convention matches left-associative function application.

The operational semantics of this language is unchanged from CBV-calculus, counting $()$ as a value which has no reduction rule. That is, we have the following definitions.

Definition. Values in STLC

$$v:=()\mid \lambda {x:\t}. e\\ $$

Definition. Evaluation Contexts of STLC

$$E:=[\cdot]\mid E\ e\mid v\ E$$

Definition. Reduction Rules of STLC

$$\frac{e\to e'}{E[e]\to E[e']}\quad\quad \frac{}{(\lambda{x:\t}.e)v\to e[x\mapsto v]}$$

One other small change is that the presence of $()$ means there are now closed -terms can get stuck. For example

$$() (\lambda{x:\Unit}.x)$$

is a perfectly good closed $\lambda$-term that is also stuck. We would like to eliminate these, and the type system will allow us to do so.

1.2. Typing Rules

The typing rules for STLC are an inductive relation on three inputs:

• a typing context $\Gamma: \Var\to\Type$ that maps variables to types
• an expression $e$; and
• a type $\t$.

$\Gamma \proves e:\t$ means that we can prove that expression $e$ has type $\t$ in typing context $\Gamma$ using the typing rules. Specially, $\proves e:\t$ is a short-hand for $\emptyset\proves e:\t$.

Specifically, typing rules for STLC is the four rules as follows,

$$\begin{aligned} \frac{ }{\Gamma\proves ():\Unit}\quad \frac{\Gamma(x)=\t}{\Gamma\proves x:\t}\quad \frac{\Gamma,x:\t_1\proves e:\t_2}{\Gamma:\lambda x:\t_1.e:\t_1\to \t_2}\quad \frac{\Gamma\proves e_1:\t_1\to \t_2\quad e_2:\t_1}{\Gamma\proves e_1\ e_2:\t_2} \\ \end{aligned}$$

$\Gamma, x:\t$ means exactly the same as $\Gamma[x\mapsto \tau]$

1.3. Expressive power

It’s reasonable to reconsider the types of natural numbers using Church’s encoding,

$$\bar 1:=\lambda fx.f\ x$$

The application typing rule indicates that $f:\t_1\to \t_2$ and $x:\t_1$, so $\bar 1:\t_1\to\t_2\to\t_1\to \t_2$. Since

$$\bar 0:=\lambda fx.x$$

Then we have $\bar 0:\t_1\to\t_2\to\t_1\to\t_1$. which means $\t_1=\t_2$. Then we can show using mathematical induction that

$$\forall n\in \Nat.\bar n:\t\to\t\to\t\to\t$$

However with the defined function

$$\Add :=\lambda mn.n\ \Succ\ m$$

we could found that $\Add$ is not of type $\t\to\t\to\t$ in this case.

It is for this reason that most typed language include things like numbers and booleans directly as language primitives.

Another example is the $\Omega$ operator where

$$\Omega := (\lambda x. x\ x)(\lambda x. x\ x)$$

One can found that there is no way to give this a type by showing that we cannot give a type to $\lambda x. x\ x$. In fact, we will later see that we cannot write down any nonterminating program in STLC (this is called type-soundness)

Definition. Type soundness
A type system is called type-sound if well-typed programs don’t get stuck.

2. Products, Sums, and Datatypes

$$\begin{aligned} &\text{Types}& &\tau:=\Unit\mid \tau_1\to\tau_2\\ &\text{Terms}& &e:=()\mid x\mid \lambda x:\t\ e\mid e_1\ e_2\\ &\text{Values}& &v:=() \mid \lambda x:\t\ e \text{ (closed)} \end{aligned}$$

Recall that the type system of STLC guaranteed type soundness, but it restricted us substantially. For instance, our encoding of numbers as Church numerals no longer worked the way we wanted. Instead, we will see how to add various other types to the language as primitives.

1.1. Integers

We extend the syntax of both types, terms, and values to STLC by defining integers. We use $\otimes$ to denote arithmetic operations $(+, −, *, \exp)$.

$$\begin{array}{l} \tau:=\cdots \mid \text { int } \\ e:=\cdots\mid n\mid e_{1} \otimes e_{2} \\ v:=\cdots \mid n \end{array}$$

we then need to extend corresponding semantics and update the type system with rules for integers where

$$E:=\cdots\mid E \otimes e\mid v\otimes E\quad\quad\frac{m= n_1\otimes n_2 (\text{mathematically})}{n_1\otimes n_2\to n}$$

and

$$\frac{ }{\Gamma\proves n:\Int}\quad \quad \frac{\Gamma\proves e_1:\Int\quad \Gamma\proves e_2:\Int}{\Gamma\proves e_1\otimes e_2:\Int}$$

By using the manually defined integers, we do not have the full power of Church numerals, which allowed us to define bounded for loops, but we have gotten a substantial feature back.

1.2. Pairs

Another useful data structure that we previously encoded as pairs.

$$\begin{array}{l} \t:=\cdots \mid \t_{1} \times \t_{2} \\ e:=\cdots\mid\left(e_{1}, e_{2}\right)\mid\Proj_{1}\ e \mid\Proj_{2}\ e \\ v:=\cdots\mid\left(v_{1}, v_{2}\right) \end{array}$$

1.3. Records

$$\begin{array}{l} \ell \in \Lab \\ \tau:=\cdots \mid\{\ell_{1}: \tau_{1}, \ldots, \ell_{n}: \tau_{n}\} \\ \boldsymbol{e}:=\cdots\mid \{\ell_{1}=e_{1}, \ldots, \ell_{n}=e_{n}\}\mid e . \ell \\ v:=\cdots \mid\{\ell_{1}=v_{1}, \ldots, \ell_{n}=v_{n}\} \end{array}$$

1.4. Sums

3. Type Inference

Languages like Haskell and OCaml perform type inferences. For instance, in the expression

$$(f\ 3)$$

the language knows that must be a function that has type $\Int\to\alpha$ for some type variable $\alpha$.
If there are other occurrences of $f$, those will provide different constraints, and these constraints must all have a common solution for the program to have a type.

3.1. Unification

Definition. Unification

Briefly, unification is the process of taking two terms and finding a variable substitution that will take the two input terms to the same result.

Type inference and pattern matching in many languages are instances of unification. Pattern matching is generally done by unifying language expressions, while type inference is done by unifying type expressions.

Definition. Unifier

A unifier is a substitution that unifies a given collection of (unordered) terms. That is, given a collection

$$\{s_1\doteq t_1, s_2\doteq t_2,\ldots, s_n\doteq t_m\}$$

of terms, a unifier is a substitution

$$\gamma(\cdot)=\cdot[u_1\mapsto v_1, u_2\mapsto v_2,\ldots, u_n\mapsto v_n]$$

such that $\forall i\in \{1,2\ldots,m\},\gamma(s_i)=\gamma(t_i)$. where $\{u_k\}_{k=1}^n$ and $\{v_k\}_{k=1}^n$ are two collections of subterms.

As a notation, we will write = $[x\mapsto s, y\mapsto t, \ldots]$ to indicate the parallel substitution, not a sequential one. In particular, given a substitution like $x[x\mapsto g(y), y\mapsto z]$ would produce $g(y)$, which is different then the sequential behavior of $g(z)$.

It’s obvious that if we can find a unifier between two terms, we can then find a unifier between any finite number of terms.
Even when unifiers exist, they are not necessarily unique. However, if a unifier does exist, we can show that there is always a most general unifier (MGU) that is unique up to renaming.

Definition. Most General Unifiers (MGU)

A substitution $\gamma$ is a most general unifier for $s$ and $t$ if

• is a unifier for $s$ and $t$, and
• any other unifier $\gamma'$ for $s$ and $t$ is a refinement of . That is, we can get $\gamma'$ from $\gamma$ by doing more substitutions.

Algorithm. Robinson’s unification algorithm (1965)

Define a recursive function $\Unif$ that takes a set of equality constraints and produces their MGU (if exists) as follows

$$\begin{aligned} \Unif(\emptyset)&:=\Id\\ \Unif(\{x\doteq x\}\cup E) &:= \Unif(E)\\ \Unif(\{f(s_1,\ldots ,s_n)=f(t_1,\ldots ,t_n)\} \cup E) &:= \Unif(\{s_1\doteq t_1, \ldots, s_n \doteq t_n\}\cup E)\\ \Unif(\{x\doteq t\}\cup E) &:= [x\mapsto t] ; \Unif(E[x\mapsto t]) \text{ if }x\notin \FV(t) \end{aligned}$$

If $E$ is a set of equality constraints, then $E[x\mapsto t]$ denotes the result of apply the substitution $[x\mapsto t]$ to all terms in $E$.

The only nontrivial part if the fourth rule, we actually create part of the unifier substitution. Note the sequential composition operator, so this is the substitution $[x\mapsto t]$ sequentially composed with the result of $\Unif(E[x\mapsto t])$.

3.2. Type Inference

Definition. Most General Type (MGT)

A type of a term is called most general if any other type of this term is a substituted instance of this type.

Note that type inference is no more than unification between type expressions. Still using STLC, Robinson’s algorithm gives MGT.

Suppose we want to infer the type of a $\lambda$-term $e$. WLOG, assume $e$h as no variables bound more than once and no variable with a binding occurrence that also occurs free. (Barendregt variable convention allows us to make such an assumption)

Now let $e_1, \ldots ,e_n$ be an enumeration of all subterms of $e$. First create a unique type variable $\alpha_i$ to each $e_i$ for $1\leq i\leq n$ , and also a different unique type variable $\beta_x$ for each variable $x$ that occurs in $e$. Then take the following constraints.

$$\begin{aligned} &\text{Syntactical Form}& &\text{Constraint}\\ &e_i=()& & \alpha_i\doteq \Unit\\ &e_i=x& & \alpha_i\doteq\beta_x\\ &e_i=\lambda x.e_j& & \alpha_i\doteq \beta_x\to\alpha_j\\ &e_i=e_j\ e_k& &\alpha_j\doteq \alpha_k\to \alpha_i \end{aligned}$$

If there are more types like $\Int$ and $\Bool$ in this language, we can also design rules for these types, which is similar to the ones we’ve shown.