Simply Typed Lambda Calculus

Simply typed lambda calculus extends lambda calculus by assigning types to each term, ensuring that only valid operations occur. This prevents meaningless expressions and introduces structure to computation. Simply typed lambda calculus is more restrictive than untyped lambda calculus but ensures logical consistency.

Basic Notation and Typing Rules

Each term in lambda calculus is assigned a type, written as:

which means variable $x$ has type $\alpha$.

Typing Approaches

There are two main approaches to typing in lambda calculus:

1. Church-style typing (explicit typing) ~ C++

   • Every variable and function must have an explicit type annotation.

   • The type of a term is written directly in the lambda expression.

   • Example:

     $$\lambda x_{\alpha }.x$$

     Here, $x$ is explicitly declared as having type $\alpha$.

   • More restrictive, as all terms must be explicitly typed.

   • Easier to analyze and ensures that every function has a known type.

2. Curry-style typing (implicit typing) ~ Python

   • Types are not explicitly written in lambda expressions.

   • Instead, types are inferred from the context $\mathrm{\Gamma }$ (typing environment).

   • Example:

     $$\mathrm{\Gamma }⊢x:\alpha$$

     This means $x$ has type $\alpha$ in the context $\mathrm{\Gamma }$, but we do not explicitly write the type in the expression.

   • More flexible, allowing implicit type inference.

   • Common in functional programming languages like Haskell and OCaml, where types are inferred automatically.

Key Differences

🚀 Church typing is stricter and ensures correctness, while Curry typing allows greater flexibility through type inference!