Changes between Version 46 and Version 47 of TypeFunctionsSolving
 Timestamp:
 Aug 14, 2008 9:33:54 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v46 v47 11 11 An equality constraint that in a certain scope may be used to derive wanted equalities. 12 12 ''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. 14 14 ''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 17 In positions where we can have both flexible and rigid variables, we use `x, y, z`. 16 18 17 19 … … 29 31 30 32 1. '''Family equality:''' `co :: F t1..tn ~ t` or 31 2. '''Variable equality:''' `co :: a~ t`, where we again distinguish two forms:32 a. '''Variableterm equality .''' `co :: a ~ t`, where `t` is '''not''' a variable, or33 b. '''Variablevariable equality .''' `co :: a ~ b`, where `a < b`.33 2. '''Variable equality:''' `co :: x ~ t`, where we again distinguish two forms: 34 a. '''Variableterm equality:''' `co :: x ~ t`, where `t` is ''not'' a variable, or 35 b. '''Variablevariable equality:''' `co :: x ~ y`, where `x < y`. 34 36 35 37 where … … 37 39 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 38 40 * the lefthand side of an equality may not occur in the righthand 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). 40 42 41 43 The second bullet of the where clause is trivially true for equalities of Form (1) and it implies that the left and righthand sides are different. … … 47 49 The following is interesting to note: 48 50 49 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.50 51 * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of newsingle, but they are not the same. 51 52 * Normal equalities are '''never''' selfrecursive. They can be mutually recursive. A mutually recursive group will exclusively contain variable equalities. … … 87 88  Does OccursCheck + Decomp + Triv + Swap (of newsingle) 88 89 check [[t ~ t]] = [] 90 check [[x ~ y]]  x < y = [[x ~ y]] 91  otherwise = [[y ~ x]] 89 92 check [[x ~ t]]  x `occursIn` t = fail 90 93  otherwise = [[x ~ t]] 91 94 check [[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]] 97 96 check [[s1 s2 ~ t1 t2]] = check [[s1 ~ t1]] ++ check [[s2 ~ t2]] 98 97 check [[T ~ S]] = fail … … 100 99 flatten :: Type > (Type, [FlattenedEqInst]) 101 100  Result type has no synonym families whatsoever 102 flatten [[F t1..tn]] = ( x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn)101 flatten [[F t1..tn]] = (alpha, [[F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 103 102 where 104 103 (t1', eqt1) = flatten t1 105 104 .. 106 105 (tn', eqtn) = flatten tn 107 NEW x108  also need to add x:= F t1'..tn'106 NEW alpha 107  also need to add alpha := F t1'..tn' 109 108 flatten [[t1 t2]] = (t1' t2', eqs++eqt) 110 109 where