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


Ignore:
Timestamp:
Dec 9, 2012 9:56:07 PM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeNatSolver

    v7 v8  
    147147      3. Generate new derived facts. 
    148148 
    149  
    150  
    151  
    152  
    153  
    154  
    155  
    156  
    157  
     149==== Using IFF Rules ==== 
     150 
     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. 
     155 
     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). 
     160 
     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 
     163subtraction: 
     164{{{ 
     165    forall a b c. (a + b ~ c) => (c - a ~ b) 
     166}}} 
     167 
     168==== Using Axioms ==== 
     169 
     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`). 
     174 
     175 
     176==== Using the Order Model ==== 
     177 
     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). 
     182 
     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 
     189variables. 
     190 
     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. 
     194 
     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`. 
     198 
     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. 
     202 
     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) 
     207{{{ 
     208    B                                            B 
     209    |\                                          / \ 
     210    | C                                        C   D 
     211    |/                                          \ / 
     212    A                                            A 
     213 
     214 Invariant does not hold                 Invariant holds 
     215}}} 
     216 
     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. 
     220 
     221 
     222==== Using Extended Assumptions === 
     223 
     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. 
     230 
     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: 
     236{{{ 
     237    assumptions: C: x + y ~ z 
     238    cur. goal:   D: y + x ~ z 
     239 
     240    extended assumptions: C: x + y ~ z, Add_Comm(C) : y + x ~ z 
     241    solved:               D = Add_Comm(C) 
     242}}} 
     243 
     244Note that the extended assumptions are very similar to derived constraints, 
     245except that we keep their proofs. 
     246 
     247 
     248==== Re-examining Wanteds ==== 
     249 
     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 
     254(`reExamineWanteds`). 
     255 
     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)). 
     262 
     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. 
     266 
     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: 
     270{{{ 
     271    inert: [W] A : x <= 5 
     272    new:   [W] B : y <= 5 
     273 
     274    Can't solve B, add to inert, kick out A 
     275    inert: [W] B : y <= 5 
     276    new:   [W] A : x <= 5 
     277 
     278    Can't solve A, add to inert, kick out B... 
     279 
     280    ... and we are back to the beginning. 
     281}}} 
     282 
     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. 
     286 
     287 
     288 
     289 
     290 
     291 
     292 
     293 
     294 
     295 
     296 
     297 
     298 
     299 
     300 
     301 
     302 
     303 
     304 
     305 
     306 
     307 
     308 
     309 
     310 
     311 
     312 
     313 
     314 
     315 
     316 
     317 
     318 
     319 
     320