I am working on a type system supporting overloading. I have a rough idea of how type inference is usually implemented in such a scenario, but I am wondering how - after type inference is completed - the correct implementation of an overloaded operator can be chosen. Or, in other words, how the inferred type can be passed back down the syntax tree to the operator.
For a small example, consider the expression
(x + y) + 1 where
x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N.
:: stands for type of, and
a | b stands for type
a or type
The way, I assume, type inference would now work, is to traverse the syntax tree, and for each node return a type constraint:
(x + y) + 1 => ((N & (N[a=N] | S[a=S])), (N & N) -> N) | ((S & (N[a=N] | S[a=S])), (S & N) -> S) => N[a=N] 1 => N + => (N -> N -> N) | (S -> S -> S) x + y => ((N & (N | S)), (N & a) -> N) | ((S & (N | S)), (S & a) -> S) => N[a=N] | S[a=S] x => N | S y => a + => (N -> N -> N) | (S -> S -> S)
a & b in this example stands for unifying the types
[a=T, b=U] is a set of equality constraints for type variables.
As expected the return type of the given expression is inferred as
N[a=N], that is
N where the type variable
a is expected to be
Therefore, of the two provided implementations for the
+ operator (
N -> N -> N,
S -> S -> S),
N -> N -> N should be used. In the given example, the resulting type is inferred, but not the type of the overloaded operator. My question is if there is a common pattern that is used to inform the
+ node in the syntax tree of the used implementation.