ByteLabs

Again I would like to draw an interesting example from Benjamin Pierce’s book Types and Programming Languages that is originally due to Kfoury, Tiuryn, and Urzyczyn. The following Haskell program is well typed but takes a very long time to typecheck:

module Main (main) where
main =
 let f0 = \x -> (x,x)
     f1 = \y -> f0 (f0 y)
     f2 = \y -> f1 (f1 y)
     f3 = \y -> f2 (f2 y)
     f4 = \y -> f3 (f3 y)
     f5 = \y -> f4 (f4 y)
 in
 f5 (\z -> z)

It has long been believed that type-checking programs in languages that allow for let-polymorphism appears to be “essentially linear” in the size of the input program. It therefore came as a surprise that its worst-case complexity is still exponential as the above example demonstrates ;-)