Changes between Version 25 and Version 26 of TypeFunctionsSolving
 Timestamp:
 Aug 3, 2008 9:07:21 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v25 v26 58 58 == Normalisation == 59 59 60 (Ignoring the coercions for the moment.) 61 62 '''SLPJ''': added comments/invariants below, pls check. 63 64 {{{ 65  EqInst Arbitrary equalities 66  FlattenedEqInst Any type function application is at the top 67  RewriteInst Satisfies invariants above 60 The following function `norm` turns an arbitrary equality into a set of normal equalities. (It ignores the coercions for the moment.) 61 {{{ 62 data EqInst  arbitrary equalities 63 data FlatEqInst  synonym families may only occur outermost on the lhs 64 data RewriteInst  normal equality 68 65 69 66 norm :: EqInst > [RewriteInst] … … 81 78 82 79 check :: FlattenedEqInst > [FlattenedEqInst] 83  Does OccursCheck + Decomp + Swap 80  Does OccursCheck + Decomp + Swap (of newsingle) 84 81 check [[t ~ t]] = [] 85 82 check [[x ~ t]]  x `occursIn` t = fail … … 95 92 96 93 flatten :: Type > (Type, [FlattenedEqInst]) 97  Result type has no type functions whatsoever94  Result type has no synonym families whatsoever 98 95 flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn) 99 96 where … … 114 111 * 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 righthand sides do not contain synonym familles; hence, any recursive occurrences of a lefthand side imply that the equality is unsatisfiable.) 115 112 * 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? 117 114 118 115 119 116 == Solving == 120 117 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 `newsingle.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 newsingle.) 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. 126 123 127 124 * (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]] 128 125 '''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`. 129 126 130 Observation: 127 === Observations === 128 * Rule (Local) substituting variable equalities is the most expensive rule as it needs to traverse all type terms. 131 129 * Only (Local) when replacing a variable in the ''lefthand side'' of an equality of Form (1) can lead to recursion with (Top). 132 130