Changes between Version 44 and Version 45 of TypeFunctionsTypeChecking

Timestamp:

12/28/06 14:17:10 (6 years ago)

Author:

chak

Comment:

--

TypeFunctionsTypeChecking

@@ -117 +117 @@
 == Unification in the presence of type functions ==
 
-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.
+We 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.
 
-'''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?
+'''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?
 
-Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates.
+Needed equalities are then checked against the axioms and given equalities during context simplification, much like class predicates.