## Understanding typing judgments

### Introduction

For many people interested in type systems and type theory, their first encounter with the literature presents them with this:

frac(Gamma,x:tau_1 $--_Sigma e : tau_2)(Gamma$--_Sigma (lambda x:tau_1.e) : tau_1 -> tau_2) ->I

frac(Gamma $--_Sigma f : tau_1 -> tau_2 \qquad Gamma$--_Sigma x : tau_1)(Gamma $--_Sigma f x : tau_2) ->E Since this notation is ubiquitous, authors (reasonably) expect readers to already be familiar with it and thus provide no explanation. Because the notation is ubiquitous, the beginner looking for alternate resources will not escape it. All they will find is that the notation is everywhere but exists in myriad minor variations which may or may not indicate significant differences. At this point the options are: 1) to muddle on and hope understanding the notation isn’t too important, 2) look for introductory resources which typically take the form of 50+ 500+ page textbooks, or 3) give up. The goal of this article is to explain the notation part-by-part in common realizations, and to cover the main idea behind the notation which is the idea of an inductively defined relation. To eliminate ambiguity and make hand-waving impossible, I’ll ground the explanations in code, in particular, in Agda. That means for each example of the informal notation, there will be how it would be realized in Agda.1 It will become clear that I’m am not (just) using Agda as a formal notation to talk about these concepts, but that Agda’s2 data type mechanism directly captures them3. The significance of this is that programmers are already familiar with many of the ideas behind the informal notation, and the notation is just obscuring this familiarity. Admittedly, Agda is itself pretty intimidating. I hope most of this article is accessible to those with familiarity with algebraic data types as they appear in Haskell, ML, Rust, or Swift with little to no need to look up details about Agda. Nevertheless, Agda at least has the benefit, when compared to the informal notation, of having a clear place to go to learn more, an unambiguous meaning, and tools that allow playing around with the ideas. ### Parsing and reading To start, if you are not already familiar with it, get familiar with the Greek alphabet. It will be far easier to (mentally) read mathematical notation of any kind if you can say “Gamma x” rather than “right angle thingy x” or “upside-down L x”. Using the example from the introduction, the whole thing is a rule. The “$->I$” part is just the name of the rule (in this case being short for “$->$Introduction”). This rule is only part of the definition of the judgment of the form: Gamma$--_Sigma e : tau

The judgment can be viewed as a proposition and the rule is an “if-then” statement read from top to bottom. So the “$->I$” rule says, “if Gamma, x : tau_1 $--_Sigma e : tau_2 then Gamma$--_Sigma lambda x : tau_1.e : tau_1 -> tau_2”. It is often profitable to read it bottom-up as “To prove Gamma $--_Sigma lambda x : tau_1.e : tau_1 -> tau_2 you need to show Gamma, x : tau_1$--_Sigma e : tau_2”.

