Changes between Version 30 and Version 31 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 10:41:56 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v30 v31  
    2828Central to the algorithm are '''normal equalities''', which can be regarded as a set of rewrite rules.  Normal equalities are carefully oriented and contain synonym families only as the head symbols of left-hand sides.  They assume one of the following three forms: 
    2929 
    30  1. `co :: F t1..tn ~ t`, 
    31  2. `co :: x ~ t`, where `x` is a flexible type variable, or 
    32  3. `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable. 
     30 1. '''Family equality:''' `co :: F t1..tn ~ t`, 
     31 2. '''Flexible variable equality:''' `co :: x ~ t`, where `x` is a flexible type variable, or 
     32 3. '''Rigid variable equality:''' `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable. 
    3333 
    3434where 
    3535 
    36  * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, and 
    37  * we call the Forms (2) & (3) '''variable equalities''', and require that the left- and right-hand side need to be different, and that the left-hand side does not occur in the right-hand side. 
     36 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families and 
     37 * left-hand side of an equality may not occur in the right-hand side. 
     38 
     39The second bullet of the where clause is trivially true for equalities of Form (1) and it implies that the left- and right-hand sides are different. 
    3840 
    3941=== Observations === 
     
    116118== Solving == 
    117119 
     120'''TODO:''' Partition the rules depending on which if the three forms of normal equalities they apply to!!! 
     121 
    118122Notes: 
    119123