Changes between Version 44 and Version 45 of TypeFunctionsTypeChecking
 Timestamp:
 Dec 28, 2006 10:17:10 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsTypeChecking
v44 v45 117 117 == Unification in the presence of type functions == 118 118 119 We do ''not'' rewrite type function applications implicitly during unification. Instead, unifcation returns all '' required'' equalities that are nonsyntactic. 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.119 We do ''not'' rewrite type function applications implicitly during unification. Instead, unifcation returns all ''needed'' equalities that are nonsyntactic. 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. 120 120 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? 122 122 123 Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates.123 Needed equalities are then checked against the axioms and given equalities during context simplification, much like class predicates. 124 124 125 125