[Haskell-cafe] Exponential complexity of type checking (Was:
Type-level naturals & multiplication)
brad.larsen at gmail.com
Tue Oct 13 12:04:46 EDT 2009
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.
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?)
More information about the Haskell-Cafe