On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones <[email protected]> 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 [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
