[evmar]

Thanks for highlighting this bit, I also find it very interesting to think about!

Here's a related property I've also discovered of 'advanced' type systems.

In my understanding of how unification happens in systems like H-M, you first give every expression its own type variable, then perform a search to produce assignments to those that remain valid and leave the remainders generic.

But as your type system gets fancier, and particularly in the presence of union types and subtyping, this search process can feel like "make whatever type judgements are necessary to make this program still compile". E.g. in code like

    let x = new Set();
    x.add('hello');
    x.add(3);  // oops, meant to add the string '3'
    f(x);

The inferencer can just reason "oh apparently x is Set<number|string>", and "oh apparently f() operates over all kinds of sets, Set<{}>". And especially when there's never a more specific type for things to "bottom out" on (like say f just forwards the set elements to JSON.stringify(), which accepts both string and number already), nothing will ever reveal to you that you actually wrote a bug.

But then meanwhile even in Haskell you run into cases where the inferencer wasn't generic enough, like https://wiki.haskell.org/Monomorphism_restriction , so it's not even clear cut that you want the inferencer to be smarter or dumber. As my coworker says: as a programmer you have to be able to basically run the inferencer in your head, and that becomes very hard when the inferencer gets very smart. (See the RxJS bug in the above blog post.)

[whatshisface]

That problem has a simple solution: you, the programmer, should write type signatures in appropriate places as a combination of what documentation and assert statements do in other languages. No compiler today could be reasonably expected to guess which inferences the human brain will find surprising, which is why it's up to the programmer.

[evmar]

This is the point under discussion though -- humans think they're reasoning the same way as the inferencer but can't get it right in the limit, so they're not really equipped to know where they ought to have added type annotations. See e.g. the comment here about the inferencer working 'backwards': https://github.com/ReactiveX/rxjs/issues/4959#issuecomment-5... .

[lonelappde]

You add the types on every function definition, and almost never have a problem.

Many people forget that the point of type inference is to eliminate uselessly redundant clutter, not to completely eliminate types from source code. A function is usually called many times, so keeping types on public API definitions and eliminating types from call sites and throwaway REPL code eliminates a huge amount of wasted typing (hah!) with near no loss of clarity.

[WorldMaker]

In the case of an RxJS pipeline, as one example, you often have a huge variety of lambda functions that may indeed be called many times, but often exist themselves as "one off" pieces in a pipeline. Leaving the types to be inferred and/or generic, is sometimes even necessary for the most code-reuse of functions between pipelines. It's also rare for such functions to feel like they are a part of a public API definition, because they feel so huge a part of internal and boring plumbing.

As someone that has done a lot of RxJS (and kindred libraries) programming over the last few years, I have a lot of sympathy for anyone hurt by type inference changes in the middle of those pipelines. Some of my ugliest rats nests of explicit any types and/or worse have been buried in RxJS pipelines next to // TODO and // HACK marker warnings to future spelunkers (myself included) about how much I was fighting the inferencing engine and losing in that particular combo of Typescript version and available typings. It's usually great when I can fix those later, and so far Typescript continues to move in that direction where those rats nests only get cleaner when I get a chance to revisit them. (But again, I sympathize with that existential fear that Typescript inferencing magic can sometimes take an unexpected step back until you understand why the change was made and how it benefits you elsewhere and/or once you figure out the root cause.)

[jbverschoor]

> appropriate places This

[mumblemumble]

This seems like a good task for a linter and some commit hooks.

During development, I like to keep my types unspecified until I'm confident that things have congealed properly. But before merging, I like to make sure and add type annotations to anything that's meant for public consumption.

Partially for readability and documentation. Partially because adding those annotations ensures that the type checker and I are on the same page. But mostly because those manual type annotations represent a promise that I, the programmer, have made about the current and future behavior of a certain chunk of code. Once those promises have been codified, then the type checker has my back and can help warn me if I'm about to break one of them with a careless change at some point in the future.