Changes between Version 41 and Version 42 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 7, 2008 11:08:28 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v41 v42  
    125125  * !SubstFam (formerly, IdenticalLHS) only applies to family equalities (both local and wanteds) 
    126126  * Top only applies to family equalities (both locals and wanteds) 
    127  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. 
     127 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. 
    128128 * Rules applying to variable equalities: 
    129129  * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds) 
    130130 * 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. 
    131131 * 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. 
     132 * 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). 
    132133 
    133134Notes: 
     
    174175}}} 
    175176 
     177=== === 
     178 
     179Example 4 of Page 9 of the ICFP'09 paper. 
     180 
     181{{{ 
     182  F [Int] ~ F (G Int)  |-  G Int ~ [Int], H (F [Int]) ~ Bool 
     183=(norm)=> 
     184  F [Int] ~ a, F b ~ a, G Int ~ b 
     185  |- 
     186  G Int ~ [Int], H x ~ Bool, F [Int] ~ x 
     187(SubstFam w/ F [Int]) 
     188  F [Int] ~ a, F b ~ a, G Int ~ b 
     189  |- 
     190  G Int ~ [Int], H x ~ Bool, x ~ a 
     191(SubstFam w/ G Int) 
     192  F [Int] ~ a, F b ~ a, G Int ~ b 
     193  |- 
     194  b ~ [Int], H x ~ Bool, x ~ a 
     195(SubstVar w/ x) 
     196  F [Int] ~ a, F b ~ a, G Int ~ b 
     197  |- 
     198  b ~ [Int], H a ~ Bool, x ~ a 
     199}}} 
     200 
     201'''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). 
    176202 
    177203== Termination ==