This page compares λ-calculi according to various interesting properties they have. We give a table which concisely lays out all of the information for the calculi we discuss, followed by an explanation of each property featured in the table.
System
Implicit types?
Polymorphic types?
Type constructors?
Dependent types?
Type
:
Type
{\displaystyle {\text{Type}}:{\text{Type}}}
Turing complete?
Normalizing?
Consistent?
Type checking decidable?
Typability decidable?
Types unique?
Subject reduction theorem?
Untyped λ-calculus
Yes
No
No
No
No
Yes
No
No
Yes
Yes
Yes
Yes
Implicitly simply typed λ-calculus
Yes
No
No
No
No
No
Yes
Yes
Yes
Yes
No
Yes
Explicitly simply typed λ-calculus (λ→)
No
No
No
No
No
No
Yes
Yes
Yes
Yes
Yes
Yes
Implicitly typed second-order λ-calculus
Yes
Yes
No
No
No
No
Yes
Yes
No
No
No
Yes
Explicitly typed second-order λ-calculus (λ2)
No
Yes
No
No
No
No
Yes
Yes
Yes
Yes
Yes
Yes
Hindley-Milner type theory
Yes
Yes
No
No
No
Yes
No
No
Yes
Yes
No
Yes
λP
No
No
No
Yes
No
No
Yes
Yes
Yes
Yes
Yes
Yes
λP2
No
Yes
No
Yes
No
No
Yes
Yes
Yes
Yes
Yes
Yes
λω
No
No
Yes
No
No
No
Yes
Yes
Yes
Yes
Yes
Yes
λω
No
Yes
Yes
No
No
No
Yes
Yes
Yes
Yes
Yes
Yes
λPω
No
No
Yes
Yes
No
No
Yes
Yes
Yes
Yes
Yes
Yes
Calculus of constructions (λPω)
No
Yes
Yes
Yes
No
No
Yes
Yes
Yes
Yes
Yes
Yes
Naïve type theory (λ*)
No
Yes
Yes
Yes
Yes
?
No
No
No
No
Yes
Yes
