Changes between Version 19 and Version 20 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 14, 2006 12:27:52 AM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v19 v20  
    106106 * [wiki:TypeFunctionsSynTC/GHC Type equations in GHC] 
    107107 
    108 == A first (naive) attempt == 
    109  
    110  
    111 To solve  {{{(C implies t1=t2)}}} with respect to Ax 
    112  
    113  1. We interpret Ax /\ C as a rewrite system (from left to right). 
    114  2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. 
    115  
    116  
    117 Immediately, we find a problem with this solving strategy. 
    118 Consider our running example. 
    119  
    120 Rewrite rules 
    121 {{{ 
    122 (forall a. S [a] = [S a]) /\      (R1) -- axioms 
    123 (T Int = Int)                     (R2) 
    124  
    125  /\ 
    126  
    127 (T [Int] = S [Int]) /\            (R3) -- local assumptions 
    128 (T Int = S Int)                   (R4) 
    129  }}} 
    130  
    131 applied to {{{(T [Int] = [Int])}}} 
    132  
    133 yields 
    134 {{{ 
    135 T [Int] -->* [S Int]       (R3,R1) 
    136  
    137 [Int] -->* [Int] 
    138 }}} 
    139  
    140 Hence, our (naive) solver fails, but 
    141 clearly the (local) property  (T [Int] = [Int]) 
    142 holds. 
    143  
    144 The trouble here is that 
    145  
    146  * the axiom system Ax is confluent, but 
    147  * if we include the local assumptions C, the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) 
    148  
    149  
    150 Possible solutions: 
    151  
    152 Enforce syntactic conditions such that Ax /\ C is confluent. 
    153 It's pretty straightforward to enforce that Ax and 
    154 constraints appearing in type annotations and data types 
    155 are confluent. The tricky point is that if we combine 
    156 these constraints they may become non-confluent. 
    157 For example, imagine 
    158  
    159 {{{ 
    160 Ax : T Int = Int 
    161  
    162    a= T Int      -- from f :: a=T Int => ... 
    163  
    164       implies  
    165  
    166         (a = S Int -- from a GADT pattern 
    167  
    168             implies ...) 
    169 }}} 
    170  
    171 The point is that only during type checking we may 
    172 encounter that Ax /\ C is non-confluent! 
    173 So, we clearly need a better type checking method. 
    174  
    175  
    176  
    177 == A second attempt == 
    178  
    179 To solve  {{{(C implies t1=t2)}}} with respect to Ax 
    180  
    181  1. First: 
    182    1. We interpret Ax /\ C as a rewrite system (from left to right)   and  
    183    2. perform completion until the rewrite system is confluent. 
    184  2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. 
    185  
    186  
    187 Step (1.1) is new and crucial. For confluent rewrite systems the 
    188 checking step (2) will work fine (we also need termination of course). 
    189 But how do we now that completion will succeed? 
    190 The important condition is to guarantee that Ax is confluent (and 
    191 terminating) then completion will be successful (i.e. terminated 
    192 and produce a confluent rewrite system). 
    193  
    194 Let's take a look at our running example. 
    195 {{{ 
    196 (forall a. S [a] = [S a]) /\      (R1) -- axioms 
    197 (T Int = Int)                     (R2) 
    198  
    199  /\ 
    200  
    201 (T [Int] = S [Int]) /\            (R3) -- local assumptions 
    202 (T Int = S Int)                   (R4) 
    203 }}} 
    204 The axioms are clearly confluent 
    205 but there's a critical pair between (R2,R4). 
    206  
    207 Completion yields 
    208  
    209 {{{ 
    210 (S Int = Int)                     (R5) 
    211 }}} 
    212 Now, we can verify that (T [Int] = [Int]) 
    213  
    214 by executing 
    215  
    216 {{{ 
    217 T [Int] -->* [Int]       (R3,R1,R5) 
    218  
    219 [Int] -->* [Int] 
    220 }}} 
    221  
    222 The completion method in more detail. 
    223  
    224 === There are two kinds of critical pairs === 
    225  
    226  * Axiom vs local assumption, see (R2,R4) above 
    227  * Local assumption vs local assumption. For example, 
    228 {{{ 
    229   T Int = S Int  /\  
    230   T Int = R Int 
    231 }}} 
    232   Completion yields 
    233 {{{ 
    234   S Int = R Int 
    235   R Int = S Int 
    236 }}} 
    237  
    238 NOTE: Axiom vs axiom impossible cause axiom set is confluent 
    239  
    240  
    241 Towards establishing a connection between completion and CHR derivation steps  
    242  
    243  
    244 NOTE:  
    245  
    246 There's a straightforward translation from type functions to constraints. For each n-ary function symbol T, we introduce a n+1-ary constraint symbol T. Thus, we can represent  
    247 {{{T Int = Int}}}  as 
    248 {{{ T Int a /\ a=Int}}} 
    249 For example, {{{T Int = S Int}}} is represented by  
    250 {{{T Int a /\ S Int b /\ a=b}}} 
    251  
    252  
    253 We can verify that the completion method success by showing that each critical pair arises in the `corresponding' CHR derivation (this derivation terminates if the axiom system is confluent and terminating, hence, we'll only encounter a finite number of critical pairs, hence, completion terminates). 
    254  
    255 Recall the critical pair (axioms vs local assumption) from above 
    256 {{{ 
    257 T Int = Int     -- axiom 
    258 T Int = S Int  -- local assumption 
    259 }}} 
    260 In the CHR world, we'll represent both as 
    261 {{{ 
    262 T Int a <==> a=Int         -- axiom turned into CHR 
    263  
    264 T Int b /\ S Int c /\ b=c  -- local assumption turned into CHR 
    265                            -- constraints 
    266 }}} 
    267 In the CHR world, we find that 
    268 {{{ 
    269     T Int b /\ S Int c /\ b=c 
    270 --> b=Int /\ S Int c /\ b=c      -- apply CHR 
    271 <--> b=Int /\ c=Int /\ S Int Int -- equivalence transformation 
    272                                  -- apply mgu 
    273 }}} 
    274 directly corresponds to  
    275 {{{ 
    276 S Int = Int 
    277 }}} 
    278 generated by our completion method 
    279  
    280 Recall the critical pair (local assumption vs local assumption) 
    281 {{{ 
    282   T Int = S Int  /\  
    283   T Int = R Int 
    284 }}} 
    285 represented in the CHR world as 
    286 {{{ 
    287  T Int a /\ S Int b /\ a=b /\ 
    288  T Int c /\ R Int d /\ c=d 
    289 }}} 
    290 In the CHR world, we find that 
    291 {{{ 
    292     T Int a /\ S Int b /\ a=b /\ 
    293     T Int c /\ R Int d /\ c=d 
    294 -->T Int a /\ S Int b /\ a=b /\   
    295    c=a /\ R Int d /\ c=d 
    296  
    297       -- apply FD rule 
    298       -- T a b /\ T a c ==> b=c 
    299  
    300 <--> T Int a /\ S Int a /\ R Int a /\ 
    301      a=b, c=a, d=a 
    302 }}} 
    303 directly corresponds to 
    304 {{{ 
    305 S Int = R Int 
    306 R Int = S Int 
    307 }}} 
    308  
    309 The general cases are as follows. 
    310  
    311 ==== Axiom vs local assumption case ==== 
    312  
    313 {{{ 
    314 forall as. (T t1 ... tn = s)  -- axiom 
    315  
    316 T t1' ... tn' = s'            -- local assumption 
    317 }}} 
    318 where exist phi, dom(phi)=as such that phi(ti) = ti' for i=1,...,n 
    319  
    320  
    321 completion yields 
    322 {{{ 
    323     s' = phi(s) 
    324     phi(s) = s'        
    325 }}} 
    326  
    327 NOTE: We may need both orientation see above example. 
    328 We assume that symbol t refers to types NOT containing type functions and s refers to types which may contain type functions (can be lifted, more below) 
    329  
    330  
    331 Explaining completion in terms of CHRs. 
    332 Above translates to 
    333 {{{ 
    334 T t1 ... tn b <==> C 
    335  
    336 T t1' ... tn' b' /\ C' 
    337 }}} 
    338 where  s is translated to (C | b) and s' is translated to (C | b') 
    339  
    340 (see above where each type function type is represented by 
    341 a variable under some CHR constraints) 
    342  
    343 The type functions 
    344 {{{ 
    345     s' = phi(s) 
    346     phi(s) = s'        
    347 }}} 
    348 resulting from completion 'appear' in the CHR derivation 
    349 (i.e. the operational effect is the same) 
    350 {{{ 
    351      T t1' ... tn' b' /\ C'    -- apply CHR 
    352 --> b=b', phi(C) /\ C' 
    353 }}} 
    354  
    355 ==== Local assumption vs local assumption ==== 
    356  
    357 {{{ 
    358 T t1 ... tn = s1 
    359 T t1 ....tn = sn 
    360 }}} 
    361  
    362 completion yields 
    363 {{{ 
    364   s1 = s2 
    365   s2 = s1 
    366 }}} 
    367 In the CHR world, above represented by 
    368  
    369 {{{ 
    370 T t1 ... tn a /\ C1 
    371 T t1 ....tn b /\ C2 
    372 }}} 
    373 where s1 translated to (C1 | a) 
    374       s2 translated to (C1 | n) 
    375  
    376 Then,  
    377 {{{ 
    378     T t1 ... tn a /\ C1 /\ 
    379     T t1 ....tn b /\ C2 
    380  
    381 --> FD rule step 
    382  
    383     T t1 ... tn a /\ C1 /\ 
    384     a=b /\ [a/b] C2 
    385 }}} 
    386  
    387 Again, the operational effect of the type function generated 
    388 is also present in the CHR derivation 
    389  
    390  
    391 Lifting the restriction that t refers to types NOT containing 
    392 type functions (we only lift this restriction for 
    393 local assumptions). 
    394  
    395 Consider 
    396 {{{ 
    397 forall a. T [a] = [T a]      -- axiom 
    398  
    399 T [S Int] = s                -- local assumption 
    400 }}} 
    401  
    402 We can normalize 
    403 {{{ 
    404 T [S Int] = s 
    405 }}} 
    406 to 
    407 {{{ 
    408 T [b] = s 
    409 S Int = b 
    410 }}} 
    411 Method from above applies then. 
    412  
    413 NOTE: Regarding generation of implication constraints. 
    414 GENERATEIMP 
    415  
    416 The literate implication constraints generated out of the 
    417 program text may look as follows 
    418 {{{  
    419 a=T Int implies ( a= S Int implies ...) 
    420 }}} 
    421  
    422 The above can be simplified to 
    423 {{{  
    424 (a=T Int /\ a = S Int) implies ... 
    425 }}} 
    426 Before we proceed with the completion method, we first 
    427 need to apply some closure rules (eg. transitivity, left, right etc) 
    428 Hence, from the above we generatet 
    429 {{{ 
    430    a=T Int /\ a = S Int /\  
    431    T Int = a /\ S Int = a /\       -- symmetry 
    432    T Int = S Int /\ S Int = T Int  -- transitivity 
    433 }}} 
    434 We omit the trival (reflexive) equations 
    435 {{{  
    436 T Int = T Int /\ S Int = S Int  
    437 }}} 
    438  
    439 ---- 
    440  
    441 == Special forms of type equations == 
    442  
    443 We impose some syntactic restrictions on type instances and normalise equations arising during type checking to ensure that type checking remains (a) deterministic, (b) a simple rewrite model is sufficient to reduce type function applications, and (c) it hopefully remains decidable. 
    444  
    445 === Type variables === 
    446  
    447 We have three kinds of type variables: 
    448  
    449  * ''Schema variables'': These are type variables in the left-hand side of type equations that maybe instantiated during applying a type equation during type rewriting.  For example, in `type instance F [a] = a`, `a` is a schema variable. 
    450  * ''Rigid variables'': These are variables that may not be instantiated (they represent variables in signatures and existentials during matching). 
    451  * ''Wobbly variables'': Variables that may be instantiated during unification. 
    452  
    453 === Normal type equations === 
    454  
    455 ''Normal type equations'' `s = t` obey the following constraints: 
    456  
    457  * ''Constructor based'': The left-hand side `s` must have for form `F s1 .. sn` where `F` is a type family and the `si` are formed from data type constructors, schema variables, and rigid variables only (i.e., they may not contain type family constructors or wobbly variables). 
    458  * ''Non-overlapping'': For any other axiom or local assumption `s' = t'`, there may not be any substitution ''theta'', such that (''theta'' `s`) equals (''theta'' `s'`). 
    459  * ''Left linear'': No schema variable appears more than once in `s`. 
    460  * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family occuring in `t` must be strictly less than the number of data type constructor and variable symbols in `s`. 
    461  
    462 Examples of normal type equations: 
    463 {{{ 
    464 data C 
    465 type instance Id a = a 
    466 type instance F [a] = a 
    467 type instance F (C (C a)) = F (C a) 
    468 type instance F (C (C a)) = F (C (Id a)) 
    469 type instance F (C (C a)) = C (F (C a)) 
    470 type instance F (C (C a)) = (F (C a), F (C a)) 
    471 }}} 
    472  
    473 Examples of type equations that are ''not'' normal: 
    474 {{{ 
    475 type instance F [a] = F (Maybe a)            -- Not decreasing 
    476 type instance G a a = a                      -- Not left linear 
    477 type instance F (G a) = a                    -- Not constructor-based 
    478 type instance F (C (C a)) = F (C (Id (C a))) -- Not decreasing 
    479 }}} 
    480 Note that `forall a. (G a a = a) => a -> a` is fine, as `a` is a rigid variables, not a schema variable. 
    481  
    482 We require that all type family instances are normal.  Moreover, all equalities arising as local assumptions need to be such that they can be normalised (see below).  NB: With `-fundecidable-indexed-types`, we can drop left linearity and decreasingness. 
    483  
    484 === Semi-normal type equations === 
    485  
    486 If an equation `s = t` does not contain any schema variables and is normal, except that it's left-hand side `F s1 .. sn` contains one or more type family constructors in the `si`, we call it ''semi-normal''. 
    487  
    488 === Normalisation of equalities === 
    489  
    490 Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` (not containing schema variables) leads to a (possibly empty) set of normal equations, or to a type error.  We proceed as follows: 
    491  
    492  1. Reduce `s` and `t` to NF, giving us `s'` and `t'`. 
    493  2. If `s'` and `t'` are identical, we succeed (with no new rule). 
    494  3. If `s'` or `t'` is a rigid variable, we fail.  (Reason: cannot instantiate rigid variables.) 
    495  4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check). 
    496  5. If `s'` = `C s1 .. sn` and `t'` = `C t1 .. tn`, then yield the union of the equations obtained by normalising all `ti = si`. 
    497  6. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we fail.  (Reason: unfication failure.) 
    498  7. Now, at least one of `s'` and `t'` has the form `F r1 .. rn`, where F is a type family: 
    499    * If `s' = t'` is normal, yield it. 
    500    * If `t' = s'` is normal, yield it. 
    501    * If `s' = t'` is semi-normal, yield it. 
    502    * If `t' = s'` is semi-normal, yield it. 
    503    * Otherwise, fail.  (Reason: a wobbly type variable, lack of left linearity, or non-decreasingness prevents us from obtaining a normal equation.  If it is a wobbly type variable, the user can help by adding a type annotation; otherwise, we cannot handle the program without (maybe) losing decidability.) 
    504  
    505 Rejection of local assumptions that after normalisation are either not left linear or not decreasing may lead to incompleteness.  However, this should only happen for programs that are invalid or combine GADTs and type functions in ellaborate ways. 
    506  
    507 ---- 
    508  
    509 == Maintaining type equations == 
    510  
    511 The set of ''given'' equalities (i.e., those that we use as rewrite rules to normalise type terms) comprises two subsets: 
    512  
    513  * ''Axioms'': The equations derived from type family instances.  They are the only equations that may contain schema variables, and they are normal for well-formed programs. 
    514  * ''Local assumptions:'' The equations arising from equalities in signatures and from GADT pattern matching after normalisation. 
    515  
    516 The set of axioms stays the same throughout type checking a module, whereas the set of local assumptions grows while descending into expressions and shrinks when ascending out of these expressions again.  We have two different sorts of local assumptions: 
    517  
    518  * ''Normal assumptions'': These are not altered anymore once they have been added to the set of local assumptions, until the moment when they are removed again. 
    519  * ''Semi-normal assumptions:'' These are only added tentatively.  They are reconsidered whenever a new rule is added to the local assumptions, because a new rule may lead to further normalisation of semi-normal assumptions.  If a semi-normal assumption is further normalised, the original assumption is removed and the further normalised one added (which can again trigger subsequent normalisation).  NB: Strictly speaking, we can leave the original (semi-normal) equation in the set together with its further normalised version.