> Well, while Ur is full of undecidable type inference issues, I generally > try to keep type _checking_ (of sufficiently annotated programs) > decidable or at least predictable. It seems hard to support predictable > checking of same-module type class usage without requiring restrictions > that don't apply elsewhere. To explain: >
If picking up the instances must lead to undecidable type checking then removing the class declaration seems very good to me. Yet if the restrictions you mention could be mild while still leaving type checking decidable and allowing instance detection then maybe keeping the class declaration could be considered. What sort of restrictions would be required? > When a type class is considered as an abstract type-level function, I > believe it is decidable whether a particular type equals an application > of the class. However, when inference must be done where a type class's > definition is exposed, I _think_ the problem is clearly undecidable, > being an easy reduction target for the problem of higher-order > unification. So I guess a sufficient (but perhaps too onerous) restriction could be for the programmer to provide annotations showing which types are class applications? Also, now that you are a professor, maybe you could put a student to showing undecidability by working through your reduction! _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
