Changes between Version 16 and Version 17 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 12, 2006 9:15:50 PM (9 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.