Advanced Type Mechanisms

CS › PL Theory
$$\newcommand{\t}{\tau} \newcommand{\proves}{\vdash} \newcommand{\T}{\textsf{T}} \newcommand{\tt}{\mathbb 1} \newcommand{\bt}{\mathbb 0} \newcommand{\Int}{\textsf{int}} \newcommand{\Bool}{\textsf{bool}} \newcommand{\Proj}{\textsf{proj}} \newcommand{\Unit}{\textsf{unit}} \newcommand{\Let}{\textsf{let}} \newcommand{\List}{\textsf{list}} \newcommand{\Fold}{\textsf{fold}} \newcommand{\Unfold}{\textsf{unfold}} \newcommand{\Lab}{\textbf{Lab}} \newcommand{\Unif}{\textsf{Unif}} \newcommand{\Id}{\textsf{Id}} \newcommand{\FV}{\textsf{FV}} \newcommand{\st}{<:} \newcommand{\Void}{\textsf{void}} \newcommand{\Let}{\textsf{let}} \newcommand{\In}{\textsf{in}} \newcommand{\Type}{\textbf{Type}} $$

Structural subtyping: Haskell, Go, Typescript
nominal subtyping: C++, Java
Duck typing: Python, Javascript (if it works it works, otherwise RTE)

1. Subtyping

Many modern languages include a features called subtyping. Subtyping is particularly well known in OOP, and indeed was first introduced in the first object oriented language: Simula.

Definition. subtyping
$\t_1$ is a subtype of $\t_2$, $\t_1<:\t_2$

terms described by $\t_1$ is a subset of terms described by $\t_2$ ($\t_1$ is more precise than $\t_2$). This is introduced by design of OOP.

$\T$ is the set pf all types.

Definition. Subtyping relation.

The relation $<:\subset\T\times \T$ is a partial order, that is

  1. $\tau<:\tau$

  2. $\tau_1<:\tau_2\land \tau_2<:\tau_3\implies \tau_1<:\tau_3$

  3. $\t_1<:\t_2\land \t_2<:\t_1\implies \t_1=\t_2$

Substitution

$$\frac{\Gamma\proves e:\t'\quad\t'<:\t}{\Gamma\proves e:\t} $$

Definition. Top Type $\tt\in\T$

$$\forall\tau\in\T.\tau<:\tt $$

e.g. $\textsf{Object}$ type in Java

define bottom type $\bt\in\T$

$$\forall \tau\in\T.\bt<:\tau $$

there is no such type in Java.

Definition. Product Subtyping.

Covariant subtyping

$$\frac{\tau_1'<:\tau_1\quad\tau_2'<:\tau_2}{\tau_1'\times\tau_2'<:\tau_1\times\tau_2} $$

Sums

$$\frac{\tau_1'<:\tau_1\quad \tau_2'<:\tau_2}{\tau_1'+\tau_2'<:\tau_1+\tau_2} $$

Records,

depth

