This repository contains a small example of a correct-by-construction type checker for the simply-typed lambda calculus implemented in Agda.
To get the code working, follow these steps:
- Install Agda by following the instruction on the website.
- Install the
standard-library
using the installation guide. - To test that everything works, compile the
src/Everything.agda
file.
The type checker is built up using various components, outlined below.
A small example where the type checker is used can be found in the Everything
module.
We define the scope (the available variables) as a list of available names:
Scope : (name : Set) → Set
Scope name = List name
Now, to extends scope α
with name x
, we simply have to write x ∷ α
.
To be able to assert a name's availability within the scope, we also define a proof-relevant "in" predicate:
data _∈_ {name : Set} (x : name) : Scope name → Set where
here : ∀ {ns : Scope name} → x ∈ (x ∷ ns)
there : ∀ {n : name} {ns : Scope name} (_ : x ∈ ns) → x ∈ (n ∷ ns)
We construct a well-scoped syntax for the language:
data Type : Set where
TyNat : Type
TyArr : (a b : Type) → Type
data Term (α : Scope name) : Set where
TVar : (x : name) → x ∈ α → Term α
TLam : (x : name) (v : Term (x ∷ α)) → Term α
TApp : (u v : Term α) → Term α
In our syntax, the identity function (λ x → x
) would look like this: TLam "x" (TVar "x" here)
.
This term would type check against type TyArr TyNat TyNat
, but also against TyArr (TyArr TyNat TyNat) (TyArr TyNat TyNat)
.
Next, we specify the typing rules of the language:
data _⊢_∶_ (Γ : Context α) : Term α → Type → Set where
TyTVar
: (p : x ∈ α)
----------------------------------
→ Γ ⊢ TVar x p ∶ lookupVar Γ x p
TyTLam
: Γ , x ∶ a ⊢ u ∶ b
-------------------------------
→ Γ ⊢ TLam x u ∶ TyArr a b
TyTApp
: Γ ⊢ u ∶ (TyArr a b)
→ Γ ⊢ v ∶ a
------------------------------------
→ Γ ⊢ TApp u v ∶ b
infix 3 _⊢_∶_
Now we can write Γ ⊢ u ∶ t
for u
has type t
under context Γ
(where u
and Γ
are parametrised with scope α
).
We begin the implementation of the type checker by defining a variable context as an All
.
We parametrise the context on Scope
and define a variable lookup function:
Context : (v : Set) → (α : Scope name) → Set
Context v α = All (λ _ → v) α
lookupVar : (Γ : Context v α) (x : name) (p : x ∈ α) → v
lookupVar (v ∷ _ ) x here = v
lookupVar (_ ∷ ctx) x (there p) = lookupVar ctx x p
Given a predicate P
, All P xs
means that every element in xs
satisfies P
.
Here it allows us to assign a type to each variable in the scope.
Note that Context
takes a parameter v
, which allows us to determine what kind of value we want to assign to variables.
When used in a type checker, we pass Type
as an argument for v
.
If we wanted to use Context
in an interpreter instead, we would pass the value type.
We define a simple evaluator monad with String
errors:
EvalError = String
Evaluator : Set → Set
Evaluator a = EvalError ⊎ a
Type-checking function application requires conversion checking, i.e. checking whether two types are equal. In simply-typed lambda calculus, conversion is just definitional equality, so implementing a conversion checker is straightforward:
convert : (a b : Type) → Evaluator (a ≡ b)
convert TyNat TyNat = return refl
convert (TyArr la lb) (TyArr ra rb) = do
refl ← convert la ra
refl ← convert lb rb
return refl
convert _ _ = evalError "unequal types"
Finally, we define the bidirectional-style type checking functions mutually:
inferType : ∀ (Γ : Context α) u → Evaluator (Σ[ t ∈ Type ] Γ ⊢ u ∶ t)
checkType : ∀ (Γ : Context α) u (ty : Type) → Evaluator (Γ ⊢ u ∶ ty)
inferType ctx (TVar x index) = return (lookupVar ctx x index , TyTVar index)
inferType ctx (TLam x body) = evalError "cannot infer the type of a lambda"
inferType ctx (TApp lam arg) = do
(TyArr a b) , gtu ← inferType ctx lam
where _ → evalError "application head should have a function type"
gtv ← checkType ctx arg a
return (b , TyTApp gtu gtv)
checkType ctx (TLam x body) (TyArr a b) = do
tr ← checkType (ctx , x ∶ a) body b
return (TyTLam tr)
checkType ctx (TLam x body) _ = evalError "lambda should have a function type"
checkType ctx term ty = do
(t , tr) ← inferType ctx term
refl ← convert t ty
return tr
Things to note:
- Both
inferType
andcheckType
return a typing judgement for the specific input term (and type, in case ofcheckType
), so we know not just that we get a correct typing derivation but also that it is a derivation for the given input(s). - We make use of Agda's
do
-notation for theEvaluator
monad. This includes the ability to pattern match on the output of a statement in ado
-block, and the use ofwhere
to deal with the cases that are not on the "happy path" (in this case, by throwing an error if the head of an application does not have a function type). - In the final case for
checkType
, we call the conversion checker, which (if it succeeds) returns an equality proof. We then match this equality proof againstrefl
, unifying the left- and right-hand sides of the equality for the remainder of thedo
-block. - Since we return an error message instead of providing evidence of a contradiction in the negative cases, our type checker is sound but not complete, i.e. "if it returns a derivation, we know it is correct; but there is nothing to prevent us from writing a function that always returns an error, even when there exists a correct derivation" (see PLFA: Inference).