Typeclasses/constraint-based name overloading

[robrix]

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.

[robrix]

cf #35 re: type-directed program synthesis cf #36 re: implicits

[robrix]

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.