A pure language is one in which replacing any subexpression of any expression with the evaluation of that subexpression yields an equivalent expression.
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.
Performance matters for any task that has a deadline, not just crypto and real-time stuff. That's why we make performance improvements, after all.
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.
Performance matters a little bit - most of the time we don't make perfomance improvements. Really in a context where performance was of serious importance I would want to have an explicit model of it to be sure I could reason about it compositionally.
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.
Yes, compositional reasoning is important, but it depends on being able to substitute equivalent code. If you're too strict about what counts as equivalent (including performance in the type system, say) it would be harder to make local changes since fewer substitutions would be possible.
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.
> If you're too strict about what counts as equivalent (including performance in the type system, say) it would be harder to make local changes since fewer substitutions would be possible.
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.
I think this is a good take. Is there a natural definition of equivalence that includes standard output effects but excludes time and space effects, short of enumerating all effects and saying which ones are ok?
From a denotational/lambda-calculus perspective it's very natural to consider all expressions that reduce to the same expression as equivalent, at which point you have that definition of equivalence. Of course in the pure lambda calculus all "programs" are just (equivalent to) values. To get any effects like input/output you have to add extra values, and at that point you decide what the equivalence semantics of these "special" values are. That's kind of the Haskell perspective, and where I think it falls down is in the interaction between sequenced I/O and pure functions; the pure subset of Haskell can be fully evaluated at compile time (if you work in e.g. Idris this becomes true in a very direct sense: your (total) pure functions can be used in types), but as soon as a value depends on user input that obviously ceases to be the case, whereas expect to be able to decompose their program into pure and impure fragments and reason about these separately.
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.
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.