Changes between Version 45 and Version 46 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 14, 2008 7:45:49 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v45 v46  
    2626== Normal equalities == 
    2727 
    28 Central 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: 
    29  
    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. 
     28Central 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 two major forms: 
     29 
     30 1. '''Family equality:''' `co :: F t1..tn ~ t` or 
     31 2. '''Variable equality:''' `co :: a ~ t`, where we again distinguish two forms: 
     32  a. '''Variable-term equality.''' `co :: a ~ t`, where `t` is '''not''' a variable, or 
     33  b. '''Variable-variable equality.''' `co :: a ~ b`, where `a < b`. 
    3334 
    3435where 
    3536 
    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. 
     37 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 
     38 * the left-hand side of an equality may not occur in the right-hand side, and 
     39 * the relation `a < b` is a total order on type variables, where `x < a` whenever `x` is a flexible and `a` a rigid type variable (otherwise, the details of the total order are irrelevant). 
    3840 
    3941The 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. 
     42 
     43Furthermore, we call a variable equality whose left-hand side is a flexible type variable (aka unification variable) a '''flexible variable equality''', and correspondingly, a variable equality whose left-hand side is a rigid type variable (aka skolem variable) a '''rigid variable equality.''' 
    4044 
    4145=== Observations ===