2009/10/13 Lennart Augustsson :

Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ...

xn will have a type with 2^n type variables so it has size 2^n.

Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will be 2^(number of dup's). I experimented and found that GHC can stand pretty long line of dup's. More than 20, at least. One part of our program took too much time to typecheck some time ago. 3 and half minutes for ~900 lines module. Most of operations was inside heavily parametrized monad (5 parameters, each is a Peano number). Then my colleague moved parameters into associated types of relevant type class and now it typechecks in ten seconds.

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

On Wednesday 14 October 2009 5:25:10 am Roel van Dijk wrote:

With newtypes I can probably abstract even more. (newtype X a b = X (a (a b))

In fact, with GHC extensions, you don't need newtypes: {-# LANGUAGE LiberalTypeSynonyms #-} type T a = (a,a) type X f a = f (f a) f0 :: a -> T a f0 x = (x,x) f1 :: a -> X T a f1 = f0 . f0 f2 :: a -> X (X T) a f2 = f1 . f1 f3 :: a -> X (X (X T)) a f3 = f2 . f2 f4 :: a -> X (X (X (X T))) a f4 = f3 . f3

Inferring the type of f5 also stops my machine in its tracks. But I *was* able to infer the type of (f4 . f4).

:t (f4 . f4)

(f4 . f4) :: a -> T16 (T16 a)

:t f5

Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms, while checking f5 does for some reason. I'm perplexed that having f5 defined in the file doesn't trigger the explosion unless you declare a type (even in terms of X and T) or ask for its type at the prompt. -- Dan

On Wednesday 14 October 2009 6:15:11 am Roel van Dijk wrote:

If you declare a type for f5 then ghci must check if that type is correct, which triggers the explosion. If you don't declare a type then it won't infer the type until necessary. Basically, ghci is lazy

Well, that may be the explanation, but it's a bit more convoluted than I'd have initially thought. For instance, if I write: e = head () it fails immediately with a type error, so clearly it must be doing some level of checking immediately. However, it only needs to check 'head' and '()' to notice that they're incompatible, so I suppose it may not need to compute the type of e (were it well-typed). But then, adding: f6 = f5 . f5 produces no more delay than before. Nor does: g = snd . f5 So ghci is able to verify that f5 can be instantiated to the forms a -> b and b -> c in the first case, and that it is of the form a -> (b,c) in the second case, without blowing up. However, either of: e = f5 () e' () = f5 () does blow up, so it must be verifying more than the fact that f5 is of the form a -> b, where a can be instantiated to (), which is odd if it's smart enough to only compute the portion of the type necessary to verify that applications can be well typed. -- Dan