diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2014-12-10 14:56:30 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2014-12-10 16:01:19 +0000 |
commit | a225c70e00586e2f38a0e27fae698324ae81b006 (patch) | |
tree | eefa979d19e3455f17e016954bb93305c1068529 /compiler/typecheck/Flattening-notes | |
parent | fca85c9b1617417a6170f3591a29d1fe36d35da5 (diff) | |
download | haskell-a225c70e00586e2f38a0e27fae698324ae81b006.tar.gz |
Comments only: move flattening notes to TcFlatten
Diffstat (limited to 'compiler/typecheck/Flattening-notes')
-rw-r--r-- | compiler/typecheck/Flattening-notes | 202 |
1 files changed, 1 insertions, 201 deletions
diff --git a/compiler/typecheck/Flattening-notes b/compiler/typecheck/Flattening-notes index ffe39ab5e5..2aa9243743 100644 --- a/compiler/typecheck/Flattening-notes +++ b/compiler/typecheck/Flattening-notes @@ -9,207 +9,6 @@ ToDo: * RAE: I think it would be better to split off CNonCanonical into its own type, and remove it completely from Ct. Then, we would keep CIrredCan -=========================== - -The inert equalities -~~~~~~~~~~~~~~~~~~~~ - -Definition: can-rewrite relation. -A "can-rewrite" relation between flavours, written f1 >= f2, is a -binary relation with the following properties - - R1. >= is transitive - R2. If f1 >= f, and f2 >= f, - then either f1 >= f2 or f2 >= f1 - -Lemma. If f1 >= f then f1 >= f1 -Proof. By property (R2), with f1=f2 - -Definition: generalised substitution. -A "generalised substitution" S is a set of triples (a -f-> t), where - a is a type variable - t is a type - f is a flavour -such that - (WF1) if (a -f1-> t1) in S - (a -f2-> t2) in S - then neither (f1 >= f2) nor (f2 >= f1) hold - (WF2) if (a -f-> t) is in S, then t /= a - -Definition: applying a generalised substitution. -If S is a generalised substitution - S(f,a) = t, if (a -fs-> t) in S, and fs >= f - = a, otherwise -Application extends naturally to types S(f,t) - -Theorem: S(f,a) is well defined as a function. -Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S, - and f1 >= f and f2 >= f - Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF) - -Notation: repeated application. - S^0(f,t) = t - S^(n+1)(f,t) = S(f, S^n(t)) - -Definition: inert generalised substitution -A generalised substitution S is "inert" iff - - (IG1) there is an n such that - for every f,t, S^n(f,t) = S^(n+1)(f,t) - - (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t - that is, each individual binding is "self-stable" - ----------------------------------------------------------------- -Our main invariant: - the inert CTyEqCans should be an inert generalised substitution ----------------------------------------------------------------- - -Note that inertness is not the same as idempotence. To apply S to a -type, you may have to apply it recursive. But inertness does -guarantee that this recursive use will terminate. - -The main theorem. - Suppose we have a "work item" - a -fw-> t - and an inert generalised substitution S, - such that - (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_) - (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) - (T3) a not in t -- No occurs check in the work item - - (K1) if (a -fs-> s) is in S then not (fw >= fs) - (K2) if (b -fs-> s) is in S, where b /= a, then - (K2a) not (fs >= fs) - or (K2b) not (fw >= fs) - or (K2c) a not in s - or (K3) if (b -fs-> a) is in S then not (fw >= fs) - (a stronger version of (K2)) - - then the extended substition T = S+(a -fw-> t) - is an inert generalised substitution. - -The idea is that -* (T1-2) are guaranteed by exhaustively rewriting the work-item - with S(fw,_). - -* T3 is guaranteed by a simple occurs-check on the work item. - -* (K1-3) are the "kick-out" criteria. (As stated, they are really the - "keep" criteria.) If the current inert S contains a triple that does - not satisfy (K1-3), then we remove it from S by "kicking it out", - and re-processing it. - -* Note that kicking out is a Bad Thing, because it means we have to - re-process a constraint. The less we kick out, the better. - -* Assume we have G>=G, G>=W, D>=D, and that's all. Then, when performing - a unification we add a new given a -G-> ty. But doing so does NOT require - us to kick out an inert wanted that mentions a, because of (K2a). This - is a common case, hence good not to kick out. - -* Lemma (L1): The conditions of the Main Theorem imply that there is no - (a fs-> t) in S, s.t. (fs >= fw). - Proof. Suppose the contrary (fs >= fw). Then because of (T1), - S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we - have (a -fs-> a) in S, which contradicts (WF2). - -* The extended substitution satisfies (WF1) and (WF2) - - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1). - - (T3) guarantees (WF2). - -* (K2) is about inertness. Intuitively, any infinite chain T^0(f,t), - T^1(f,t), T^2(f,T).... must pass through the new work item infnitely - often, since the substution without the work item is inert; and must - pass through at least one of the triples in S infnitely often. - - - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f), - and hence this triple never plays a role in application S(f,a). - It is always safe to extend S with such a triple. - - (NB: we could strengten K1) in this way too, but see K3. - - - (K2b): If this holds, we can't pass through this triple infinitely - often, because if we did then fs>=f, fw>=f, hence fs>=fw, - contradicting (L1), or fw>=fs contradicting K2b. - - - (K2c): if a not in s, we hae no further opportunity to apply the - work item. - - NB: this reasoning isn't water tight. - -Key lemma to make it watertight. - Under the conditions of the Main Theorem, - forall f st fw >= f, a is not in S^k(f,t), for any k - - -Completeness -~~~~~~~~~~~~~ -K3: completeness. (K3) is not ncessary for the extended substitution -to be inert. In fact K1 could be made stronger by saying - ... then (not (fw >= fs) or not (fs >= fs)) -But it's not enough for S to be inert; we also want completeness. -That is, we want to be able to solve all soluble wanted equalities. -Suppose we have - - work-item b -G-> a - inert-item a -W-> b - -Assuming (G >= W) but not (W >= W), this fulfills all the conditions, -so we could extend the inerts, thus: - - inert-items b -G-> a - a -W-> b - -But if we kicked-out the inert item, we'd get - - work-item a -W-> b - inert-item b -G-> a - -Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl. -So we add one more clause to the kick-out criteria - -Another way to understand (K3) is that we treat an inert item - a -f-> b -in the same way as - b -f-> a -So if we kick out one, we should kick out the other. The orientation -is somewhat accidental. - ------------------------ -RAE: To prove that K3 is sufficient for completeness (as opposed to a rule that -looked for `a` *anywhere* on the RHS, not just at the top), we need this property: -All types in the inert set are "rigid". Here, rigid means that a type is one of -two things: a type that can equal only itself, or a type variable. Because the -inert set defines rewritings for type variables, a type variable can be considered -rigid because it will be rewritten only to a rigid type. - -In the current world, this rigidity property is true: all type families are -flattened away before adding equalities to the inert set. But, when we add -representational equality, that is no longer true! Newtypes are not rigid -w.r.t. representational equality. Accordingly, we would to change (K3) thus: - -(K3) If (b -fs-> s) is in S with (fw >= fs), then - (K3a) If the role of fs is nominal: s /= a - (K3b) If the role of fs is representational: EITHER - a not in s, OR - the path from the top of s to a includes at least one non-newtype - -SPJ/DV: this looks important... follow up - ------------------------ -RAE: Do we have evidence to support our belief that kicking out is bad? I can -imagine scenarios where kicking out *more* equalities is more efficient, in that -kicking out a Given, say, might then discover that the Given is reflexive and -thus can be dropped. Once this happens, then the Given is no longer used in -rewriting, making later flattenings faster. I tend to thing that, probably, -kicking out is something to avoid, but it would be nice to have data to support -this conclusion. And, that data is not terribly hard to produce: we can just -twiddle some settings and then time the testsuite in some sort of controlled -environment. - -SPJ: yes it would be good to do that. - The coercion solver ~~~~~~~~~~~~~~~~~~~~ Our hope. In GHC currently drawn from {G,W,D}, but with the coercion @@ -230,3 +29,4 @@ flattening algorithm. Flattening (T a) looks at the roles of T's parameters, and chooses the role for flattening `a` appropriately. This is why there must be the [Role] parameter to flattenMany. Of course, this non-uniform rewriting may gum up the proof works. + |