[ali_m]

Type annotations may be part of the language spec, but the way they are enforced is not. Different type checking libraries have made different design choices (leniency vs strictness, type inference vs gradual typing etc.). Although these differences don't matter at runtime, they do mean that code which passes one particular type checker might fail with another.

[throwaway81523]

There actually seems to be no story about inductive types (e.g. trees) in Python and this appears due to well known theoretical difficulties combining subtyping (required for OO) and type inference (?). I.e. it is a hard problem. There are a few long term open mypy github issues about it, and some hacky workarounds, but no real answer. This is also why languages like Haskell (with good support for inductive types) tend to not have OO. I'm not exactly familiar with the issues, but there is some PLT literature about it, by Anton Setzer and others.

[joshuamorton]

Can you elaborate on this? Forward refs and recursive types are accepted on most places that isn't NewType, so you can make them, but not in a one liner.

[throwaway81523]

Sorry about the slow reply but I just noticed your question. Haskell supports recursive types just fine. The issue I'm mentioning is that it is hard to express those types in MyPy, which is a static typechecking add-on for Python, not Haskell.

[davnicwil]

Is the solution here just to skip type checking the code of dependencies, and just check the types at the interface with your own code using your tool of choice? Or is it more complex than that?

[neilparikh]

I think that mostly works, but it's still possible that different tools assign different semantics for the same syntax, which could then interact in a weird way if the library author wrote the interface annotations with Tool A's semantics in mind, while you ended up checking them against your code with Tool B.

I think the type systems are simple enough that this is probably a theoretical concern, and won't come up often in practice.

[jraph]

I think so. When typing checking a project, its dependencies don't get type checked as well as far as I know. Type errors in dependencies are kind of not relevant for you, and many dependencies are not type-annotated anyway.

[ali_m]

Well you probably do still want the type checker to at least look at the public interfaces of any libraries you depend on, since you want it to enforce that you're calling into them correctly.

[jraph]

Absolutely. It should probably not report errors that are not in your code, by default anyway, but still extract information about typing relevant to you as much as it can.