As far as I'm concerned, purity is more fundamental than impurity, because we can always emulate impurity using a pure language (as is shown in this article), but it's not possible to emulate purity using an impure language.
This only leaves us with the challenge of performance. While we can always describe e.g. x86 assembly in terms of a pure intermediate representation language (e.g. GHC Core), transforming this description back into equally performant x86 doesn't seem easy.
Also, anyone care to produce some benchmarks comparing the imperative Python/Haskell quicksort implementations? They look so similar, it'd be quite interesting to see how well GHC can optimize this sort of stuff.
Purity is tricky to define. For example (stolen from Reddit user gasche), 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. You could try to patch it up by saying the impurity must be observable via pure code, but that makes the definition circular. 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).
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.)
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.
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.
Is a function like trace pure in your definition? trace's side effects seem to fall into the "unobservable implementation detail" category next to the missile launches.
It's not observable to the calling function (the return value didn't change) so it doesn't count.
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.
> 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 ...
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.
AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restriction. Please correct me if I'm wrong. From a quick reading I can't tell if the new paper makes progress on that front, what do you think?
> if you can measure how much time a computation takes, then Haskell is impure
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
> 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.
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.
Congrats, you've discovered entropy. The reason time seems to flow in one direction is only because there was an extremely low entropy state at the beginning.
Yes, but entropy means that the universe is not symmetric with respect to time, doesn't it? That is, enqk's statement is in fact a refutation of smilliken's claim. Dismissing it with "Congrats, you've discovered entropy" doesn't answer it at all.
Entropy is not due to the equations of our universe, but rather the initial conditions. So the asymmetry might be apparent but the equations might still be symmetric. Related is the idea of spontaneous symmetry breaking.
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.
> Of course, we don't have time symmetry in the equations anyway because of the weak force.
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.
The answer, as you point out, is that CP violation implies T violation. Experimentally testing T violation is much, much harder, and I don't think has really been done in many systems (look at Fitch and Cronin's work for an example), but we know CP violation implies it. So it's there. Or at least, to our best knowledge, it's there -- T violation is not very well understood.
I think the idea is that with perfect knowledge of the current state of the universe, you could deduce that yes, that water was once a snowflake of some known configuration.
Even if it is true in theory, it is not practically true, as the information required to reverse such a transform rapidly exceeds what you can collect even in theory in a single coherent system. While this is by no means the end of your problems, one simple question you can ask yourself is how exactly you intend to re-collect the photons that the snowflake emitted while melting as they head off to the ends of the universe at light speed?
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.
> 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.
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.
% make hs
Results: [25872791,24253954,21258158]
make hs 6.53s user 3.99s system 245% cpu 4.282 total
% make py
24029582
25343914
20814678
make py 22.37s user 0.11s system 99% cpu 22.593 total
You can see the code as tested here[0]. I am not an expert on either Haskell or Python performance, all I did was use -O for python3 and -O2 for GHC. This was on a 2.8 GHz Core i7 Macbook, FWIW.
Edit: Since 'contents' was unspecified I used one million random ints.
I was playing around a little more and I noticed that stack sets the following
ghc-options by default:
-threaded -rtsopts -with-rtsopts=-N
which I assumed explained some of the speedup, so I disabled them and got a
reduction to 99% cpu as expected, but unexpectedly the single threaded version
was about twice as fast:
% make hs
Results: [24605537,25150983,21576960]
make hs 3.13s user 0.07s system 99% cpu 3.211 total
$ time make hs
Results: [24639155,24977202,20874958]
make hs 8.39s user 5.93s system 322% cpu 4.435 total
$ time make py
24894022
25787638
21979201
make py 14.33s user 0.02s system 99% cpu 14.353 total
$ time make py PYTHON=pypy3
25059732
25318854
21254890
make py PYTHON=pypy3 4.02s user 0.06s system 99% cpu 4.082 total
Oh come on, how can you expect similar execution time between a compiled language like Haskell and an interpreter like Python? I would be very surprised if the latter was not several times slower, purity or not.
If anything, you may want to compare compiled Haskell code to an impure, imperative language that is also strongly typed, compiled to machine language, and garbage collected, like Go.
> it's not possible to emulate purity using an impure language
It sounds as if a pure language cannot be implemented in terms of an impure language. E.g. a pure language won't be implementable in an instruction set of any modern CPU. I must be missing something.
Impurity is a lack of constraints. You can, with impure code, write an interpreter for a language that constrains code to being pure, and implemented correctly, you can then depend on code written in that langauge to be pure.
His point is that there's no lost benefit in calling pure code from impure code - the code is already unconstrained. Calling impure code from pure code, though, means you've lost the purity constraint, which means you've lost the nice emergent properties you get from that constraint.
Even if you write 'pure' code in an impure environment, you can't depend on it being pure, because that constraint isn't actually enforced. No matter how pure I try to keep my Javascript, I can never depend on it being pure - there could be a bug, or someone could add impurity at the bottom of the callstack, breaking referential transparency.
Following your argument to the extreme, Haskell is also an impure language: there could be a bug in the compiler, or someone could introduce impurity in it! Even worse, someone could call unsafePerformIO!
You would argue: but that goes against the Haskell specification, that impurity is not proper Haskell!
And exactly: the "purity" comes from an abstraction, which is a contract between you and some other developers. The fact that JavaScript the language does not enforce such contracts does not mean that you can not get into agreements with other developers. Sure, the JavaScript interpreter won't complain when the contract is broken, in the same way that the CPU is not complaining when Haskell has a bug, in this case, JavaScript is not the one making the purity promise---a developer is.
As such, I believe that in JavaScript, a library author can make claims about the purity of some code. Sure, some adversarial coder could use monkeypatching to break it---and some adversarial coder could also gives you instances of some type class that call unsafePerformIO under the hood. In the end, we are talking about degrees to which some purity can be ensured, and levels at which the contracts are enforced.
I know some Haskell developers would like to think that they are programing in this perfect language and that it is impossible to do functional programming in other languages. But I disagree, and actually, I believe that bringing the design tools of functional programming to mainstream languages is a worthy goal that should not be discouraged.
In theory it would be possible to write a specification for a pure subset of JavaScript. But it's very important to acknowledge that this pure subset doesn't exist, and won't exist unless and until such a specification is written, to the point that it's possible to write an automated tool that can verify whether a given piece of code conforms to this specification. And if such a specification did exist, we would likely call it a "language" in its own right.
Once you write that language and confirm that your library conforms to it you can say your library is pure. Saying your library is pure before you've actually formally checked it is like saying your library doesn't have any bugs in before you've made any attempt to look for them - i.e. almost certainly a false, and so irresponsible to claim that it qualifies as a lie in my book.
I 100% agree that purity is still incredibly useful for reasoning about and maintaining code in any language, but I think you're underselling the benefits of statically verifying that you haven't unintentionally introduced impurity somewhere. Oh, and ideally it'd also allow for some nice optimisations, but I'm not sure to what extent that's being done.
It's important that we separate the concept of a language and its implementation. You cannot define a pure language using an impure language, but what type of language you use to implement a pure language is up to you.
Purity is not a really property of functions, but of optimizations. A pure function is simply those functions for which a "pure optimization" is desirable, and that ultimately depends on what you care about. Every impure function can become pure just by finding a context where the side-effects are moot. (Redirect all output to /dev/null and suddenly you won't care if your printf calls get elided or memoized.)
Python (in its CPython) incarnation is pretty slow usually. You can use PyPy (a JIT implementation of most of the Python spec) for dramatically more speed, but the code needs to be ported to work under PyPy.
The real comparison should be a language that is both functional and imperative and that allows you to write as brief a source code as you can do in Haskell.
Such a language is Common Lisp, and it will compile directly to machine language doing many optimizations.
The only incompatibility is the `.copy()` calls which should be replaced by `list(contents)`, then it'll be cross-compatible between P2 and P3.
Here's what I get with that (on a 2010 MBP) using the random generation of lgas above (1M random ints):
> time python2.7 qs.py
python2.7 qs.py 41.92s user 0.37s system 98% cpu 42.837 total
> time python3.6 qs.py
python3.6 qs.py 42.99s user 0.32s system 98% cpu 44.047 total
> time pypy qs.py
pypy qs.py 3.27s user 0.12s system 94% cpu 3.603 total
There's a fair bit of variation but pypy is between 3.4 and 4
But since Haskell of course compiles to C or C--, it obviously doesn't follow that you can't implement purity in an impure language -- just not at the level of the typical metacircular interpreter beloved of FP people.
I'm not sure what you'r saying exactly. A related issue is the "monads let us do things that are difficult to express in other ways" argument of Wadler's paper Essence of Functional Programming. I believe it, but also it's clear that the real attraction of monads is their rigorous foundation. They are simple to reason about correctly and mathematically about while providing useful features. What I'd argue is not the case is that it's difficult for a programming language implementer to come up with an abstraction that does something similar in an adhoc, less well-founded way.
Maybe it's the same with implementing purity in a non-pure language. It's harder to hit the target of elegance, but it's the de facto situation on any existing hardware.
Since I've got a stray downvote, let me clarify: I'm pro-FP. Purity amounts to referential transparency which is uncomplicated. Haskell and similar languages have the character of arithmetic expressions (no side effects) evaluated mechanically. This claim is uncontroversial and is supported by the well known papers of Strachey and Landin. Monads are useful but their use does represent a decision to bring "the awkward squad" of side effects etc. into the clean elegant world of calculating the value of expressions. Alternative approaches might see imperative code written separately from pure code.
It's surely a category error to say that purity is more essential than impurity. What's pure is the expression one types in, and its various reduced forms, culminating in a value. Impure is the messy causal world of real hardware and objects which have stubborn or mutable properties: the whole address-based system of letters in postboxes, for example. The world has state. That doesn't make the platonic ideal of an arithmetic expression any less real, but it's an abstraction of a certain circumscribed set of operations that we perform, typically on a blackboard or with pencil and paper. It's a tiny part of reality.
> it's not possible to emulate purity using an impure language
The fact that Haskell code is routinely compiled into machine language, which is the most impure and imperative kind of code possible, disproves your point.
The first code block reads like a definition, or the 'what' of quicksort, which has to be fleshed out using the 'how' of quicksort. And it just so happens that 'what' is declarative, and 'how' is imperative (i.e., do this, do that, that's how).
Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this:
'sort is a map that takes a sequence S of orderable items, to one of its permutations P such that for every two adjacent elements e1, e2 in P, e1 < e2'
I'm not familiar with Haskell syntax but I'm sure this definition can be encoded in Haskell. Actually imperatively speaking, this is a sort algorithm itself, the very less discussed (probably because of very high complexity) 'permutation sort', i.e. you keep permuting the input sequence and keep checking your e1/e2 condition until it is satisfied.
So we can define sort, but then we can specify a language to not compute based on that definition but instead pick from one of the preferable computation schemes that are also defined in that langauge (quicksort, mergesort, etc, etc). But then we specify not to use the definition of that scheme but instead use an algorithm for it (e.g., the imperative algorithm for quicksort).
I guess this is a form of semantic layering, something that I'm interested in as a topic of study.
I can't find it now, but there is this article/blog somewhere where the author writes only two functions: One tests if a list is sorted and the other generates a seemingly unspecified permutation of a list.
Then they combine the two in some simple way, and out pops a sorting function with no "how" specification. Due to laziness, the testing function "drives" how the permutation function picks its elements and the whole thing devolves to selection sort.
If anyone remembers the source for this, please post it.
That's where formal proofs come into play, because you need to somehow show that the implementation actually does what the definition states. Since Haskell isn't a proof checker you can't use it for this. The newish and very promising looking language Idris [1], which is very similar to Haskell, can actually do this because of having dependent types. Upon a quick search I found this great example [2] of a proof that insertion sort does indeed return the list sorted, all in the type system. I can really recommend Type Driven Development [3], a recently released book on development in Idris.
Well, if you decides like the GP does, that the definition is the Haskell code, it's not a proof checker, but it's an automatic proof writer that (except from bugs on GHC) is expected to write correct proofs.
It would also be interesting to extend this language to the one that also has partial conditions satisfied, e.g.:
- We have a set S of tuples (a,b,c) sorted by (a,b)
- We would like to sort S by (a,b,c)
- Therefore we only need to only sort subsets (a,b,cx)
By the way, permutation sort would be reducing the sorting algorithm to a problem of search in the configuration space of N variables. Speaking generally, you may reduce any problem to a search problem; so this doesn't only work for sorting.
Is the ST performance better or worse than the purely functional approach? It actually looks pretty good, not really any more verbose than Java to be honest.
Some algorithms require mutation to have a decent time complexity and ST allows you to implement those.
There is a tiny cost for each mutable memory location since the garbage collector has to work around then. A single array won't even be measurable, though.
Also, there are some referentially transparent algorithms that can't be implemented via ST - like laziness.
Direct mutations for a mutating algorithm is certainly faster than rebuilding a data structure representing a set of variables. Most of the time. Though, there are exceptions where they're equivalent thanks to GHC's optimizations (e.g. splitting up a record's fields into n registers).
The article is assuming a little too much when it's claimed that the first implementation doesn't sort in place.
It's not clear how GHC would optimize this (even more if you don't use the unsorted list for anything else), and it would be interesting to see the benchmarks for that version too.
This only leaves us with the challenge of performance. While we can always describe e.g. x86 assembly in terms of a pure intermediate representation language (e.g. GHC Core), transforming this description back into equally performant x86 doesn't seem easy.
Also, anyone care to produce some benchmarks comparing the imperative Python/Haskell quicksort implementations? They look so similar, it'd be quite interesting to see how well GHC can optimize this sort of stuff.