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
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 for any abstraction where has a type is and has a type is . 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 explaination:
- T-Variable: with the premise, term binds to type in context is truth. We can make a conclusion, in context , we can judge the type of is .
- T-Abstraction: with the premise, with context and term binds to type we can judge term has type . We can make a conclusion, in context , we can judge the type of is .
- T-Application: with the premise, with context and term binds to type and with context we can judge term has type . We can make a conclusion, in context , we can judge the type of is .
author: Lîm Tsú-thuàn/林子篆/Danny