How should I read type system notation?

Question

I sometimes read articles or papers about type systems that use some funny-looking, two-dimensional notation with lots of unfamiliar symbols and Greek letters. The notation seems mathematical, but it’s entirely unlike any mathematics I learned in school. It’s quite intimidating, and I don’t even know where to start.

How should I read this notation? What does it mean?

Answer 1

The notation used to describe type systems varies from presentation to presentation, so giving a comprehensive overview is impossible. However, most presentations share a large, common subset, so this answer will attempt to provide a foundation of enough of the basics to understand variations on the common theme.

Syntax and grammars

Type systems as applied to programming language are syntactic systems. That is, a type system is a set of rules that operate on the (abstract) syntax of a programming language. For this reason, comprehensive treatments of type systems begin by providing the grammar of all the syntactic constructs considered by the type system using BNF notation. In the simplest typed languages, syntax is needed for precisely two things: expressions and types.

For example, let’s consider the grammar for an extremely simple language of booleans and integers: $$ \begin{array}{rcll} e \hskip{-10mu} &::=&\hskip{-10mu} \mathsf{true}\hskip{10mu}|\hskip{10mu}\mathsf{false} &\textrm{boolean literal}\\ & | &\hskip{-10mu} 0 \hskip{5mu}|\hskip{5mu} 1 \hskip{5mu}|\hskip{5mu} {-1} \hskip{5mu}|\hskip{5mu} 2 \hskip{5mu}|\hskip{5mu} {-2} \hskip{5mu}|\hskip{5mu} \ldots &\textrm{integer literal}\\ & | &\hskip{-10mu} \mathbf{if}\ e\ \mathbf{then}\ e\ \mathbf{else}\ e &\textrm{conditional}\\ & | &\hskip{-10mu} e + e \hskip{10mu}|\hskip{10mu} e - e \hskip{10mu}|\hskip{10mu} e × e &\textrm{arithmetic}\\ & | &\hskip{-10mu} e = e \hskip{10mu}|\hskip{10mu} e < e \hskip{10mu}|\hskip{10mu} e > e &\textrm{comparison}\\[8pt] \tau \hskip{-10mu} &::=&\hskip{-10mu} \mathsf{Bool} &\textrm{booleans}\\ & | &\hskip{-10mu} \mathsf{Int} &\textrm{integers} \end{array} $$ Here, $e$ corresponds to an expression and $\tau$ corresponds to a type, which is a standard notational convention. Some presentations use other symbols for types, such as $t$, $T$, $\sigma$, or other lowercase Greek letters, but the overall structure will look roughly the same.

More complex languages will naturally have more complex grammars: imperative languages will include the grammar of statements, languages with pattern-matching will include the grammar of patterns, and so on. This language is so simple that it doesn’t even have variables! However, this core syntactic division between terms (things that have types) and types is essential, as defining the relationship between them is what type systems are all about.

Relations, judgments, axioms, and inference rules

Once the grammar has been specified, the next step is to define the typing relation, which is generally written $e : \tau$ and can be read “$e$ has type $\tau$”. Intuitively, we understand that some statements of this form “make sense” and others do not:

• $1 + 2 : \mathsf{Int}$ means “$1 + 2$ has type $\mathsf{Int}$”, which certainly makes sense.

• $1 + 2 : \mathsf{Bool}$ means “$1 + 2$ has type $\mathsf{Bool}$”, which does not make sense.

• $\mathsf{true} + 2 : \mathsf{Int}$ means “$\mathsf{true} + 2$ has type $\mathsf{Int}$”, which makes even less sense, as the expression $\mathsf{true} + 2$ is nonsense and does not have any type at all.

We’d like to write down some rules that precisely capture our intuitions about which statements “make sense” and which do not. To do this, we’ll define the typing judgment, which is written using the following notation: $$ ⊢ e : \tau $$ Here, the $⊢$ can be read to mean “the following statement is true”. (The $⊢$ might seem a bit unnecessary, and indeed it is sometimes omitted in simple systems like this one, but it will play a more significant role later.) Using this notation, we can write down the some of the typing rules for our type system: $$ \begin{array}{l}\hline ⊢ \mathsf{true} : \mathsf{Bool}\end{array} \quad \quad \begin{array}{l}\hline ⊢ \mathsf{false} : \mathsf{Bool}\end{array} $$ The horizontal bar over each of these rules with nothing on top means that they are always true, which makes them axioms. We also have an infinite number of similar axioms for integer literals: $$ \begin{array}{l}\hline ⊢ 0 : \mathsf{Int}\end{array} \quad \begin{array}{l}\hline ⊢ 1 : \mathsf{Int}\end{array} \quad \begin{array}{l}\hline ⊢ -1 : \mathsf{Int}\end{array} \quad \begin{array}{l}\hline ⊢ 2 : \mathsf{Int}\end{array} \quad \cdots $$

