Changes between Version 16 and Version 17 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 12, 2006 9:15:50 PM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v16 v17  
    434434---- 
    435435 
    436 == Restrictions on type equations == 
    437  
    438 We impose some syntactic restrictions on programs 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. 
     436== Special forms of type equations == 
     437 
     438We 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. 
    439439 
    440440=== Type variables === 
     
    477477We 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. 
    478478 
     479=== Semi-normal type equations === 
     480 
     481If 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''. 
     482 
    479483=== Normalisation of equalities === 
    480484 
     
    482486 
    483487 1. Reduce `s` and `t` to NF, giving us `s'` and `t'`. 
    484  2. If `s'` and `t'` are the same variable, we succeed (with no new rule). 
     488 2. If `s'` and `t'` are identical, we succeed (with no new rule). 
    485489 3. If `s'` or `t'` is a rigid variable, we fail.  (Reason: cannot instantiate rigid variables.) 
    486490 4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check). 
     
    488492 6. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we fail.  (Reason: unfication failure.) 
    489493 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   * If `s' = t'` is normal, yield it. 
     495   * If `t' = s'` is normal, yield it. 
     496   * If `s' = t'` is semi-normal, yield it. 
     497   * If `t' = s'` is semi-normal, yield it. 
    494498   * 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.) 
    495499 
    496500Rejection 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. 
    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.