Even so, "undecidable" doesn't need to be a problem. It would be possible that the undecidable Swift program is such a random mess that nobody would be likely to write it by accident.
However, it is worth looking into more practical aspects of how Swift's type system works, and there I share your concerns. Swift is the _only_ language I have ever used where I have ever seen the error message "the type checker was unable to infer the type of this expression" etc. - sometimes on dead simple code. Worse, I once tried to write an expressive, generic, functional framework, only to discover that it was completely unusable because the type errors that Swift returned were simply wrong and to fix it you had to put in type annotations in a bunch of places (without necessarily knowing where, just from the error messages), making the whole API extremely verbose and not particularly declarative anymore.
It's more common than you'd think: https://typing-is-hard.ch
> the type errors that Swift returned were simply wrong and to fix it you had to put in type annotations in a bunch of places (without necessarily knowing where, just from the error messages)
The diagnostics engine was completely overhauled in Swift 5.2, so this shouldn't happen anymore: https://swift.org/blog/new-diagnostic-arch-overview/
Keep in mind that Swift's type system is sound. It's just not decidable in its current state.
Undecidability means there's no algorithm that is guaranteed to terminate, not that any algorithm will crash. In this case, using a completion procedure to convert the same-type constraints into a confluent rewrite system should be sufficient. If completion fails an error can be diagnosed. This shouldn't break any real code in practice.
Someone found this in Java as well. Accidental Turing completeness crops up everywhere, it's actually rather hard to ensure decidability. It's a favorite pastime of people in this area; I'm somewhat disappointed you didn't find it to be interesting. In any case, personal attacks against the Swift compiler engineers (many who are quite competent at the things you are claiming they are lacking) are not appropriate.
Working at FAANG is an abject lesson in learning that assuming 'competence' (i.e. knowing mastery-level detail, taking responsibility everywhere, and going off on world-creating tangents rather than fixing bugs) is damn rare, nearly all of my career's achievements have come of accepting that and doing deep dives into problems.
Something is pretty broken over there, and it's especially not charming to read the team chiming in with 'lol haskell too!' - can I bill you for the type inference crashes and workarounds I've had to do because no one bothered saying anything until August 2020? https://twitter.com/krzyzanowskim/status/1305579668104331264...
I'll be happy to admit I'm wrong when Swift UI 2021 is rendering lazy lists just fine on Mac and iOS, otherwise, its just me hearing about ARC optimizations for the 50th time and trusting it. https://twitter.com/jckarter/status/1305562770859933696?s=20
That's not related to the decidability of that specific algorithm in the generics implementation, though.
Did you file bugs for the type checker problems you found? (I’m not being snarky; I’d love to take a look at them)
How is it that a single person named Edwin Brady can think of, implement and have a programming language with a decidable type system that is more complex than Swift, working on it part-time?
I'm sorry, I consider a company worth a trillion dollars, sitting on billions of dollars it doesn't know what to spend on, that spends billions per year on R&D, to know the basic properties of the type system their most actively developed programming language uses.
That's just me.
(It should be clear, but this is both factual and a joke. The core team is good people, Slava is good people, Slava is not on the core team.)
The tone sounds histrionical because it is way ahead of the herd's perception. It's been terrifying to have feet in multiple communities, have a strong foot in Apple's community, and see how things are done over there and gotten worse over the years, particularly after Swift's release.
https://forums.swift.org/t/swift-type-checking-is-undecidabl...
Swift's core team recently found out that they don't understand the type system they've created - they were fixing compiler 'bugs' for months without getting anywhere, until one of them finally realized hey, I should probably attempt to understand what we've built, not just 'fix' a never ending stream of bugs we seem to be having.
Turns out, the type system they built guarantees 100% that type checking is undecidable (in software developer terms, you can crash the compiler by typing perfectly legal Swift code and nobody at Apple knows how to fix it without breaking existing code because they didn't even know they built a language that has this property up until very recently). They figured this out after announcing a stable ABI by the way. Upon discovery, some of the core team members said the discovery was great/nice work.
It's not like we have people who use mathematics to prove properties of type systems without any shadow of a doubt or anything. I wonder how many of them are working on Swift or are employed at Apple, within their multi-billion dollar R&D budget... I wouldn't at all be surprised if the answer was zero, given that it was a software developer who knew a little math who made this discovery.