Changes between Version 19 and Version 20 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 14, 2006 12:27:52 AM (9 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.