Changes between Version 11 and Version 12 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 11, 2006 10:16:55 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v11 v12  
    11= Type Checking with Indexed Type Synonyms = 
    2  
    3  
    4 == Outline == 
    5  
    6  * Background  
    7  * The challenge 
    8  * A first (naive) attempt 
    9  * A second attempt 
    10     * type checking with type functions using local completion 
    11     * method can be proven correct by establishing a connection 
    12       between type function and CHR derivations 
     2[[PageOutline]] 
    133 
    144== Background == 
     
    441431T Int = T Int /\ S Int = S Int  
    442432}}} 
     433 
     434---- 
     435 
     436== Restrictions on valid programs == 
     437 
     438We 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. 
     439 
     440=== Type variables === 
     441 
     442We have three kinds of type variables: 
     443 
     444 * ''Schema variables'' 
     445 
     446=== Normal type equations === 
     447 
     448''Normal type equations'' `s = t` obey the following constraints: 
     449 
     450 * ''Constructor based'': The left-hand side `s` must have for form `F s1 .. sn` where `F` is a type family and no type family occur in the `si`. 
     451 * ''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'`). 
     452 * ''Left linear'': No schema variable appears more than once in `s`. 
     453 * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family in `t` must be strictly less than the number of data type constructor and variable symbols in `s`. 
     454 
     455We require that all axioms and local assumptions are normal.  In particular, all type family instances and all equalities in signatures need to be normal.  NB: With `-fundecidable-indexed-types`, we can drop left linearity and decreasingness.