Changes between Version 44 and Version 45 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Dec 28, 2006 10:17:10 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v44 v45  
    117117== Unification in the presence of type functions == 
    118118 
    119 We do ''not'' rewrite type function applications implicitly during unification.  Instead, unifcation returns all ''required'' equalities that are non-syntactic.  That has two advantages: (1) the computation of coercions is completely decoupled from unification and (2) unification does not have to know anything about equality axioms and given equalities. 
     119We do ''not'' rewrite type function applications implicitly during unification.  Instead, unifcation returns all ''needed'' equalities that are non-syntactic.  That has two advantages: (1) the computation of coercions is completely decoupled from unification and (2) unification does not have to know anything about equality axioms and given equalities. 
    120120 
    121 '''TODO:''' The whole extension would be a lot less invasive if we could arrange for unification to enter the required constraints into a pool in the monad instead of returning them (as the type of the unification routines would stay the same).  Is this possible? 
     121'''TODO:''' The whole extension would be a lot less invasive if we could arrange for unification to enter the needed equalities into a pool in the monad instead of returning them (as the type of the unification routines would stay the same).  Is this possible? 
    122122 
    123 Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates. 
     123Needed equalities are then checked against the axioms and given equalities during context simplification, much like class predicates. 
    124124 
    125125