This is not good. One of the author's arguments is that type inference in an IDE is bad because sometimes I read code in a book where I don't have type inference...

I don't know about other folks, but the vast majority of code I read is in my editor, where the type inference saves me a ton of time and pain.

> Type inference is bad. It makes code harder to read, and languages that use it too much are harder to write.

If inference is bad, maybe the second sentence shouldn't leave it up to the reader to infer what "it" means. Surely it would be much easier to read as "Type inference [...] type inference [...] type inference".

Bad:

- Omitting return types in non-private interfaces (eg crossing module or package boundaries, or anything used as input to generate documentation of same)

- Omitting concrete input parameter types

- Omitting explicit, known constraints on generic/polymorphic parameters

Subjective:

- Omitting any of the same on private equivalents which form something like an internal interface

- Omitting annotations of constant/static aspects of an interface whose inferred types are identical to their hypothetical annotation

Subjective but mostly good:

- Relying on inference in type derivation, where type derivation is the explicit goal of that API

- Preferring inference of interface/protocol/contract types over explicit annotation of concrete types which happen to satisfy them

- Omitting annotations for local bindings without distant indirection

Unambiguously good:

- Omitting local annotations of direct assignment where the type is obvious in situ

- Omitting redundant annotations of the same type which have the same effect without that redundancy

Sometimes you'll read something and think "I'm not taking the bait".

Hard disagree. One of the reasons I fell in love with F# was the succint code one can write, specifically due to the compilers ability to infer types.

"My favorite languages feature types very prominently, therefore any software engineering approach that doesn't do so is invalid, and here are some reasons I thought of".

He posts this on HN, which happens to be built in Arc Scheme, a Lisp dialect (which is dynamically typed). I wonder if the author has written software that has better uptime and more popularity than HN? Is the author's codebase truly easier to understand?

Explicit typing is great until your code is littered with shared_ptr<vector<shared_ptr<map<string,T>>>> everywhere.

> In Rust and Haskell you have to at least annotate the parameter types and return type of functions.

In Rust you do, but in Haskell you don't.

For me it makes sense to distinguish between type inference at the call site or the definition site. As a caller of a function, I don't want to have to spell out type parameters for that function if they can be inferred (but forcing inference is also not great because it's helpful to have type parameters that have nothing to do with the inputs and merely depend on the outputs).

At the definition site, I agree with the author that type inference is more of a burden for the most part, at least if the function is more than a hidden implementation detail of the class/module/file.

I think the article's take on type inference is a bit heavy-handed and misses some of the nuances of modern software development.

First off, the complaint about reduced readability outside of IDEs feels like a niche problem. Sure, it's a valid point when you're reading code on paper or in a basic text editor, but let's be real: most of us live in IDEs with excellent type hinting capabilities. The argument kind of falls apart when you consider that good variable naming can often make the need for explicit types less critical. Plus, isn't the goal of any good codebase to be as self-documenting as possible?

Regarding OCaml's type inference being a "footgun," it seems like a bit of an exaggeration. Yes, OCaml's system is powerful and can lead to some head-scratching moments, but isn't that just part of the learning curve with any powerful tool? It sounds like the frustration comes more from not leveraging the type system correctly rather than an inherent flaw with type inference. And honestly, adding type annotations for debugging is a pretty standard practice across many languages—not just OCaml.

The point about academic effort being wasted on type inference research also misses the mark. This research pushes the boundaries of what's possible with programming languages, leading to more expressive and safer languages. To frame this as a waste is to ignore the broader benefits of advancing programming language theory. Sure, it'd be nice if papers spent more time on practical applications, but that doesn't mean the theoretical aspects aren't valuable.

It feels like the article is conflating personal gripes with systemic issues. Type inference, when used correctly, can significantly reduce boilerplate and make code more concise and readable. Of course, it's not a silver bullet, and there are situations where explicit type annotations are beneficial for clarity, especially in public APIs. But to dismiss type inference outright seems like throwing the baby out with the bathwater.

