# Expressions with exponentially large types

Consider Haskell expressions like

let f x = (x, x) in let g = f . f . f in let h = g . g . g in h . h . h

I'll call this expression *E*(3, 3) because there are three layers using *f*, *g* and *h*, and in each layer three copies of a function are composed, as in *f* . *f* . *f*.
In this expression, the type of *g* is

- α → (((α, α), (α, α)), ((α, α), (α, α)))

which has the shape of a complete binary tree of depth three; I'll call it *T*(3). The type of *h* is obtained by substituting this type into itself to depth three, and is therefore *T*(9); and the type of the whole expression is correspondingly *T*(27). When printed out, it contains 2^{27}+1 occurrences of α.

Generalizing, the expression *E*(*k*, *n*) builds up functions whose types are *T*(*n*), *T*(*n*^{2}), ..., *T*(*n*^{k}) and has a type containing 2^{nk}+1 occurrences of α. If the type of *E*(3, 3) isn't big enough, then *E*(4, 4) still fits on one line:

let f x = (x, x) in let g = f . f . f . f in let h = g . g . g . g in let p = h . h . h . h in p . p . p . p

and has a type containing 2^{256}+1 occurrences of α – that's about 10^{77}.

It's still more satisfying to avoid the pair constructor and use a Church encoding instead. In the expression

let f x p = p x x in let g = f . f . f in let h = g . g . g in h . h . h

the type of *g* is

- α -> (((((α -> α -> β) -> β) -> ((α -> α -> β) -> β) -> γ) -> γ) -> ((((α -> α -> β) -> β) -> ((α -> α -> β) -> β) -> γ) -> γ) -> δ) -> δ

which contains the expected eight occurrences of α, but also eight β's, four γ's and two δ's. And so on.