Find the most general types of the following lambda calculus terms

Question

I am having trouble understand why these are the most general types for their respective Church numerals:

2 = λf.λx. f (f x) : (α → α) → α → α 

1 = λf.λx. f x : (α → β) → α → β

0 = λf.λx. x : β → α → α

I thought that all Church numerals had the same type :

(α → α) → α → α 

Also how would I find a general type for the add operator

λm.λn.λf.λx. m f (n f x)

Any help would really be appreciated, thank you!

Answer 1

Let's start with the Church numeral for zero:

λf.λx. x : β → α → α

Looking only at λf.λx. part, one can deduce that we have a two-argument function, hence its type is α → β → γ, where α and β stand for arguments' types and γ stands for the result type. Now, the body x constraints the type further: our function's return type must be the same as its second argument's type. That results in α → β → β, or after renaming (α ↔ β): λf.λx. x : β → α → α. That's the most general type for zero, since we didn't use the fact that f should be a function, in fact, the Church zero numeral in untyped lambda calculus doesn't care: it just forgets it's first argument. And since β is just a placeholder, you can specialize it to α → α, which results in a more concrete type for zero -- λf.λx. x : (α → α) → α → α.

Let's look at 1:

λf.λx. f x : (α → β) → α → β

Again, it's a two-argument function: α → β → γ, but this time (look at the body of 1) we know the first argument f is a function, so f has some type δ → ε, which we should substitute for α: (δ → ε) → β → γ. Now, we know that we must be able to apply f to x, which means that the type of x and the type of f's argument must be equal: δ = β, thus, we've reached (β → ε) → β → γ. But that is not all we know, f x has type ε, and our numeral returns f x, applying this information, we get ε = γ. Incorporating all that, we arrive at (β → γ) → β → γ, or after renaming: λf.λx. f x : (α → β) → α → β. Again we didn't use any information about our usage intensions, that's why we've got the most general type and, of course, it can be specialized (by the restriction β = α) to λf.λx. f x : (α → α) → α → α.

It's 2's turn now:

λf.λx. f (f x) : (α → α) → α → α

I won't repeat all the steps this time, but (as an intermediate step) we can arrive at λf.λx. f (f x) : (α → β) → α → β. Notice, however, that this time we're feeding f's result into itself: f (f x), and this means that f's input and output types must be equal, thus β = α, and the most general type is λf.λx. f (f x) : (α → α) → α → α this time.

(*) Note that Church's 3, 4, etc. have the same most general type as 2 do, because multiple function applications don't give us any additional information to specialize the type further.

---

As for the addition function λm.λn.λf.λx. m f (n f x), let me be a bit more terse:

• Assume the expression has type α → β → γ → δ → ε.
• m is a function of 2 arguments: α must be restricted to α' → α'' → α'''
• Same for n: β must be restricted to β' → β'' → β'''
• m's and n's first argument has the same type, which is the type of f: α' = β' = γ
• n's second argument's type is δ
• n's result type equals to m's second argument type: β''' = α''
• Let's combine all the above knowledge for n : γ → δ → α''
• Same for m : γ → α'' → ε
• Hence, the result type is (γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

Let's rename the variables to make it look a bit prettier:

the most general type for λm.λn.λf.λx. m f (n f x) is

(β → γ → ε) → (β → α → γ) → β → α → ε.

Let's check that it can be specialized to what one would expect to be a binary operation on Church numerals (β = α → α, γ = α, ε = α):

((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.