[Haskell-cafe] Exponential complexity of type checking (Was:
Type-level naturals & multiplication)
Dan Doel
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
real code.
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.
-- Dan
More information about the Haskell-Cafe
mailing list