## DEV Community is a community of 892,765 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

Posted on • Originally published at dannypsnl.github.io on

# 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 λ→ 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 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 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.

## Discussion (1) Unfortunately, this kind of article with so many latex symbols, post it to dev.to is so hard. 😭