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

[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.

  -- Lennart

On Tue, Oct 13, 2009 at 6:04 PM, Brad Larsen <brad.larsen at gmail.com> wrote:
> On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones
> <simonpj at microsoft.com> wrote:
>> | > Is there any way to define type-level multiplication without requiring
>> | > undecidable instances?
>> |
>> | No, not at the moment.  The reasons are explained in the paper "Type
>> | Checking with Open Type Functions" (ICFP'08):
>> |
>> |    http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf
>> |
>> | We want to eventually add closed *type families* to the system (ie,
>> | families where you can't add new instances in other modules).  For
>> | such closed families, we should be able to admit more complex
>> | instances without requiring undecidable instances.
>>
>> It's also worth noting that while "undecidable" instances sound scary, but all it means is that the type checker can't prove that type inference will terminate.  We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad.
>>
>> Simon
>>
>
> I have written code that makes heavy use of multi-parameter type
> classes in the ``finally tagless'' tradition, which takes several
> seconds and many megabytes of memory for GHCI to infer its type.
> However, that example is rather complicated, and I am not sure its
> type inference complexity is exponential---it is at least very bad.
>
> Are there any simple, well-known examples where Haskell type inference
> has exponential complexity?  Or Hindley-Milner type inference, for
> that matter?  (Haskell 98 is not quite Hindley-Milner?)
>
> Sincerely,
> Brad Larsen
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>