$$\frac{\tau_1'<:\tau_1\quad\tau_2'<:\tau_2\quad\ldots\quad\tau_n'<:\tau_n}{\{l_1:\tau_1',\ldots l_n:\tau_n'\}<:\{l_1:\tau_1,\ldots l_n:\tau_n\}} $$

width

note that the order doesn’t matter

this is like removing a member method or member variable from a class, producing a superclass

$$\frac{m\leq n}{\{l_1:\tau_1,\ldots l_m:\tau_n \}<:\{l_1:\tau_1,\ldots l_n:\tau_m\}} $$

Functions

$\tau_1<:\tau_1'$ is called contravariant in input

$\tau_2'<:\tau_2$ is called a covariant in output

$$\frac{\tau_1<:\tau_1'\quad \tau_2'<:\tau_2}{\tau_1'\to\tau_2'<:\tau_1\to\tau_2} $$

2. Recursive Types

In Java, a IntList type is like

1
2
3
4
class IntList { 
	int data; 
	IntList next; 
}

In OCaml, a IntList type is like

1
type intList = Empty | Cons of int * intList

Obverse that so far we cannot even describe a list type. We can describe types for list of any finitely many size, but we just cannot describe a type of $\textsf{list}$. For example, we hope the type of a list of integers is something like

$$\textsf{intList} = \Unit + (\Int × \textsf{intList}) $$

that is

$$\frac{}{\left[\right]:\textsf{intList}}\quad\quad\quad \frac{l:\textsf{intList}}{\textsf{concat}([a], l):\textsf{intList}} $$

This is not representable using what we’ve learnt so far because we don’t have the power of self-referential so far.
To implement this, we’ll introduce the fixed-point type $\mu$-operator.

2.1. $\mu$ operator

Definition. $\mu\alpha.\t$
Given $\t$ as a type and $\alpha$ as a type variable, $\mu\alpha.\t$ is defined to be the least fixed point of the function $\mathcal T\alpha=\t$ . That is

$$\mu\alpha.\t:=\textsf{lfp}(\mathcal T\alpha) $$

Such a fixed point exists and is unique as long as $\alpha\neq\t$ . Note that if $\t$ does not reference $\alpha$, then $\mu\alpha.\t=\t$.
For example,

$$\textsf{intList}=\mu\alpha.\mathcal T\alpha=\mu\alpha.\Unit+(\Int\times \alpha) $$

Syntactically, $\mu\alpha.\t$ emphasizes another concept we have previously seen: type variables. In this expression, $\alpha$ is a type variable that is bound by the constructor $\mu$. These variables and binders have the same notions of scope, free and bound variables, renaming, and safe substitution as variables in $\lambda$-calculus.

The $\mu$-constructor is even sufficient to build mutually-recursive types. For example, if $\alpha_1=\t_1$and $\alpha_2=\t_2$ where both $\t_1$ and $\t_2$ may refer to either or both of $\alpha_1$ and $\alpha_2$, we can define the mutually-recursive types $\sigma_1$ and $\sigma_2$ by:

$$\sigma_1:=\mu\alpha_1.(\t_1[\alpha_2\mapsto \mu\alpha_2.\t_2])\\ $$

and

$$\sigma_2:=\mu\alpha_2.(\t_2[\alpha_1\mapsto \mu\alpha_1.\t_1]) $$

2.2. Recursive Types in Programming Languages

There are two approaches to using recursive types in languages: equirecursive (等递归) and isorecursive (同构递归).

In equirecursive, $\mu\alpha.\t$ and $\t[\alpha\mapsto \mu\alpha.\t]$ are considered to be the same type

$$\mu\alpha.\t:=\tau[\alpha\mapsto \mu\alpha.\t] $$

In isorecursive, these two typed are not considered isomorphic instead of equal, i.e.

$$\mu\alpha.\t\equiv \tau[\alpha\mapsto \mu\alpha.\t] $$

which means that we can convert one term into another, but explicitly. We introduce such conversion as the $\Fold$ and $\Unfold$ functions as follows

$$\begin{aligned} \Fold:\tau[\alpha\mapsto \mu\alpha.\t]\to \mu\alpha.\t\\ \Unfold:\mu\alpha.\t\to\tau[\alpha\mapsto \mu\alpha.\t] \end{aligned} $$

These definitions make so much sense once you notice that a type is just a equivalence class of terms.

To use these functions explicitly, we’ll add these functions to our language syntax

$$\begin{aligned} e&:=\cdots\mid \Fold\ e\mid\Unfold\ e\\ v&:=\cdots\mid\Fold\ v \end{aligned} $$

as always, we’ll define the typing rules and operational semantics while adding new syntactical forms.

  • Typing rules
$$\frac{\Gamma\proves e:\t[\alpha\mapsto \mu\alpha.\t]}{\Gamma\proves \Fold\ e:\mu\alpha.\t}\quad\quad \frac{\Gamma\proves e:\mu\alpha.\t}{\Gamma\proves \Unfold\ e:\t[\alpha\mapsto \mu\alpha.\t]} $$

This is natural because a isomorphism is defined to be nothing more than a bijection.

  • Operational semantics

The semantic rules for these new operations consider them both evaluation contexts, and the introduction and elimination forms cancel each other, as normal.

$$E:=\cdots\mid \Fold\ e\mid \Unfold\ e\quad\quad \frac{}{\Unfold\ (\Fold\ v)\to v} $$

3. Polymorphism $\lambda$-calculus

Recall that we used recursive type to construct $\textsf{intList}$ type, but what if we want a list of any type? Or, if we want a $\Id$ function that is generic?
The solution is to add a new constructor the universally quantifies over types. That is,

$$\t:=\cdots\mid \alpha\mid \forall.\alpha.\t $$

The type $\forall\alpha.\t$ is a polymorphic type, or a type schema, which is a pattern with type variables that can be instantiated to obtain actual types. For example, the polymorphic type of $\Id$ would be

$$\Id:\forall \alpha.\alpha\to\alpha $$

Note. Like the recursive type constructor $\mu$, this $∀$ constructor binds a type variable with the same notions of scope, free and bound variables, renaming, and safe substitution as both for types and for terms.

The language that results from adding these types is known as the polymorphic $\lambda$-calculus. It has the same terms and evaluation rules as STLC, but with these extra polymorphic types. All terms that were well-typed before will still be well-typed, but now more terms will be typable as well.

3.1. Typing Rules

Except for the four typing rules of STLC

$$\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} $$