In the end, it all boils down to using the right tool for the job and understanding the trade-offs. There's no one-size-fits-all answer in programming, and dismissing type inference entirely overlooks its benefits in many scenarios.

Bullocks. I wrote thousands if not hundred thousandths lines of untyped Python code in over 15 years, for critical systems and thousands of users. It works for me. I'm not confused about the code, I can code and debug quicker than many of my typed-language colleagues and even now that python supports type hints I often only use them in bigger projects or in places where they're actually convenient. It's simply the way of working that a developer is used to.

Type inference has usability problems (2019): https://austinhenley.com/blog/typeinference.html

  ((((3::Int)+(9::Int)::Int)+(15::Int)::Int)+(18::Int)::Int)+(5::Int)::Int

I think this article makes some really valid points. Many languages try to address the spooky action at a distance type errors by requiring explicit annotation of types at certain boundary type conditions like function argument and return arguments -- which can help but can still also being annoying when the type system knows the types you want to write but you still have to figure them out and type them in yourself. A lot of times it's less cognitive load to verify that a type declaration is what you expect than it is to write it yourself (something we often do with tools like rust-analyzer or highlighting over variables in ide to see the type).

Personally I'd like to see languages embrace "format on save" as an explicit part of language ui to improve ergonomics here. Firstly, a first class auto formatting tool is just great and spamming cmd-s as you write code until it auto formats nicely is a really quick way to observe and address syntax issues -- to me that part of the experience is already important enough to explicitly incorporate making that developer experience work well a goal of language design.

But secondly -- if you do embrace auto format on save at language design level, there's a lot more you can do than just auto format the code! You also gain a really nice channel for communicating information about "program change" to the developer. Say you allow in the language to differentiate between inferred and not inferred types -- and then at auto format time, the inferred types are explicitly added to the code (in some heuristically useful set of places-- or even just everywhere that a non type inferenced language would require explicit types).

In that world, as you make changes to the code, your git diff state is going to start giving you a lot of potentially useful feedback about what actually happens in your program when you make certain changes. Additionally because the inferred types are automatically added -- you can easily have a mode to hide them when you want a less noisy view. Mayb the convention would become that committeed code is always serialized to a form that conveys more of the statically knowable program information by default -- which your ide can hide to give you a more streamlined view -- rather than the other way around). And then the parts of your code you know are boundaries or apis or not expected to change types, you just update the annotation to indicate that the type is not supposed to be reinferred and a type error will be issued if it doesn't match instead of being updated. Now you've got a nice way of constraining program evolution in desired directions to help tame complexity or at least force explicit acknowledgement as certain assumptions about the program structure become invalid over time ...

I think a neat ide feature would be to auto hide all the types and only show them as a pop up tooltip or something similar.

This way you can read the code more easily and if you want to see the type it's there for you.

100% agreed. I want to see the types, and not just when hovering.

Now, if the IDE autocompletes the type declaration for me somehow, that's great! That's a win-win: I save time but still maintain readability.

> languages that use it too much are harder to write. It’s a false economy whereby you save unobservable milliseconds of typing today and make everything else worse.

I enjoyed this reference to a false dichotomy while making one itself. Languages don't make programmers leave out annotations where it aids readability.

One of my dream ideas is to write a codemod that either adds all the implicit type inferencing explicitly, or removes it.

It's great that we don't have to type every type definition. But when reading code, it sure is much easier seeing exactly what every type is explicitly. You can look object by object in most ides by hovering over each item, but it doesn't have the at-a-glace see-it-all viewability; hence the idea, just rewrite the code with or without the explicit types, as desired.

There's still a lot of type narrowing and other things that happen that aren't super visible, that alter the known typing state as we go. I have less of an idea of what to do with that.

The claim about inferences rules in academic papers is false. Gentzen’s inference rules are usually used to specify how to type check and not type inference even though inference rules and type inference overlap in the use of the word inference.

