Imperative Haskell • Hacker News Board

Re: Imperative Haskell

#41

Post by empath75 » Wed, May 31, 2017, 1:04 PM UTC

enqk wrote: post #21

smilliken wrote: post #15

Earlier quoted context omitted.

> 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 dat…

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

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.

Re: Imperative Haskell

#42

Post by mac01021 » Wed, May 31, 2017, 1:14 PM UTC

quadrupleslap wrote: post #27

enqk wrote: post #21

Earlier quoted context omitted.

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

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.

Is there any evidence that this is true?

Re: Imperative Haskell

#43

Post by theoh » Wed, May 31, 2017, 1:30 PM UTC

runeks wrote: post #3

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 de…

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.

Re: Imperative Haskell

#44

Post by jerf » Wed, May 31, 2017, 1:50 PM UTC

mac01021 wrote: post #42

quadrupleslap wrote: post #27

Earlier quoted context omitted.

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.

Is there any evidence that this is true?

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.

Re: Imperative Haskell

#45

Post by marcosdumay » Wed, May 31, 2017, 3:22 PM UTC

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.

Re: Imperative Haskell

#46

Post by marcosdumay » Wed, May 31, 2017, 3:25 PM UTC

infinisil wrote: post #38

fizixer wrote: post #31

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…

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…

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.

Re: Imperative Haskell

#47

Post by skybrian » Wed, May 31, 2017, 3:48 PM UTC

lmm wrote: post #20

cousin_it wrote: post #11

Earlier quoted context omitted.

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 outpu…

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 nee…

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.

Re: Imperative Haskell

#48

Post by runeks » Wed, May 31, 2017, 4:02 PM UTC

nine_k wrote: post #4

runeks wrote: post #3

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 de…

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

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.

Re: Imperative Haskell

#49

Post by cousin_it » Wed, May 31, 2017, 4:03 PM UTC

skybrian wrote: post #47

lmm wrote: post #20

Earlier quoted context omitted.

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 nee…

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 reas…

Great point, I hadn't realized that purity must be performance-agnostic to make optimizations valid.

Re: Imperative Haskell

#50

Post by lmm » Wed, May 31, 2017, 4:04 PM UTC

skybrian wrote: post #47

lmm wrote: post #20

Earlier quoted context omitted.

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 nee…

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 reas…

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.