So what is the judgment saying? First, the judgment is, in this case, a four argument relation. The arguments of this relation are Gamma, Sigma, e, and tau. We could say the name of this relation is the perspicuous (_)$--_((_)) (_) : (_). Note that it does not make sense to ask what “⊢” means or what “:” means anymore than it makes sense to ask what “->” means in Haskell’s \ x -> e.4 In the context of type systems, Gamma is called the context, Sigma is called the signature, e is the term or expression, and tau is the type. Given this, I would read Gamma$--_Sigma e : tau as “the expression e has type tau in context gamma given signature sigma.” For the “->E” rule we have, additionally, multiple judgements above the line. These are joined together by conjunction, that is, we’d read “->E” as "if Gamma $--_Sigma f : tau_1 -> tau_2 and Gamma$--_Sigma x : tau_1 then Gamma $--_Sigma f x : tau_2 In most recent type system research multiple judgments are necessary to describe the type system, and so you may see things like Gamma$-- e > tau or Gamma $-- e_1 "~" e_2. The key thing to remember is that these are completely distinct relations that will have their own definitions (although the collection of them will often be mutually recursively defined). ### Inductively Defined Relations #### Relations Relations in set theory are boolean valued functions. Being programmers, and thus constructivists, we want evidence, so a relation$R : A xx B -> bb2$becomes a type constructor R : (A , B) -> Set.$R(a,b)$holds if we have a value (proof/witness) w : R a b. An inductively defined relation or judgment is then just a type constructor for an (inductive) data type. That means, if R is an inductively defined relation, then its definition is data R : A -> B -> Set where .... A rule is a constructor of this data type. A derivation is a value of this data type, and will usually be a tree-like structure. As a bit of ambiguity in the terminology (arguably arising from a common ambiguity in mathematical notation), it’s a bit more natural to use the term “judgment” to refer to something that can be (at the meta level) true or false. For example, we’d say$R(a,b)$is a judgment. Nevertheless, when we say something like “the typing judgment” it’s clear that we’re referring to the whole relation, i.e.$R$. #### Parameters of the judgments Since a judgment is a relation, we need to describe what the arguments to the relation look like. Typically something like BNF is used. The BNF definitions provide the types used as parameters to the judgments. It is common to use a Fortran-esque style where a naming convention is used to avoid the need to explicitly declare the types of meta-variables. For example, the following says meta-variables like n, m, and n_1 are all natural numbers. n, m ::= Z$ S n

BNF definitions translate readily to algebraic data types.

Agda note: Set is what is called * in Haskell. “Type” would be a better name. Also, these sidebars will cover details about Agda with the aim that readers unfamiliar with Agda don’t get tripped up by tangential details.

Sometimes it’s not possible to fully capture the constraints on well-formed syntax with BNF. In other words, only a subset of syntactically valid terms are well-formed. For example, Nat Nat is syntactically valid but is not well-formed. We can pick out that subset with a predicate, i.e. a unary relation. This is, of course, nothing but another judgment. As an example, if we wired the Maybe type into our type system, we’d likely have a judgment that looks like tau\ tt"type" which would include the following rule:

frac(tau\ tt"type")(("Maybe"\ tau)\ tt"type")

In a scenario like this, we’d also have to make sure the rules of our typing judgment also required the types involved to be well-formed. Modifying the example from the introduction, we’d get:

frac(Gamma,x:tau_1 $--_Sigma e : tau_2 \qquad tau_1\ tt"type" \qquad tau_2\ tt"type")(Gamma$--_Sigma (lambda x:tau_1.e) : tau_1 -> tau_2) ->I

#### A simple inductively defined relation in Agda

As a very simple example, let’s say we wanted to provide explicit evidence that one natural number was less than or equal to another in Agda. Scenarios like this are common in dependently typed programming, and so we’ll start with the Agda this time and then “informalize” it.

Agda notes: In Agda identifiers can contain almost any character so Z<=n is just an identifier. Agda allows any identifier to be used infix (or more generally mixfix). The underscores mark where the arguments go. So _isLessThanOrEqualTo_ is a binary infix operator. Finally, curly brackets indicate implicit arguments which can be omitted and Agda will “guess” their values. Usually, they’ll be obvious to Agda by unification.

In the informal notation, the types of the arguments are implied by the naming. n is a natural number because it was used as the metavariable (non-terminal) in the BNF for naturals. We also implicitly quantify over all free variables. In the Agda code, this quantification was explicit.

frac()(Z <= n) tt"Z<=n"

frac(m <= n)(S m <= S n) tt"Sm<=Sn"

Again, I want to emphasize that these are defining isLessThanOrEqualTo and $<=$. They can’t be wrong. They can only fail to coincide with our intuitions or to an alternate definition. A derivation that $2 <= 3$ looks like:

In Agda:

In the informal notation:

