[aw1621107]

Fascinating! Thanks for the insight!

Does the up to 60% figure include programs that make heavy use of GADTs, or are those even worse in terms of the proportion of compilation time spent type checking?

I had no idea Swift's type checking algorithm is exponential. How easy is it to run into those conditions?

[octachron]

For GADTs heavy programs, it depends a lot on how much work the exhaustiveness check for pattern matching is doing behind the scene: With GADTs, one can encode a Turing machine in the type system. In that pathological case, analyzing that a pattern match is exhaustive might require to check if the encoded Turing machine stops in n steps. Consequently, it is perfectly possible to write programs where the compiler spends 99% of its time on analyzing pattern matching. But it is also possible to write GADTs heavy programs that don't require such expensive analyses.

I have no first-hand experience with Swift but the previous discussion at https://news.ycombinator.com/item?id=12108876 and the description of the problematic algorithm seems to indicate that numerical or mathematical code can run quite easily into the issue.

However, I must add that type inference algorithms being exponential in the source code size is nothing new: OCaml and Haskell inference are also exponential in the source code size. But that is because the size of types can be exponential in the source code size. Moreover, type inference complexity in OCaml and Haskell is linear in the size of types. And since in practice, no one ever uses exponentially growing types, type inference stays well behaved.

The specific issue with Swift is really more that even for simple result types, the inference may still have to do an exponential amount of guess work.