[eru]

What do you mean by types being dealt with at the IDE level?

Depending on your type system, a well-typed program can eg run faster, because the compiler / interpreter can elide certain runtime safety checks that would be necessary in untyped code.

If your type system is crazy enough, you can even track the runtime complexity of your program at the type level, including whether your program runs in finite time. See eg Dhall (https://dhall-lang.org/) whose type systems only allows programs running in finite time.

[gmueckl]

I think what GP means is that the IDE for a theoretical programming language could automatically infer types and have you not type any code for that explicitly. It might even not show you types as code at all and by default and overlay/add this info only on request.

Generally, there is this huge disconnect between how code is expressed as text and how it is handled in as a graph structure inside the tooling. It is soon time to move beyond simple text files for code, I believe.

[eru]

ML family languages (like Haskell) had proper type inference for decades now. And yes, integrating that with your editor/IDE is a good idea.

Depending on what you want to do, you might also want to start with the types and have the computer figure out the implementation.

> It might even not show you types as code at all and by default and overlay/add this info only on request.

Types annotations are often are great documentation, and there's a lot of practical knowledge in the ML communities about what types annotations to show in the source for helping with understand and debugging and which ones to leave out as clutter.

I wrote 'proper type inference' above, because it's much more powerful than the watered down version Go and C++ give you. See eg https://news.ycombinator.com/item?id=8447280 for a Rust example.