[Haskell-cafe] Docs on the current and future constraint solver?

[Thomas Schilling]

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 <coreyoconnor at 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 at 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.