Changes between Version 11 and Version 12 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 11, 2006 10:16:55 PM (9 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.