I can't remember the name of the actual type inference algorithm used by swift, but my recollection is that its approach to bidirectional inference is much more, we'll say, powerful. It does allow some things that most other languages cannot do.

The Damas-Hindley-Milner type system (sometimes Hindley-Milner, I'm not sure to this day why Damas is included by some, and not by others, and honestly at this point I'm not really interested in finding out :D my education has had Damas so that's my default) is the basis of more or less all functional languages, and is linear time. But that is largely possible due a function named 'f' only has one declaration, and one type (that type might be generic, but under these type systems that is a single type)

Now consider an expression: f x (f y (f z 1))

In DHM, f has a type for all a->b->c, all of which are fixed - they may be explicit types or they might be type parameters, so in the above we know that the type of x must be a'0, the type of (f y (f z 1)) must be b'0. In f y (f z 1), y must be a'1, the type of (f z 1) must be b'2, but also in this case we know the type of c'1 must be the same as b'0, so we've unified those types, hurrah!. The same then happens in f z 1, z must be of type a'2, and 1 is Int, so b'2 is unified with Int, e.g. b'2 == Int, and similarly to earlier we know that the return type c'2 must be the same as b'1.

From that you can probably see the general gist of how this inference operates in linear time.

The first complexity swift has comes from the ability to have overloads of a function, so the type of f might be a->b->c, or c->b->a, or a->b->c->d, or even a->b->c, a->b->a, a->b->d. We can discard the function with a mismatching number of parameters[1], but we have multiple possible types to select from, so in f x (f y (f z 1)) (ignore the non-swift syntax) swift cannot immediately assign a type to x, it also cannot immediately assign a type to f y (f z 1), it cannot immediately assign a type to y, it cannot immediately assign a type to f z 1, or z. We'll leave 1 until later - for now just assume it's an Int. Swift's type system is much closer to a generalized constraint solver: instead of a fairly direct linear path for assigning types, it has to try to find the a combination of the correct types and the functions those that correspond to those types, ensuring that the return types of each function works in the bounds of the caller. For example you could have (excuse the syntax)

f(Int, Int) -> Int // f_0
f(String, Int) -> String // f_1
f(Float, String) -> String // f_2
f(Int, String) -> Int // f_3

Now consider what happens in the above nested calls: f z 1 this could be either f_0 or f_1, now consider f y (f z 1), currently we have two options for f z 1, one returns an Int and one returns a string, but that means we could be calling f_1, f_2, or f_3, so the return type can still be String or Int. Which means f x (f y (f z 1)) can now be f_0, f_1, f_2, or f_3. If you wrote let v : String = f x (f y (f z 1)) (ignore the syntax nonsense I'm just trying to be consistent with the expression), then you've provided a concrete type so it can reduce the possible options of the outer expression to just f_1 or f_2.

Basically to get to a complete solution it has to determine the specific types of x, y, and z for a call to f, while at the same time the type of f determines the types of x, y, and z.

You can probably see how it's possible to construct expressions where this can start taking a, uh... long time.

Despite this complexity, most code decays to linear time, but "most" is not "all", and it is possible to write reasonable looking, and probably objectively reasonable, code where the inference becomes exponential over the set of types and overloads.

So that's the basic model of the type system which leads to this, but there are ways in which this is exacerbated. Let's go back to 1, earlier we said it is an Int, but it actually isn't, it is an integer literal, and types can implement a protocol (this is exactly equivalent to trait in rust, type class in Haskell - they're all literally the same type theoretic construct) - something like ConvertibleFromIntegerLiteral though definitely don't quote me on this :D. While that may not sound super useful, but it allows somethings someDouble + 1 to work entirely from within the logic of the type system, with no special casing of "I am adding this numeric type to an integer literal".

However I believe in the original version of swift, that meant

let x = 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1....;

Would take a lot of time very quickly because without being careful about how you prioritize search and similar, every call to + (in type theory and reason arithmetic operators are functions) might be to Double + Double or Int + Int, and that therefore mean each of the +s around them could be Int or Double, so that's fun. But that's also too simple because other types implement convertible from Int: Int8, Int16, Int32, UInt, UInt8, ..., Float, etc so suddenly there are many options.

In my experience the easiest way to cause this to happen in code that isn't written with the intent of demonstrating edge cases (e.g. the original 1+1+1... example above isn't what you would write in practice) is actually closures, I assume because absent an explicit type signature the type system simply has a single gigantic expression so essentially the entire body of the closure becomes exciting. Given the above complexity of the type inference system, at a base level it seems surprising to me that it generally handles most even relatively complex code, and that's because the actual algorithm involved is quite a bit more clever than the naive explanation above, however at a fundamental level their are expressions where inference becomes an exponential operation, but I think in some cases they become undecidable (which would assume is considered an error, as saying "we can't tell if your code is correct" seems somehow worse than "this takes to long, please provide us with some type information" :D).

