Changes between Version 12 and Version 13 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 11, 2006 11:26:34 PM (9 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v12 v13  
    434434----
    435435
    436 == Restrictions on valid programs ==
     436== Restrictions on type equations ==
    437437
    438438We 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.
     
    442442We have three kinds of type variables:
    443443
    444  * ''Schema variables''
     444 * ''Schema variables'': These are type variables in the left-hand side of type equations that maybe instantiated during applying a type equation during type rewriting.  For example, in `type instance F [a] = a`, `a` is a schema variable.
     445 * ''Rigid variables'': These are variables that may not be instantiated (they represent variables in signatures and existentials during matching).
     446 * ''Wobbly variables'': Variables that may be instantiated during unification.
    445447
    446448=== Normal type equations ===
     
    448450''Normal type equations'' `s = t` obey the following constraints:
    449451
    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`.
     452 * ''Constructor based'': The left-hand side `s` must have for form `F s1 .. sn` where `F` is a type family and the `si` are formed from data type constructors, schema variables, and rigid variables only (i.e., they may not contain type family constructors or wobbly variables).
    451453 * ''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'`).
    452454 * ''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 
    455 We 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.
     455 * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family occuring in `t` must be strictly less than the number of data type constructor and variable symbols in `s`.
     456
     457Examples of normal type equations:
     458{{{
     459data C
     460type instance Id a = a
     461type instance F [a] = a
     462type instance F (C (C a)) = F (C a)
     463type instance F (C (C a)) = F (C (Id a))
     464type instance F (C (C a)) = C (F (C a))
     465type instance F (C (C a)) = (F (C a), F (C a))
     466}}}
     467
     468Examples of type equations that are ''not'' normal:
     469{{{
     470type instance F [a] = F (Maybe a)            -- Not decreasing
     471type instance G a a = a                      -- Not left linear
     472type instance F (G a) = a                    -- Not constructor-based
     473type instance F (C (C a)) = F (C (Id (C a))) -- Not decreasing
     474}}}
     475Note that `forall a. (G a a = a) => a -> a` is fine, as `a` is a rigid variables, not a schema variable.
     476
     477We 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.
     478
     479=== Normalisation of equalities ===
     480
     481Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` leads to a (possibly empty) set of normal equations, or to a type error.  We proceed as follows:
     482
     483 1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`.
     484 2. If `s'` and `t'` are the same variable, we succeed (with no new rule).
     485 3. If `s'` and `t'` are distinct rigid variables, we fail.
     486 4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check).
     487 5. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we reject the program.
     488 6. If `s'` = `C s1 .. sn` and `t'` = `C t1 .. tn`, then yield the union of the equations obtained by normalising all `ti = si`.
     489
     490Rejection 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 combine GADTs and type functions in ellaborate ways.