[psykotic]

> If you want to refactor, it's up to you to delete the types.

The fact that

    f(g(x))

and

    { let y = g(x); f(y) }

are equally robust to changes in g(x)'s type is an advantage of type inference. It doesn't seem reasonable to place an additional burden on the person who chose to assign a name to the subexpression value.

> Personally I really like the spot readability of explicit types.

You can use an IDE that displays inferred types as type inlays (for variables) and as sidebar info (for expressions). But I've often wanted a way to export such sideband data (including subexpression types and cross-reference links) so you could display it for code reviews, etc, without teaching those tools about your language specifically, so I'm sympathetic to the general goal.

Regarding explicitness and readability, I like Rust's idea of letting you partially specify types by using _ as a placeholder to say "infer this part". For example, you can specify that something is a Vec without specifying its item type:

    let v: Vec<_> = iter.collect();

[mike_hock]

Explicit types are a form of assertion. In the example

    { let y = g(x); f(y) }

I do not want to assert anything on the type of y but in

    {
        let y: Foo = g(x);
        // Do complex stuff with y
        f(y)
    }

I wrote the middle part with a specific mental model of what y is, and if that changes, I want to review that section to make sure that the semantics still match what I thought they were and does not just happen to be valid syntactically.

I do not want some automated tool to either strip assertions from my code, nor do I want it to synthesize assertions from a static analysis run of a particular version of the code. If I'm just gonna mindlessly remove all assertions and re-synthesize them on every refactor, they're useless.

[rektide]

> You can use an IDE that displays inferred types as type inlays

This isn't captured in the code & that is a huge weakness. Being able to see the code change over time is, in my view, a huge advantage.

Reliance on high-tech tools to discern meaning & do the inference for us feels far weaker than simply encoding the good information into the code. That just seems far better to me, far more robust. Some of this is that I'm a vim user and don't want to have to go lookup & configure a LSP daemon for each file I evaluate, but some of it just feels like base common sense, that the tradeoff of actually being explicit are overwhelming & clear.

I think I argued against this pretty resolutely the first time around. I don't think your post adds anything or changes my mind at all.