So this language would not be general purpose, as it would not be suitable for high-performance computing.
Large scale simulations almost always involve arrays that are modified in place. Being able to somehow declare a collection to be immutable would be highly useful, but not having the option of mutable collections limits the kinds of problems that can be approached with the language.
Another example is completely pure array programming such as in Accelerate[0] or Futhark[1].
So there are "effects" (non-functional state changes) that are encapsulated ("benign").
I learned this term in reference to Standard ML at CMU.
This is different from what you're asking because it isn't a compiler optimization and it isn't actually checked by the language at all, but it works pretty well in practice.
It's like unsafe in Rust: you write most of your code assuming a useful property that you then break in the small percentage of code that needs to break it.
The caveat is that, in my experience, it's a fair bit harder to reason about performance, as the execution model is even more abstracted away from the hardware than even something like the C model is (which is no longer a good fit either, in this era of speculative execution and multi-level caches.)
One solution is to have a tool developed and distributed along with the compiler (so it can never fall out of sync with the compiler, that's why) annotate the code with notes about performance.
For example, a tail-recursive function needs to have it’s type as tail-recursive.
Tail recursion is not necessary to annotate imo, but I guess the compiler/linter could maybe complain if it finds recursion it can't do a tail call optimisation for. These kinds of warnings are similar to mutable languages warning about things that are probably bad but sometimes necessary.
The reason it must be made explicit is because when somebody else comes later on to change that function they may miss the fact that it doesn’t explode only because it’s tail-recursive.
You could of course document the requirement - but why document if you can make it a compiler option? “I don’t want this to compile unless I get the behaviour I expect from it”.
Also as far as I am aware C-style functions can not be tail-recursive because they can not clean up the stack after themselves, thus you can’t support tail-recursion across FFI.
This somewhat resembles immer.js (uses a proxy around an immutable structure which records updates). Contrast this approach to Clojure transients (whose children don't magically become transient), and whatever Haskell does (https://news.ycombinator.com/item?id=24740384).
[1]: https://docs.rs/im/
The borrow checker is about validating that references don't outlive their target, and R^W.
This sounds nice, but is there a way to accomplish it without losing some expressibility or concision? Rather than looking at JS, consider low-level operations on a small chunk of memory as a niche example. Interpreting the same region as a buffer of 64-bit ints vs 16-bit uints gives entirely different behavior to the standard operators like addition, multiplication, and shifts, and there are plenty of cases where it makes sense to mix and match those operators. It's possible to construct a single type that encompasses all that behavior, but the price for doing so is a formidable wall of similar-looking method names rather than just being able to use a plus sign or other easier-to-understand constructs.
The variable doesn't change its type though, instead you change your interpretation of it. That's a very different and explicit operation & manipulation.
Although example 1 doesn't strictly have anything to do with types, you could get the same behaviour with `x = 0` in any language with closures (like javascript), or `foo = 0` in a language which passes parameters by (mutable) references as long as that information is not visible in the caller.
1. Variables should not be allowed to change their type.
2. Objects containing the same values should be equal by default.
3. Comparing objects of different types is a compile-time error.
4. Objects must always be initialized to a valid state. Not doing so is a compile-time error.
5. Once created, objects and collections must be immutable.
6. No nulls allowed.
7. Missing data or errors must be made explicit in the function signature.
The idea being that each feature or constraint _enables_ you to reason and predict more about a program than you could otherwise.
I encourage anyone interested in these ideas to play around with F# or a similar language and get a feeling for how they influence your code. If you've mastered one paradigm such as OO one of the best ways to find holes in your mental models is to try and find another point of view to look at the same problems. Even if you keep writing most of your code like you do today, in the language you do today, it can still be beneficial.