April 13, 2016 02:41 UTC (Last updated on August 24, 2019 21:37 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 |--_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’s^{2} data type mechanism directly captures them^{3}. 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.

```
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 <= 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:

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

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.

```
-- 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 itparameterizesthe data declaration and that it is aparameter. When it occurs to the right of the colon we say itindexesthe data declaration and that it is anindex. 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.

```
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 `#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
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:τ`

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

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

```
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).
```

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

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

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