Type inference

I've written extensively about the type inference algorithm in previous posts, so I'll try not to repeat myself.

The type solver's purpose is to generate solutions for two kinds of problems:

• For functions which have multiple overloads, select the correct overload based on the input arguments.
• For functions which have template parameters, determine what type is bound to each template parameter.

I want to focus on this second item. For each templated function call, the solver creates a BindingEnv ("binding environment") object that stores the values of each type variable. So if I have a function such as:

def min[%T](a0:T, a1:T) -> T;

The BindingEnv stores the definition of T. If there is more than one call to "min" in a given expression:

let a = min(b, min(c, d));

...then the algorithm creates two BindingEnvs, each of which may have a different value for T. These values are referred to as substitutions. For example if I add a substitution declaring that "T" is an "int", what I am really saying is that types 'T' and 'int' are equivalent.

Unfortunately, having multiple environments creates a number of problems. The first has to do with backtracking.

Here's how backtracking works: Say we call our 'min' function with two incompatible arguments, such as List[String] and float. The solver first attempts to add a substitution for T := List[String]. However, when it gets to  the second argument, it realizes that T cannot be equivalent to both List[String] and float, so it needs to 'unbind' the previous substitution. The way this works is that BindingEnv has the ability to backtrack to a previous state - you call env.getCurrentState(), which returns a token (an int, actually), which can then be used to call env.backtrack(token) and remove all of the substitutions that were added subsequent to the call to getCurrentState().

However, where we run into trouble is when more than one BindingEnv is involved, because now we need to backtrack multiple environments and keep them in sync. A more robust approach is to just have a single environment for the whole expression, with one single backtracking state.

But then how do we deal with multiple different occurrences of 'T' in the same expression? The answer is we need to relabel all of the variables in each call: That is, we transform 'T' into 'T1' or 'T2', depending on which T we are talking about. Now all type variables are unique, so we don't have to worry about collisions anymore, and we can have just a single environment.

Another limitation of the current solver is that within an environment any given variable can only have a single substitution that is currently active. Say for example we know that 'T' == 'List[S]' where S is another type variable. Later we refine this and add 'T' == 'List[String]'. We don't remove the old substitution - instead we add a new one on top, so that it hides the previous substitution. That way, if we have to backtrack, it will revert to the previous value of 'T' rather than losing it entirely.

The problem with this approach is that it's attempting to do the reconciliation between the new and old substitutions too early - for example if we have 'T' == 'List[A]' and 'T' == 'List[B]', and we don't know what 'A' and 'B' are yet, there's no way to know which of the two definitions should win. Instead, what we should do is keep both definitions, and reconcile them later.

In fact, what I'd like to do is to make the type inference algorithm have clearly defined phases. (It has phases now, but they aren't cleanly separated.) The phases would be:

• Gather constraints - walk through the entire expression and find all overloaded functions, type variables, and other "choice points" - places in the expression where the type solver is able to choose between several alternatives.
• Relabeling - replace all type variables with new ones that have unique names.
• Unification - this is where we identify all possible substitutions. Note that some substitutions are conditional - say I have two overloaded versions of "print", one which takes a String, and the other takes a %T, then the substitution for %T is only meaningful if the second overload is chosen.
• Constraint simplification - if we have a set of substitutions {T := S, S := int} we can replace them with {T := int, S := int}.
• Overload selection - this is a fairly standard constraint minimization algorithm. For each choice point, we compute a ranking that says how good the choice is. For example, if we have a function that returns a uint8, but the variable being assigned to is a uint16, that's not as good of a choice as a function that returns a uint16. The algorithm attempts to maximize the ranking for the whole expression. (Because the choice points are interdependent, choosing the best result for one node in the expression tree may cause a worse choice elsewhere.)
• Error reporting: If any of the phases fails, or the final result would produce type conversion warnings, we want to clearly inform the user of what went wrong.
• Finalization: Replace all of the temporary type variables with the actual concrete types that they are bound to in the environment.

In any case, I have a ways to go before this particular vision can be achieved.