Well now you can write full types in both of them

You can write them, but without most of the benefits of static types

You can typecheck them with mypy or pyright or at runtime with typeguard.

It is not ideal, but pretty good in terms of benefits.

That’s great, but sometimes those tools fail to spot an error silently, where a compiler plus runtime checks usually won’t.

As an extensive user and a fan of these Python type checking tools, I do not remember this happening for some years now. Do you have a particular example where it should be improved?

Yea, at work mypy fails quite often on the old code there.

Never once happened to me in years of typescript, though I agree it’s obviously possible

Such a major failure was my first (and last) experience with TS about two years ago. Had all the "strict" options set, was quite happy finally using a "type safe JS", and boom, it exploded at runtime with some nasty bug which was discovered not before having the code run in production. Than I learned that TS' "type system" isn't sound, and you're required to write tests even for the parts that should be actually covered by the "types". That's not helpful at all. That's not what I expect from type safety.

Was this blow up due to a dependency with an 'any' type somewhere, and your code the dependency library some garbage? That's what bit me, even with the strictest ts settings, this can't be picked up by tsc.

I don't know anymore what it was concretely. That was two years ago on some project that wasn't even part of my usual duties. We lost some team members and I had to look after some extra projects. As I have quite some experience with JS I was given a TS task.

At this point I was even quite eager to update my JS skills with TS knowledge. All in all it was fun to write this project. But my error was to trust the types like I would when programming on my main project in Scala. Big error…

Since than I think TS is much oversold.

You can do fun things with the types (even some things that I miss in Scala, and there is not much to miss in Scala in general!), but you just can't trust the TS types. So this makes them superfluous in some sense. (Yes, some types are better than no types; especially when it comes to the IDE experience; but as long as any lib call (due to trivial bugs in "typing-files"), or some "impossible" input can break things this is not as helpful as one would like; especially when coming form really strongly typed languages).

Same. As long as you sanitize dynamic serialized input like json while parsing this is not a problem.

Later versions are very strict even about dynamic types, treating them as Union[] rather than Any, forcing you to check the type before using it. Likewise with strict non nullable.

I still use python type hints (and TypeScript) - and while they have benefits, I find that they fall short of something like Rust, Haskell, etc (because they are just that - hints). I don't have the surety that the types as annotated are the same as the types at runtime.

Just to make it clear. If you use typeguard @typechecked annotations snd the type hint does not match reality at runtime it will blow up with an error telling you.

The same, but at "lint time" (not runtime) will happen with mypy or pyright, although I am sure there are rough edges.

Checking types at runtime is dynamic typing. It's equal to writing something like `if (typeOf(someValue) == "someRuntimeType") {…}`.

This misses all the advantages of static types.

Typeguard checks at runtime. Mypy and pyright check at "lint time". They do static analysis of the code without running it.

this is putting the cart before the horse given that in any real-world facing application it's not the language that determines the shape of the program but the data and rest of the world that interfaces with your program.

Dynamic languages are in many ways simply a recognition of that fact, namely that data is sparse, incremental, changes and accretes and so on. There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.

> There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.

Scala developers would disagree.

Especially in business applications strong static types are extremely helpful to prevent bugs and model the domains of interest in a proper way.

I agree; I would expect to see such languages feature much more prominently there, especially in the subtle and convoluted business/legal complex.

One may argue that the proof-strength formality can be a hindrance: in such domains, inconsistencies and contradictions abound, and some of them cannot be predicted in advance. But I believe that languages like Idris can accommodate this. Maybe I am wrong, or maybe they can, but not more efficiently than more free-form languages.

...but ok, I am failing to see what I can do with COBOL that I cannot do with Idris, business-logic-wise. lol