robrix
Typeclasses/constraint-based name overloading
It’d be great to be able to define a typeclass, instance(s), and then automatically use the appropriate instance (or supplied parameter) when using an overloaded symbol.
Right now we define the “class” by using a type definition, e.g.:
Functor : ∀ f : Type -> Type . Type
Functor = \ f
. ∀ a : Type
. ∀ b : Type
. ( a -> b)
-> (f a -> f b)
and then define “instances” using the class name in the type:
map : Functor Maybe
map = \ _ b f m . m (Maybe b) (nothing b) (\ a . just b (f a))
This is tidy enough, but callers have to manually supply an “instance,” which means a bunch of extra parameters everywhere; and there’s no general symbol named map, so it has to be explicitly bound as an extra parameter, and explicitly supplied by callers. Automatically supplying a definition of map via some sort of typeclass resolution/constraints would be a big improvement.
The design landscape is vast: we also need to decide how/whether to deal with canonicity, and thence orphans; how/whether to handle superclasses; and how/whether to specialize & inline when the specific instance is known.