# Expressions with exponentially large types

Consider Haskell expressions like

letfx= (x,x)inletg=f.f.finleth=g.g.ginh.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:

letfx= (x,x)inletg=f.f.f.finleth=g.g.g.ginletp=h.h.h.hinp.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

letfxp=pxxinletg=f.f.finleth=g.g.ginh.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.