Of course, the typing rules for literals are fairly boring. Things get much more interesting when we consider rules for expressions that have subexpressions! Here are the typing rules for $+$ and $<$: $$ \begin{array}{l} ⊢ e_1 : \mathsf{Int} \\ ⊢ e_2 : \mathsf{Int} \\ \hline ⊢ e_1 + e_2 : \mathsf{Int} \end{array} \quad \quad \quad \begin{array}{l} ⊢ e_1 : \mathsf{Int} \\ ⊢ e_2 : \mathsf{Int} \\ \hline ⊢ e_1 < e_2 : \mathsf{Bool} \end{array} $$ Now we have things both above and below the horizontal bars, which makes these inference rules. These represent conditional typing rules: the statement under the bar is true if all of the statements above the bar are true. For example, the first rule can be read as “if $e_1 : \mathsf{Int}$ and $e_2 : \mathsf{Int}$ are true, then $e_1 + e_2 : \mathsf{Int}$ is true,” which should hopefully make intuitive sense.

Rules for $-$, $×$, $=$, and $>$ are nearly identical to the ones given above, but the rule for $\mathbf{if} \ldots \mathbf{then} \ldots \mathbf{else}$ must be slightly more complex. This is because the branches of these expressions can be any type, as long as they agree. That is, both $$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ 2 $$ and $$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ \mathsf{false}\ \mathbf{else}\ \mathsf{true} $$ are legal, but $$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ \mathsf{true} $$ is not. To capture this, the typing rule uses a variable to stand for the type of the branches: $$ \begin{array}{l} ⊢ e_1 : \mathsf{Bool} \\ ⊢ e_2 : \tau \\ ⊢ e_3 : \tau \\ \hline ⊢ \mathbf{if}\ e_1\ \mathbf{then}\ e_2\ \mathbf{else}\ e_3 : \tau \end{array} $$ When the rule is applied, any type may be picked for $\tau$ as long as the choice is used consistently.

This notation originates in formal logic, and in particular, the style used to specify type systems most closely resembles natural deduction. Though I will not go into the formal details of the notation in this answer, rules expressed in this way can be used to construct formal proofs about the system’s properties, which is important for proving things like type soundness.

Judgments as an algorithmic specification

So far, I’ve intentionally refrained from saying anything about the computational interpretation of typing judgments. In general, judgments are just logical rules, and some type systems specified this way do not directly correspond to a decidable typechecking algorithm. However, if you are not used to thinking about proof systems, this perspective can be extremely difficult to wrap your head around.

Fortunately, in many cases, there is a way to read typing rules that directly yields a typechecking algorithm: it’s possible to interpret $⊢ e : \tau$ as a function from an expression $e$ to its type $\tau$. This is because there is usually exactly one rule defined for each case in the grammar of expressions, which makes it possible to think of each typing rule as a distinct case in a recursive typechecking function.

For example, consider the rules for our little language given above. They correspond directly to an $\mathrm{infer}$ function with the following shape: $$ \begin{array}{l} \mathrm{infer} : \mathsf{Expr} → \mathsf{Type} \\ \mathrm{infer}(e) = \mathbf{match}\ e\ \mathbf{where} \\ \quad \begin{alignedat}{2} &\mathsf{true}\ |\ \mathsf{false} &&↦ \mathsf{Bool} \\ &0\ |\ 1\ |\ {-1}\ |\ 2\ |\ \ldots &&↦ \mathsf{Int} \\ &e_1 + e_2 &&↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Int}; \\ &&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_2) = \mathsf{Int}; \\ &&&\phantom{{}↦{}} \mathsf{Int} \\ &e_1 < e_2 &&↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Int}; \\ &&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_2) = \mathsf{Int}; \\ &&&\phantom{{}↦{}} \mathsf{Bool} \\ &\mathbf{if}\ e_1\ \mathbf{then}\ e_2\ \mathbf{else}\ e_3 &&↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Bool}; \\ &&&\phantom{{}↦{}} \mathbf{let}\: \tau = \mathrm{infer}(e_2); \\ &&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_3) = \tau; \\ &&&\phantom{{}↦{}} \tau \end{alignedat} \end{array} $$

Even when it isn’t possible to perform such a direct translation from typing rules to typechecking algorithm, it can be extremely helpful to consider information flow when reasoning about logical judgments. That is, for the $⊢ e : \tau$ judgment we defined above, $e$ can be considered an “input” to the judgment and $\tau$ considered an “output”. This strict directionality does not always apply to every rule in a type system, but it often applies to many of them, and it is a useful way to wrap your head around what the rules represent.

Variables, contexts, and environments

