(I'm not sure what category to use to ask this.) I'm wondering how the Swift type inference/checking algorithm works. I've been reading that some languages use a unification algorithm to infer types, in an entire function body at once, or in a larger chuck of code. But often those languages seem more academic, or simplified, and don't have things like function overloading, or objects and methods.
So I'm wondering, does Swift type check a function body with something like unification, or does it use a more restricted process to proceed line-by-line, and "bottom up" in the AST?
I've been working with some code for unification and Hindley-Milner type inference for a simplified language. It's cool the way it works, but if you throw in overloading, it's seems I'd need to add an ability to backtrack (like Prolog) and there might be a lot of backtracking as the algorithm searches the various possible pathways. A similar challenge with objects and methods, because it needs to know the type of the x in x.foo(a, b) before it can even lookup foo.
Swift’s type inference happens on a per-expression (er, per-statement, see Slava’s more comprehensive answer below!) basis (not exactly line-by-line but not a whole function body at once like you mention), but within an expression types can end up propagating bidirectionally not just ‘bottom up’.
Yeah, this can become an issue in Swift as well where in the face of substantial overloading you can end up with compile times scaling exponentially relative to expression size. Various heuristics and improvements have been implemented to help with the most common cases where this arises.
I think this makes more sense in the Development > Compiler section, so I moved it there for you (something I only recently discovered I could do as a "regular"-level user; mwahahahaha consider this me drunk with power ).
Inside a named function declaration (result builders and multi-statement closures are a bit trickier), Swift type checks statements one at a time, with type information only flowing in one direction. So for example, if you have this, the type of bar() cannot influence the type of x:
let x = foo()
bar(x)
A single expression is type checked by assigning type variables to each sub-expression and using a constraint solver to assign concrete types to these type variables. (And single-expression closures are checked as part of the containing expression.) Overloads are modeled with disjunctions ("the type of X is Foo OR Bar Or Baz") and this requires exploring a search space with backtracking as you noted.
So for example in bar(foo()), the type of bar() can determine which overload of foo() is chosen, and vice versa.
The solver's goal is to find one or more solutions, where each solution selects a choice of overloads and assigns types to each sub-expression. If there are multiple valid solutions that represent different choices of overloads, the solver uses various heuristics to pick the best one, or diagnoses ambiguity.
).