Changes between Version 46 and Version 47 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 14, 2008 9:33:54 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v46 v47  
    1111  An equality constraint that -in a certain scope- may be used to derive wanted equalities. 
    1212 ''Flexible type variable'',  ''unification variable'', ''HM variable''::  
    13   Type variables that may be '''globally''' instantiated by unification. 
     13  Type variables that may be '''globally''' instantiated by unification.  We use Greek letters `alpha, beta,`... as names for these variables. 
    1414 ''Rigid type variable'', ''skolem type variable'':: 
    15   Type variable that cannot be globally instantiated, but it may be '''locally''' refined by a local equality constraint. 
     15  Type variable that cannot be globally instantiated, but it may be '''locally''' refined by a local equality constraint.  We use Roman letters `a, b,`... as names for these variables. 
     16 
     17In positions where we can have both flexible and rigid variables, we use `x, y, z`. 
    1618 
    1719 
     
    2931 
    3032 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`. 
     33 2. '''Variable equality:''' `co :: x ~ t`, where we again distinguish two forms: 
     34  a. '''Variable-term equality:''' `co :: x ~ t`, where `t` is ''not'' a variable, or 
     35  b. '''Variable-variable equality:''' `co :: x ~ y`, where `x < y`. 
    3436 
    3537where 
     
    3739 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 
    3840 * 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). 
     41 * the relation `x < y` is a total order on type variables, where `alpha < a` whenever `alpha` is a flexible and `a` a rigid type variable (otherwise, the details of the total order are irrelevant). 
    4042 
    4143The 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. 
     
    4749The following is interesting to note: 
    4850 
    49  * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 
    5051 * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same. 
    5152 * Normal equalities are '''never''' self-recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities.  
     
    8788-- Does OccursCheck + Decomp + Triv + Swap (of new-single) 
    8889check [[t ~ t]] = [] 
     90check [[x ~ y]] | x < y = [[x ~ y]] 
     91                | otherwise = [[y ~ x]] 
    8992check [[x ~ t]] | x `occursIn` t = fail 
    90                           | otherwise = [[x ~ t]] 
     93                | otherwise = [[x ~ t]] 
    9194check [[t ~ x]] | x `occursIn` t = fail 
    92                           | otherwise = [[x ~ t]] 
    93 check [[a ~ t]] | a `occursIn` t = fail 
    94                           | otherwise = [[a ~ t]] 
    95 check [[t ~ a]] | a `occursIn` t = fail 
    96                           | otherwise = [[a ~ t]] 
     95                | otherwise = [[x ~ t]] 
    9796check [[s1 s2 ~ t1 t2]] = check [[s1 ~ t1]] ++ check [[s2 ~ t2]] 
    9897check [[T ~ S]] = fail 
     
    10099flatten :: Type -> (Type, [FlattenedEqInst]) 
    101100-- Result type has no synonym families whatsoever 
    102 flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn) 
     101flatten [[F t1..tn]] = (alpha, [[F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
    103102  where 
    104103    (t1', eqt1) = flatten t1 
    105104    .. 
    106105    (tn', eqtn) = flatten tn 
    107     NEW x 
    108     -- also need to add x := F t1'..tn' 
     106    NEW alpha 
     107    -- also need to add alpha := F t1'..tn' 
    109108flatten [[t1 t2]] = (t1' t2', eqs++eqt) 
    110109  where