The language we’ve been using as a running example so far is exceptionally simple. One complication I’ve intentionally chosen to avoid so far is variables, but we need to consider them if we want to be able to write typing rules for any useful programming language. Let’s therefore expand our example language by adding functions, making it a variant of the simply typed lambda calculus (STLC). This requires the following additions to the language’s grammar: $$ \begin{array}{rcll} e \hskip{-10mu} &::=&\hskip{-10mu}\ldots\\ & | &\hskip{-10mu} x &\textrm{variable}\\ & | &\hskip{-10mu} λx{:}\tau. e &\textrm{function abstraction}\\ & | &\hskip{-10mu} e\ e &\textrm{function application}\\[8pt] \tau \hskip{-10mu} &::=&\hskip{-10mu}\ldots\\ & | &\hskip{-10mu} \tau → \tau &\textrm{functions} \end{array} $$ Here, $x$ stands for “some variable”. If you are unfamiliar with the lambda calculus, the notation used here might appear somewhat exotic, but it is likely not as foreign as it seems: the STLC syntax $λx{:}\tau. e$ corresponds directly to (x:τ) => e in TypeScript, and $f\ x$ corresponds to f(x).

With these additions to our grammar, the notation used for our typing relation does not change—it’s still just $e : \tau$—but the structure of our typing judgment must be extended. The trouble appears when we attempt to write a typing rule for variables: $$ \begin{array}{l} \hline ⊢ x : \text{???} \end{array} $$ The problem is that the type of a variable depends on the context it appears in. Therefore, we need to extend the typing judgment to keep track of the types of all variables that happen to be in scope, which we do using the following notation: $$ Γ ⊢ e : \tau $$ $Γ$ is called “the context” or “the type environment”, and the role of the $⊢$ now becomes clearer: it separates contextual assumptions from the statement to be proved. The extended judgment can therefore be pronounced “under the context $Γ$, the expression $e$ has type $\tau$”, and algorithmically, $Γ$ can be considered an additional “input” to the judgment of type Map<Variable, Type>. However, formally speaking, every typing rule must be defined syntactically, so contexts are explicitly represented in typing rules as syntactic constructs with the following shape: $$ \begin{array}{rcll} Γ \hskip{-10mu} &::=&\hskip{-10mu} \varnothing &\textrm{empty context}\\ & | &\hskip{-10mu} Γ, x{:}\tau &\textrm{variable binding} \end{array} $$ Sometimes $\bullet$ is used instead of $\varnothing$ to represent the empty context. Under this representation, a context is essentially an association list mapping variable names to types.

Most typing rules have no reason to care about the context. Most inference rules just pass it along unaltered, and most axioms ignore it altogether. For example, here are a couple typing rules from above adapted to our new judgment: $$ \begin{array}{l}\hline Γ ⊢ \mathsf{true} : \mathsf{Bool} \end{array} \quad \quad \begin{array}{l} Γ ⊢ e_1 : \mathsf{Int} \\ Γ ⊢ e_2 : \mathsf{Int} \\ \hline Γ ⊢ e_1 + e_2 : \mathsf{Int} \end{array} $$ However, the context is essential for two new typing rules, which handle variable uses and lambda expressions: $$ \begin{array}{l} x{:}\tau \in Γ \\ \hline Γ ⊢ x : \tau \end{array} \quad \quad \begin{array}{l} Γ,x{:}\tau_1 ⊢ e : \tau_2 \\ \hline Γ ⊢ (λx{:}\tau_1. e) : \tau_1 → \tau_2 \end{array} $$ The second of these two rules is the more complex one, as it’s where all the magic happens: while typechecking the body $e$ of the lambda expression, the context is extended with a new binding $x{:}\tau_1$. This information is then utilized by the first rule, which says that if there is a variable binding $x$ with type $\tau$ in the current context (and therefore in scope), then $x$ has type $\tau$. In other words, the context is used as a communication mechanism to propagate information between these two rules.

(Observant readers may note that this model does not handle variable shadowing. As a simplifying assumption, type systems specified this way usually assume that all variables have already been resolved and made unique.)

