3 ms·
>> Python doesn't have any sound type system Neither do popular statically typed languages like Scala, Java, C#, … - sound in the context of PL theory means th
by CraigJPerry 5y ago
>> Python doesn't have any sound type system
Neither do popular statically typed languages like Scala, Java, C#, … - sound in the context of PL theory means the type checker will only accept a correctly typed program. Which is not true for any of these languages i mentioned - you can get the compiler to accept an incorrectly typed program.
>> you can't have (currently) proper static typing in Python
That’s an even bigger group of languages in that bucket, typing is undecidable in “favourite” languages like Rust, ocaml, c++, f#
- still_grokking 5y agoScala's base caluculus is proven sound! The implemented language as such has minor soundness holes, correct. But you need to resort to "murky" parts (like combinations of null, top and bottom types and sub-type relationships between them) to exploit this. In practice I've never run into any case of this soundness holes. You need to explicitly construct a pathological case. (Just avoid null and you should be safe in any case afik). This can't be said about things like MyPy or TS. There you run into soundness holes on a daily basis. OCaml and F# are undecidable? Also because of sub-typing? And what's the problem with Rust? It doesn't have sub-typing. The problems with sub-typing in general could go away in the future when algebraic sub-typing catches on.