# Changes between Version 25 and Version 26 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/03/08 02:07:21 (5 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## TypeFunctionsSolving

v25 v26
5858== Normalisation ==
5959
60 (Ignoring the coercions for the moment.)
61
63
64 {{{
65 --    EqInst             Arbitrary equalities
66 --    FlattenedEqInst    Any type function application is at the top
67 --    RewriteInst        Satisfies invariants above
60The following function `norm` turns an arbitrary equality into a set of normal equalities.  (It ignores the coercions for the moment.)
61{{{
62data EqInst         -- arbitrary equalities
63data FlatEqInst     -- synonym families may only occur outermost on the lhs
64data RewriteInst    -- normal equality
6865
6966norm :: EqInst -> [RewriteInst]

8178
8279check :: FlattenedEqInst -> [FlattenedEqInst]
83 -- Does OccursCheck + Decomp + Swap
80-- Does OccursCheck + Decomp + Swap (of new-single)
8481check [[t ~ t]] = []
8582check [[x ~ t]] | x `occursIn` t = fail

9592
9693flatten :: Type -> (Type, [FlattenedEqInst])
97 -- Result type has no type functions whatsoever
94-- Result type has no synonym families whatsoever
9895flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn)
9996  where

114111 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.)
115112 * Use flexible tyvars for flattening of locals, too.  (We have flexibles in locals anyway and don't use (Unify) on locals, so the flexibles shouldn't cause any harm, but the elimination of skolems is much easier for flexibles - we just instantiate them.)
116  * Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too?
113 * '''TODO:''' Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too?
117114
118115
119116== Solving ==
120117
121  * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families.  Moreover, it only applies to wanted equalities.  (Rationale: Local equality constraints don't justify global instantiation of flexible type variables.)  '''SLPJ''': right, precisely as in `new-single.tex`.
122
123  * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds.  '''SLPJ''' by "applies to" I think you mean that only those forms are considered to substitute.  We must ''perform'' the substitution on all constraints, right?  '''SLPJ''' why does it not apply to wanteds?[[BR]][[BR]]
124  In principle, a rewrite rule could be discarded after an exhaustive application of (Local).  However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around.[[BR]][[BR]]
125  NB: (Local) -for Forms (2) & (3)- is the most expensive rule as it needs to traverse all type terms.
118 * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families.  Moreover, it only applies to wanted equalities.  (Rationale: Local equality constraints don't justify global instantiation of flexible type variables - just as in new-single.)
119
120 * (Local) only substitutes normal variable equalities - and currently also only local equalities, not wanteds.  (We should call this Rule (Subst) again.)
121
122 In principle, a rewrite rule could be discarded after an exhaustive application of (Local).  However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around.
126123
127124 * (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local).  '''SLPJ''' good point: in view of (Local) there's no need for (IdenticalLHS) to deal with a given `a~t`.  So if epsilon1 is 'g', the LHS could be restricted to form `F t1..tn` which would be good (in the paper).[[BR]][[BR]]
128125 '''SLPJ''' but why do you say that we don't want IdenticalLHS on wanteds?  What about `F a ~ x1, F a ~ Int`.  Then we could unify the HM variable `x` with `Int`.
129126
130 Observation:
127=== Observations ===
128 *  Rule (Local) -substituting variable equalities- is the most expensive rule as it needs to traverse all type terms.
131129 * Only (Local) when replacing a variable in the ''left-hand side'' of an equality of Form (1) can  lead to recursion with (Top).
132130