I find this slightly depressing that using global mutable state had such a significant performance given the functional programming (encompassing Idris) is very much in favor of immutable data structures and purity. I know it's best to explicitly switch to mutability iff a bottleneck is found (like how `mut` is explicit and not default in Rust), but I want to believe that Idris can live in a purity. This makes me think my opinions are not far off from religion.
Immutability is an implementation detail with no inherent value. What we actually care about is referential transparency, encapsulation & tracking of effects, performance, abstraction, thread/type/memory safety, etc. The State monad in Haskell is implemented without mutation, but presents an API with mutation. The ST monad is implemented with mutation but presents a pure and referentially transparent external API.
It is fair to say that functional programming is primrarily in favor of immutable data structures because it is simpler to implement them efficiently in a setting where referential transparency is the default. Mutation (meaning referential intrasparency) is just more complicated, and we need heavier machinery to structure it nicely. We may use linear/substructural types, uniqueness types, regions, etc for this purpose, but here are a number of choices, and the picture is not as clear-cut as with plain pure lambda calculi. Just remember that mutation is not bad by itself, many functional programmers are often happy to speed up production code with mutation, it's just that it is usually more complicated to structure nicely.
> Immutability is an implementation detail with no inherent value. What we actually care about is referential transparency, encapsulation & tracking of effects, performance, abstraction, thread/type/memory safety, etc. The State monad in Haskell is implemented without mutation, but presents an API with mutation. The ST monad is implemented with mutation but presents a pure and referentially transparent external API.
Both State- and ST-using code is harder to understand than code that doesn't use them. Immutable semantics are easier to reason about. Of course the implementation of those semantics may involve mutation at some lower level. But ideally we would have a runtime system that could implement immutable semantics with no loss of efficiency compared to implementing those lower-level mutations explicitly in our code.
Computer hardware has no concept of immutability or local state on the hardware level. You only have memory regions. If you want to get a feeling for this, I suggest to start learning assembly language.
Even if computers had immutable memory, then you still need to initialize memory regions with constant values and that would be a mutation.
It is possible to protect memory regions from writing, but these regions are still writable by the operating system kernel. And this is purely for safety and not for performance.
(And don't get me started on CPU caches and registers)
I think you need to see it as something like, the idea is that immutable data structures and purity are considered an excellent base layer for defining code, like also in math where integrals and differential equations are "purely functional" even though they implement or describe "phenomena of mutation." Mutable arrays are present in Haskell, they are just described on the linguistic level with immutable purity.
