Re: [Haskell-cafe] Docs on the current and future constraint solver?
On Fri, Jul 16, 2010 at 08:36:46AM -0700, Corey O'Connor wrote: On Wed, Jul 14, 2010 at 4:42 PM, Thomas Schilling nomin...@googlemail.com wrote: This solver is currently being implemented in GHC (there's a branch on darcs.h.o), but correctness comes first. It'll probably take a while until this new solver becomes efficient. Is this the URL of the branch? http://darcs.haskell.org/ghc-new-tc/ghc/ Yes. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
On Thu, Jul 15, 2010 at 12:57 AM, Simon Peyton-Jones simo...@microsoft.com wrote: Corey | On 14 July 2010 18:39, Corey O'Connor coreyocon...@gmail.com wrote: | I believe I have run headlong into issue #3064 in ghc | (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know | is this: | * this is a performance issue with the system used to solve type | constraints. | * the solver is undergoing an overhaul to resolve performance issues | in addition to other issues. | * An efficient constraint solver is difficult. NP-Complete in the general | case? It would be very helpful to have your code as a test case. Can you boil out a concrete program that demonstrates very poor performance of the type checker, and submit a Trac report? That way we'll test the new type inference engine against it. Lacking the example, we won't. Which is isn't a promise that we'll solve your problem -- but it's much easier to solve if we have a concrete example. Many thanks! Understood. I'll work on getting a nice, self-contained example. Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
On Wed, Jul 14, 2010 at 4:42 PM, Thomas Schilling nomin...@googlemail.com wrote: This solver is currently being implemented in GHC (there's a branch on darcs.h.o), but correctness comes first. It'll probably take a while until this new solver becomes efficient. Is this the URL of the branch? http://darcs.haskell.org/ghc-new-tc/ghc/ Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Docs on the current and future constraint solver?
Corey | On 14 July 2010 18:39, Corey O'Connor coreyocon...@gmail.com wrote: | I believe I have run headlong into issue #3064 in ghc | (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know | is this: | * this is a performance issue with the system used to solve type | constraints. | * the solver is undergoing an overhaul to resolve performance issues | in addition to other issues. | * An efficient constraint solver is difficult. NP-Complete in the general | case? It would be very helpful to have your code as a test case. Can you boil out a concrete program that demonstrates very poor performance of the type checker, and submit a Trac report? That way we'll test the new type inference engine against it. Lacking the example, we won't. Which is isn't a promise that we'll solve your problem -- but it's much easier to solve if we have a concrete example. Many thanks! Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
On Wed, Jul 14, 2010 at 4:42 PM, Thomas Schilling nomin...@googlemail.com wrote: The latest work is OutsideIn(X): http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn This is quite long paper. It describes a framework for constraint-based type inference and then instantiates it with a constraint solver that supports type families, GADTs and type classes. Sounds like it's a long paper with good reason ;-) I will start working my way through it. Thanks for the information. Cheers, Corey O'Connor On 14 July 2010 18:39, Corey O'Connor coreyocon...@gmail.com wrote: I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case? Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current? I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- If it looks like a duck, and quacks like a duck, we have at least to consider the possibility that we have a small aquatic bird of the family Anatidae on our hands. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
On Thu, Jul 15, 2010 at 12:42:41AM +0100, Thomas Schilling wrote: simplifications are possible. To make this efficient, the solver also regularly canonicalises constraints. E.g., function symbols go to the left and constructors to the right. One minor correction: the canonicalisation of constraints actually has more to do with ensuring that the solving process terminates than it does with efficiency. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Docs on the current and future constraint solver?
I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case? Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current? I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
The latest work is OutsideIn(X): http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn This is quite long paper. It describes a framework for constraint-based type inference and then instantiates it with a constraint solver that supports type families, GADTs and type classes. Constraint-based type inference divides type checking into two phases: constraint-generation and solving. In practice the two may be interleaved for efficiency reasons, of course. As an example (does not type check): type family C a type instance C Int = Int c :: a - C a f :: Int - Bool f = \n - c n In order to type check f we generate the *wanted* constraints (~ denotes equality) (c - C c) ~ (d - e) -- from c - n (d - e) ~ (Int - Bool) -- from type signature From the type family declarations we additionally get the top-level axiom: C Int ~ Int The wanted constraints are now simplified, e.g., c ~ d, C c ~ e -- from the first constraint d ~ Int, e ~ Bool -- from the second constraint c ~ Int, C c ~ Bool, d ~ Int, e ~ Bool-- from the above constraints C Int ~ Bool -- also Now we get an error when combining this with the top-level axiom. If the user specifies type class constraints in the type signature or performs a GADT pattern match we additionally get *given* constraints. The general solver state thus takes the form: G = W where G are the given constraints and W the wanted constraints and = is implication. The solver then reacts two constraints from G, two constraints from W, or one from each, until no more simplifications are possible. To make this efficient, the solver also regularly canonicalises constraints. E.g., function symbols go to the left and constructors to the right. Further performance improvements must come from clever indexing the current state to make the search for applicable rules efficient. This solver is currently being implemented in GHC (there's a branch on darcs.h.o), but correctness comes first. It'll probably take a while until this new solver becomes efficient. The paper does not talk about efficiency, but it lists all the rules and many other details. / Thomas On 14 July 2010 18:39, Corey O'Connor coreyocon...@gmail.com wrote: I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case? Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current? I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- If it looks like a duck, and quacks like a duck, we have at least to consider the possibility that we have a small aquatic bird of the family Anatidae on our hands. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
