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.