I think a lot of the type system and language for swift is really nice, I also think a lot of rust is really nice, they've just taken different approaches and tradeoffs (ignoring the very different decisions around object lifetime as that isn't really involved in how the type systems and interfaces feel) that result in complexity in different areas. Swift does also have other considerations that I feel are less of an actual choice (it's possible it would have done this anyway): ignoring the different inference algorithms most of the type system of each is the same - they both inherit from the "true" functional languages, they both model type polymorphism in the same manner. But swift also has classes in the traditional polymorphic inheritance model, because it has to interact pretty much seamlessly with objective-c (to the extent that the vtable pointer itself is compatible with objective-c's isa pointer).

Again there are tradeoffs everywhere - the class portion of swift has a bunch of costs, but at the same time means that it is much easier for the type system to understand the C++ object model, which is much harder in rust (for instance, it is very difficult for rust to model the behavior of C++ types that have things like copy constructors). Noting of course that easier does not mean easy, because, you know, C++ :D

[1] In general most functions written in languages like Haskell are literally a->b->c: e.g if you write a function that takes two arguments and returns a value, it is the same type as a function that takes one argument and returns a function that takes another argument. At a core level in fact all functions only take one argument, and everything else is syntactic sugar. The equivalent of a two argument function in languages like C, rust, Swift, etc is (a, b)->c.

Haskell (and other languages like it) doesn't support overloading, which helps a ton AFAICT.

My impression on the contrary is that the Swift people are generally very good at what they do, including pretty good at language design. (Look at their work on ABI stability, it is pretty impressive.)

I do agree that it's interesting that they decided that a naive approach to overloading using backtracking was okay, and now it comes back to bite them massively. This does sound like a design mistake. I would hazard to guess that it comes from engineering experience, rather than lack of expertise: my impression is that while academics tend to be fairly rigid in their design principle ("no exponential worse cases!", "let-polymorphism will be saved at all costs!", "principality forever!", etc.), experienced engineers have a more pragmatic approach where they know that many constraints can typically be relaxed in practice, and it's okay. I can sort of guess how the discussion went:

• "So we've been trying to come with an efficient overloading-resolution algorithm for a few months now, it does not cover all use-cases, we need to extend the overload declaration mechanism to let users express X and Y and Z so that we can check this efficiently."

• "Enough is enough! Let's do the dumb thing of just backtracking on every possible choice, and picking the choice that works."

• "But... this is exponential!"

• "Sure, but exponential is fine because user expressions are short in practice! Today's machine are fast, they can deal with exponentials on small inputs just fine. Users will much prefer a simple system that is easy to reason about, and fast enough in practice, to the complexity monster that you have been designing and refining for months. Let's cut down on our complexity budget for this corner of the language."

• "But..."

• "Let's run the dumb algorithm on our testsuite, you will see that it is fast enough in practice."

... and that's (maybe?) how it went. Of course, hindsight is 20/20, and in retrospect it is strange that they did not consider the fact that people do in fact write reasonably-complex nested trees of overloadable infix operators, and try to put some of those in their testsuite before deciding to go for this approach.

Well. Would you consider ML, Haskell, and Java to have proper type systems? Because ML and Haskell require exponential time to type check, and type checking Java is undecidable (so there are short Java programs for which type checking runs forever, and this is not a bug). Fortunately none of these behaviors comes up much in practice.

ML and Haskell are hard to type check because is polymorphism, and Java because of subtyping. The difficulty in Swift is about operator overloading. Not obvious to me how much this is a poor implementation vs. provably hard.

https://static.aminer.org/pdf/20170130/pdfs/popl/o8rbwxmj6h2cxf7qdezlupsbgn5u40wn.pdf

https://arxiv.org/pdf/1605.05274

Swift is a relatively new language…

It did have to inherit a lot of objective-c compatibility support though. I wonder how much that hamstrung the overall design of the language.

It took 42 seconds to type check "a project that makes heavy use of overloading and generics," per the post, not "a simple expression." Compilers do occasionally get into pathological holes in typechecking, and Swift moreso than compilers who don't implement type checking with a SAT solver, but the claims in the post that the time spent in type checking a whole project are improved are not unreasonable here, and certainly not so unreasonable that they would make me question the expertise of the dev team.

I also sometimes wonder about the impossibility of going back on decisions, and not even making a cultural effort. So we can't remove overloading and ExpressibleByX, but couldn't Apple at least start suggesting that they're not a good idea in new code? Like, in WWDC sessions? It's hard for Apple to admit mistakes, but still. We've known for years that certain kinds of things are extremely slow to compile and while some improvements are possible, they're never going to become fast.

But, operators are functions too, and they don't get argument labels. You'd have a hard time getting people to give up the ability to use + between a variety of same-typed operand pairs. The promise of source stability locked that in many years ago.

That is: One of the reasons they did add type-based overloading is to get the definition of the basic number types out of the language and into the standard library, which entails operator overloading. That is, static func + (lhs: Int, rhs: Int) -> Int and static func + (lhs: Double, rhs: Double) -> Double must be defined in the standard library, because Int and Double are. Their call sites look like 2 + 2 and 3.0 + 3.0. So these addition functions can only be distinguished by operator types, unless we had a different name than + for each known type. Some languages use +. for floats but we'd also have to distinguish Int64, UInt8… or give up on those and use named functions.