4. Simply Typed Lambda Calculus: Typing
import LeanLambda.UntypedThe simply typed lambda calculus keeps the terms and beta reduction from the untyped calculus and adds a typing judgment. As before, we begin with de Bruijn terms and then define typing for named terms through compilation.
4.1. Simple Types
A simple type is either a type variable or a function type. Here α
ranges over type variables, and the arrow associates to the right. These
variables are atomic for now; polymorphism will later add binders for them.
A,B ::= \alpha \mid A \to B
namespace SimplyTypedopen Untypedinductive Ty where
| var (name : String)
| arr (domain codomain : Ty)
deriving DecidableEq, Repr, Lean.ToExprsyntax:max "#" ident : terminfixr:60 " ⇒ " => Ty.arrmacro_rules
| `(#$X:ident) => do
let X' : Lean.TSyntax `term := ⟨Lean.Syntax.mkStrLit X.getId.toString⟩
`(Ty.var $X')example : #A ⇒ #B ⇒ #C = #A ⇒ (#B ⇒ #C) := ⊢ Ty.var "A" ⇒ Ty.var "B" ⇒ Ty.var "C" = Ty.var "A" ⇒ Ty.var "B" ⇒ Ty.var "C" All goals completed! 🐙4.2. Typing with De Bruijn Indices
The judgment Δ ; Γ ⊢ᴺᵇ t : A says that t has type
A. It uses one context for each kind of variable. The bound context
Δ is a list of types, so de Bruijn index n receives the type at
position n. The free context Γ associates free variable names
with their types.
Index 0 denotes the innermost binder. Consequently, when checking a
lambda whose parameter has type A, we add A to the front of
Δ. Application has the usual rule: a function of type A → B
must be applied to an argument of type A.
\frac{\Delta[n] = A}{\Delta;\Gamma \vdash n : A}
\qquad
\frac{\Gamma(x) = A}{\Delta;\Gamma \vdash x : A}
\frac{A,\Delta;\Gamma \vdash e : B}
{\Delta;\Gamma \vdash \lambda.\,e : A \to B}
\qquad
\frac{\Delta;\Gamma \vdash e_1 : A \to B
\qquad \Delta;\Gamma \vdash e_2 : A}
{\Delta;\Gamma \vdash e_1\ e_2 : B}
abbrev BoundContext := List Tyabbrev BinderContext := List (String × Ty)abbrev FreeContext := List (String × Ty)abbrev BinderContext.names (Δ : BinderContext) : List String :=
Δ.map Prod.fstabbrev BinderContext.types (Δ : BinderContext) : BoundContext :=
Δ.map Prod.sndnamespace DBinductive HasType : BoundContext → FreeContext → Untyped.DB → Ty → Prop where
| bound :
Δ[n]? = some A →
HasType Δ Γ (.bound n) A
| free :
Γ.lookup x = some A →
HasType Δ Γ (.free x) A
| lam :
HasType (A :: Δ) Γ body B →
HasType Δ Γ (.lam body) (A ⇒ B)
| app :
HasType Δ Γ fn (A ⇒ B) →
HasType Δ Γ arg A →
HasType Δ Γ (.app fn arg) Bnotation:50 Δ " ; " Γ " ⊢ᴺᵇ " t " : " A => HasType Δ Γ t Anotation:50 Γ " ⊢ᵇ " t " : " A => HasType [] Γ t A
For small concrete examples, typecheck repeatedly applies these four
rules; lookups in explicit contexts are then computed by Lean.
syntax "typecheck" : tacticmacro_rules
| `(tactic| typecheck) => `(tactic| repeat' constructor)example : [] ⊢ᵇ DB[λ 0] : #A ⇒ #A := ⊢ [] ⊢ᵇ (DB.bound 0).lam : Ty.var "A" ⇒ Ty.var "A" All goals completed! 🐙example : [("x", #A)] ⊢ᵇ DB[x] : #A := ⊢ [("x", Ty.var "A")] ⊢ᵇ DB.free "x" : Ty.var "A" All goals completed! 🐙end DB4.3. Typing Named Terms
To type a named term beneath lambdas, the binder context Δ records
name–type pairs, with the innermost binder first. Its list of names tells the
compiler how bound occurrences become de Bruijn indices; the corresponding
list of types is the bound context of the compiled term. Thus named typing is
defined by the de Bruijn judgment rather than by a second set of rules.
A variable refers to the first binder with the same name. If that binder is
at position n, its type is read from position n as well. When no
such binder exists, the variable is looked up in the free context Γ.
\frac{\mathsf{lookup}(\Delta;\Gamma,x)=A}
{\Delta;\Gamma \vdash x:A}
\qquad
\frac{(x:A),\Delta;\Gamma \vdash e:B}
{\Delta;\Gamma \vdash \lambda x.\,e:A\to B}
\frac{\Delta;\Gamma \vdash e_1:A\to B
\qquad \Delta;\Gamma \vdash e_2:A}
{\Delta;\Gamma \vdash e_1\ e_2:B}
namespace Term@[simp] def lookupName (Δ : BinderContext) (Γ : FreeContext) (x : String) : Option Ty :=
match Δ.names.idxOf? x with
| some n => Δ.types[n]?
| none => Γ.lookup xdef HasType (Δ : BinderContext) (Γ : FreeContext) (e : Untyped.Term) (A : Ty) : Prop :=
DB.HasType Δ.types Γ (Untyped.Term.toDBWith Δ.names e) Anotation:50 Δ " ; " Γ " ⊢ᴺ " e " : " A => HasType Δ Γ e Anotation:50 Γ " ⊢ " e " : " A => HasType [] Γ e AThe familiar named rules are consequences of this compiled definition.
@[grind .] theorem HasType.var
: lookupName Δ Γ x = some A
→ Δ;Γ ⊢ᴺ .var x : A
:= Δ:BinderContextΓ:FreeContextx:StringA:Ty⊢ lookupName Δ Γ x = some A → Δ ; Γ ⊢ᴺ Term.var x : A
Δ:BinderContextΓ:FreeContextx:StringA:Ty⊢ lookupName Δ Γ x = some A → Δ ; Γ ⊢ᴺ Term.var x : AΔ:BinderContextΓ:FreeContextx:StringA:Tyval✝:ℕ⊢ lookupName Δ Γ x = some A → Δ ; Γ ⊢ᴺ Term.var x : A Δ:BinderContextΓ:FreeContextx:StringA:Ty⊢ lookupName Δ Γ x = some A → Δ ; Γ ⊢ᴺ Term.var x : AΔ:BinderContextΓ:FreeContextx:StringA:Tyval✝:ℕ⊢ lookupName Δ Γ x = some A → Δ ; Γ ⊢ᴺ Term.var x : A
All goals completed! 🐙@[grind .] theorem HasType.lam
: (((x, A) :: Δ) ; Γ ⊢ᴺ body : B)
→ (Δ ; Γ ⊢ᴺ .lam x body : A ⇒ B)
:= x:StringA:TyΔ:List (String × Ty)Γ:FreeContextbody:TermB:Ty⊢ ((x, A) :: Δ ; Γ ⊢ᴺ body : B) → Δ ; Γ ⊢ᴺ Term.lam x body : A ⇒ B All goals completed! 🐙@[grind .] theorem HasType.app
: (Δ ; Γ ⊢ᴺ fn : A ⇒ B)
→ (Δ ; Γ ⊢ᴺ arg : A)
→ (Δ ; Γ ⊢ᴺ .app fn arg : B)
:= Δ:BinderContextΓ:FreeContextfn:TermA:TyB:Tyarg:Term⊢ (Δ ; Γ ⊢ᴺ fn : A ⇒ B) → (Δ ; Γ ⊢ᴺ arg : A) → Δ ; Γ ⊢ᴺ fn.app arg : B All goals completed! 🐙example : [] ⊢ Term[λx. x] : #A ⇒ #A := ⊢ [] ⊢ Term.lam "x" (Term.var "x") : Ty.var "A" ⇒ Ty.var "A" All goals completed! 🐙example : [] ⊢ Term[λx. λy. x] : #A ⇒ #B ⇒ #A := ⊢ [] ⊢ Term.lam "x" (Term.lam "y" (Term.var "x")) : Ty.var "A" ⇒ Ty.var "B" ⇒ Ty.var "A" All goals completed! 🐙example : [("y", #A)] ⊢ Term[(λx. x) y] : #A := ⊢ [("y", Ty.var "A")] ⊢ (Term.lam "x" (Term.var "x")).app (Term.var "y") : Ty.var "A" All goals completed! 🐙
This is Curry-style typing: lambda binders carry no type annotations. Typing
is therefore not a function from terms to types. For example, the same
identity term has type A → A for every simple type A.
end Termend SimplyTyped