Changes between Version 17 and Version 18 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 12, 2006 9:45:40 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v17 v18  
    499499 
    500500Rejection 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. 
     501 
     502---- 
     503 
     504== Maintaining type equations == 
     505 
     506The set of ''given'' equalities (i.e., those that we use as rewrite rules to normalise type terms) comprises two subsets: 
     507 
     508 * ''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. 
     509 * ''Local assumptions:'' The equations arising from equalities in signatures and from GADT pattern matching after normalisation. 
     510 
     511The 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: 
     512 
     513 * ''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. 
     514 * ''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.