there are two new typing rules introduced by polymorphism

$$\frac{\Gamma\proves e:\t\quad\alpha\not\in\FV(\t)}{\Gamma\proves e:\forall\alpha.\t} \quad\quad \frac{\Gamma\proves e:\forall\alpha.\t}{\Gamma\proves e:\t[\alpha\mapsto\t']} $$

which are named Generalize rule and Instantiate rule respectively. The generalize rule indicates that the types themselves are open, that is, they may contain free variables. This rule aligns with the generalization rule in first order logic system quite well.

Definition. $\Void$

$$\Void:=\forall\alpha.\alpha $$

This is fun because nothing has type $\forall\alpha.\alpha$, and $\Void$ is said to be uninhabited

With polymorphic types, we can now type $\omega:=\lambda x.x\ x$ to be

$$\omega:\forall\beta.(\forall\alpha.\alpha\to\alpha)\to\beta\to\beta $$

which is a valid and meaningful type. However using only polymorphic types is still not enough to type $\Omega:=\omega\ \omega$, and we still need recursive types for that.

In fact, polymorphic $\lambda$-calculus on its own (without recursive types or something similar) still has the same property of STLC that every well-typed program terminates. A proof could be found here

While polymorphic $\lambda$-calculus allows for reuse of programs in very convenient ways, it has a major downside: type inference is now undecidable. A compiler could try its best and ask programmers to insert type annotations when it fails, but we can also restrict the use of polymorphism to regain decidability. Hindley–Milner type system and System F are two such methods.

3.2. Hindley–Milner type system

Languages like Haskell and OCaml uses Hindley–Milner type system, which restrict polymorphism in two ways:

  1. Type quantification can only appear at the top level of a type. That is, we only allow polymorphic expressions of the form $\forall\alpha_1\forall\alpha_2\ldots\forall\alpha_n.\t$ where $\t$ is quantifier-free.
  2. Polymorphism can only be introduced in the context of a $\Let$ expression, not arbitrary variable bindings.
    Together, these restrictions result in the following modifications to the language
$$\begin{aligned} &\text{Quantifier-free Terms} & \t &:=\Unit\mid\alpha\mid\t_1\to\t_2\\ &\text{Primitive }\Let &e &:=\cdots\mid \Let\ x=e_1\ \In\ e_2 \end{aligned} $$

with an replace Generalize rule with the following PolyLet rule.

$$\frac{ \Gamma\proves e_1:\t_1\quad\quad \Gamma,x\proves \forall\alpha_1\forall\alpha_2\cdots\forall\alpha_n.\t_1\proves e_2:\t_2\quad\quad \{\alpha_1,\alpha_2,\cdots,\alpha_n\}=\FV(\t_1)\setminus\FV(\Gamma)}{\Gamma\proves \Let\ x = e_1\ \In\ e_2:\t_2} $$

We previously considered the term $\Let\ x = e_1\ \In\ e_2$ to be syntactic sugar for $(\lambda x.e_2)\ e_1$. While the two still have the same semantic rules, they are no longer equivalent in the type system.

The mechanism that polymorphism can only be introduced with let expressions is known as Let-polymorphism, which is the most distinguishable feature in Hindley-Milner type system. Both Haskell and OCaml use let-polymorphism. In theory, this could cause the type checker to require exponential time, but in practice it is not a problem.

3.3. System F

Definition. System F
When we first introduced STLC, we used Church-style terms with types explicitly annotated on function arguments. The corresponding version of polymorphic $\lambda$-calculus is called System F / Second order lambda calculus.

In System F, we explicitly abstract terms with respect to types and explicitly instantiate those types before using the term. We therefore augment the syntax of STLC with new types and terms as follows.

$$\begin{aligned} \t&:=\cdots\mid \alpha\mid \forall\alpha.\t\\ e&:=\cdots\mid \Lambda\alpha.e\mid e\ \t \end{aligned} $$

These new terms are known as type abstraction and type application respectively. Operationally, we can add the following semantic rule

$$\frac{ }{(\Lambda\alpha.e)\ \t\to e[\alpha\to\t]} $$

This just gives a rule for instantiating a polymorphic type. Since these reductions only involve types, they can be performed at compile time

Definition. Type context
Let $\sim$ be an equivalence relation defined on the set $\Type$ of all types, then a type context $\Delta$ is defined to be a (partial) quotient map, that is,

$$\Delta:\Type\to(\Type/\sim) $$

Each equivalence class defined from the equivalence relation is called a kind. It’s obvious that when the type system is simple and has only one kind, then we can treat $\Delta$ as a set.

The type system has two classes of judgements

$$\Delta\proves \t\quad\quad \Delta;\Gamma\proves e:\t $$
  • The first says that $\t$ is well-typed in the type context $\Delta$ (there indeed exists such type $\t$ in $\Delta$!)
  • The second says that we can prove $e$ has type $\t$ in type context $\Delta$ and variable context $\Gamma$

The rules for the well-formed types are as follows.

$$\begin{aligned} \frac{ }{\Delta\proves \Unit}\quad\quad \frac{\alpha\in\Delta}{\Delta\proves\alpha}\quad\quad \frac{\Delta\proves \t_1\quad\Delta\proves \t_2}{\Delta\proves \t_1\to\t_2}\quad\quad \frac{\Delta,\alpha\proves \t}{\Delta\proves\forall\alpha.\t} \\ \end{aligned} $$

The last two rules are saying that $\Delta$ is closed under $\to$ and $\forall$

The typing rules for rules in system F are as follows

$$\begin{aligned} \frac{ } {\Delta;\Gamma\proves ():\Unit}\quad& \frac{\Gamma(x)=\t\quad\Delta\proves \t} {\Delta;\Gamma\proves x:\t}\quad \frac{\Delta;\Gamma;x:\t_1\proves e:\t_2\quad \Delta\proves \t_1}{\Delta;\Gamma\proves\lambda x:\t_1.e:\t_1\to\t_2}\quad &\frac{\Delta;\Gamma\proves e_1:\t_1\to\t_2\quad \Delta;\Gamma\proves e_2:\t_1} {\Delta;\Gamma\proves e_1\ e_2:\t_2} \\\\ &\frac{\Delta,\alpha\Gamma\proves e:\t\quad \alpha\not\in\FV(\Gamma)}{\Delta;\Gamma\proves \Lambda\alpha.e:\forall\alpha.\t}\quad \frac{\Delta;\Gamma\proves e:\forall\alpha.\t\quad\Delta\proves \t'}{\Delta;\Gamma\proves e\ \t':\t[\alpha\mapsto \t']}& \end{aligned} $$
  • The first four rules are the same as the rules for STLC, but with $\Delta$ included and a requirement that any types that appear be well-formed.
  • The last two rules specify the types for type abstractions and applications, also requiring that types be well-formed. In fact, one can show that if $\Delta;\Gamma\proves e:\t$ , then and all type annotations occurring $e$ in must be well-formed in $\Delta$. In particular $\proves e:\t$ is only possible when $e$ and $\t$ are both closed.

4. Existential Types

5. Propositions as Types and Curry–Howard