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


Ignore:
Timestamp:
Dec 9, 2012 9:56:07 PM (3 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