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
