|
|
Pure simply typed lambda-calculus (from Fig 9-1 TAPL)
|
|
Typing
|
Evaluation
|
|
|
|
Γ, x: T1 |- t2: T2 | Γ |- \x: T1. t2: T1 → T2 |
| (T-Abs) |
|
|
Γ |- t1: T1 → T2 Γ |- t2: T1 | Γ |- t1 t2: T2 |
| (T-App) |
|
(\x:T1.t2). v1 | [x / v1] t2 |
| (E-AppAbs) |
|
Lemma 9.3.1 Inversion of the typing relation (without booleans, if)
- If Γ |- x: R, then x:R ∈ Γ
- If Γ |- \x: T. t: R, then R=T→S for some S with
Γ ⊢ t: S
- If Γ |- u t: R, then there is some type T such that
Γ ⊢ u:T→R and Γ ⊢ t: T
Theorem 9.3.3 Uniqueness of types
In a given typing context Γ, a term t (with all fee variables in the domain of Γ has at most one type. Moreover there is just one derivation of
this typing built from the inference rules that generate the typing relation
|
Simply typed lambda-calculus with subtyping (from Fig 15-1 TAPL)
|
|
Typing
|
Subtyping
|
|
|
|
Γ, x: T1 |- t2: T2 | Γ |- \x: T1. t2: T1 → T2 |
| (T-Abs) |
|
|
Γ |- t1: T1 → T2 Γ |- t2: T1 | Γ |- t1 t2: T2 |
| (T-App) |
|
Γ |- t: S S <: T | Γ |- t: T |
| (T-Sub) |
|
T1 <: S1 S2 <: T2 | S1 → S2 <: T1 → T2 |
| (S-Arrow) |
|
|
