6 ms·
I don't think anyone, mathematicians or functional programmers, have a problem with mutation [0]. They have a problem with names suddenly changing without being
by tel 12y ago
I don't think anyone, mathematicians or functional programmers, have a problem with mutation [0]. They have a problem with names suddenly changing without being too explicit about that fact.
In particular, mathematics certainly doesn't prohibit you from using whatever kind of notation you like to explain your concept, but it has suggested a certain primacy of the notion of a (pure) function. The reasons are both ones of mathematical "elegance" (whatever that means) and pedagogy. They're a fantastically important fundamental building block.
Mathematicians would never claim that pure functions are the only thing around, but by and large they'd assume that's what you were talking about given no other indication. Furthermore if you introduced something new (say something with a notion of mutation) then you'd merely be obliged to explain exactly what that new thing is with sufficient formality so that the reader can be assured that its behavior is completely reasonable.
All of this holds identically for functional programming. The only additional challenge is that FPers are accidental intuitionists so you can't merely name the behavior of a new kind of notation but must actually exhibit an interpreter of that new notation into more common notation. This is significantly more heavy-handed than most mathematicians would do.
[0] Or any other side effects. The whole argument is parametric in your choice of side effect.
- orbifold 12y agoFrom a mathematicians perspective, functional programming languages do a fairly bad job at being able to express algorithms in the way mathematicians have been writing them down since before computers existed. There is little difference between writing $x_{k+1} = f(x_{k})$ and $x = f(x)$ in an imperative language. In some cases the index k can even be identified as a multiplicator of some discrete timestep, in which case what the hardware is doing is in very close correspondence to the abstract iterative process. All the operations in abstract algebra are actually destructive by default, if you do a multiplication, then that is a map m : A \otimes A \to A If you want a copy of the values you put in you have to pre- compose, with a diagonal map \Delta: A \to A \otimes A, which might even not exist (it doesn't if \otimes is the tensor product of vector spaces for example). Even application of a morphism on its own is treated as irreversible, once you've applied a morphism to an Object you can't get it back unless you are in a special category like Set, or the morphism happens to be invertible. The fact that functional programming languages hide copying behind your back does not make sense physically either, on a hardware level duplication is fairly expensive, because it decreases entropy. There are countless examples in Computational Physics and Numerics, where pure functional programming languages fall flat on the nose. I'm thinking about finite-element methods with adaptive refinements, all the code for computer algebra and computational group theory, etc., not to mention all the Fortran/C/C++ code that is in existence in physics (At Cern they have written 60 million lines of it). It might be that the experts in functional programming languages simply don't have the expertise necessary to come up with viable solutions, because things like repa and accelerate are not realistic alternatives when it comes to real world applications.
- tel 12y agoI'm sadly not actually able to follow what you're getting at here. I think there are a few threads going on that I'd be interested in following up on, whether imperative/mutable semantics are common in mathematics, whether it makes sense to call something in abstract algebra as "destructive", what copying means, whether analyzing computational physics/numerics is a similar task, whether functional programming experts are capable of building real world applied math tools... Ultimately, though, I'm not sure which ones move the conversation along productively. I think perhaps the most interesting one is the notion of copying. It is certainly the case that modern FP assumes copying is okay. This comes naturally from the "structural properties" of implication in type theory and there's plenty of work studying type theories which are "substructural" and thus don't assume an ambient copy/destroy comonoid. I don't honestly consider this out of scope of FP, although no languages implement it today. There is a need to pick a "default semantics sweet spot" and linear logic may have not yet proven it pays its way on the weight/power tradeoff spectrum. But maybe it will be shown to in time? In the mean time you can do plenty of work in abstract algebra without talking about mutation or destruction at all. You mention category theory but ignore the prime dictum of CT: it's all about the arrows. Categories certainly exist which embody destructive internal algebras---CT would be pretty useless if it didn't---but externally we consider arrows and compositions of arrows alone. This is where the real power of CT comes from anyway.
- orbifold 12y agoPerhaps a few points of clarification are in order, my original comment had too many different threads mixed together. I will first try to expand on my remarks on copying and then try to respond to some of the things you said. 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 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.
- Klockan 12y agoJava has no functions and is the language which gets harped on the most, so this is obviously not the main issue.