#kse

Curry Typing

Curry-style typing is a more flexible approach to assigning types in lambda calculus. Unlike Church-style typing, types are not explicitly written in the expressions but are instead inferred from the context. This makes Curry typing less strict and closer to modern functional programming languages, where type inference plays a significant role.

Basic Notation

Curry-style typing is expressed using typing judgments, written as:

Γ ⊢ x : α

where:

$Γ$ (the typing context) contains known type assignments.
$x$ is the term being typed.
$α$ is the inferred type of $x$ .

Unlike Church-style typing, types are not explicitly written in the lambda expression itself. Instead, the type of each term is derived from the context.

Remark

In Curry typing, it is common to use $\frac{b l a, b l a}{b l a}$ notation to represent implication $⟹$ . For example:

Γ ⊢ u : (α \to β), Γ ⊢ v : α ⟹ Γ ⊢ (u v) : β is the same as \frac{Γ ⊢ u : (α \to β), Γ ⊢ v : α}{Γ ⊢ (u v) : β}

Curry Typing Rules

Curry-style typing follows a set of inference rules to determine the type of expressions.

1. Variable Typing Rule

If $x$ has type $α$ in the context $Γ$ , then:

Γ, x : α ⊢ x : α

This means we can directly infer the type of a variable from the context.

Example:

If $Γ$ states that $x$ is an integer, then:

Γ, x : int ⊢ x : int

2. Function Application Rule

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

\frac{Γ ⊢ u : (α \to β), Γ ⊢ v : α}{Γ ⊢ (u v) : β}

Example:

If we have:

(λ x . x) 5

Since $λ x . x$ has type $(int \to int)$ and $5$ has type $int$ , the application results in $int$ .

3. Function Abstraction Rule

If $u$ has type $β$ in context $Γ, x : α$ , then the function $λ x . u$ has type $(α \to β)$ :

\frac{Γ, x : α ⊢ u : β}{Γ ⊢ (λ x . u) : (α \to β)}

Example:

For the function:

λ x . x + 1

we assign:

int \to int

since $x$ is inferred to be an integer.

Typing Examples

Example 1: Identity Function

λ p . λ q . p

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 α))$ .

✅ Final Type:

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

Notice!

Function $λ p . λ q . p$ returns a new function!

Example 2: Function Application

λ z . (z M) N

Assigning Types

Assume $z$ is of type $(α \to β)$ .
Assume $M$ is of type $α$ .
Then, $(z M)$ results in type $β$ .
Assume $N$ has type $γ$ .
Since $(z M) N$ means applying $(z M)$ to $N$ , we require $β = γ \to δ$ .
Thus, $(z M) N$ has type $δ$ .

✅ Final Type:

(λ z . (z M) N) : (α \to (γ \to δ)) \to δ

Why Curry Typing is More Flexible

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

It does not require explicit type annotations in lambda expressions.
It allows type inference, meaning types are deduced from context instead of being written explicitly.
It enables polymorphism, meaning functions can be used with multiple types.
It is more similar to real-world functional programming languages like Haskell, where types are inferred automatically.

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

🚀 Curry typing is more flexible and allows implicit type inference, making it practical for programming languages!