#kse

Church Typing

Church-style typing is a strict approach to assigning types in lambda calculus. It ensures that every variable and function has an explicit type annotation, making the system more structured and predictable.

Basic Notation

Each term in lambda calculus is explicitly typed. The general form is:

λ x^{α} . u

This means:

$x$ is a variable.
$α$ is its type.
$u$ is the expression that uses $x$ .

For example, the identity function in Church-style typing:

λ x^{α} . x

has the type:

α \to α

Church Typing Rules

Church-style typing follows strict inference rules to determine the type of expressions.

1. Variable Typing Rule

If $x$ has type $α$ , then in any context $Γ$ , we can state:

Γ ⊢ x : α

Example:

If $x$ is an integer, then:

Γ ⊢ x : int

2. Function Typing (Lambda Abstraction Rule)

If an expression $u$ has type $β$ when $x$ has type $α$ , then the function $λ x . u$ has type $α \to β$ :

Γ, x : α ⊢ u : β \Rightarrow Γ ⊢ (λ x . u) : (α \to β)

Example:

For the function:

λ x^{int} . y^{string}

we assign:

int \to string

3. Function Application Rule

If $u$ is a function of type $α \to β$ , and $v$ has type $α$ , then applying $u$ to $v$ results in type $β$ :

Γ ⊢ u : (α \to β), Γ ⊢ v : α \Rightarrow Γ ⊢ (u v) : β

Example:

If we have:

(λ x^{int} . "x") 5

Since $λ x . x$ has type $int \to string$ , and $5$ has type $int$ , the result is a $string$ .

Typing Example: Selecting the First Argument

Consider the function:

λ p . λ q . p

Step 1: Assigning Types

Assume $p$ has type $α$ .
Assume $q$ has type $β$ .
Since $λ q . p$ returns $p$ , it has type $(β \to α)$ .
Then, $λ p . λ q . p$ has type $(α \to (β \to α))$ .

Notice!

Function $λ p . λ q . p$ produces another function that selects the first argument $p$ !

Step 2: Typing Derivation

Typing $p$
$Γ, p : α ⊢ p : α$
Typing $λ q . p$

Since $p$ has type $α$ , we infer:
$Γ, q : β, p : α ⊢ q : β$
So,
$Γ, p : α ⊢ (λ q . p) : (β \to α)$
Typing the full abstraction $λ p . λ q . p$
$Γ ⊢ (λ p . λ q . p) : (α \to (β \to α))$

✅ Final Type:

(λ p . λ q . p) : (α \to (β \to α))

Why Church Typing is More Restrictive

Church-style typing is more strict than Curry-style typing because:

It requires every term to have an explicit type annotation.
It does not allow implicit type inference, unlike Curry typing.
It prevents ambiguity in function definitions.
It ensures that every function has a well-defined type signature.

Feature	Church Typing	Curry Typing
Explicit types	✅ Required	❌ Inferred
Type annotations	✏️ Written in terms	🚀 Inferred from context
Flexibility	❌ More strict	✅ More flexible
Common in	Formal systems, logic	Functional programming

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