Exactly. When I initially started using typed Python, I would write code as though I were using a statically-typed language. In order to appease mypy, I found myself increasingly needing to either rewrite my code in awkward ways or add explicit ignore comments.

What happened is I started losing out on the advantages that Python provides as a dynamically-typed language without truly gaining those of statically-typed ones. Then I realized, type hints are just that: hints. They're a form of documentation. In some cases, they're very helpful, but in other cases, it doesn't really make sense to use them. I don't need to appease mypy. The type hints are their for the benefit of myself and other developers.

There is definitely truth to this statement. However often when I write something that’s hard to type, it’s a code smell. Ex. A complex nested map should probably be represented by a few concrete classes/abstractions.

(Similar to when you something you wrote is hard to test, it’s probably just poorly abstracted code.)

I agree and I think a good thing about the type hints is they help uncover these kinds of code smells. But there are definitely cases where it's definitely not worth the effort to fight mypy.

One example is that variable re-assignment can cause type errors in mypy but re-assigning a variable to a value of a different type is an extremely common and reasonable thing to do in Python. Another situation where strict typing can be borderline hopeless is when parsing e.g. very dynamic content like json. Sure you could encode every possible situation using types but this would basically defeat the purpose of using Python for such a task.

> rewrite my code in awkward ways or add explicit ignore comments.

Probably just used to writing poor quality (immediately unintelligible to someone other than the author but functional) code then.

Using typing in Python is a code smell. Lack of understanding of what the language is for and how to use it.

> Python type annotations are more useful for a human as a form of documentation, than they ever will be to a machine

I mean, machines serve people (for now!). So in addition to type documentation, type annotations are useful for things like "jump to definition" and "find references" and automatic refactoring. Moreover, the utility of annotations for type documentation depends on the correctness of those type annotations--if you don't have something like Mypy, then those inevitably annotations grow outdated over time and incorrect type annotations are even worse than none at all.

> tools like pytype or mypy will never capture all the complicated hacks possible in the Python type system

Technically you can represent any complicated hack if only via `any`, but that's just pedantry and we all know what you mean. Even still, it's not like "well you can't represent everything, so there's no point in trying to appease mypy" (which may not be your intended implication--I can't tell). The benefits of appeasing mypy are proportional to the amount of your code that is properly annotated--this is the thesis of gradual typing.

> as evidenced by only 15% of repos passing mypy

This very likely indicates that 85% of repos aren't running mypy regularly, or they're in some transition state. Certainly more than 15% of real-world Python can be described via Python type annotations.

I've used python typing heavily at work and was really useful to detect bugs and helped with developement.

> as evidenced by only 15% of repos passing mypy

That is no evidence. Of course, if you don't have mypy in CI (or pre-commit hooks or whatever), your repo will not pass mypy. But if you have it in CI, then you can rely on them being correct.

> tools like pytype or mypy will never capture all the complicated hacks possible

But they can either enforce everything being correctly typed (if you go to really strict settings), or yes, you will have some code untyped, so you will be careful around that part. It's not like all or nothing.

Python does ignore them at runtime, but as long as you're validating your inputs (e.g. using Pydantic for HTTP request validation) then you can trust that the static types are truthful

I want to emphasize for folks reading: if you want actual type enforcement and you want that type enforcement with minimum boilerplate, Pydantic is a fantastic option (I'm sure there are others as well). It's a great library that's totally use-agnostic (it's not HTTP specific, you can use it for whatever) and quite tight. Caveats are that it uses runtime validation to enforce types so there's a performance cost, but it's a performance hit that is mostly eclipsed by all the other huge performance hits that litter your typical Python implementation.

Pydantic is amazing!

IIRC, pydantic was quite big and I chose typeguard instead for a smaller project. Might be an option.

> trust that the static types are truthful

That's often a mistake even in typed languages like typescript. Satisfying a static type analyzer isn't enough. Real data is whatever it is going to be. If your types are meaningless at runtime, you can easily encounter type mismatches.

Static typing as implemented in typescript and python type hints is a tool for engineers instead of a tool for systems.

The types are usually ignored, but not entirely erased- Pydantic uses type hints to do validation at runtime, so if you construct a Pydantic object with invalid data it will throw an error, so eg

    foo=PydanticFoo(**request.json())

Will try and validate a json request against the implied schema provided by the type hints on PydanticFoo while constructing it and will throw if it fails.

You missed my point. If you validate input, then the static types are representative of runtime types

Ack, so I did :P

This is only because the Python type hinting ecosystem is so bad. Tons of projects don't have type hints, there are multiple conflicting interpretations of the types, MyPy is very buggy (Pyright is much much better but few people use it).

Compare it to Typescript which is a similar sort of tacked on type hinting system - Typescript is basically always machine checked.

Type annotations are used at runtime in some cases, most notably when defining dataclasses.

I find this a bit of a wart on the dataclass implementation. Type hints (to me) are more like a comment than a statement. So, from my perspective, dataclasses feel like they're pulling data out of nearby comments. Ick.

But it's a wart worth the conciseness, at least, until a better idea comes along.

Maybe if type hints could be optionally enforced as a language feature, I'd feel it was more integrated.

Most static typed compiled languages also ignore types at runtime :)

