Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Imperative Haskell

vaibhavsagar.com

Post reply on HN
Print view View original

21–30 of 73 posts

Re: Imperative Haskell

#21

Post by enqk »

smilliken wrote: post #15
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…

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

Re: Imperative Haskell

#22

Post by Tarean »

aetherspawn wrote: post #2

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.

Re: Imperative Haskell

#23

Post by chrisdone »

cousin_it wrote: post #11
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…

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…

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

Re: Imperative Haskell

#25

Post by cousin_it »

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…

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?

Re: Imperative Haskell

#26

Post by arximboldi »

T-R wrote: post #7
nine_k wrote: post #4

Earlier quoted context omitted.

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

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.

Re: Imperative Haskell

#27

Post by quadrupleslap »

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?

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.

Re: Imperative Haskell

#28

Post by quadrupleslap »

arximboldi wrote: post #26
T-R wrote: post #7

Earlier quoted context omitted.

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

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

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.

Re: Imperative Haskell

#29

Post by ridiculous_fish »

chrisdone wrote: post #23
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…

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

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.

Re: Imperative Haskell

#30

Post by pdpi »

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?

sure. As long as time is symmetrical, and advancing time by -t cancels out advancing time by t.
Post reply on HN