frac(frac()(Z <= S Z))(frac(S Z <= S (S Z))(S (S Z) <= S (S (S Z)))

### Big-step operational semantics

Here’s a larger example that also illustrates that these judgments do not need to be typing judgments. Here we’re defining a big-step operational semantics for the untyped lambda calculus.

x variable
v ::= λx.e
e ::= v $e e$ x

In informal presentations, binders like lambda are handled in a fairly relaxed manner. While the details of handling binders are tricky and error-prone, they are usually standard and so authors assume readers can fill in those details and are aware of the concerns (e.g. variable capture). In Agda, of course, we’ll need to spell out the details. There are many approaches for dealing with binders with different trade-offs. One of the newer and more convenient approaches is parametric higher-order abstract syntax (PHOAS). Higher-order abstract syntax (HOAS) approaches allow us to reuse the binding structure of the host language and thus eliminate much of the work. Below, this is realized by the Lambda constructor taking a function as its argument. In a later section, I’ll use a different approach using deBruijn indices.

Agda note: Set1 is needed for technical reasons that are unimportant. You can just pretend it says Set instead. More important is that the definitions of Expr and Value are a bit different than the definition for _isLessThanOrEqualTo_. In particular, the argument (A : Set) occurs to the left of the colon. When an argument occurs to the left of the colon we say it parameterizes the data declaration and that it is a parameter. When it occurs to the right of the colon we say it indexes the data declaration and that it is an index. The difference is that parameters must occur uniformly in the return type of the data constructors while indexes can be different in each data constructor. The arguments of an inductively defined relation like _isLessThanOrEqualTo_ will always be indexes (though there could be additional parameters.)

frac(e_1 darr lambda x.e \qquad e_2 darr v_2 \qquad e[x$->v_2] darr v)(e_1 e_2 darr v) tt"App" frac()(v darr v) tt"Trivial" The e darr v judgment (read as “the expression e evaluates to the value v”) defines a call-by-value evaluation relation. e[x$->v] means “substitute v for x in the expression e”. This notation is not standardized; there are many variants. In more rigorous presentations this operation will be formally defined, but usually the authors assume you are familiar with it. In the tt"Trivial" rule, the inclusion of values into expressions is implicitly used. Note that the rule is restricted to values only.

The tt"App" rule specifies call-by-value because the e_2 expression is evaluated and then the resulting value is substituted into e. For call-by-name, we’d omit the evaluation of e_2 and directly substitute e_2 for x in e. Whether e_1 or e_2 is evaluated first (or in parallel) is not specified in this example.

The EvaluateTrivial constructor explicitly uses the Val injection of values into expressions. The EvaluateApp constructor starts off with a series of implicit arguments that introduce and quantify over the variables used in the rule. After those, each judgement above the line in the tt"App" rule, becomes an argument to the EvaluateApp constructor.

In this case ↓ is defining a functional relation, meaning for every expression there’s at most one value that the expression evaluates to. So another natural way to interpret ↓ is as a definition, in logic programming style, of a (partial) recursive function. In other words we can use the concept of mode from logic programming and instead of treating the arguments to ↓ as inputs, we can treat the first as an input and the second as an output.

↓ gives rise to a partial function because not every expression has a normal form. For _EvaluatesTo_ this is realized by the fact that we simply won’t be able to construct a term of type e EvaluatesTo v for any v if e doesn’t have a normal form. In fact, we can use the inductive structure of the relationship to help prove that statement. (Unfortunately, Agda doesn’t present a very good experience for data types indexed by functions, so the proof is not nearly as smooth as one would like.)

### Type systems

Next we’ll turn to type systems which will present an even larger example, and will introduce some concepts that are specific to type systems (though, of course, they overlap greatly with concepts in logic due to the Curry-Howard correspondence.)

#### Terms and types

Below is an informal presentation of the polymorphic lambda calculus with explicit type abstraction and type application. An interesting fact about the polymorphic lambda calculus is that we don’t need any base types. Via Church-encoding, we can define types like natural numbers and lists.

α type variable
τ ::= τ → τ $∀α. τ$ α

x variable
c constant
v ::= λx:τ.e $Λτ.e$ c
Δ ::= . $Δ, α We see that this is just a (snoc) list. In the first case,$Gamma$, it is a list of pairs of variables and types, i.e. an association list mapping variables to types. Often it will be treated as a finite mapping. In the second case,$Delta$, it is a list of type variables. Since I’m using deBruijn notation, there are no variables so we end up with a list of types in the first case. In the second case, we would end up with a list of nothing in particular, i.e. a list of unit, but that is isomorphic to a natural number. In other words, the only purpose of the type context,$Delta$, is to make sure we don’t use unbound variables, which in deBruijn notation just means we don’t have deBruijn indexes that try to traverse more lambdas than enclose them. The Agda code for the above is completely straight-forward. #### The Signature Signatures keep track of what primitive, “user-defined” constants might exist. Often the signature is omitted since nothing particularly interesting happens with it. Indeed, that will be the case for us. Nevertheless, we see that the signature is just another association list mapping constants to types. Σ ::= .$ Σ, c:τ

The main reason I included the signature, beyond just covering it for the cases when it is included, is that sometimes certain rules can be better understood as manipulations of the signature. For example, in logic, universal quantification is often described by a rule like:

frac(Gamma $-- P[x$->c] \qquad c\ "fresh")(Gamma $-- forall x.P) What’s happening and what “freshness” is is made a bit clearer by employing a signature (which for logic is usually just a list of constants similar to our TypeContext): frac(Gamma$--_(Sigma, c) P[x$->c] \qquad c notin Sigma)(Gamma$--_Sigma forall x.P)

#### Judgment

To define the typing rules we need two judgements. The first, Delta $-- tau, will be a simple judgement that says$tau$is a well formed type in$Delta$. This basically just requires that all variables are bound. frac(alpha in Delta)(Delta$-- alpha)

frac(Delta, alpha $-- tau)(Delta$-- forall alpha. tau)

frac(Delta $-- tau_1 \qquad Delta$-- tau_2)(Delta $-- tau_1 -> tau_2) The Agda is The meat is the following typing judgement, depending on the judgement defining well-formed types. I’m not really going to explain these rules because, in some sense, there is nothing to explain. Beyond explaining the notation itself, which was the point of the article, the below is “self-explanatory” in the sense that it is a definition, and whether it is a good definition or “meaningful” depends on whether we can prove the theorems we want about it. frac(c:tau in Sigma \qquad Delta$-- tau)(Delta;Gamma $--_Sigma c : tau) tt"Const" frac(x:tau in Gamma \qquad Delta$-- tau)(Delta;Gamma $--_Sigma x : tau) tt"Var" frac(Delta;Gamma$--_Sigma e_1 : tau_1 -> tau_2 \qquad Delta;Gamma $--_Sigma e_2 : tau_1)(Delta;Gamma$--_Sigma e_1 e_2 : tau_2) tt"App"

frac(Delta;Gamma $--_Sigma e : forall alpha. tau_1 \qquad Delta$-- tau_2)(Delta;Gamma $--_Sigma e[tau_2] : tau_1[alpha$->tau_2]) tt"TyApp"

frac(Delta;Gamma, x:tau_1 $--_Sigma e : tau_2 \qquad Delta$-- tau_1)(Delta;Gamma $--_Sigma (lambda x:tau_1.e) : tau_1 -> tau_2) tt"Abs" frac(Delta, alpha;Gamma$--_Sigma e : tau)(Delta;Gamma |--_Sigma (Lambda alpha.e) : forall alpha. tau) tt"TyAbs"

Here’s the corresponding Agda code. Note, all Agda is doing for us here is making sure we haven’t written self-contradictory nonsense. In no way is Agda ensuring that this is the “right” definition. For example, it could be the case (but isn’t) that there are no values of this type. Agda would be perfectly content to let us define a type that had no values.

tySubst : TType -> TType -> TType
tySubst t1 t2 = tySubst' t1 t2 Z
where tySubst' : TType -> TType -> Nat -> TType
tySubst' (TTVar Z) t2 Z = t2
tySubst' (TTVar Z) t2 (S _) = TTVar Z
tySubst' (TTVar (S n)) t2 Z = TTVar (S n)
tySubst' (TTVar (S n)) t2 (S d) = tySubst' (TTVar n) t2 d
tySubst' (t1 => t2) t3 d = tySubst' t1 t3 d => tySubst' t2 t3 d
tySubst' (Forall t1) t2 d = tySubst' t1 t2 (S d)

data _isIn_at_ {A : Set} : A -> List A -> Nat -> Set where
Found : {a : A} -> {l : List A} -> a isIn (l , a) at Z
Next : {a : A} -> {b : A} -> {l : List A} -> {n : Nat} -> a isIn l at n -> a isIn (l , b) at (S n)

data _hasType_inContext_and_given_ : TExpr -> TType -> Context -> TypeContext -> Signature -> Set where
ConstJ : {t : TType} -> {c : Nat}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> t isIn Sigma at c
-> t isValidIn Delta
-> (TVal (TConst c)) hasType t inContext Gamma and Delta given Sigma

VarJ : {t : TType} -> {x : Nat}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> t isIn Gamma at x
-> t isValidIn Delta
-> (TVar x) hasType t inContext Gamma and Delta given Sigma

AppJ : {t1 : TType} -> {t2 : TType} -> {e1 : TExpr} -> {e2 : TExpr}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> e1 hasType (t1 => t2) inContext Gamma and Delta given Sigma
-> e2 hasType t1 inContext Gamma and Delta given Sigma
-> (TApp e1 e2) hasType t2 inContext Gamma and Delta given Sigma

TyAppJ : {t1 : TType} -> {t2 : TType} -> {e : TExpr}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> e hasType (Forall t1) inContext Gamma and Delta given Sigma
-> t2 isValidIn Delta
-> (TTyApp e t2) hasType (tySubst t1 t2) inContext Gamma and Delta given Sigma

AbsJ : {t1 : TType} -> {t2 : TType} -> {e : TExpr}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> e hasType t2 inContext (Gamma , t1) and Delta given Sigma
-> (TVal (TLambda t1 e)) hasType (t1 => t2) inContext Gamma and Delta given Sigma

TyAbsJ : {t : TType} -> {e : TExpr}
-> {Sigma : Signature} -> {Gamma : Context} -> {Delta : TypeContext}
-> e hasType t inContext Gamma and (S Delta) given Sigma
-> (TVal (TTyLambda e)) hasType (Forall t) inContext Gamma and Delta given Sigma

Here’s a typing derivation for the polymorphic constant function:

Having written all this, we have not defined a type checking algorithm (though Agda’s auto tactic does a pretty good job); we’ve merely specified what evidence that a program is well-typed is. Explicitly, a type checking algorithm would be a function with the following type:

In fact, we’d want to additionally prove that this function never returns Nothing if there does exist a typing derivation that would give e the type t in signature sig. We could formalize this in Agda by instead giving typeCheck the following type:

This type says that either typeCheckDec will return a typing derivation, or it will return a proof that there is no typing derivation. As the name Decidable suggests, this may not always be possible. Which is to say, type checking may not always be decidable. Note, we can always check that a typing derivation is valid — we just need to verify that we applied the rules correctly — what we can’t necessarily do is find such a derivation given only the expression and the type or prove that no such derivation exists. Similar concerns apply to type inference which could have one of the following types:

where Σ indicates a dependent sum, i.e. a pair where the second component (here of type e hasType t inContext Nil and Z given sig) depends on the first component (here of type TType). With type inference we have the additional concern that there may be multiple possible types an expression could have, and we may want to ensure it returns the “most general” type in some sense. There may not always be a good sense of “most general” type and user-input is required to pick out of the possible types.

Sometimes the rules themselves can be viewed as the defining rules of a logic program and thus directly provide an algorithm. For example, if we eliminate the rules, types, and terms related to polymorphism, we’d get the simply typed lambda calculus. A Prolog program to do type checking can be written in a few lines with a one-to-one correspondence to the type checking rules (and, for simplicitly, also omitting the signature):