3 ms·

That's certainly a design choice they're free to make. Undecidability itself is less of a deal-breaker, although I would argue that a statically-typed language

That's certainly a design choice they're free to make. Undecidability itself is less of a deal-breaker, although I would argue that a statically-typed language which is unsound defeats the purpose of having static types in the first place. Ideally, you want type inference to terminate in the amount of time it takes to type a few keystrokes to get realtime assistance, so decidability is still an over-approximation from a tooling standpoint and in practice anything strongly super-linear is not a fun experience to use.

wiseowise 4y ago
I still don't follow how you came from > I know of no other programming language that puts as much effort into context- and structure-aware refactoring To soundness and decidability. Was there some study done where soundness and decability of Kotlin is provided?
- bmc7505 4y ago
  > I still don't follow... The premise was "toolability" in language design, which is one of Kotlin's main design principles. To do type-safe completion, navigation or refactoring, you need soundness, and to do it rapidly in the context of a live programming environment, you need to be able to resolve a type with keystroke latency. Rapzid asked [paraphrasing] "why not TypeScript, C#, or F#?" to which I responded that I do not consider these languages "toolable" because type checking is essentially broken (i.e., it might take forever, or give the wrong answer). > Was there some study done...? No, not that I am aware of. If you find one, I would be keen to read about it.
  - koyote 4y ago
    Have you ever used VS/Resharper/Rider with C#? I don't understand how you can come to the conclusion that type checking is broken and the language is not toolable? Can you give an example of where Kotlin's tooling achieves something that is not achievable at the moment in a C# IDE? (I've not used Kotlin much but I have never felt that the tooling for C# was lacking, so I am genuinely curious)
    - bmc7505 4y ago
      > Have you ever used VS/Resharper/Rider with C#? Yes, and to be clear I have never encountered these issues on practical problems. I am also not claiming Kotlin has or lacks these properties, just pointing out the fact if you care about toolability, soundness and decidability are important factors to consider and if there is a language design issue, it makes me less confident in any tooling which is built around it. It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine. Re: type checking in C#, maybe try the following example? https://learn.microsoft.com/en-us/archive/blogs/ericlippert/lambda-expressions-vs-anonymous-methods-part-five https://learn.microsoft.com/en-us/archive/blogs/ericlippert/...
      - lmm 4y ago
        > It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine. This is bad advice. Such an approach will go wrong often enough to burn you, and it will go wrong silently, whereas the kind of issues you describe tend to lead to something far more visible (and therefore correctible) like a complier internal error or an IDE refusing to perform a refactor.
      - jcparkyn 4y ago
        There's a fairly big difference between: a) "most of the time" being 60% (very roughly what I'd expect when doing renaming beyond a single function in JS, and that's being optimistic). b) "most of the time" being 99% (very roughly what I'd expect in a typical C#/java/kotlin codebase that isn't using too much reflection). Even aside from that, I'd argue that nullability, array covariance, and reflection all have MUCH bigger practical impacts on typechecking reliability than Turing-completeness. Most languages will simply fail to compile if the computed types require too much recursion, making the issue relatively moot. Type-checkers don't actually need to solve the halting problem to be sound, they just need to guarantee completion for _most_ types of code, and anything that can't be guaranteed can simply be rejected.

wiseowise 4y ago

I still don't follow how you came from > I know of no other programming language that puts as much effort into context- and structure-aware refactoring To soundness and decidability. Was there some study done where soundness and decability of Kotlin is provided?

bmc7505 4y ago
> I still don't follow... The premise was "toolability" in language design, which is one of Kotlin's main design principles. To do type-safe completion, navigation or refactoring, you need soundness, and to do it rapidly in the context of a live programming environment, you need to be able to resolve a type with keystroke latency. Rapzid asked [paraphrasing] "why not TypeScript, C#, or F#?" to which I responded that I do not consider these languages "toolable" because type checking is essentially broken (i.e., it might take forever, or give the wrong answer). > Was there some study done...? No, not that I am aware of. If you find one, I would be keen to read about it.
- koyote 4y ago
  Have you ever used VS/Resharper/Rider with C#? I don't understand how you can come to the conclusion that type checking is broken and the language is not toolable? Can you give an example of where Kotlin's tooling achieves something that is not achievable at the moment in a C# IDE? (I've not used Kotlin much but I have never felt that the tooling for C# was lacking, so I am genuinely curious)
  - bmc7505 4y ago
    > Have you ever used VS/Resharper/Rider with C#? Yes, and to be clear I have never encountered these issues on practical problems. I am also not claiming Kotlin has or lacks these properties, just pointing out the fact if you care about toolability, soundness and decidability are important factors to consider and if there is a language design issue, it makes me less confident in any tooling which is built around it. It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine. Re: type checking in C#, maybe try the following example? https://learn.microsoft.com/en-us/archive/blogs/ericlippert/lambda-expressions-vs-anonymous-methods-part-five https://learn.microsoft.com/en-us/archive/blogs/ericlippert/...
    - lmm 4y ago
      > It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine. This is bad advice. Such an approach will go wrong often enough to burn you, and it will go wrong silently, whereas the kind of issues you describe tend to lead to something far more visible (and therefore correctible) like a complier internal error or an IDE refusing to perform a refactor.
    - jcparkyn 4y ago
      There's a fairly big difference between: a) "most of the time" being 60% (very roughly what I'd expect when doing renaming beyond a single function in JS, and that's being optimistic). b) "most of the time" being 99% (very roughly what I'd expect in a typical C#/java/kotlin codebase that isn't using too much reflection). Even aside from that, I'd argue that nullability, array covariance, and reflection all have MUCH bigger practical impacts on typechecking reliability than Turing-completeness. Most languages will simply fail to compile if the computed types require too much recursion, making the issue relatively moot. Type-checkers don't actually need to solve the halting problem to be sound, they just need to guarantee completion for _most_ types of code, and anything that can't be guaranteed can simply be rejected.