Of course this means "pure" is not an absolute term but rather relative to a given definition of "equivalent". But this isn't circular and is practically useful: if you're working in a context where precise execution time matters (e.g. cryptography) you really do need to use a different concept of "pure" language from what you would use in a more "normal" context where two programs that produce the same output are equivalent even if they take a different amount of time to execute.
I think it might be better to think of purity as a way of ensuring that performance and logical correctness are independent effects. Purity allows us to safely improve performance by making local substitutions of faster but logically equivalent code, without having to reason globally about correctness. It's also what allows us to tolerate variation in performance (within reason) without threatening correctness.
For crypto we can reason separately about logical effects (does the crypto work) versus information leakage. For a user interface, we can treat dropped frames as a performance problem rather than a correctness problem.
This is useful even though we still care about performance. Substituting a much slower function for a faster one probably isn't okay, but purity lets us understand the effect.
I find any single effect is easy to reason about in isolation, it's the interaction that gets tricky. Viewing purity as isolating performance is just one perspective on this - you can equally view it as isolating state mutation, or isolating async transitions.
You can look at const correctness in C++, Java checked exceptions, async versus non-async functions [1], and Rust's ownership model as other examples where making fine distinctions for good reason has a side effect of making substitution harder - or perhaps safer, depending on your point of view.
If you need it, you need it, but when you don't, it's a luxury to be able to substitute whatever you like and see what happens.
[1] http://journal.stuffwithstuff.com/2015/02/01/what-color-is-y...
I think this is avoidable if your types/effects can decompose properly into orthogonal factors. E.g. with a Future type and a generic monad abstraction it's fairly easy to substitute a sync call for an async call - you have to be explicit about the change you're making, but only very slightly, and you'd never get confused between changing sync/async and changing the "actual" type that's returned.
From an operational perspective a good definition of equivalence would be very difficult. E.g. if your language allows making system calls there are dozens or hundreds of those with no real model of how they interact, so it's very hard to say when one sequence of system calls is equivalent to another. Possibly the most natural notion of operational equivalence is to say two programs are equivalent if they execute the same sequence of CPU instructions, but that would mean that nontrivial programs were virtually never equvialent to each other, even if they both just printed the same string.
Equivalence: unification of types (can't make I'll-typed substitutions)
Output only effects: have your language define only one such monad
About to depart on a flight, so can't elaborate further.
I think it's pretty easy.
Purely functional (it's important to retain the word "function") means that we have a language in which the value of a function application "f x" depends only on the body expression of "f" and the function argument "x". That's why we say "purely" functional, because it's just functions of this flavor.
In types, f : X -> Y means that for all terms in X, f x maps to a unique term in Y. In Haskell's, Elm's and PureScript's case, it's weakly normalizing (meaning it might get in an infinite loop). In Agda's case, it's strongly normalizing (modulo implementation bugs).
> if you can measure how much time a computation takes, then Haskell is impure, because a lazy value takes longer to compute the first time than the second
Time is an operational concern. "Purely functional" is concerned with what things mean, what do syntactic expressions in the language denote? If 1+1 launches missiles every time it's evaluated, or causes the machine to get hotter by 1°C, that's an implementation detail that is not observable in the language. 1+1 normalizes to 2. You can do all your regular equational reasoning and follow the substitution model. You might chide the writer of the interpreter or compiler, though.
For example, here is a substitution stepper for a dialect of Haskell http://chrisdone.com/toys/duet-gamma/, and each line in the bottom left is equivalent to the line after it. You can pick any of those lines as your starting point.
> And that raises another problem, where printing to standard output becomes "pure" if the standard output can't be observed by pure code (which is true in Haskell).
It doesn't "become" pure. You're making a category error by calling an implementation detail by names that we reserve for expressions in a language. We should use "observe" in a precise way: to observe means to write a case analysis on something.
> You could try to patch it up by saying the impurity must be observable via pure code, but that makes the definition circular.
Where exactly is the circular part?
Perhaps a way to think about it is as a way defining the contract between a library function and its callers regarding what substitutions are permissible. For example, substituting a faster algorithm is likely observable to the end user, but the calling function will continue to return the same value so it's a compatible substitution.
Similarly, turning on compiler optimizations or debug logging should not be a correctness issue, though it certainly matters or we wouldn't do it.
This information may be out of date. There are now at least two Agda formalisations of runST (by Andrea Vezzosi and András Kovács), and a paper by Timany et al. on the subject of runST has been submitted to ICFP'17.
http://code.haskell.org/~Saizan/ST/ST.agda
http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d...
gettimeofday requires IO, so the computation would depend on dynamic inputs, but that doesn't make it impure. If the program knows how long one of its computations took, that's only because an oracle (outer layer of abstraction) told it.
> Another problem with seeing purity as fundamental is that our physical reality isn't a persistent data structure
I like this line of reasoning, but would take the opposite conclusion. The universe is symmetric with respect to time, and indeed, information is conserved. Past states aren't easily accessible, but they have not been erased. This sounds like a fine working definition for persistent data structures.
> there's a strong suspicion that the (pure) type signature of runST has no pure implementation
Interesting, thanks for bringing it up!
That line of research exists, but it's different from persistent data structures. The search term is "reversible computing", and the main idea is that you never erase bits because that would irreversibly increase entropy. One difference is that persistent data structures allow access to past states in O(1), while reversible computing requires you to spend time on uncomputing. Right now it's mostly a curiosity because it requires hardware that doesn't exist, so I'd be wary of using it as a foundation of CS. It might well become important in the future though, due to lower energy requirements.
Bringing a snowflake back to its previous shape after it has melted?
Of course, we don't have time symmetry in the equations anyway because of the weak force. But because the weak force is weak//doesn't matter much for the physics of many systems, we can often write the equations of physics as a time-symmetric term which essentially decides the motion plus a very small time-asymmetric term. So we can deal with the small term using techniques like perturbation theory, and use time symmetry for the rest.
Could you expand on what you mean here? I've expected for a while that there was going to be something non-time-reversal-symmetric with the weak force, on the basis of parity violation (space-reversal doesn't give you the same equations) plus relativity (space and time are the same thing, at least kind of). But getting there directly from parity violation might require a faster-than-light frame of reference to observe it from, which is... let's just say it's experimentally difficult.
How does the weak force break time symmetry?
If the universe is externally a pure value, it doesn't matter to us on the inside. The universe is impure from our point of view.
Also, a pure data structure doesn't just imply that you have a puddle of water that you can put back together into a snowflake; it practically (that is, in practice, not in the colloquial sense of the term) implies that you have both at the same time. When I'm working with pure data structures I don't have to laboriously translate back and forth, I have them both in hand. This is partially because pure data structures simply have no concept of time at all in them. And you can't save this argument by claiming you can transform them back and forth at will, because as I mentioned, no, you can not. Common sense can be clad with solid mathematical arguments here; you can not, in our real universe, ever do that, so even the superficially appealing theoretical answer must give way to a more sophisticated and correct theoretical analysis in which in fact you can't reverse arbitrary transforms in practice. (You can do it at a small scale for small numbers of qubits. You can do it for a constrained number of qubits specially set up and isolated for just such an occasion, aka "quantum computer".... and note how hard even that is, we've still not managed to isolate very many qubits at a time that way! But you can not do it in general.)
Whether an entity external to our universe could do it is something you'd have to take up with them.
Purity is a simplification of the real world, in the same way that the abstract ideal of a circle is a simplification of objects in the real world.
But that simplification yields great benefits (kind of in the same way that ideal geometric shapes allow mathematical reasoning). It seems to describe the simplifications that the real world "approaches" (like a mathematical limit).
So it does seem fundamental. But yet not "real." I don't think those are contradictory.
It makes intuitive sense that non-purity could open up algorithmic possibilities, some of which would be faster. But that doesn't really touch on whether purity is "fundamental" in the sense described above.
I don't see why this is an issue when pseudo-random generators are in fact deterministic yet for purposes of pivot selection the seed does not need to be fresh on each invocation barring an adversarial context, in which you'd just pass in the seed from the effectful part of the program.
Another problem with seeing purity as fundamental is that our physical reality isn't a persistent data structure (past states aren't accessible), so the best algorithms possible won't treat it as one. Among the tons of papers describing fast algorithms, practically none are using purity, unless they required purity to begin with.
And there's a third problem, specific to Haskell, that might interest you. The article is using ST to implement an impure computation. You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and there's a strong suspicion that the (pure) type signature of runST has no pure implementation at all, even with quadratic or exponential slowdowns. The reason is tricky to explain, but it's well covered on StackOverflow and Reddit.
(That's not even going into the issues of quicksort. Suffice to say that a pure quicksort is hard to write, ST or no. The problem is that you need good pivot selection to prevent the quadratic worst case, but randomized pivot selection will lead to observable impurity in the output, because quicksort isn't stable. So you must use something like median of medians, making the algorithm much slower and more complicated.)