Definitely disagree. The language where this really shines is Swift, where type inference is used really heavily.

It's really great for stuff like passing enums as function arguments. You can write `context.setColor(.red)` instead of `context.setColor(Color.red)`, the latter of which I find just unnecessarily repetitive.

The coolest part about this is when you're using a new unfamiliar API, you can let your IDE's auto complete suggest options for you just by typing '.' and pick from the list of options shown inline.

I get their argument on reading code in less than an IDE environment (ie. book), but in general, I think _limited_ type inference is good (on classes/structs and functions). Not having local variable types is a net positive in general, but I agree with the author that full type inference (on functions) removes too much documentation. In OCaml one should therefore use interface files always IMO.

Type inference is a good thing. If you abuse it, the same way you abuse lambdas or any other feature, it can get bad.

The fact is that in many languages, type checking and type inference are coupled together (for languages with DT, bidirectional type checking is needed). When writing proofs, it is almost impossible to let user specify every type.

Ok, let’s go back to normal imperative programming. What about alias analysis? What to do with devirtualization? You NEED type inference. That is being said, I am not a fan of the “usual” ocaml’s style where ppl seem to write as less type annotations as they can. That is not user friendly.

“I don’t want to infer types from my code. I’d rather infer the code from the types.”

Ditto.

The world where data and it’s type is the SSOT means you can trivially validate every bit of code that touches it.

Hmm I code a lot in vim without any plugins (I just have syntax highlighting). It has never really been a problem for me (say in C++, Rust or Kotlin): I guess I'm training my memory a bit more?

I'll admit, once in a while I write something like `let a: Int = <the_var_which_type_I_dont_know>` and compile, such that the compiler says something like "expected an Int, got a HashMap<String, Int>". But pretty rarely.

So yeah, I kind of like type inference.

In C# I've been preferring to only use var when the type appears in the expression so that it can be inferred by humans if you printed it out. In rust I've been using type inference per the usual rust coding conventions. I haven't quite sorted out in my head which way I really think is better.

OCaml's type system allows for expressing complex data structures and behaviors in a concise and readable manner. These types can significantly improve code clarity by providing explicit declarations of intent and structure. Here are some examples:

  type 'a binary_tree =
    | Leaf
    | Node of 'a binary_tree * 'a * 'a binary_tree

  type http_response = [
    | `Ok of string
    | `Error of int
    | `Redirect of string
  ]

  module type QUEUE = sig
    type 'a t
    exception Empty
    val empty: unit -> 'a t
    val enqueue: 'a -> 'a t -> 'a t
    val dequeue: 'a t -> 'a option * 'a t
  end

  type _ expr =
    | Int : int -> int expr
    | Bool : bool -> bool expr
    | If : bool expr * 'a expr * 'a expr -> 'a expr

  type person = {
    name: string;
    age: int;
    address: string; 
  }

I inherited thousands of untyped Python code for critical systems, and it was an unmaintainable hot mess that caused a constant stream of pain. No kidding that was one of the main reasons we had to build a second version of the system.

I love Python, but I use it carefully in large scale production settings. Python with a Typescript-like static type system would hit the sweet spot for me (and yes, I've used mypy, but it doesn't hit the same spot).

Man I wish I could somehow convince developers to learn the difference between "dynamically typed", "statically typed", and "gradually typed" languages. An "untyped" language nearly doesn't make any sense semantically: when you have more than one type of value, you have types.

In Python's case, there are probably thousands of types in the standard library alone.

Congratulations, you've achieved perpetual job security as no new developer can actually work on that codebase as well as you do.

Also you're confusing dynamic typing and type inference.

The fact that people can get used to something and be productive with it doesn't mean that its not objectively worse than the alternative.

Do you have any sources or links where you or others expand on these ideas? I daydream about something like this every so often.

In my experience IDEs and language servers for a language like F# have a convenient "Add explicit type annotation" that will do just as you're suggesting.