If this still seems a bit confusing to you, it may help to consider the way these additions affect our $\mathrm{infer}$ function from earlier: $$ \begin{array}{l} \mathrm{infer} : (\mathsf{Context}, \mathsf{Expr}) → \mathsf{Type} \\ \mathrm{infer}(Γ, e) = \mathbf{match}\ e\ \mathbf{where} \\ \quad \begin{alignedat}{2} &\ldots\\ &x &&↦ \mathrm{lookup}(Γ, x) \\ &(λx{:}\tau_1. e') &&↦ \mathbf{let}\: Γ' = \mathrm{extend}(Γ, x, \tau_1); \\ &&&\phantom{{}↦{}} \mathbf{let}\: \tau_2 = \mathrm{infer}(Γ', e'); \\ &&&\phantom{{}↦{}} \mathsf{\tau_1 → \tau_2} \end{alignedat} \end{array} $$

The only remaining rule we need to add to cope with the addition of functions is a rule for function application: $$ \begin{array}{l} Γ ⊢ e_1 : \tau_1 → \tau_2 \\ Γ ⊢ e_2 : \tau_1 \\ \hline Γ ⊢ e_1\ e_2 : \tau_2 \end{array} $$ That’s it!

Other common notation and considerations

The above describes the large majority of notation used to specify type systems if measured by volume, but modifications and extensions to this foundation are extremely common. It would be impossible to cover all of them, but fortunately, good papers usually explain whatever nonstandard notation they choose to introduce. However, some conventions are common enough that they are often used without explanation; this section attempts to provide a basic survey and describe a few notational quirks.

Since this is not and can never be an exhaustive list, please open a separate question if you find some notation not covered here!

Inference rule layout

So far, all of the examples in this answer have laid out inference rules in a very regular, vertical way. However, placing each condition on its own line is not by any means required, so several conditions may appear side-by-side: $$ \begin{array}{c} Γ ⊢ e_1 : \mathsf{Int} \hskip{25mu} Γ ⊢ e_2 : \mathsf{Int} \\ \hline Γ ⊢ e_1 + e_2 : \mathsf{Int} \end{array} $$ Vertical and horizontal arrangement may even be combined within the same rule.

Side conditions

Usually, the conditions that appear above the horizontal bar in an inference rule are themselves judgments that must be satisfied by some combination of inference rules and axioms. However, this is not always the case: rules may also include arbitrary boolean expressions known as side conditions, which must all be true in order for the rule to be applied. The $x{:}\tau \in Γ$ condition in our typing rule for variables is an example of a side condition.

A special type of side condition that sometimes appears in algorithmic type systems is written $\alpha\ \mathbf{fresh}$. This means that $\alpha$ should be a fresh type variable, i.e. a type variable distinct from all other type variables.

Subtyping

Subtyping introduces a weaker notion of consistency between types than strict equality, and the subtyping relation must be explicitly defined. It is usually denoted $\tau_1 <: \tau_2$, which can be read as “$\tau_1$ is a subtype of $\tau_2$”.

The relation is often defined using the same syntax used to define judgments. For example, a very simple subtyping relation might introduce two special types, $\top$ (pronounced “top”) and $\bot$ (pronounced “bottom”), which are the supertype and subtype of all types, respectively. This relation can be expressed using three simple axioms: $$ \begin{array}{l}\hline \tau <: \tau \end{array} \quad \quad \begin{array}{l}\hline \tau <: \top \end{array} \quad \quad \begin{array}{l}\hline \bot <: \tau \end{array} $$ The first rule is the reflexive rule, often abbreviated to “refl”, which states that every type is a subtype of itself and ensures that subtyping is strictly weaker than equality.

The defined subtyping relation must then be used explicitly in every rule that permits subtyping. For example, a system that supports subtyping might use the following rule for function application: $$ \begin{array}{l} Γ ⊢ e_1 : \tau_2 → \tau_3 \\ Γ ⊢ e_2 : \tau_1 \\ \tau_1 <: \tau_2 \\ \hline Γ ⊢ e_1\ e_2 : \tau_3 \end{array} $$

Multiple contexts

Some type systems define typing judgments involving more than one context. The second context is usually named $Δ$. Common notations for multi-context rules are $Γ;Δ ⊢ e : \tau$ (used when both contexts are morally “inputs”) and $Γ ⊢ e : \tau ⊣ Δ$ (used when $Δ$ is morally an “output”).

The second context may be used for any number of different things. Perhaps certain variables can be referenced from inside certain expressions but not others, or perhaps an output context is used to keep track of which variables are “consumed” in a resource-aware programming language.

Bidirectional typechecking

Bidirectional typechecking is an approach for performing a limited form of nonlocal type inference without the need to use a constraint solver. A bidirectional system splits the usual $Γ ⊢ e : \tau$ typing judgment into two specialized judgments:

• $Γ ⊢ e ⇐ \tau$ is the checking judgment, which checks that $e$ has some expected type $\tau$. Algorithmically, $\tau$ is an input to this judgment.

• $Γ ⊢ e ⇒ \tau$ is the inference judgment, which is used whenever expected type information is not available. Algorithmically, $\tau$ is an output from this judgment.

The two judgments are defined in a mutually-recursive way to propagate type information bidirectionally, which allows some type annotations to sometimes be omitted. For example, the checking variant of the rule for lambda abstraction may omit the annotation on the variable binder since it can be determined from the expected type: $$ \begin{array}{c} Γ,x{:}\tau_1 ⊢ e ⇐ \tau_2 \\ \hline Γ ⊢ (λx. e) ⇐ \tau_1 → \tau_2 \end{array} $$