Imperative Haskell
vaibhavsagar.com
vaibhavsagar.com
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.
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.
You can write the same code, but you can't rely on the enforcement of the same contract unless it is built into the language.
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.
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.
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.
% 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
Edit: Since 'contents' was unspecified I used one million random ints.
-threaded -rtsopts -with-rtsopts=-N
% make hs
Results: [24605537,25150983,21576960]
make hs 3.13s user 0.07s system 99% cpu 3.211 total[0]: https://github.com/vaibhavsagar/thursday-presentations/blob/...
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.
$ 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 totalAnother 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.)
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?
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.
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?
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.
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.
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.
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.
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...
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.
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
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.
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.
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.
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.
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.
[1]: https://www.idris-lang.org/
[2]: https://github.com/davidfstr/idris-insertion-sort
[3]: https://www.manning.com/books/type-driven-development-with-i...
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.
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.
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.