Type inference occasionally bites one's hand when pushing data across an FFI boundary. In one instance I was writing some graphics code for a project and for some reason the colors in the rendering model were coming out all wrong on the screen (TL;DR it ended up looking like two of the color channels were missing from some texture maps) and it turns out that Rust inferred the type of the buffer as a vector of f64s instead of a vector of f32s. Putting the type in specifically fixed the problem promptly.

Lesson learned: Sometimes type inference fails, and always annotate your types at FFI boundaries!

Yeah, it's important to annotate anything that interacts with the outside world, because that code/API isn't available for the compiler to reason about before run-time. Same goes with HTTP endpoints (on both the client and the server)

So I think "easy to mentally model" gets harder and harder to achieve as the type system becomes more powerful. If your conclusion is that we keep the type system limited in power, that's valid! but not what I'm exploring.

Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement.

With my proposed system, all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor. The "algorithm" becomes extremely simple, with almost no intermediate steps.

Of course, proof will be in the pudding, if I can actually achieve a pleasant editing experience :)

> all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor

So there are two possible reasons I can see for automatically "annotating" all the types:

- Caching that info to easily show in the editor (which is a good feature, but many editors already do this without having to modify the source; it happens entirely editor-side)

- Using the "current" inferred type as a jumping-off point for determining the "next" inferred type

The second was my original interpretation, and what sounded so distressing as a user

Consider this situation:

1. Your program and the inferred types are in one state

2. You modify some code which changes an inferred type

3. You change the (visible) code back to what it was previously, but now the inferred type is different because it was partially based on the previous inferred type

This is what sounds like a nightmare, assuming I understand correctly that it's possible on the described system. The inferred types are now a state machine, where it matters not just what code is on screen, but how it got there.

Hm so it is a state machine, but (my hope is that) all state transitions are simple and direct (and observable!) outcomes of user action. If the transitions get at all complex or unobservable, I'll probably call it a failed experiment.

It might also end up being the case that users keep types "visible" at all times, only turning them off in certain situations. I can also imagine a flag to "only hide inferred types that are primitives" or something similar.

Fair enough, and it's certainly an interesting experiment, don't want to discourage experimentation

But I will say I think the desire to show the inferred types is orthogonal to the desire to persist them on disk, in the source-of-truth code files. If the state machine really is what you want to experiment with then have fun, but if your desire is just to give the user more visibility into inference, I think there are simpler ways to go about that

> Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement.

How much state gets hidden is 100% on the quality of the implementation, isn’t it? There’s nothing that forbids an implementation from dumping that hidden state in whatever form it wants to (as an example, compare C++ diagnostics of different compilers or different versions of a compiler)

> The "algorithm" becomes extremely simple, with almost no intermediate steps.

I don’t see how it can become simple merely be the way things are presented. If you write f(foo,qbar,baz,quux) in a language where overload resolution is complex and the compiler has 20 overloads to pick from, but can’t find a ‘best’ one, it still has to show you what overloads it considered, how it ranked them and why, and which ones were left.

So, if you want type errors to be extremely simple, I think you need a simple language (type-wise)

Although I personally think type inference is the killer feature that makes static typing accessible (almost always auto), I've seen hostility to it, in particular among C++ and C# programmers. The point of this project, as you say, is to be as explicit as possible in the code, while at the same time presenting a view of the code that is less cluttered.

My initial impression is that if I were to use a system like this, I would want any type annotation that differs from the default inference to be visible. The only choice left, then, is when to display redundant annotations, which is where a lot of the disagreement around type inference is, even without this scheme.