5 ms·

Any software developer using any software released by Apple within it's first 2-3 years is a free beta tester. Swift's core team recently found out that they d

Any software developer using any software released by Apple within it's first 2-3 years is a free beta tester. 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.

anoncareer0212 6y ago
He's right. 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.
slicebo123 6y ago
Is there some thread/blog_post you could provide talking about the discovery of the type system issue?
- slicebo123 6y ago
  Guessing it's this: https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...
- eyesee 6y ago
  I believe GP is referring to this post: https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...
dwarfland 6y ago
Swift is a shitshow
Tainnor 6y ago
You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable. 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.
- slavapestov 6y ago
  > You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable. It's more common than you'd think: https://typing-is-hard.ch 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/ https://swift.org/blog/new-diagnostic-arch-overview/
- favorited 6y ago
  > Other type systems can at least be unsound, I don't know if any of them is undecidable. Keep in mind that Swift's type system is sound. It's just not decidable in its current state.
  - Tainnor 6y ago
    Is that proven or just conjectured?
slavapestov 6y ago
> 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). 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.
- deleted 6y ago
  [deleted]
stephencanon 6y ago
Hey now, let's not slander Slava by accusing him of being on the core team. (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.)
- slavapestov 6y ago
  Thankfully the core team membership predicate is decidable, at least.
saagarjha 6y ago
> Turns out, the type system they built guarantees 100% that type checking is undecidable 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.
- anoncareer0212 6y ago
  It's not quite that simple, OP is right, pace on Swift improvement slowed to a crawl for 3? years now as they played whack-a-mole with type inference and got to stable ABI. It was only supposed to take a year, and, it's utterly __shocking__ to find out the type inference whack-a-mole intractable _after_ pushing the stable ABI. 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.
  - slavapestov 6y ago
    The issue OP mentioned is certainly not intractable to fix, and in general type inference doesn't have much to do with the stable ABI. The ABI work was about refactoring some compiler internals and implementing library evolution support, which as far as I'm aware is unique among statically-compiled languages: https://swift.org/blog/library-evolution/ https://swift.org/blog/library-evolution/. There was also a lot of work on code size improvements, runtime memory usage, and compilation time. The pace at which language features are added is not the only valid measure of language development.
    - anoncareer0212 6y ago
      Those are all arguments your team has been repeating for a while, and I used to be amenable to, but am no longer given the amount of time that has elapsed. 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?s=20 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 https://twitter.com/jckarter/status/1305562770859933696?s=20

anoncareer0212 6y ago

He's right. 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.

slicebo123 6y ago

Is there some thread/blog_post you could provide talking about the discovery of the type system issue?

slicebo123 6y ago
Guessing it's this: https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...
eyesee 6y ago
I believe GP is referring to this post: https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...

dwarfland 6y ago

Swift is a shitshow

Tainnor 6y ago

You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable. 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.

slavapestov 6y ago
> You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable. It's more common than you'd think: https://typing-is-hard.ch 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/ https://swift.org/blog/new-diagnostic-arch-overview/
favorited 6y ago
> Other type systems can at least be unsound, I don't know if any of them is undecidable. Keep in mind that Swift's type system is sound. It's just not decidable in its current state.
- Tainnor 6y ago
  Is that proven or just conjectured?

slavapestov 6y ago

> 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). 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.

deleted 6y ago
[deleted]

stephencanon 6y ago

Hey now, let's not slander Slava by accusing him of being on the core team. (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.)

slavapestov 6y ago
Thankfully the core team membership predicate is decidable, at least.

saagarjha 6y ago

> Turns out, the type system they built guarantees 100% that type checking is undecidable 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.

anoncareer0212 6y ago
It's not quite that simple, OP is right, pace on Swift improvement slowed to a crawl for 3? years now as they played whack-a-mole with type inference and got to stable ABI. It was only supposed to take a year, and, it's utterly __shocking__ to find out the type inference whack-a-mole intractable _after_ pushing the stable ABI. 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.
- slavapestov 6y ago
  The issue OP mentioned is certainly not intractable to fix, and in general type inference doesn't have much to do with the stable ABI. The ABI work was about refactoring some compiler internals and implementing library evolution support, which as far as I'm aware is unique among statically-compiled languages: https://swift.org/blog/library-evolution/ https://swift.org/blog/library-evolution/. There was also a lot of work on code size improvements, runtime memory usage, and compilation time. The pace at which language features are added is not the only valid measure of language development.
  - anoncareer0212 6y ago
    Those are all arguments your team has been repeating for a while, and I used to be amenable to, but am no longer given the amount of time that has elapsed. 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?s=20 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 https://twitter.com/jckarter/status/1305562770859933696?s=20