Changes between Version 30 and Version 31 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 10:41:56 AM (7 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