[Haskell-cafe] Exponential complexity of type checking (Was:
Type-level naturals & multiplication)
dan.doel at gmail.com
Tue Oct 13 18:10:08 EDT 2009
On Tuesday 13 October 2009 1:06:41 pm Brad Larsen wrote:
> Good example! I have a feeling that the `dup' example is a bit
> contrived, not something that one would be likely to find in the wild.
This is, after all, why HM is useful. In general, there are programs that take
exponential time/space to type check, but those programs don't come up much in
Also, you can do better than 2^n:
f0 x = (x,x)
f1 = f0 . f0
f2 = f1 . f1
f3 = f2 . f2
Here, if fN results in a nested tuple of size M, then f(N+1) results in a
tuple of size M^2, since we replace all the variables with a copy of the
tuple. So we have 2, 4, 16, 256, ... 2^(2^N) .... Turning f0 into an M-tuple
gets you M^(2^N), I believe, and composing K times at each step would get you
M^(K^N). But anyhow, we have not merely an exponential, but a double
exponential. :) f4 takes a noticeable amount of time to check here (in ghci),
and f5 makes my machine start swapping.
Of course, one isn't likely to write code like this, either.
More information about the Haskell-Cafe