127 | | We should apply !SubstFam first as it cheaper and potentially reduces the number of applications of Top. On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with !SubstFam. (That strategy should lend itself well to an implementation.) But be careful, we need to apply Top exhaustively, to avoid non-termination. More precisely, if we interleave Top and SubstFam, we can easily diverge. |
| 127 | We should apply !SubstFam first as it cheaper and potentially reduces the number of applications of Top. On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with !SubstFam. (That strategy should lend itself well to an implementation.) But be careful, we need to apply Top exhaustively, to avoid non-termination. More precisely, if we interleave Top and !SubstFam, we can easily diverge. |
| 177 | === === |
| 178 | |
| 179 | Example 4 of Page 9 of the ICFP'09 paper. |
| 180 | |
| 181 | {{{ |
| 182 | F [Int] ~ F (G Int) |- G Int ~ [Int], H (F [Int]) ~ Bool |
| 183 | =(norm)=> |
| 184 | F [Int] ~ a, F b ~ a, G Int ~ b |
| 185 | |- |
| 186 | G Int ~ [Int], H x ~ Bool, F [Int] ~ x |
| 187 | (SubstFam w/ F [Int]) |
| 188 | F [Int] ~ a, F b ~ a, G Int ~ b |
| 189 | |- |
| 190 | G Int ~ [Int], H x ~ Bool, x ~ a |
| 191 | (SubstFam w/ G Int) |
| 192 | F [Int] ~ a, F b ~ a, G Int ~ b |
| 193 | |- |
| 194 | b ~ [Int], H x ~ Bool, x ~ a |
| 195 | (SubstVar w/ x) |
| 196 | F [Int] ~ a, F b ~ a, G Int ~ b |
| 197 | |- |
| 198 | b ~ [Int], H a ~ Bool, x ~ a |
| 199 | }}} |
| 200 | |
| 201 | '''TODO:''' If we use flexible variables for the flattening of the wanteds, too, the equality corresponding to `x ~ a` above will be oriented the other way around. That can be a problem because of the asymmetry of the SubstVar and SubstFun rules (i.e., wanted equalities are not substituted into locals). |