Global type inference is not a positive in my book. In my experience it becomes very hard to understand the types involved if they are not explicit at systems boundaries.
I can also imagine that it must be hard to maintain, like sometimes the types must accidentally change
Being hard to maintain and having no static types at all, did not stop Python rising to conqueror the world. Type inference allows us to at least give those users the succinctness they are used to, if not the semantics. Those who like explicit types can add as many annotations as they need in OCaml.
> Those who like explicit types can add as many annotations as they need in OCaml.
They cannot add it in other people's libraries.
> did not stop Python rising to conqueror the world
I wasn't talking popularity, I was talking maintainability. Python is not a stellar example of maintainability (source: maintained the Python API for a timeless debugger for 5 years).
Python's ubiquity is unfortunate, thankfully there seems to be a movement away from typeless signatures, both with Python's gradual typing (an underwhelming implementation of gradual typing, unfortunately) and Typescript.
Does it matter that much how the internals of someone else's library are implemented? The tooling will tell you the types anyway and module interfaces will have type signatures.
There’s a trade off - was the mistake here or there? The type checker cannot know. But for those few cases you can add an annotation. Then the situation is, in the worst case, as good as when types are mandatory.
> But for those few cases you can add an annotation.
not in other people's code. My main concern is that gradual typing makes understanding other people's code more difficult.
Idiomatic Haskell warns against missing signatures[1], Rust makes them mandatory. Rather than global inference, local inference stopping at function boundaries is the future, if you ask me.
> the situation is, in the worst case, as good as when types are mandatory
The worst case is actually worse than when types are mandatory, since you can get an error in the wrong place. For example, if a function has the wrong type inferred then you get an error when you use it even though the actual location of the error is at the declaration site. Type inference is good but there should be some places (ex. function declarations) where annotations are required.
I can also imagine that it must be hard to maintain, like sometimes the types must accidentally change