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

Show
Ignore:
Timestamp:
12/09/12 13:56:07 (6 months ago)
Comment:

--

Unmodified
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
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