# Foundations of Functional Programming/Comparison of λ-calculi

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? ${\displaystyle {\text{Type}}:{\text{Type}}}$ property? 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