Changes between Version 13 and Version 14 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 12, 2006 1:33:02 AM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v13 v14  
    483483 1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`. 
    484484 2. If `s'` and `t'` are the same variable, we succeed (with no new rule). 
    485  3. If `s'` and `t'` are distinct rigid variables, we fail. 
     485 3. If `s'` or `t'` is a rigid variable, we fail.  (Reason: cannot instantiate rigid variables.) 
    486486 4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check). 
    487  5. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we reject the program. 
    488  6. If `s'` = `C s1 .. sn` and `t'` = `C t1 .. tn`, then yield the union of the equations obtained by normalising all `ti = si`. 
    489  
    490 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 combine GADTs and type functions in ellaborate ways. 
     487 5. If `s'` = `C s1 .. sn` and `t'` = `C t1 .. tn`, then yield the union of the equations obtained by normalising all `ti = si`. 
     488 6. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we fail.  (Reason: unfication failure.) 
     489 7. Now, at least one of `s'` and `t'` has the form `F r1 .. rn`, where F is a type family: 
     490   * If `s'` = `F s1 .. sn` and is constructor-based and left-linear, and if `s' = t'` is decreasing, yield `s' = t'`. 
     491   * If `t'` = `F t1 .. tn` and is constructor-based and left-linear, and if `t' = s'` is decreasing, yield `t' = s'`. 
     492   * If `s'` = `F s1 .. sn` and some `si` contains a type family application of the form `G r1 .. rn`, yield the union of the equations obtained by normalising both `G r1 .. rn = a` and `F s1 .. sn = t'` with `G r1 .. rn` replaced by `a`, which is a new rigid type variable. 
     493   * If `t'` = `F t1 .. tn` and some `ti` contains a type family application of the form `G r1 .. rn`, yield the union of the equations obtained by normalising both `G r1 .. rn = a` and `F t1 .. tn = s'` with `G r1 .. rn` replaced by `a`, which is a new rigid type variable. 
     494   * 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.) 
     495 
     496Rejection 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 combine GADTs and type functions in ellaborate ways.  (We still lack an example that produces such a situation, though.) 
     497 
     498'''TODO:''' I am wondering whether we can do that pulling out type family applications from left-hand sides and turning them into extra type equations lazily.