Bounded quantification (or, typeclasses)

[thautwarm]

it's simple.

Add a TImplicit in the type hierarchies, and extract all implicit types wrapping arrow types when instantiating.

type ty =
| ...
| Implicit of ty * ty (* the first element is the instance *)

Further, you should maintain a scope from symbols(unique) to types, remember the current scope when instantiating.

Finally(after type inference), access the remembered scope(symbols to types) and the implicit type, search the symbol available in scope, select the one whose type is the most specific, take this symbol as the argument of the bounded function.

type 'a eq = { (==) : 'a -> 'a -> bool }
let int_eq = {(==) = compare}

let (==) : {'a eq} => 'a -> 'a -> bool = fun inst ->
    fun lhs rhs -> inst.(==) lhs rhs

(* during type inference and compilation, we resolved {'a eq} to be {int eq}, and  *)
(* remember the available symbols*)
1 == 2 

(* after type infer, we know int_eq is the available symbol whose type is the most specific *)

[tomprimozic]

It's been a while since I've looked into implicits, but IIRC the difficult parts are:

• higher-order implicits: if you have eq : int -> int -> bool and eq : implicit {eq : a -> a -> bool} -> a list -> a list -> bool, can you derive eq : int list -> int list -> bool (easy in this case but can get more complicated in general... basically Turing-complete)
• uniqueness checking: what to do if both eq : a -> a -> bool and eq : int -> int -> bool are available - (report an error, resolve using some kind of priorities, ...)
• instance coherence problem: if you create a Set using eq1 : int -> int -> bool but then use it in context with eq2 : int -> int -> bool

Haskell and Scala have different solutions to these problems, neither of which I particularly like...

I have some ideas how to solve them, but they're very complex and not very well developed :)

[thautwarm]

the higher order cases

let list_eq : forall a. eq a => eq (list a) = fun inst -> {
    (==) = List.forall inst.eq
} 

The instantiations cause passing into implicit arguments, let's see an example:

[1] == [2]

After type inference, for ==([1], [2]) we generate some IR look like

Call(
      Instance(
          type = forall a. eq (list a),
          scope = (* available symbols of this site *), 
          expr= (*unique symbol of == *)
       ), 
      (*ir of [1] *), 
      (*ir of [2] *)
)

We can perform instance resolution, and find out let list_eq : forall a. eq a => eq (list a) matches, however, we still need to instantiate list_eq, so we search for the scope again, find out a most specific eq a, and use it to construct a forall a. eq (list a) instance. This process can be recursive(list a uses itself, even the polymorphic recursions), though you might need some extra checking for the termination guarantee. Yes it's turing complete, but the code just works like a charm if you assure the termination yourself.

I personally prefer not to support polymorphic recursions without explicit annotations.

the uniqueness checking

I think most specific instance just answers your questions.. .

instance coherence problem

As for instance coherence problem, this is quite a big topic, and thank you very much to bring this here. There're so many solutions to this, orphan instances and contextual dispatching(in Haskell, you can also write the Labelled classes, though a bit verbose than compiler builtin support), IIRC are the most popular 2 ways.

However, there is a commonly adapted design for the overlaps or duplications of instance resolution, that we can just produce an error when this sort of stuffs get raised, and tell users to there're some other approaches to resolve, which IMHO is quite a conservative, working and smart strategy.

Not every user of a programming language is clever(enough), they might not know what they're doing, so use a conservative approach by default, and tell them other solutions are available then, I cannot criticize the designers if they do this.