Understanding typing judgments

April 13, 2016 02:41 UTC (Last updated on August 2, 2024 02:45 UTC)

Tags: Agda, type theory

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 \vdash_\Sigma e : \tau_2}{\Gamma \vdash_\Sigma (\lambda x:\tau_1.e) : \tau_1 \to \tau_2} {\to}I\]

\[\frac{\Gamma \vdash_\Sigma f : \tau_1 \to \tau_2 \qquad \Gamma \vdash_\Sigma x : \tau_1}{\Gamma \vdash_\Sigma f x : \tau_2} {\to}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 “|{\to}I|” part is just the name of the rule (in this case being short for “|{\to}| Introduction”). This rule is only part of the definition of the judgment of the form:

\[\Gamma \vdash_\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 “|{\to}I|” rule says, “if |\Gamma, x : \tau_1 \vdash_\Sigma e : \tau_2| then |\Gamma \vdash_\Sigma \lambda x : \tau_1.e : \tau_1 \to \tau_2|”. It is often profitable to read it bottom-up as “To prove |\Gamma \vdash_\Sigma \lambda x : \tau_1.e : \tau_1 \to \tau_2| you need to show |\Gamma, x : \tau_1 \vdash_\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 |(\_)\vdash_{(\_)} (\_) : (\_)|. 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 \vdash_\Sigma e : \tau| as “the expression e has type tau in context gamma given signature sigma.” For the “|{\to}E|” rule we have, additionally, multiple judgements above the line. These are joined together by conjunction, that is, we’d read “|{\to}E|” as “if |\Gamma \vdash_\Sigma f : \tau_1 \to \tau_2| and |\Gamma \vdash_\Sigma x : \tau_1| then |\Gamma \vdash_\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 \vdash e > \tau| or |\Gamma \vdash e_1 \sim 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 \times B \to \mathbf 2| 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.

data Nat : Set where
    Z : Nat
    S : Nat -> Nat

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\ \mathtt{type}| which would include the following rule:

\[\frac{\tau\ \mathtt{type}}{(\mathrm{Maybe}\ \tau)\ \mathtt{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 \vdash_\Sigma e : \tau_2 \qquad \tau_1\ \mathtt{type} \qquad \tau_2\ \mathtt{type}}{\Gamma \vdash_\Sigma (\lambda x:\tau_1.e) : \tau_1 \to \tau_2} {\to}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.

data _isLessThanOrEqualTo_ : Nat -> Nat -> Set where
    Z<=n : {n : Nat} -> Z isLessThanOrEqualTo n
    Sm<=Sn : {m : Nat} -> {n : Nat} -> m isLessThanOrEqualTo n -> (S m) isLessThanOrEqualTo (S n)

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 \leq n} \mathtt{Z\leq n}\]

\[\frac{m \leq n}{S m \leq S n} \mathtt{Sm\leq Sn}\]

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

In Agda:

twoIsLessThanThree : (S (S Z)) isLessThanOrEqualTo (S (S (S Z)))
twoIsLessThanThree = Sm<=Sn (Sm<=Sn Z<=n)

In the informal notation:

\[\frac{\frac{}{Z \leq S Z}}{\frac{S Z \leq S (S Z)}{S (S Z) \leq 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.

-- PHOAS approach to binding
mutual
    data Expr (A : Set) : Set where
        Val : Value A -> Expr A
        App : Expr A -> Expr A -> Expr A
        Var : A -> Expr A

    data Value (A : Set) : Set where
        Lambda : (A -> Expr A) -> Value A

-- A closed expression
CExpr : Set1
CExpr = {A : Set} -> Expr A

-- A closed expression that is a value
CValue : Set1
CValue = {A : Set} -> Value A

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 \downarrow \lambda x.e \qquad e_2 \downarrow v_2 \qquad e[x\mapsto v_2] \downarrow v}{e_1 e_2 \downarrow v} \mathtt{App}\]

\[\frac{}{v \downarrow v} \mathtt{Trivial}\]

The |e \downarrow v| judgment (read as “the expression |e| evaluates to the value |v|”) defines a call-by-value evaluation relation. |e[x\mapsto 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 |\mathtt{Trivial}| rule, the inclusion of values into expressions is implicitly used. Note that the rule is restricted to values only.

The |\mathtt{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.

subst : {A : Set} -> Expr (Expr A) -> Expr A
subst (Var e) = e
subst (Val (Lambda b)) = Val (Lambda (λ a -> subst (b (Var a))))
subst (App e1 e2) = App (subst e1) (subst e2)

data _EvaluatesTo_ : CExpr -> CValue -> Set1 where
    EvaluateTrivial : {v : CValue} -> (Val v) EvaluatesTo v
    EvaluateApp : {e1 : CExpr} -> {e2 : CExpr}
        -> {e : {A : Set} -> A -> Expr A}
        -> {v2 : CValue} -> {v : CValue}
        -> e1 EvaluatesTo (Lambda e)
        -> e2 EvaluatesTo v2
        -> (subst (e (Val v2))) EvaluatesTo v
        -> (App e1 e2) EvaluatesTo v

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 |\mathtt{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
e ::= v | e e | e[τ] | x

In this case I’ll be using deBruijn indices to handle the binding structure of the terms and types. This means instead of writing |\lambda x.\lambda y. x|, you would write |\lambda \lambda 1| where the |1| counts how many binders (lambdas) you need to traverse to reach the binding site.

data TType : Set where
    TTVar : Nat -> TType                    -- α
    _=>_ : TType -> TType -> TType          -- τ → τ
    Forall : TType -> TType                 -- ∀α. τ

mutual
    data TExpr : Set where
        TVal : TValue -> TExpr              -- v
        TApp : TExpr -> TExpr -> TExpr      -- f x
        TTyApp : TExpr -> TType -> TExpr    -- e[τ]
        TVar : Nat -> TExpr                 -- x

    data TValue : Set where
        TLambda : TType -> TExpr -> TValue  -- λx:τ.e
        TTyLambda : TExpr -> TValue         -- Λτ.e
        TConst : Nat -> TValue              -- c

The Context

In formulating the typing rules we need to deal with open terms, that is terms which refer to variables that they don’t bind. This should only happen if some enclosing terms did bind those variables, so we need to keep track of the variables that have been bound by enclosing terms. For example, when type checking |\lambda x:\tau.x|, we’ll need to type check the subterm |x| which does not contain enough information in itself for us to know what the type should be. So, we keep track of what variables have been bound (and to what type) in a context and then we can just look up the expected type. When authors bother formally spelling out the context, it will look something like the following:

Γ ::= . | Γ, x:τ
Δ ::= . | Δ, α

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.

data List (A : Set) : Set where
    Nil : List A
    _,_ : List A -> A -> List A

Context : Set
Context = List TType

TypeContext : Set
TypeContext = Nat

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:τ
Signature : Set
Signature = List TType

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 \vdash P[x\mapsto c] \quad c\ \mathrm{fresh}}{\Gamma \vdash \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 \vdash_{\Sigma, c} P[x\mapsto c] \quad c \notin \Sigma}{\Gamma \vdash_\Sigma \forall x.P}\]

Judgment

To define the typing rules we need two judgements. The first, |\Delta \vdash \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 \vdash \alpha}\]

\[\frac{\Delta, \alpha \vdash \tau}{\Delta \vdash \forall \alpha. \tau}\]

\[\frac{\Delta \vdash \tau_1 \quad \Delta \vdash \tau_2}{\Delta \vdash \tau_1 \to \tau_2}\]

The Agda is

data _<_ : Nat -> Nat -> Set where
    Z<Sn : {n : Nat} -> Z < S n
    Sn<SSm : {n m : Nat} -> n < S m -> S n < S (S m)

data _isValidIn_ : TType -> TypeContext -> Set where
    TyVarJ : {n : Nat} -> {ctx : TypeContext} -> n < ctx -> (TTVar n) isValidIn ctx
    TyArrJ : {t1 t2 : TType} -> {ctx : TypeContext} -> t1 isValidIn ctx -> t2 isValidIn ctx -> (t1 => t2) isValidIn ctx
    TyForallJ : {t : TType} -> {ctx : TypeContext} -> t isValidIn (S ctx) -> (Forall t) isValidIn ctx

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 \vdash \tau}{\Delta;\Gamma \vdash_\Sigma c : \tau} \mathtt{Const}\]

