Changes between Version 41 and Version 42 of TypeFunctionsSolving

Timestamp:

08/07/08 04:08:28 (5 years ago)

Author:

chak

Comment:

--

TypeFunctionsSolving

@@ -125 +125 @@
   * !SubstFam (formerly, IdenticalLHS) only applies to family equalities (both local and wanteds)
   * Top only applies to family equalities (both locals and wanteds)
- We should apply !SubstFam first as it cheaper and potentially reduces the number of applications of Top.  On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with !SubstFam.  (That strategy should lend itself well to an implementation.)  But be careful, we need to apply Top exhaustively, to avoid non-termination.  More precisely, if we interleave Top and SubstFam, we can easily diverge.
+ We should apply !SubstFam first as it cheaper and potentially reduces the number of applications of Top.  On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with !SubstFam.  (That strategy should lend itself well to an implementation.)  But be careful, we need to apply Top exhaustively, to avoid non-termination.  More precisely, if we interleave Top and !SubstFam, we can easily diverge.
  * Rules applying to variable equalities:
   * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds)
  * With !SubstFam and !SubstVar, we always substitute locals into wanteds and never the other way around.  We perform substitutions exhaustively.  For !SubstVar, this is crucial to avoid non-termination.
  * We should probably use !SubstVar on all variable equalities before using !SubstFam, as the former may refine the left-hand sides of family equalities, and hence, lead to Top being applicable where it wasn't before.
+ * We use !SubstFam and !SubstVar to substitute wanted equalities '''only''' if their right-hand side contains a flexible type variables (which for variable equalities means that we apply !SubstVar only to flexible variable equalities).
 
 Notes:
@@ -174 +175 @@
 }}}
 
+=== ===
+
+Example 4 of Page 9 of the ICFP'09 paper.
+
+{{{
+  F [Int] ~ F (G Int)  |-  G Int ~ [Int], H (F [Int]) ~ Bool
+=(norm)=>
+  F [Int] ~ a, F b ~ a, G Int ~ b
+  |-
+  G Int ~ [Int], H x ~ Bool, F [Int] ~ x
+(SubstFam w/ F [Int])
+  F [Int] ~ a, F b ~ a, G Int ~ b
+  |-
+  G Int ~ [Int], H x ~ Bool, x ~ a
+(SubstFam w/ G Int)
+  F [Int] ~ a, F b ~ a, G Int ~ b
+  |-
+  b ~ [Int], H x ~ Bool, x ~ a
+(SubstVar w/ x)
+  F [Int] ~ a, F b ~ a, G Int ~ b
+  |-
+  b ~ [Int], H a ~ Bool, x ~ a
+}}}
+
+'''TODO:''' If we use flexible variables for the flattening of the wanteds, too, the equality corresponding to `x ~ a` above will be oriented the other way around.  That can be a problem because of the asymmetry of the SubstVar and SubstFun rules (i.e., wanted equalities are not substituted into locals).
 
 == Termination ==