3 ms·

What does this mean? It is the end of Swift?

fanf2 6y ago
The important context in the intro is, "The type checker needs to be able to determine that x and y have the same type, and reject the code if not. This is what we mean by computing canonical types." There's a summary at the end titled, "what does this mean?" which says that undecidability doesn't bite in practice with real-world code, but the type system features discussed in the post have been the cause of bugs: "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." So the question arising from this undecidability is how to fix it: "What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. [...] I'm optimistic that introducing this restriction should have very little impact on real-world code."
Someone 6y ago
No. This probably is similar to the definite assignment problem (https://en.wikipedia.org/wiki/Definite_assignment_analysis https://en.wikipedia.org/wiki/Definite_assignment_analysis) in the sense that the problem for the current language is undecidable, but you can pick a usable subset of the language in which it is solvable (Java picked a very small subset for the definite assignment problem, making it very easy to implement that aspect of the language, without losing much expressiveness in practice) If so, the main question the developers of Swift face is to decide in what way(s)/how much to constrain the current language. A side effect of that could be that the compiler gets faster because the type checker will no longer have to consider some dark corners of the type system that were removed from the language.

The important context in the intro is, "The type checker needs to be able to determine that x and y have the same type, and reject the code if not. This is what we mean by computing canonical types." There's a summary at the end titled, "what does this mean?" which says that undecidability doesn't bite in practice with real-world code, but the type system features discussed in the post have been the cause of bugs: "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." So the question arising from this undecidability is how to fix it: "What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. [...] I'm optimistic that introducing this restriction should have very little impact on real-world code."

Someone 6y ago

No. This probably is similar to the definite assignment problem (https://en.wikipedia.org/wiki/Definite_assignment_analysis https://en.wikipedia.org/wiki/Definite_assignment_analysis) in the sense that the problem for the current language is undecidable, but you can pick a usable subset of the language in which it is solvable (Java picked a very small subset for the definite assignment problem, making it very easy to implement that aspect of the language, without losing much expressiveness in practice) If so, the main question the developers of Swift face is to decide in what way(s)/how much to constrain the current language. A side effect of that could be that the compiler gets faster because the type checker will no longer have to consider some dark corners of the type system that were removed from the language.