Swift Type Checking Is Undecidable
Slava Pestov, in 2020:
More precisely, the introduction of SE-0142 and SE-0157 has made canonical type computation into an undecidable problem.
[…]
Clearly, the
GenericSignatureBuilderis able to solve word problems for at least some semi-groups today (as well as protocols that don’t correspond to semi-groups; which is any protocol that has at least one associated type that does not conform to the protocol recursively). After all, the standard library and a large amount of user-written code makes use of generics, and works correctly.We are also aware of examples where we don’t manage to canonicalize types properly, causing miscompiles and crashes. We’ve been fixing these gradually over time, but we continue to discover more problems as we fix them. This was a strong hint that the underlying approach was not correct, which is why I spent some time thinking about the fundamentals of this problem. Indeed, we can now see that the reason we have struggled with correctness in this area of the language is that a solution is impossible in the general case.
What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. If a protocol obeys the restriction, the algorithm should always terminate with the correct result. If a protocol does not obey the restriction, we want to be able to produce a diagnostic instead of crashing or miscompiling.
Note that the C# and other languages also have undecidable type systems.
A year and a half ago I wrote how Swift type checking is undecidable, then last year I sketched out a new way of formalizing Swift generics as a term rewrite system . Since then I’ve been working on implementing this idea with the goal of replacing the GenericSignatureBuilder.
[…]
It uses a lot of memory, because answering generic signature queries requires keeping these rather large lazily-built GenericSignatureBuilder instances around for each generic signature the type checker encounters. In extreme examples you can make it allocate gigabytes of memory and end up with an effectively non-terminating compilation.
[…]
The new implementation is called the “Requirement Machine”. The source code is in the lib/AST/RequirementMachine directory of the source tree. […] I’ve measured a significant memory usage reduction when the Requirement Machine was enabled for queries in Swift 5.6.
[…]
I started writing a paper about the Requirement Machine. I’m not going to post a PDF yet because it is still a work in progress. In particular, the minimization algorithm is not documented, and some parts are out of date since it represents the state of the design from June last year. If you’re curious, install a TeX distribution and run “make” in the docs/RequirementMachine directory of the source tree.
