NOTE: simply typed lambda calculus

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

\[ add := \lambda m. \lambda n. \lambda s. \lambda z. m\;s\;(n\;s\;z) \]

people prefer just + more.

But once we introduce such fundamental operations into the system, validation would be a thing. This is the main reason to have a \[\lambda \to\] system(a.k.a. simply typed lambda calculus). It gets name \[\lambda \to\] is because it introduces one new type: Arrow type, represent as \[T_1 \to T_2\] for any abstraction \[\lambda x.M\] where \[x\] has a type is \[T_1\] and \[M\] has a type is \[T_2\]. Therefore we can limit the input to a specified type, without considering how to add two Car together!

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:

\[ \frac{ x:T \in \Gamma }{ \Gamma \vdash x:T } \;\;\;\; T-Variable \\ \frac{ \Gamma, x:T_1 \vdash t_2: T_2 }{ \Gamma \vdash \lambda x:T_1.t_2 : T_1 \to T_2 } \;\;\;\; T-Abstraction \\ \frac{ \Gamma, t_1:T_1 \to T_2 \; \Gamma \vdash t_2: T_1 }{ \Gamma \vdash t_1 \; t_2 : T_2 } \;\;\;\; T-Application \]

Here is explaination:

T-Variable: with the premise, term \[x\] binds to type \[T\] in context \[\Gamma\] is truth. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[x\] is \[T\].
T-Abstraction: with the premise, with context \[\Gamma\] and term \[x\] binds to type \[T_1\] we can judge term \[t_2\] has type \[T_2\]. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[\lambda x:T_1.t_2\] is \[T_1 \to T_2\].
T-Application: with the premise, with context \[\Gamma\] and term \[t_1\] binds to type \[T_1 \to T_2\] and with context \[\Gamma\] we can judge term \[t_2\] has type \[T_1\]. We can make a conclusion, in context \[\Gamma\], we can judge the type of \[t_1 \; t_2\] is \[T_2\].