3 ms·

> Do you mean JVM language? TypeScript, C#, and F# at least come to mind. As I mentioned in another comment [1] on this thread, soundness and decidability are

> Do you mean JVM language? TypeScript, C#, and F# at least come to mind. As I mentioned in another comment [1] on this thread, soundness and decidability are non-negotiable for me. Types in C#, F# and TS are all Turing Complete [2], and therefor these languages are tooling-adverse in the sense that static analysis is fundamentally unreliable. [1]: https://news.ycombinator.com/item?id=33329509#33332183 https://news.ycombinator.com/item?id=33329509#33332183 [2]: https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html

lmm 4y ago
> As I mentioned in another comment [1] on this thread, soundness and decidability are non-negotiable for me. Types in C#, F# and TS are all Turing Complete [2], and therefor these languages are tooling-adverse in the sense that static analysis is fundamentally unreliable. How on earth do you consider Kotlin acceptable then? Kotlin's type system has never been shown to be sound or decidable and is visibly a lot more ad-hoc than any of that list (and if by some miracle it was sound or decidable last week, I'm sure whatever new feature they added this week broke it). I suspect the only reason it hasn't been formally proven to be Turing Complete is that Kotlin's developers haven't bothered to write a specification for it - as far as I can see your link's example for C# would translate directly into Kotlin with the same properties.
- bmc7505 4y ago
  Try it! I certainly have. You may find encoding a typelevel TM or λ-calculus more difficult than it appears... > link's example for C# would translate directly into Kotlin T() is not possible for a generic T in Kotlin.
  - lmm 4y ago
    > Try it! I certainly have. You may find encoding a typelevel TM or λ-calculus more difficult than it appears... These languages were stable, well-specified, and heavily studied for years before these cases were found. One person noodling around for a few weeks failing to find an example is not evidence of anything; a language being too obscure to have seen much academic study is not an indicator that it's likely to have a good type system, if anything it's the opposite. > T() is not possible for a generic T in Kotlin. T isn't generic in that code, it's just a class.
    - bmc7505 4y ago
      > One person noodling around for a few weeks Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. > a language being too obscure to have seen much academic study Doesn't seem too obscure to me. https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotlin+acm https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotl... > T isn't generic in that code, it's just a class. I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. It's tricky to get Kotlin to do much compile time computation. Not saying that it's impossible, but LMK when you've actually tried it. Here's some sample code if you want to try encoding a Boolean logic: https://github.com/breandan/galoisenne/blob/2e465e7a753f634100c40de6f5daa7356ca07b1b/src/commonMain/kotlin/ai/hypergraph/kaliningraph/automata/ECA.kt#L104 https://github.com/breandan/galoisenne/blob/2e465e7a753f6341...
      - lmm 4y ago
        > Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. Well, your own link proves it, doesn't it? Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. > I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. That's the whole point - the type system has to decide which overload to dispatch it to at compile time, which it can only do by performing an arbitrarily complex computation. I ported that code directly to Kotlin and it doesn't compile but it "should", which, well, I don't know what you were expecting or what you'd accept as proof when we've already got an academic paper that proves the point.
        bmc7505 4y ago
        > Well, your own link proves it, doesn't it? That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's about as far as I've been able to get. If it's possible to implement general recursion, I'm not quite sure how - yet. > Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..." > I ported that code directly to Kotlin Can you share your translation of Eric's code? Maybe we can get it to work. [1]: https://fool2013.cs.brown.edu/tate.pdf https://fool2013.cs.brown.edu/tate.pdf
wiseowise 4y ago
Literally majority of languages are either unsound, undecidable or both in the link that you've provided. The only exceptions are Haskell, Idris, ML and Go (given the date of the post, this was pre generics which would probably exclude it also).
- bmc7505 4y ago
  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.
      - 4y ago

lmm 4y ago

> As I mentioned in another comment [1] on this thread, soundness and decidability are non-negotiable for me. Types in C#, F# and TS are all Turing Complete [2], and therefor these languages are tooling-adverse in the sense that static analysis is fundamentally unreliable. How on earth do you consider Kotlin acceptable then? Kotlin's type system has never been shown to be sound or decidable and is visibly a lot more ad-hoc than any of that list (and if by some miracle it was sound or decidable last week, I'm sure whatever new feature they added this week broke it). I suspect the only reason it hasn't been formally proven to be Turing Complete is that Kotlin's developers haven't bothered to write a specification for it - as far as I can see your link's example for C# would translate directly into Kotlin with the same properties.

bmc7505 4y ago
Try it! I certainly have. You may find encoding a typelevel TM or λ-calculus more difficult than it appears... > link's example for C# would translate directly into Kotlin T() is not possible for a generic T in Kotlin.
- lmm 4y ago
  > Try it! I certainly have. You may find encoding a typelevel TM or λ-calculus more difficult than it appears... These languages were stable, well-specified, and heavily studied for years before these cases were found. One person noodling around for a few weeks failing to find an example is not evidence of anything; a language being too obscure to have seen much academic study is not an indicator that it's likely to have a good type system, if anything it's the opposite. > T() is not possible for a generic T in Kotlin. T isn't generic in that code, it's just a class.
  - bmc7505 4y ago
    > One person noodling around for a few weeks Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. > a language being too obscure to have seen much academic study Doesn't seem too obscure to me. https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotlin+acm https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotl... > T isn't generic in that code, it's just a class. I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. It's tricky to get Kotlin to do much compile time computation. Not saying that it's impossible, but LMK when you've actually tried it. Here's some sample code if you want to try encoding a Boolean logic: https://github.com/breandan/galoisenne/blob/2e465e7a753f634100c40de6f5daa7356ca07b1b/src/commonMain/kotlin/ai/hypergraph/kaliningraph/automata/ECA.kt#L104 https://github.com/breandan/galoisenne/blob/2e465e7a753f6341...
    - lmm 4y ago
      > Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck. Well, your own link proves it, doesn't it? Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. > I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. That's the whole point - the type system has to decide which overload to dispatch it to at compile time, which it can only do by performing an arbitrarily complex computation. I ported that code directly to Kotlin and it doesn't compile but it "should", which, well, I don't know what you were expecting or what you'd accept as proof when we've already got an academic paper that proves the point.
      - bmc7505 4y ago
        > Well, your own link proves it, doesn't it? That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's about as far as I've been able to get. If it's possible to implement general recursion, I'm not quite sure how - yet. > Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable. They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..." > I ported that code directly to Kotlin Can you share your translation of Eric's code? Maybe we can get it to work. [1]: https://fool2013.cs.brown.edu/tate.pdf https://fool2013.cs.brown.edu/tate.pdf

wiseowise 4y ago

Literally majority of languages are either unsound, undecidable or both in the link that you've provided. The only exceptions are Haskell, Idris, ML and Go (given the date of the post, this was pre generics which would probably exclude it also).

bmc7505 4y ago
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.
    - 4y ago