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

[Brad Larsen]

On Tue, Oct 13, 2009 at 12:32 PM, Serguey Zefirov <sergueyz at gmail.com> wrote:
> 2009/10/13 Lennart Augustsson <lennart at augustsson.net>:
>> 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.
>

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.

Heavily parameterized type classes, on the other hand, are more common
in real code.  Hence, that is more likely where someone would run into
really awful type inference performance without expecting it.

Brad