Last time I introduce lambda calculus.Lambda calculus is powerful enough for computation. But it’s not good enough for people, compare with below Church Numerals
people prefer just
But once we introduce such fundamental operations into the system, validation would be a thing. This is the main reason to have a λ→ system(a.k.a. simply typed lambda calculus). It gets name λ→ is because it introduces one new type: Arrow type, represent as T1→T2 for any abstraction λx.M where x has a type is T1 and M has a type is T2. Therefore we can limit the input to a specified type, without considering how to add two
To represent this, syntax needs a little change:
term ::= terms x variable λx: T.term abstraction term term application
Abstraction now can describe it’s parameter type. Then we have typing rules:
Here is the explanation:
- T-Variable: with the premise, term x binds to type T in context Γ is truth. We can make a conclusion, in context Γ, we can judge the type of x is T.
- T-Abstraction: with the premise, with context Γ and term x binds to type T1 we can judge term t2 has type T2. We can make a conclusion, in context Γ, we can judge the type of λx:T1.t2 is T1→T2.
- T-Application: with the premise, with context Γ and term t1 binds to type T1→T2 and with context Γ we can judge term t2 has type T1. We can make a conclusion, in context Γ, we can judge the type of t1t2 is T2.