Types

\[ \newcommand{\target}[2]{\class{mathjax-symbol mathjax-symbol-#1}{#2}} \newcommand{\type}[3]{#1 \target{type}{\vdash} #2 \target{type}{:} #3} \newcommand{\abs}[3]{\target{abs}{\lambda} #1 \target{abs}{:} #2\target{abs}{.} #3} \newcommand{\tabs}[2]{\target{tabs}{\Lambda} #1 \target{tabs}{.} #2} \newcommand{\arrow}{\target{arrowT}{\rightarrow}} \newcommand{\subt}{\target{subT}{<:}} \newcommand{\Int}{\mathsf{Int}} \newcommand{\Bool}{\mathsf{Bool}} \newcommand{\lett}[3]{\mathsf{let}\ \mathit{#1} : #2 = #3\ \mathsf{in}} \newcommand{\letu}[2]{\mathsf{let}\ \mathit{#1} = #2\ \mathsf{in}\ } \newcommand{\ite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} \DeclareMathOperator{\proj}{.} \newcommand{\object}[1]{\mathsf{object}\ #1\ \mathsf{end}} \newcommand{\call}[2]{#1 \# \mathit{#2}} \newcommand{\method}[2]{\mathsf{method}\ \mathit{#1} = #2} \newcommand{\self}{\mathit{self}} \newcommand{\super}{\mathit{super}} \newcommand{\refc}{\mathsf{ref}\ } \newcommand{\inherit}[2]{\mathsf{inherit}\ #1\ \mathsf{as}\ \mathit{#2}} \newcommand{\pack}[3]{\mathsf{pack}\ (#1, #2)\ \mathsf{as}\ #3} \newcommand{\unpack}[4]{\mathsf{unpack}\ (#1, #2) = #3\ \mathsf{in}\ #4} \newcommand{\override}{\ \mathsf{override}\ } \newcommand{\loc}[1]{l_{#1}} \]

Typing relation. Usually written \(\type{\Gamma}{e}{\tau}\), where \(\Gamma\) is a map from identifiers to types, \(e\) is an expression, and \(\tau\) is a type.

\(\type{\mathrm{Type Context}}{\mathrm{Expression}}{\mathrm{Type}}\)

Anonymous function.

\(\abs{\mathrm{Parameter Name}}{\mathrm{Parameter Type}}{\mathrm{Body}}\)

Type abstraction.

\(\tabs{\mathrm{Type Variable}}{\mathrm{Body}}\)

Function type.

\(\mathrm{Parameter Type} \arrow \mathrm{Return Type}\)

Subtyping relation.

Read \(\tau \subt \tau'\) as: \(\tau\) is a subtype of \(\tau'\). If \(\tau\) and \(\tau'\) are records, \(\tau\) has a superset of the fields in \(\tau'\). Alternatively, anything that expects a \(\tau'\) can take a \(\tau\).

In our discussion of semantics, we have allowed the evaluation of terms to fail, or to get stuck. For example, the following term is allowed by the syntax of IMP, but our semantics don't describe what happens if we end up with an integer in the condition of an if-then-else: 

if 1 + 2 then
  x := 1;
else
  x := 2;

We don't have a rule that reduces an if-then-else with an integer, so we can't prove that this term evaluates to a final state. If we could prove that the condition expression always evaluates to a boolean, then we would know that we could always reduce the if-then-else.

In general, we'd like to be able to check whether a term will get stuck or not before we run it. This is helpful for the programmer, because a term that gets stuck is semantically meaningless. Also, we can often implement a more efficient evaluation strategy if we know that we only need to evaluate terms that do not get stuck.

A type system is a mechanism for determining whether a term will get stuck, without actually evaluating the term. It's impossible in general to answer this question precisely (at least for Turing-complete languages---Rice's Theorem), but we can approximate it. This means that any type system we build will have some perfectly fine terms that it does not accept.

Type systems work by classifying the values that result from evaluation using a language of "value schemas" or types. A type system relates terms to types in the way that a semantics relates terms to values. This relation should have the property that if a term \(t\) has type \(\tau\), then \(t\) always evaluates to a value that has type \(\tau\). If a term \(t\) has type \(\tau\), then we say that \(t\) is well-typed with respect to \(\tau\).

In these notes, we'll discuss and formalize some type systems. We'll see that the formal tools we've developed so far give us everything we need to build type systems.

Simple types

We'll start by considering simple types, which are types that contain no quantifiers.

We'll add types to an extended lambda-calculus with integers, booleans, and records. The syntax of this language is as follows:

\begin{align*} \oplus ::=&\quad = ~|~ < ~|~ > ~|~ + ~|~ - ~|~ * ~|~ / ~|~ \mathsf{and} ~|~ \mathsf{or} && \text{operators} \\ e ::=&\quad x && \text{variable} \\ &|\quad n &&\text{integer} \\ &|\quad b &&\text{boolean} \\ &|\quad e\ e &&\text{application} \\ &|\quad \lambda x : \tau.\ e &&\text{function abstraction} \\ &|\quad \mathsf{if}\ e\ \mathsf{then}\ e\ \mathsf{else}\ e &&\text{conditional} \\ &|\quad e \oplus e &&\text{operator application} \\ &|\quad \{ {x_{i} = e_{i}}^{i \in 1 \dots n} \}&&\text{record} \\ &|\quad e.x&&\text{field access} \\ \tau ::=&\quad \Int && \text{integer type} \\ &|\quad \Bool && \text{boolean type} \\ &|\quad \tau \arrow \tau && \text{function type} \\ &|\quad \{ {x_{i}:\tau_{i}}^{i \in 1 \dots n} \}&&\text{record type} \end{align*}

We add records mostly for the discussion of subtyping later, but they're easy enough to include in the simple type system as well. Records have two operations: creation and field acccess. The semantics of records are as follows:

\begin{gather} \tag{E-Proj-1} \frac{}{\{ {x_{i} = v_{i}}^{i \in [1,n]} \} \proj x_{j} \Downarrow v_{j}} \\[2ex] \tag{E-Proj-2} \frac{e \Downarrow v}{e \proj x \Downarrow v \proj x} \\[2ex] \tag{E-Record} \frac{ \text{for all}\ i \in [1,n],\ e_{i} \Downarrow v_{i} }{\{{x_{i} = e_{i}}^{i \in [1,n]} \} \Downarrow \{ {x_{i} = v_{i}}^{i \in [1,n]} \}} \end{gather}

Essentially, record creation forces the field values to be evaluated, and projection (or field access) is only possible when the record contains a field with the right name. The semantics of the rest of the language are standard.

Note the modification of function abstraction to include a type annotation for the parameter. This is the only place that type annotations are needed in this language.

Here are a few examples of terms in this language:

  • \(\abs{x}{\Int}{x}\) is the identity function (but only for integers).
  • \(\abs{f}{\Int \arrow \Bool}{\abs{x}{\Int}{\mathsf{if} \ f \ x \ \mathsf{then} \ \mathsf{true} \ \mathsf{else} \ \mathsf{false}}}\) is a function that takes an integer predicate and returns a function that takes an integer and returns whether the integer satisfies the predicate.
  • \(\abs{x}{\Int}{\abs{y}{\Int}{\abs{k}{\Int \arrow \Int}{k\ (x + y)}}}\) is a continuation-passing style function that takes two integers and a continuation, and passes the sum of the two integers to the continuation.

Simple typing is painfully restrictive, even in these simple examples. The identity function should work for any type, not just integers. Similarly, the second function should work for any type of predicate, and the third function should work for any type of continuation.

We define a typing relation \(\type{\Gamma}{e}{\tau}\) that relates expressions \(e\) to types \(\tau\) in a context \(\Gamma\). The context \(\Gamma\) is a map from identifiers to types.

The typing relation is similar to the evaluation relations that we have seen before. The evaluation relations relate expressions to values in a context \(\sigma\), whereas the typing relation relates expressions to types.

The typing relation is defined as follows:

\begin{gather} \tag{T-Abs} \frac{\type{\Gamma, x:\tau}{e}{\tau'}}{\type{\Gamma}{(\abs{x}{\tau}{e})}{\tau \arrow \tau'}} \\[2ex] \tag{T-App} \frac{\type{\Gamma}{e}{\tau' \arrow \tau} \quad \type{\Gamma}{e'}{\tau'}}{\type{\Gamma}{e\ e'}{\tau}} \\[2ex] \tag{T-If} \frac{ \type{\Gamma}{e}{\Bool} \quad \type{\Gamma}{e'}{\tau} \quad \type{\Gamma}{e''}{\tau} }{ \type{\Gamma}{\mathsf{if}\ e\ \mathsf{then}\ e'\ \mathsf{else}\ e''}{\tau} } \\[2ex] \tag{T-Var} \frac{ x : \tau \in \Gamma }{ \type{\Gamma}{x}{\tau} } \\[2ex] \tag{T-Int} \type{\Gamma}{n}{\Int} \\[2ex] \tag{T-Bool} \type{\Gamma}{b}{\Bool} \\[2ex] \tag{T-Eq} \frac{ \type{\Gamma}{e}{\tau} \quad \type{\Gamma}{e'}{\tau} }{ \type{\Gamma}{e = e'}{\Bool} } \\[2ex] \tag{T-Arith-op} \frac{ \type{\Gamma}{e}{\Int} \quad \type{\Gamma}{e'}{\Int} \quad \oplus \in \{ +, -, *, / \} }{ \type{\Gamma}{e \oplus e'}{\Int} } \\[2ex] \tag{T-Bool-op} \frac{ \type{\Gamma}{e}{\Bool} \quad \type{\Gamma}{e'}{\Bool} \quad \oplus \in \{ \mathsf{and}, \mathsf{or} \} }{ \type{\Gamma}{e \oplus e'}{\Bool} }\\[2ex] \tag{T-Cmp-op} \frac{ \type{\Gamma}{e}{\Int} \quad \type{\Gamma}{e'}{\Int} \quad \oplus \in \{ =, <, > \} }{ \type{\Gamma}{e \oplus e'}{\Bool} } \\[2ex] \tag{T-Record} \frac{\text{for all}\ i \in [1,n],\ \type{\Gamma}{e_{i}}{\tau_{i}}}{\type{\Gamma}{\{ {x_{i} = e_{i}}^{i \in [1,n]} \}}{ \{ {x_{i} : \tau_{i}}^{i \in [1,n]} \}}}\\[2ex] \tag{T-Proj} \frac{\type{\Gamma}{e}{\{{x_{i}:\tau_{i}}^{i \in [1,n]}\}}}{\type{\Gamma}{e \proj x_{j}}{\tau_{j}}} \end{gather}

You can generate a simple type derivation for a term using this live block:

term = App(Lam("x", IntT(), If(Prim(">", [Var("x"), Int(0)]), Bool(False), Bool(True))), Int(2)) simple_type_deriv({}, term)

Help

Parametric polymorphism

We can address some of the restrictiveness of the simply typed lambda calculus by introducing polymorphism. A polymorphic term can take on different types in different program contexts. Fundamentally, polymorphism is a tool for reducing duplication in a program. It doesn't necessarily make the language more expressive—we can often remove polymorphic types from a program by creating a monomorphic version of each polymorphic term for the relevant contexts (this is sometimes used as a compilation strategy—e.g. C++ templates).

In this section, we discuss parametric polymorphism. Parametric polymorphism adds type variables and allows terms to take on different types by instantiating their type variables. Many languages provide this feature—it's often called generics.

The key extension to the STLC is a new kind of abstraction that allows types to have parameters. We write a type abstraction as \(\tabs{\alpha}{e}\). This abstraction allows \(e\) to have a type that depends on the parameter \(\alpha\). Type abstraction is analogous to lambda abstraction and has similar rules for application. If we consider the identity function \(I_{untyped} = \lambda x.\ x\), we can write it as \(I_{poly} = \tabs{\alpha}{\abs{x}{\alpha}{x}}\), which says that the identity can take any type \(\alpha\). We instantiate the identity for a particular type by applying it: \(I_{poly}[\Int]\) is the identity for integers, \(I_{poly}[\Bool]\) is the identity for Booleans, etc.

The syntax of the polymorphic lambda calculus (also called System F) is:

\begin{align*} \oplus ::=&\quad = ~|~ < ~|~ > ~|~ + ~|~ - ~|~ * ~|~ / ~|~ \mathsf{and} ~|~ \mathsf{or} && \text{operators} \\ e ::=&\quad x && \text{variable} \\ &|\quad n &&\text{integer} \\ &|\quad b &&\text{boolean} \\ &|\quad e\ e &&\text{application} \\ &|\quad \lambda x:\tau.\ e &&\text{function abstraction} \\ &|\quad \mathsf{if}\ e\ \mathsf{then}\ e\ \mathsf{else}\ e &&\text{conditional} \\ &|\quad e \oplus e &&\text{operator application} \\ &|\quad \boxed{\Lambda \alpha.\ e}&&\text{type abstraction} \\ &|\quad \boxed{e [\tau]} &&\text{type application} \\ &|\quad \{ {x_{i} = e_{i}}^{i \in 1 \dots n} \}&&\text{record} \\ &|\quad e.x&&\text{field access} \\ \tau ::=&\quad \Int && \text{integer type} \\ &|\quad \Bool && \text{boolean type} \\ &|\quad \tau \arrow \tau && \text{function type} \\ &|\quad \{ {x_{i}:\tau_{i}}^{i \in 1 \dots n} \}&&\text{record type} \\ &|\quad \boxed{\alpha} &&\text{type variable} \\ &|\quad \boxed{\forall \alpha. \tau} &&\text{universal type} \end{align*}

New constructs are boxed. We add type abstraction and application to the term grammar, and type variables and universal types to the type grammar.

The typing rules are actually only a slight extension to the rules for the STLC. We have a type abstraction rule that mirrors the evaluation rule for lambda abstraction (note the extension of the type context, which mirrors the binding of the lambda parameter in the evaluation rule). The type application rule mirrors the rule for function application: to be applied, a term must have a universal type, and application proceeds by substituting the concrete type for the type variable.

\begin{gather} \tag{T-TypeAbs} \frac{\type{\Gamma, \alpha}{e}{\tau}}{\type{\Gamma}{\tabs{\alpha}{e}}{\forall \alpha.\ \tau}}\\[2ex] \tag{T-TypeApp} \frac{\type{\Gamma}{e}{\forall \alpha.\ \tau}}{\type{\Gamma}{e[\tau']}{\tau[\alpha \mapsto \tau']}} \\[2ex] \end{gather}

With this extension, we gain a significant amount of expressiveness.

term = TypeAbs("a", Lam("x", VarT("a"), Var("x"))) poly_type_deriv({}, term)

Help

Subtyping

Now we consider subtype polymorphism. Imagine that we have a function that takes records as input. It accesses the field a, which it expects to be an integer, and no other fields. Intuitively, it shouldn't matter what else the record contains, as long as it has a field a with the right type.

Neither of our previous type systems can express this intuition. If we try to use parametric polymorphism, we might write \(\Lambda \alpha.\ \lambda x:\alpha.\ x \proj a\). Of course, that doesn't (and shouldn't) type check, because we can't pass any type \(\alpha\) to this function and expect it to work. Our language of types doesn't have a way to express the constraint "this function must take a record that has at least a field a of type int." (We can actually extend parametric polymorphism to allow for constraints like this—see row polymorphism—but it's not something we'll cover in this course.)

Subtyping Relation

We introduce subtyping, which is a new relation between types that expresses the intuition that it's safe to substitute a record with more fields in a context that expects fewer. We write "\(\tau\) is a subtype of \(\tau'\)" as \(\tau \subt \tau'\).

The syntax of the lambda calculus with subtyping is exactly the same as the simply typed calculus presented above. Even the type system remains mostly the same, just with some additional rules that enable subtyping.

Subtyping rules:

\begin{gather} \tag{T-Sub} \frac{\type{\Gamma}{e}{\tau'} \qquad \tau' \subt \tau}{\type{\Gamma}{e}{\tau}}\\[2ex] \tag{S-Refl} \tau \subt \tau\\[2ex] \tag{S-Trans} \frac{\tau_{1} \subt \tau_{2} \qquad \tau_{2} \subt \tau_{3}}{\tau_{1} \subt \tau_{3}} \\[2ex] \tag{S-Top} \tau \subt \top \\[2ex] \tag{S-Func} \frac{\tau_{1}' \subt \tau_{1} \qquad \tau_{2} \subt \tau_{2}'}{\tau_{1} \arrow \tau_{2} \subt \tau_{1}' \arrow \tau_{2}'} \\[2ex] \tag{S-Record} \frac{ \begin{gathered} \{ {x_{i}}^{i \in [1,n]} \} \subseteq \{ {x_{j}'}^{j \in [1, m]} \} \\ \text{for all}\ i \in [1,n], j \in [1, m],\ x_{i} = x_{j}' \implies \tau_{i} \subt \tau_{j}' \end{gathered} }{ \{ {x_{i}:\tau_{i}}^{i \in [1,n]} \} \subt \{ {x_{j}':\tau_{j}'}^{j \in [1,m]} \} } \end{gather}

The record subtyping rule is the most complex by far. Intuitively, \(\tau_{a}\) is a subtype of \(\tau_{b}\) if we could substitute a \(\tau_{a}\) for a \(\tau_{b}\) without any code noticing the difference. For records, this means that the subtype must have every field that the supertype does. It can have more, but it can't have fewer. In addition, for the fields that are shared, the subtype field must be a subtype of the supertype field.

It's easiest to see how this rule works with an example: \[ \underbrace{\{ x : \{ b : \Bool, a : \Int \}, y : \Int \}}_{\tau_{a}} \subt \underbrace{\{ x : \{ a : \Int \} \}}_{\tau_{b}} \] \(\tau_{a}\) has all the required fields (just \(x\)). In addition, \(\{ a : \Int, b : \Bool \} \subt \{ a : \Int \}\), so the types of the shared fields are compatible. If we consider a piece of code that takes a \(\tau_{b}\), it can only access fields \(x\) and \(a\). \(\tau_{a}\) provides both of those fields (and a few extra), so it can be passed into this code safely.

Demo

Annoyingly, these rules are not suitable for implementation in the way that we've implemented simple and polymorphic types. The rules in these other systems are syntax-directed, which means that only one rule applies to a particular judgement \(\type{\Gamma}{e}{\tau}\). The rules for subtyping don't have this property. In particular, the T-Sub rule always applies, because the conclusion of the rule matches any type judgement. The rule for transitivity of subtyping (S-Trans) has the same problem. There is a way to refactor the rules into a syntax-directed form,1 but we won't describe it in detail.

You can view subtyping derivations using the following live code block. Here are a few terms you could try:

  • Passing a record to a function that expects a supertype: 

    App(Lam("r", RecordT({"x": IntT()}), Proj(Var("r"), "x")),
    Record({"x": Int(1), "y":Int(2)}))

  • The example from above: 

    App(Lam("r", RecordT({"x": RecordT({"a": IntT()})}), Var("r")),
    Record({"x": Record({"b": Bool(True), "a": Int(0)}), "y":Int(2)}))

  • An if-then-else that produces one of two functions: 

    term = If(Var("x"),
	  Lam("y", RecordT({"a":IntT()}), Record({"q": Int(1)})),
	  Lam("z", RecordT({"b":BoolT()}), Record({"r": Bool(True), "q": Int(2)}))))

sub_type_deriv({"x": BoolT()}, term)

    Notice that to call the resulting function, we have to pass a subtype of both argument types, and we receive a supertype of both return types. The most specific supertype \(\tau\) of types \(\tau_1\) and \(\tau_2\) is called the join; we write the join of two types as \(\tau_1 \land \tau_2\). The most general subtype type \(\tau\) of types \(\tau_1\) and \(\tau_2\) is called the meet; we write the meet as \(\tau_1 \lor \tau_2\). Every pair of types in our type system has a join (because we include a top type, which is a supertype of all types). However, not every pair has a meet (for example, there is no type that is a subtype of both \(\Int\) and \(\Bool\)). We use the join and meet operations inside the type checker to compute the most general type to give if-then-else terms. (Since our types are (partially) ordered by the subtyping relation and have joins but not meets, they form a join-semilattice—a special kind of partial order. Partial orders have a special place in programming languages theory. You will encounter many more of them if you continue to study PL.)

term = Lam("x", IntT(), If(Prim(">", [Var("x"), Int(0)]), Record({"x": Var("x"), "y": Int(1)}), Record({"y": Int(2), "x": Var("x"), "z": Int(3)}))) sub_type_deriv({}, term)

Help

Properties of Type Systems

Progress

Preservation

Implementation

You can download the code for these notes here.

References & Further Reading

Footnotes:

1

See "Types and Programming Languages" Ch. 16 for details.

Last updated: 2023-05-05 Fri 17:43