Changes between Version 7 and Version 8 of Commentary/Compiler/TypeNatSolver

Dec 9, 2012 9:56:07 PM (3 years ago)



  • Commentary/Compiler/TypeNatSolver

    v7 v8  
    147147      3. Generate new derived facts.
     149==== Using IFF Rules ====
     151These rules are used to replace a wanted constraint with a collection
     152of logically equivalent wanted constraints.  If a wanted constraint
     153matches the head of one of these rules, than it is solved using the rules,
     154and the we generate new wanted constraints for the rule's assumptions.
     156The following are important properties of IFF rules:
     157  * They need to be sound (of course!)
     158  * The assumptions need to be logically equivalent to the conclusion (i.e., they should not result in a harder problem to solve than the original goal).
     159  * The assumptions need to be ''simpler'' from the point of view of the constraint solver (i.e., we shouldn't end up with the original goal after some steps---this would lead to non-termination).
     161At present, IFF rules are used to define certain operators in terms of
     162others.  For example, this is the only rule for solving constraints about
     165    forall a b c. (a + b ~ c) => (c - a ~ b)
     168==== Using Axioms ====
     170Basic operators are defined with an infinite family of axiom schemes.
     171As we can't have these written as a long list (searching might never stop!),
     172we have some custom code that checks to see if a constraint might be
     173solvable using one of the definitional axioms (see `solveWithAxiom`, `byAxiom`).
     176==== Using the Order Model ====
     178Constraints about the ordering of type-level numbers are kept in a datastructure
     179(`LeqFacts`) which forms a ``model'' of the information represented by the
     180constraints (in a similar fashion to how substitutions form a model for a
     181set of equations).
     183The purpose of the model is to eliminate redundant constraints, and to make
     184it easy to find proofs for queries of the form `x <= y`.  In practise,
     185of particular interest are questions such as `1 <= x` because these appear
     186as assumptions on a number of rules (e.g., cancellation of multiplication).
     187In the future, this model could also be used to implement an interval
     188analysis, which would compute intervals approximating the values of
     191TODO: At present, this model is reconstructed every time it needs to be used,
     192which is a bit inefficient.  Perhaps it'd be better to use this directly
     193as the representation of `<=` constraints in the inert set.
     195The model is a directed acyclic graph, as follows:
     196  * vertices: constants or variables (of kind `Nat`)
     197  * edges: the edge from `A` to `B` is a proof that `A <= B`.
     199So, to find a proof of `A <= B`, we insert `A` and `B` in the model,
     200and then look for a path from `A` to `B`.  The proofs on the path
     201can be composed using the rule for transitivity of `<=` to form the final proof.
     203When manipulating the model, we maintain the following "minimality"
     204invariant:  there should be no direct edge between two vertices `A`
     205and `B`, if there is a path that can already get us from `A` to `B.
     206Here are some examples (with edges pointing upwards)
     208    B                                            B
     209    |\                                          / \
     210    | C                                        C   D
     211    |/                                          \ /
     212    A                                            A
     214 Invariant does not hold                 Invariant holds
     217The purpose of the invariant is to eliminate redundant information.
     218Note, however, that it does not guarantee that there is a unique way
     219to prove a goal.
     222==== Using Extended Assumptions ===
     224Another way to prove a goal is to look it up in the assumptions.
     225If the goal matched an assumption exactly, then GHC would have
     226already solved it in one of its previous stages of the constraint
     227solver.  However,  due to the commutativity and associativity of some of the
     228operators, it is possible to have goal that could be solved by assumption,
     229only if the assumption was "massaged" a bit.
     231This "massaging" is implemented by the function `widenAsmps`, which
     232extends the set of assumption by performing a bit of forward reasoning
     233using a limited set of rules.   Typically, these are commutativity
     234an associativity rules, and the `widenAsmps` function tries to complete
     235the set of assumptions with respect to these operations.  For example:
     237    assumptions: C: x + y ~ z
     238    cur. goal:   D: y + x ~ z
     240    extended assumptions: C: x + y ~ z, Add_Comm(C) : y + x ~ z
     241    solved:               D = Add_Comm(C)
     244Note that the extended assumptions are very similar to derived constraints,
     245except that we keep their proofs.
     248==== Re-examining Wanteds ====
     250If none of the strategies for solving a wanted constraint worked,
     251then the constraint is added to the inert set.  Since we'd like to
     252keep the inert set minimal, we have to see if any of the existing
     253wanted constraints might be solvable in terms of the new wanted
     256It is good to keep the inert set minimal for the following reasons:
     257  * Inferred types are nicer,
     258  * It helps GHC to solve constraints by "inlining" (e.g., if we
     259    have only a single constraint `x + y ~ z`, then we can eliminate it
     260    by replacing all occurrences of `z` with `x + y`, however we can't
     261    do that if we ended up with two constraints `(x + y ~ z, y + x ~ z)).
     263We consider each (numeric) wanted constraint in the inert set and
     264check if we can solve it in terms of the new wanted and all other wanteds.
     265If so, then it is removed from the inert set, otherwise it stays there.
     267Note that we can't implement this by kicking out the existing wanted
     268constraints and putting them back on the work queue, because this would
     269lead to non-termination.  Here is an example of how this might happen:
     271    inert: [W] A : x <= 5
     272    new:   [W] B : y <= 5
     274    Can't solve B, add to inert, kick out A
     275    inert: [W] B : y <= 5
     276    new:   [W] A : x <= 5
     278    Can't solve A, add to inert, kick out B...
     280    ... and we are back to the beginning.
     283Perhaps there is a way around this but, for the moment, we just re-examine
     284the numeric wanteds locally, without going through the constraint
     285solver pipe-line.