Translating Mathematics into Code: Examples in Java, Python, Haskell and Racket

This is precisely what happens in languages without immutability / control of mutation. They effectively say "this may or may not mutate. See for yourself. Oops! It just mutated. Sorry!"

Also, isn't what you talk about in your example just a shorthand to avoid cluttering a proof or whatever? It's not that variables mutate; it's that by convention you elide the notation that shows they mutate. That makes a lot of sense: the writer and the reader assume some things and go on with a compact notation that eliminates noise. It's a useful convention, and if the reader loses track of the notation, the worst that can happen is that he/she won't be able to understand the proof.

The problem with computer programs is that it's about both the reader and the computer interpreting the program. Because variables may or may not mutate, it's harder for the computer to perform some optimizations. Because of the same reason, it's harder for humans to understand the code ("is this going to use the convention that it won't mutate variables? I have to carefully read the code and consider all paths in order to be sure").

In a sense, programming with uncontrolled mutation is like switching the default convention to its most confusing setting :)

I disagree about the sum "loop". It's merely a notation, not an actual step by step operation. Unlike a traditional imperative language's variable, i's value cannot be changed. Whatever the actual expression of f, you know i is always the same within it. You could think of it this way: "for each value v from range m..n, introduce a new variable i at each step with value v, which we will use for the expression".

When you look at the categories in use by mathematicians a surprisingly large number of them are not cartesian, this is true in particular of the categories relevant to physics, where both the category of symplectic manifolds (relevant to classical mechanics) and Hilbert spaces (relevant to Quantum Mechanics) are monoidal and not cartesian. In both cases you therefore can not copy states.

Moreover in physics things are local in the sense that the dynamics of a physical system is usually determined by differential equations. That means there is typically no situation where you have to retain much of the state of the system for a long time in order to simulate its behavior.

Even for complicated things like PDE simulations, what you really do is approximate some infinite dimensional function space locally with finite dimensional vector spaces. The state space in each step of the simulation is some tensor product. So while a computer certainly allows you to do it, it isn't really natural to constantly copy state in such simulations. Abstractly a Fortran 77 program could probably described by a collection of morphisms in some traced monoidal category, so it doesn't seem too far off from the mathematics it was invented to implement, although ultimately it clearly is deficient.

From a certain angle a lot of abstract algebra is actually more or less about creative destruction of information, certainly if you use it as a tool to study number theory, or topology. A whole class of functors there are monoidal functors from cartesian to non-cartesian categories and you carefully adjust how much information the functor loses in order to make computations feasible (Homology vs. Homotopy for example). The reason mutation doesn't seem to be prevalent, is because a lot of operations that are studied are invertible. But as soon as you for example study a group operation on a space, that is not faithful, then you won't be able to recover the original space after you've applied the group operation once, unless you've copied it before.

The connection between entropy and copying is fairly well explained in this paper I stumbled upon a while ago: http://www.pipeline.com/~hbaker1/ThermoGC.html

Of course the origins of copying in type theory is that for example Gentzen's calculus can be properly thought of as living in some cartesian closed category, as you probably know. Personally I find linear logic interesting, especially because it is able to faithfully embed intuitionistic logic and lets you talk precisely about copying. The problem is of course that type inference is undecidable for linear type theory, if I remember correctly.

In terms of expressive power Haskell is probably already fairly close to the ideal, most relevant to the discussions is I believe its inability to express laws its type classes have.

It is fairly good at expressing "free" or "cofree" things, but is not so good at expressing laws statically, not to mention providing a mechanism for proving the laws for instances. The best thing you can do is write embedded interpreters or compilers for those free / cofree things, that sort out things at runtime, or use template haskell.