From zero to 10M lines of Kotlin

Re:From zero to 10M lines of Kotlin by bmc7505 on Tuesday October 25, 2022 @11:48AM (#33332183)

Types in TS are Turing Complete [1], so any static analysis you build ontop of that language is bound to be unsound or undecidable. You could argue this rarely occurs in practice, but I would prefer a type system that is incomplete but sound and decidable. Incidentally, this issue also affects Java, which is both unsound [2] and undecidable [3]. Kotlin does have a fairly complicated subtyping relation [4], which has caused similar issues in languages like Scala [5], however whether the same issue affects languages based on mixed use-site and declaration-site variance like Kotlin is still an open question that requires further investigation.

[1]: https://github.com/microsoft/TypeScript/issues/14833

[2]: https://io.livecode.ch/learn/namin/unsound

[3]: https://arxiv.org/abs/1605.05274

[4]: https://kotlinlang.org/spec/type-system.html#subtyping

[5]: https://arxiv.org/abs/1908.05294

[ Parent | on HN ]

Re:From zero to 10M lines of Kotlin by bottlepalm on Tuesday October 25, 2022 @10:35PM (#33339093)

So your reason to avoid TypeScript is some very rarely encountered corner case? Talk about perfect being the enemy of the good.

No language is perfect. Your comment is absurd, and the citations are pedantic.

[ Parent | on HN ]

Re:From zero to 10M lines of Kotlin by seanmcdirmid on Tuesday October 25, 2022 @10:39PM (#33339119)

TypeScript works well because they don’t worry about soundness and completeness. The type system isn’t trying to be perfect, just useful. This scares PL theorists, but I think it has been a very profitable corner of the design space to explore.

[ Parent | on HN ]