149 | | |
150 | | |
151 | | |
152 | | |
153 | | |
154 | | |
155 | | |
156 | | |
157 | | |
| 149 | ==== Using IFF Rules ==== |
| 150 | |
| 151 | These rules are used to replace a wanted constraint with a collection |
| 152 | of logically equivalent wanted constraints. If a wanted constraint |
| 153 | matches the head of one of these rules, than it is solved using the rules, |
| 154 | and the we generate new wanted constraints for the rule's assumptions. |
| 155 | |
| 156 | The 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 | |
| 161 | At present, IFF rules are used to define certain operators in terms of |
| 162 | others. For example, this is the only rule for solving constraints about |
| 163 | subtraction: |
| 164 | {{{ |
| 165 | forall a b c. (a + b ~ c) => (c - a ~ b) |
| 166 | }}} |
| 167 | |
| 168 | ==== Using Axioms ==== |
| 169 | |
| 170 | Basic operators are defined with an infinite family of axiom schemes. |
| 171 | As we can't have these written as a long list (searching might never stop!), |
| 172 | we have some custom code that checks to see if a constraint might be |
| 173 | solvable using one of the definitional axioms (see `solveWithAxiom`, `byAxiom`). |
| 174 | |
| 175 | |
| 176 | ==== Using the Order Model ==== |
| 177 | |
| 178 | Constraints about the ordering of type-level numbers are kept in a datastructure |
| 179 | (`LeqFacts`) which forms a ``model'' of the information represented by the |
| 180 | constraints (in a similar fashion to how substitutions form a model for a |
| 181 | set of equations). |
| 182 | |
| 183 | The purpose of the model is to eliminate redundant constraints, and to make |
| 184 | it easy to find proofs for queries of the form `x <= y`. In practise, |
| 185 | of particular interest are questions such as `1 <= x` because these appear |
| 186 | as assumptions on a number of rules (e.g., cancellation of multiplication). |
| 187 | In the future, this model could also be used to implement an interval |
| 188 | analysis, which would compute intervals approximating the values of |
| 189 | variables. |
| 190 | |
| 191 | TODO: At present, this model is reconstructed every time it needs to be used, |
| 192 | which is a bit inefficient. Perhaps it'd be better to use this directly |
| 193 | as the representation of `<=` constraints in the inert set. |
| 194 | |
| 195 | The 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 | |
| 199 | So, to find a proof of `A <= B`, we insert `A` and `B` in the model, |
| 200 | and then look for a path from `A` to `B`. The proofs on the path |
| 201 | can be composed using the rule for transitivity of `<=` to form the final proof. |
| 202 | |
| 203 | When manipulating the model, we maintain the following "minimality" |
| 204 | invariant: there should be no direct edge between two vertices `A` |
| 205 | and `B`, if there is a path that can already get us from `A` to `B. |
| 206 | Here 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 | |
| 217 | The purpose of the invariant is to eliminate redundant information. |
| 218 | Note, however, that it does not guarantee that there is a unique way |
| 219 | to prove a goal. |
| 220 | |
| 221 | |
| 222 | ==== Using Extended Assumptions === |
| 223 | |
| 224 | Another way to prove a goal is to look it up in the assumptions. |
| 225 | If the goal matched an assumption exactly, then GHC would have |
| 226 | already solved it in one of its previous stages of the constraint |
| 227 | solver. However, due to the commutativity and associativity of some of the |
| 228 | operators, it is possible to have goal that could be solved by assumption, |
| 229 | only if the assumption was "massaged" a bit. |
| 230 | |
| 231 | This "massaging" is implemented by the function `widenAsmps`, which |
| 232 | extends the set of assumption by performing a bit of forward reasoning |
| 233 | using a limited set of rules. Typically, these are commutativity |
| 234 | an associativity rules, and the `widenAsmps` function tries to complete |
| 235 | the 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 | |
| 244 | Note that the extended assumptions are very similar to derived constraints, |
| 245 | except that we keep their proofs. |
| 246 | |
| 247 | |
| 248 | ==== Re-examining Wanteds ==== |
| 249 | |
| 250 | If none of the strategies for solving a wanted constraint worked, |
| 251 | then the constraint is added to the inert set. Since we'd like to |
| 252 | keep the inert set minimal, we have to see if any of the existing |
| 253 | wanted constraints might be solvable in terms of the new wanted |
| 254 | (`reExamineWanteds`). |
| 255 | |
| 256 | It 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 | |
| 263 | We consider each (numeric) wanted constraint in the inert set and |
| 264 | check if we can solve it in terms of the new wanted and all other wanteds. |
| 265 | If so, then it is removed from the inert set, otherwise it stays there. |
| 266 | |
| 267 | Note that we can't implement this by kicking out the existing wanted |
| 268 | constraints and putting them back on the work queue, because this would |
| 269 | lead 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 | |
| 283 | Perhaps there is a way around this but, for the moment, we just re-examine |
| 284 | the numeric wanteds locally, without going through the constraint |
| 285 | solver 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 | |