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 227+1 occurrences of α.
Generalizing, the expression E(k, n) builds up functions whose types are T(n), T(n2), ..., T(nk) and has a type containing 2nk+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 2256+1 occurrences of α – that's about 1077.
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.