[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

[Dan Doel]

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