| 1 | {{{ |
| 2 | |
| 3 | |
| 4 | === Problem with Plan MS: Termination is still an issue === |
| 5 | |
| 6 | Example: |
| 7 | |
| 8 | F and G are type function constructors. Consider the local assumptions |
| 9 | |
| 10 | F (G Int) = Int -- (1) |
| 11 | G Int = F (G Int) -- (2) |
| 12 | |
| 13 | Applying (2) on (1) yields |
| 14 | |
| 15 | F (G Int) = Int |
| 16 | --> F (F (G Int)) = Int |
| 17 | --> F (F (F (G Int))) = Int |
| 18 | --> ... |
| 19 | |
| 20 | NOTE: |
| 21 | Plan MC rejects (2), cause the type equation is non-decreasing. |
| 22 | Here we are after a more liberal type checking method. |
| 23 | |
| 24 | === Plan MS revised overview === |
| 25 | |
| 26 | Plan MS only works if we "normalize" terms. Effectively, we represent |
| 27 | terms via CHR constraints, "term reductions" are then performed via |
| 28 | CHR solving steps. |
| 29 | |
| 30 | The big picture: |
| 31 | |
| 32 | Step 1 (normal form step): |
| 33 | |
| 34 | (a) We transform local and wanted type equations to CHR constraints. |
| 35 | (b) We transform type instances to CHR simplification rules. |
| 36 | |
| 37 | Step 2 (solving step): |
| 38 | |
| 39 | To derive wanted from local type equations wrt type instances, |
| 40 | we perform CHR solving steps. These CHR solving steps can be mapped |
| 41 | to "term reduction" steps. |
| 42 | |
| 43 | |
| 44 | The advantage of this method is that we can deal with |
| 45 | "non-terminating" local type equations (see above) and |
| 46 | "non-confluent" local type equations, e.g. |
| 47 | S Int = Int /\ S Int = F Int, and we don't need to orient |
| 48 | type equations. |
| 49 | Of course, we need to impose the usual conditions on |
| 50 | type instances, ie termination and confluence. |
| 51 | |
| 52 | === CHR vs Term reductions === |
| 53 | |
| 54 | How to phrase term reduction steps in terms of CHR solving steps. |
| 55 | The main task is to put terms into normal from. |
| 56 | |
| 57 | ==== Normal form ===== |
| 58 | |
| 59 | Terms are formed as follows |
| 60 | |
| 61 | t ::= a -- variable |
| 62 | | F -- type function constructor |
| 63 | | T -- ordinary type constructor |
| 64 | | t t -- type application |
| 65 | |
| 66 | Type equations are formed as follows |
| 67 | |
| 68 | Eq ::= t = t |
| 69 | | Eq /\ Eq |
| 70 | |
| 71 | |
| 72 | Type equations can easily be put into the following normal form |
| 73 | |
| 74 | n ::= a |
| 75 | | T |
| 76 | | n n |
| 77 | |
| 78 | C ::= a = n |
| 79 | | F n = n |
| 80 | | C /\ C |
| 81 | |
| 82 | |
| 83 | a set of type equations in normal form C, consists of equations of |
| 84 | the form a = n or F n = n where the normal form type n does not refer |
| 85 | to type function constructors. |
| 86 | |
| 87 | |
| 88 | Example: |
| 89 | |
| 90 | The normal form of |
| 91 | |
| 92 | F (G Int) = Int |
| 93 | G Int = F (G Int) |
| 94 | |
| 95 | from above is |
| 96 | |
| 97 | F a = Int |
| 98 | G Int = a |
| 99 | G Int = b |
| 100 | F b = c |
| 101 | G Int = c |
| 102 | |
| 103 | The first two equations are derived from F (G Int) = Int. That is, we |
| 104 | replace G Int by a where a is a fresh wobbly variable. |
| 105 | The last three equations result from replacing G Int on the rhs of |
| 106 | G Int = F (G Int) by b which leads to G Int = F b, then we replace |
| 107 | F b by c and we are done. |
| 108 | |
| 109 | NOTE: We consider a, b, c as wobbly type variables. |
| 110 | |
| 111 | |
| 112 | Similarly, we build the normal form of type instances. |
| 113 | For example, the normal form of |
| 114 | |
| 115 | forall a. F [a] = [F a] |
| 116 | |
| 117 | is |
| 118 | |
| 119 | forall a. exists b. F [a] = b /\ b=[F a] |
| 120 | |
| 121 | |
| 122 | NOTE: |
| 123 | |
| 124 | We must build the normal form of type instances. Otherwise, application of |
| 125 | type instances may break the normal form property. Eg. consider |
| 126 | application of forall a. F [a] = [F a] |
| 127 | on F [Int] = b /\ S Int = b. |
| 128 | |
| 129 | It should be clear that a normal form equation such as F a = Int, |
| 130 | can be viewed as the CHR constraint F a Int, and |
| 131 | forall a. exists b. F [a] = [b] /\ b=F a as |
| 132 | the CHR simplification |
| 133 | rule F [a] [b] <==> F a b |
| 134 | |
| 135 | |
| 136 | ==== Mapping CHR derivations to term derivations and vice versa ==== |
| 137 | |
| 138 | |
| 139 | Let t1=t1' /\ .... /\ tk=tk' be a set of type equations and |
| 140 | C its normal form. Let TT be a set of type instances and |
| 141 | TT_n its normal form. |
| 142 | |
| 143 | We build a canonical form of t1=t1' /\ .... /\ tk=tk' |
| 144 | by solving C wrt rules TT_n plus the standard FD rule, ie |
| 145 | C -->* C'. This CHR derivation can be mapped to a term derivation |
| 146 | t1=t1' /\ .... /\ tk=tk' -->* t1''=t1''' /\ ... /\ tl''=tl''' |
| 147 | (ie a sequence of rule applications using the FC type equation rules). |
| 148 | |
| 149 | |
| 150 | The CHR solving steps in detail: |
| 151 | |
| 152 | FD solving step: |
| 153 | |
| 154 | Let C \equiv C' /\ F n1 = n2 /\ F n1 = n3. |
| 155 | |
| 156 | Then, C --> C' /\ F n1 = n2 /\ n2 = n3 |
| 157 | |
| 158 | In the above, we still use the (normal form) term representation. |
| 159 | In the CHR constraint notation, the FD solving step is written |
| 160 | |
| 161 | C' /\ F n1 n2 /\ F n1 n3 |
| 162 | --> C /\ F n1 n2 /\ n2 = n3 |
| 163 | |
| 164 | The point is that the "actual" type equations only contain |
| 165 | normal form types. |
| 166 | |
| 167 | This solving step can be mapped back to a term reduction step. |
| 168 | Let t1''=t1''' /\ ... /\ tl''=tl''' be the term representation |
| 169 | of C' /\ F n1 = n2 /\ n2 = n3 (ie we remove the wobbly variables |
| 170 | we've introduced earlier in the normal form step). |
| 171 | Then, |
| 172 | |
| 173 | t1=t1' /\ .... /\ tk=tk' --> t1''=t1''' /\ ... /\ tl''=tl''' |
| 174 | |
| 175 | this is now a term reduction step |
| 176 | (using the type equation rules of the FC system) |
| 177 | |
| 178 | |
| 179 | Type instance step: |
| 180 | |
| 181 | Let C \equiv C' /\ F n1 = n2 |
| 182 | |
| 183 | and forall a. F n3 = n4 /\ C in TT_n such that |
| 184 | phi(n3) = n1 for some substitution phi where dom(phi)=a. |
| 185 | |
| 186 | Then, C --> C' /\ phi(n4) = n2 /\ phi(C). |
| 187 | |
| 188 | As before, we also give the derivation in CHR constraint notation. |
| 189 | C' /\ F n1 n2 |
| 190 | --> C' /\ phi(n4) = n2 /\ phi(C) |
| 191 | |
| 192 | This solving step can be mapped back to a term reduction step |
| 193 | (a type instance application step). |
| 194 | |
| 195 | |
| 196 | Equivalence step: |
| 197 | |
| 198 | The FD and type instance step introduce equations among normal form types. |
| 199 | We build the mgu of these normal form equations (for this step it's |
| 200 | helpful to use the CHR constraint notation). |
| 201 | |
| 202 | |
| 203 | === Plan MS revised details === |
| 204 | |
| 205 | Let TT be a set of type instances, |
| 206 | C and W a set of constraints already in normal form where |
| 207 | C are the local equations and W are the wanted equations. |
| 208 | |
| 209 | We check that W follows from C wrt TT as follows. |
| 210 | |
| 211 | We rewrite (C | W) to (C' | W') by performing the following steps. |
| 212 | |
| 213 | Reduce C step: |
| 214 | Apply FD and CHR simp steps on C, ie C -->* C', we obtain |
| 215 | |
| 216 | (C | W) --> (C' | W) |
| 217 | |
| 218 | Reduce W type instance step |
| 219 | Apply CHR simp steps on W, ie W -->* W', we obtai |
| 220 | |
| 221 | |
| 222 | (C | W) --> (C | W') |
| 223 | |
| 224 | NOTE: we could also apply FD steps on W, no harm. |
| 225 | |
| 226 | Reduce W wrt C step: |
| 227 | |
| 228 | If C \equiv C' /\ F n1 = n2 and W \equiv F n1 = n3 /\ W' |
| 229 | then |
| 230 | |
| 231 | (C | W) --> (C | W' /\ n2 = n3) |
| 232 | |
| 233 | |
| 234 | We exhaustively apply the above steps (if TT is terminating the steps |
| 235 | are terminating). That is, |
| 236 | |
| 237 | (C | W) -->* (C' | W') |
| 238 | |
| 239 | then check if W' is a subset of C'. If yes, W follows from C wrt TT. |
| 240 | |
| 241 | NOTE: |
| 242 | |
| 243 | In the reduce W wrt C step, adding n2 = n3 to C as well is wrong. |
| 244 | We could also first reduce C -->* C', then |
| 245 | C' /\ W -->* C'' and check that C'' and C' are equivalent (by exploiting |
| 246 | the fact that C implies W iff C <-> C /\ W). |
| 247 | |
| 248 | |
| 249 | ==== A note on efficiency ==== |
| 250 | |
| 251 | The normal from representation has the advantage that searching for |
| 252 | "matchings" becomes "easier". Eg in case of the (earlier) plan MS and plan MC, |
| 253 | given the local assumption S s1 ... sn = t we traverse/search all |
| 254 | terms to find matching partners S s1 ... sn which then will be replaced by t. |
| 255 | Consider the local G Int = Int and the term [Tree [G Int]] where we first |
| 256 | traverse two list nodes and a tree node before we find the matching partner. |
| 257 | In the normal from representation, we use a "flat" representation, all potential |
| 258 | matchings must be at the "outer" level. We could even use hashing. That is, |
| 259 | the local F a = Int is assigned the hash index F, so is the wanted |
| 260 | constraint F a = Int (trivial example). When applying locals/type functions |
| 261 | we'll only need to consider the entries with hash index F. |
| 262 | |
| 263 | |
| 264 | ==== A note on evidence construction ==== |
| 265 | |
| 266 | We yet need to formalize the exact details how to map CHR evidence back |
| 267 | to term evidence. In fact, there's an issue. |
| 268 | Consider the type equation (with evidence) |
| 269 | |
| 270 | e : F (G Int) = Int |
| 271 | |
| 272 | In the normal form representation, the above is represented as |
| 273 | |
| 274 | e1 : F a = Int |
| 275 | e2 : G Int = a |
| 276 | |
| 277 | for some evidence e1 and e2. What's the connection between e and e1,e2? |
| 278 | |
| 279 | In case e : F (G Int) = Int is wanted, the method outlined above |
| 280 | will attempt to find evidence for e1 and e2. Given e1 and e2 we can then |
| 281 | build evidence e. |
| 282 | |
| 283 | In case e : F (G Int) = Int is local (ie given), the normal form construction |
| 284 | seems to be the wrong way around. Indeed, from e we can't necessarily build e1 and e2. |
| 285 | Well, the method outlined here simply assumes that |
| 286 | e1 : F a = Int, e2 : G Int = a |
| 287 | is the internal representation for |
| 288 | e : F (G Int) = Int |
| 289 | |
| 290 | NOTE: |
| 291 | |
| 292 | The user can of course use the more "compact" term representation of local assumptions, |
| 293 | but internally we'll need to keep local assumptions in normal form. |
| 294 | |
| 295 | |
| 296 | }}} |