Not true. Java, C#, Scala, Kotlin, Swift, Dart, and others all keep around type information at runtime so that casts can throw exceptions at runtime when the value isn't of the right type. Otherwise, soundness is lost.

In practice, most modern statically typed languages maintain soundness through a combination of compile time and runtime checking.

> most modern statically typed languages maintain soundness through a combination of compile time and runtime checking.

Rust, C, C++ - all do not keep around this information.

You're right that the JVM languages (and thus, naturally, C#) do it differently. I think it is a bit silly to name out each of the JVM languages separately.

Haskell, Go, and I think OCaml also rely on some amount of runtime checking for soundness.

I think basically every managed statically typed language ends up carrying around runtime representation and uses some amount of runtime checks.

Haskell has full type erasure.

It still has to carry around enough information to detect non-exhaustive matches and throw at runtime, no?

Only in the same way that "if ... else if ... else" needs to know about types, which is to say mostly not.

AFAIK - and this might be either dated or just wrong - the two places GHC doesn't fully erase are 1) polymorphic recursion (where if we squint it's probably not unreasonable to treat the dictionaries as type tags), and 2) when the programmer explicitly asks for run-time type information with Typeable.

But what are you performing the "if else" on? Type level information stored at runtime, no?

Value level information. The compiler statically knows the type that's being matched on. It's true that the generated code depends on the type, but that's not any more true than when a C compiler generates an integer comparison vs a float comparison in the conditional of that "if". All that's looked at at runtime is the data.

Yes, but those aren't types, they're values.

I am unfamiliar with Haskell and Go. What you are saying is not true for OCaml

My understanding is that you can have non-exhaustive matches which the compiler won't always catch statically and will throw a Match_failure at runtime if no case matches.

Non-exhaustive matches are always detected statically in OCaml.

However, such matches are considered valid code: "non-exhaustive match" is a warning by default, even if most people advise to turn that warning into an error.

In other words, the `Match_failure` exception is part of OCaml non-typed semantics and there is no soundness issue involved here.

But how is Match_failure detected at runtime unless type information is passed around?

There is no type information at runtime at all in OCaml. Once the program has been typed, the program is translated into an untyped lambda-calculus and all type information is throw away. In particular, pattern matching is compiled into this untyped lambda-calculus using if/then/else (and switch statement, and exception and exceptions handlers, ...). The type system is sufficient to detect before this compilation if the pattern is total or if it need to add a failure case. In this case, the `Match_failure` is just a catch-all term in this conditional expression.

For instance

  let f x = match x with
  | [] -> ()

is translated into

    (is_empty/267 =
       (function x/269 : int
         (if x/269
           (raise (makeblock 0 (global Match_failure/18!) [0: "r.ml" 1 17]))
           1)))

where you can see the exception being build and raised in the `then` branch of the test. Contrarily, the total function

  let is_empty x = match x with
  | [] -> true
  | _ :: _ -> false

becomes

  (let (is_empty/267 = (function x/269 : int (if x/269 0 1)))

And since the function doesn't need to handle the failure case, it doesn't have that `(raise ...)` case.

Another important point is that type system information is only needed to check the exhautiveness of pattern matching in presence of GADTs. Otherwise the exhautiveness of pattern matching can be checked using syntatic criteria on the pattern matching and type definitions.

Yes, sorry I meant in the context of GADTs. Is it really full type erasure if that GADT information is passed aorund?

No type information is ever passed to a compilation phase lower than the typechecker in the OCaml compiler pipeline.

In the GADTs case, the type system is only used to remove the failure branch. For instance,

    type 'a t = A: int t | B: float t
    let always_a (x:int t) = match x with
    | A -> ()
    | _ -> .

is translated to

  (let (always_a/270 = (function x/272[int] : int 0))

because the typechecker can prove that the `B` case is impossible. In other words, GADTs are yet another instance where the type system can be used to eliminate dead code in the untyped IR.

I see, so you can never really get a match_failure due to type level mismatch with GADT because it would be caught by the compiler.

Makes sense to me.

You know, that's a solid question that I don't know the answer to.

C++ community is split by the RTTI compiler flags

Rust standard library includes RTTI support, though it's very rarely used.

If you make it part of the deploy / build process and force programers to only use the subset of features supported by a type checker then you can benefit.