\[\frac{x:\tau \in \Gamma \qquad \Delta \vdash \tau}{\Delta;\Gamma \vdash_\Sigma x : \tau} \mathtt{Var}\]

\[\frac{\Delta;\Gamma \vdash_\Sigma e_1 : \tau_1 \to \tau_2 \qquad \Delta;\Gamma \vdash_\Sigma e_2 : \tau_1}{\Delta;\Gamma \vdash_\Sigma e_1 e_2 : \tau_2} \mathtt{App}\]

\[\frac{\Delta;\Gamma \vdash_\Sigma e : \forall \alpha. \tau_1 \qquad \Delta \vdash \tau_2}{\Delta;\Gamma \vdash_\Sigma e[\tau_2] : \tau_1[\alpha\mapsto\tau_2]} \mathtt{TyApp}\]

\[\frac{\Delta;\Gamma, x:\tau_1 \vdash_\Sigma e : \tau_2 \qquad \Delta \vdash \tau_1}{\Delta;\Gamma \vdash_\Sigma (\lambda x:\tau_1.e) : \tau_1 \to \tau_2} \mathtt{Abs}\]

\[\frac{\Delta, \alpha;\Gamma \vdash_\Sigma e : \tau}{\Delta;\Gamma \vdash_\Sigma (\Lambda \alpha.e) : \forall \alpha. \tau} \mathtt{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:


tyLam : TExpr -> TExpr
tyLam e = TVal (TTyLambda e)

lam : TType -> TExpr -> TExpr
lam t e = TVal (TLambda t e)

polyConst
    : tyLam (tyLam (lam (TTVar Z) (lam (TTVar (S Z)) (TVar (S Z)))))    -- Λs.Λt.λx:t.λy:s.x
    hasType (Forall (Forall (TTVar Z => (TTVar (S Z) => TTVar Z))))     -- ∀s.∀t.t→s→t
    inContext Nil and Z
    given Nil
polyConst = TyAbsJ (TyAbsJ (AbsJ (AbsJ (VarJ (Next Found) (TyVarJ Z<Sn))))) -- written by Agda

data False : Set where

Not : Set -> Set
Not A = A -> False

wrongType
    : Not (tyLam (lam (TTVar Z) (TVar Z))   -- Λt.λx:t.x
           hasType (Forall (TTVar Z))       -- ∀t.t
           inContext Nil and Z
           given Nil)
wrongType (TyAbsJ ())

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:

data Maybe (A : Set) : Set where
    Nothing : Maybe A
    Just : A -> Maybe A

typeCheck : (e : TExpr) -> (t : TType) -> (sig : Signature) -> Maybe (e hasType t inContext Nil and Z given sig)
typeCheck = ?

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:

data Decidable (A : Set) : Set where
    IsTrue : A -> Decidable A
    IsFalse : Not A -> Decidable A

typeCheckDec : (e : TExpr) -> (t : TType) -> (sig : Signature) -> Decidable (e hasType t inContext Nil and Z given sig)
typeCheckDec = ?

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:

record Σ (T : Set) (F : T -> Set) : Set where
    field
        fst : T
        snd : F fst

inferType : (e : TExpr) -> (sig : Signature) -> Maybe (Σ TType (λ t → e hasType t inContext Nil and Z given sig))
inferType = ?

inferTypeDec : (e : TExpr) -> (sig : Signature) -> Decidable (Σ TType (λ t → e hasType t inContext Nil and Z given sig))
inferTypeDec = ?

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):

lookup(z, [T|_], T).
lookup(s(N), [_|Ctx],T) :- lookup(N, Ctx, T).

typeCheck(var(N), Ctx, T) :- lookup(N, Ctx, T).
typeCheck(app(F,X), Ctx, T2) :- typeCheck(F, Ctx, tarr(T1, T2)), typeCheck(X, Ctx, T1).
typeCheck(lam(B), Ctx, tarr(T1, T2)) :- typeCheck(B, [T1|Ctx], T2).

  1. This Agda file contains all the code from this article.↩︎

  2. Most dependently typed languages, such as Coq or Epigram would also be adequate.↩︎

  3. Epigram is most notable by actually using this 2D syntax.↩︎

  4. See this StackExchange answer for more discussion of this.↩︎