Changes between Version 96 and Version 97 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 30, 2008 5:05:22 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v96 v97  
    250250 1.  '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''left-hand side''' of all equalities.  We also perform the same substitution on all class constraints. 
    251251 2. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`.  Moreover, we have to do the same for equalities of the form `co :: F t1..tn ~ alpha` unless we are in inference mode and `alpha` appears in the environment or any other wanteds. (We never instantiate any flexibles introduced by flattening locals.) 
    252 The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution.  It is an important property of propagation that we only need to substitute into right-hand sides during finalisation. 
    253  
    254 After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above). 
     252The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution.  We need to instantiate all flexibles that arose during flattening of wanteds ''before'' we instantiate any other flexibles.  Consider `F delta ~ alpha, F alpha ~ delta`, where `alpha` is a skolem and `delta` a free flexible.  We need to produce `F (F delta) ~ delta` (and not `F (F alpha) ~ alpha`).  Otherwise, we may wrongly claim to having performed an improvement, which can lead to non-termination of the combined class-family solver. 
     253 
     254Note that it is an important property of propagation that we only need to substitute into right-hand sides during finalisation.  After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above). 
    255255 
    256256== Examples ==