Karn Kallio wrote:
So, one alternative would be this: Remove [class] declarations but keep
[class] signature items. This means type classes would only be a
concept in the module system. Automatic resolution would only happen
for a type class hidden behind opaque signature ascription of a module,
though instances could then be declared elsewhere in the current way.
This is actually pretty close to what is de facto implemented right now,
so perhaps the [class] declaration is just a distraction.
Perhaps a better alternative is to make instances get picked up in the
current module (preserving the class declaration as it is).
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:
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. With the current type class implementation, there is no
worry about breaking type inference by replacing a type annotation with
another, definitionally equal type, whereas that worry would necessarily
appear with this straw man change.
One option would be to somehow make type classes abstract, even in their
modules of definition. Then there is the complication of how one
defines a new instance in such a context, which seems to grow
substantially more complex than the current "a type class is just a type
family with a bit set to ask 'please infer my instances.'" Yet the
module system provides a natural means of segregating code that needs to
know a definition from code that doesn't!
Talking through all this, I think I'm more convinced than before that I
should implement the proposal quoted at the top of this message, but I
might still be convinced otherwise. :)
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
