Expressions with exponentially large types

From Spivey's Corner
Jump to: navigation, search

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.

Card.png

Personal tools

Variants
Actions
Navigation
Tools