6 ms·

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

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.)

lmm 9y ago
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.
- cousin_it 9y ago
  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?
  - cstrahan 9y ago
    Maybe something like this: 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.
  - lmm 9y ago
    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.
- skybrian 9y ago
  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.
smilliken 9y ago
> 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 Interesting, thanks for bringing it up!
- cousin_it 9y ago
  > 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.
- enqk 9y ago
  > The universe is symmetric with respect to time, and indeed, information is conserved. Bringing a snowflake back to its previous shape after it has melted?
  - pdpi 9y ago
    sure. As long as time is symmetrical, and advancing time by -t cancels out advancing time by t.
  - 9y ago
chrisdone 9y ago
> Purity is tricky to define. 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/ 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?
- ridiculous_fish 9y ago
  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.
  - skybrian 9y ago
    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.
mietek 9y ago
> 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. http://code.haskell.org/~Saizan/ST/ST.agda http://code.haskell.org/~Saizan/ST/ST.agda http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8dbd1dced6 http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d... http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf
- cousin_it 9y ago
  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?
charlieflowers 9y ago
> 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.
platz 9y ago
> randomized pivot selection 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.

lmm 9y ago

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.

cousin_it 9y ago
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?
- cstrahan 9y ago
  Maybe something like this: 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.
- lmm 9y ago
  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.
skybrian 9y ago
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.

smilliken 9y ago

> 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 Interesting, thanks for bringing it up!

cousin_it 9y ago
> 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.
enqk 9y ago
> The universe is symmetric with respect to time, and indeed, information is conserved. Bringing a snowflake back to its previous shape after it has melted?
- pdpi 9y ago
  sure. As long as time is symmetrical, and advancing time by -t cancels out advancing time by t.
- 9y ago

chrisdone 9y ago

> Purity is tricky to define. 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/ 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?

ridiculous_fish 9y ago
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.
- skybrian 9y ago
  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.

mietek 9y ago

> 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. http://code.haskell.org/~Saizan/ST/ST.agda http://code.haskell.org/~Saizan/ST/ST.agda http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8dbd1dced6 http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d... http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf

cousin_it 9y ago
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?

charlieflowers 9y ago

> 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.

platz 9y ago

> randomized pivot selection 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.