4 ms·

Is Haskell pure? It has exceptions You can divide by zero It has unsafe IO primitives

tome 2y ago
You're right: "pure" is not a well-defined concept. The well-defined concept that describes Haskell's benefits in this regard is "referential transparency". That means that this code let x = <definition of x> in ... x ... x ... (i.e. defining a variable x and then using it some number of times) is equivalent to ... <definition of x> ... <definition of x> ... Seen in the opposite direction (transforming the bottom code to the top code) this means that extracting repeated code is always a valid thing to do. It's not valid in most other languages, and certainly no mainstream ones.
- simiones 2y ago
  Well, technically that isn't true if you use, for example, unsafePerfomIO in the defintion of x. Referential transparency is still a spectrum, just like purity. Haskell is much closer to purity than the vast majority of languages out there. Also, even if Haskell were perfectly pure, the fact that it uses lazy evaluation is far more important to actually being able to make use of referential transparency. In a strict language you will still see a massive performance differences if replacing the first version with the second, in the most common cases.
  - tome 2y ago
    > technically that isn't true if you use, for example, unsafePerfomIO in the defintion of x Ah, well, regardless of whether it holds in Haskell, referential transparency is a well-defined concept. Purity is not a well-defined concept (at least as far as I know. Please share a formal definition if you have one!). That's primarily what I'm trying to say. But I also disagree with your point about unsafePerformIO. In practice, nothing in Haskell violates referential transparency in a significant way. Who knows why? It's an emergent phenomenon that in principle need not have occurred, but in practice it did. Debug.Trace and similar are about the only things that technically violate referential transparency (and they are extremely tame). > the fact that it uses lazy evaluation is far more important to actually being able to make use of referential transparency Yes, I agree with that.
    - simiones 2y ago
      It seems that someone did come up with a formal definition to try to capture the concept [0], though I haven't looked into the details to see whether it really matches the colloquial use of the terms "pure" and "impure" functional programming. In short, the formal definition they came up with is that a language is pure if the result of a valid program is the same under any parameter passing strategy. I should note that I agree that, in practice, Haskell is almost always pure and/or referentially transparent. I was just pointing out that technically the GP was correct that it's not perfectly 100% so. [0] https://www.cambridge.org/core/journals/journal-of-functional-programming/article/what-is-a-purely-functional-language/3A39D50DA48F628D17D9A768A1FA39C3 https://www.cambridge.org/core/journals/journal-of-functiona...
      - tome 2y ago
        Sabry's definition of "pure" fails to satisfy me for two reasons: 1. It assumes that the language is "a conservative extension of the simply typed λ-calculus". That's rather high-powered yet also really restrictive! Haskell doesn't satisfy that requirement. It also assumes the language has functions. Expression languages (i.e. ones without functions) are perfectly reasonable languages and it makes sense to ask whether they are pure. 2. It assumes that a language putatively has multiple evaluation orders (which I suppose is a consequence of the assumption "It is a conservative extension of the simply typed λ-calculus"). Haskell doesn't have multiple evaluation orders. It has one! (notwithstanding you can influence it with seq/!) If you unpick the essence of what Sabry's really saying you find you can translate it into the Haskell world through imposing two conditions: C1. soundness of the β-axiom (a.k.a. referential transparency) (this plays the role of Sabry's condition that call by need and call by value have the same result). C2. That let x = <definition of x> in ... gives the same result as let !x = <definition of x> in ... whenever the latter terminates. (This plays the role of Sabry's condition that call by name and call by value have the same result.) I omitted this condition from my original. I probably shouldn't have because technically it's required, but it risks getting into the weeds of strictness versus laziness. So Sabry's definition of "pure" is a long-winded and restricted way saying something that can be much more conveniently expressed by C1 and C2. If you disagree with me, please demonstrate a property of purity that can't be deduced from C1 and C2! > I should note that I agree that, in practice, Haskell is almost always pure and/or referentially transparent. I was just pointing out that technically the GP was correct that it's not perfectly 100% so. OK, fine, but I also said the GP was correct! I am keen to point out, however, that exceptions (including division by zero) do not violate referential transparency (and if someone thinks they violate "purity" that may be a sign that "purity" is ill-defined).
afiori 2y ago
I feel like exceptions where added as a mix of "look we can do that too" and "maybe if so many functions return optional values then it is going to be too much of a pain to use" In hindsight I think few would now regret not having added them in the first place.
- fire_lake 2y ago
  > maybe if so many functions return optional values then it is going to be too much of a pain to use I strongly believe that there is a point in the PL design space that makes optionals everywhere usable. Maybe Haskell can still be the language that delivers this.
  - tome 2y ago
    To plug my own solution, my effect system Bluefin makes exceptions visible in the type, well-scoped, and also freely composable with all other effects: https://hackage.haskell.org/package/bluefin-0.0.3.0/docs/Bluefin-Exception.html https://hackage.haskell.org/package/bluefin-0.0.3.0/docs/Blu...
afiori 2y ago
>It has unsafe IO primitives To be tongue in cheek then it also has the side effect of heating the CPU.
IshKebab 2y ago
It is pure in the same way that Rust is memory safe. That is too say there are a tiny number of exceptions/escape hatches, but they are not meant to be the norm. Every day programming doesn't involve them. Exceptions aren't impure anyway.
- nextaccountic 2y ago
  Exceptions define an effect. Code with exceptions aren't actually pure in the sense that their return type doesn't fully describe what the code does, so it doesn't just map an input into an output: there is something else going on In some pure functional languages, the pure fragment doesn't have exceptions, and you add exceptions as an effect (or as a monad) (If you reify the effect with a type like Either or Result, then the code becomes pure: but that's just a monad like said above)
  - gmfawcett 2y ago
    > in the sense that their return type doesn't fully describe what the code does Sure they do, at least in Haskell. Bottom inhabits all types.
    - nextaccountic 2y ago
      There's a difference between "doesn't return because it has an infinite loop" and "doesn't return because it threw an exception" Haskell can't express the difference, but languages with effects, like Koka and F*, can! The first effect is called div in Koka and the second is called exn, section 2.2 here https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
      - gmfawcett 2y ago
        It's fine if the poster above me wishes to change languages. Anyone who chooses to stick with Haskell should get comfortable with the notion that functions can diverge, and accept that this is fully consistent with the Haskell type system. The return types may seem unhelpful, but they are accurate.

tome 2y ago

You're right: "pure" is not a well-defined concept. The well-defined concept that describes Haskell's benefits in this regard is "referential transparency". That means that this code let x = <definition of x> in ... x ... x ... (i.e. defining a variable x and then using it some number of times) is equivalent to ... <definition of x> ... <definition of x> ... Seen in the opposite direction (transforming the bottom code to the top code) this means that extracting repeated code is always a valid thing to do. It's not valid in most other languages, and certainly no mainstream ones.

simiones 2y ago
Well, technically that isn't true if you use, for example, unsafePerfomIO in the defintion of x. Referential transparency is still a spectrum, just like purity. Haskell is much closer to purity than the vast majority of languages out there. Also, even if Haskell were perfectly pure, the fact that it uses lazy evaluation is far more important to actually being able to make use of referential transparency. In a strict language you will still see a massive performance differences if replacing the first version with the second, in the most common cases.
- tome 2y ago
  > technically that isn't true if you use, for example, unsafePerfomIO in the defintion of x Ah, well, regardless of whether it holds in Haskell, referential transparency is a well-defined concept. Purity is not a well-defined concept (at least as far as I know. Please share a formal definition if you have one!). That's primarily what I'm trying to say. But I also disagree with your point about unsafePerformIO. In practice, nothing in Haskell violates referential transparency in a significant way. Who knows why? It's an emergent phenomenon that in principle need not have occurred, but in practice it did. Debug.Trace and similar are about the only things that technically violate referential transparency (and they are extremely tame). > the fact that it uses lazy evaluation is far more important to actually being able to make use of referential transparency Yes, I agree with that.
  - simiones 2y ago
    It seems that someone did come up with a formal definition to try to capture the concept [0], though I haven't looked into the details to see whether it really matches the colloquial use of the terms "pure" and "impure" functional programming. In short, the formal definition they came up with is that a language is pure if the result of a valid program is the same under any parameter passing strategy. I should note that I agree that, in practice, Haskell is almost always pure and/or referentially transparent. I was just pointing out that technically the GP was correct that it's not perfectly 100% so. [0] https://www.cambridge.org/core/journals/journal-of-functional-programming/article/what-is-a-purely-functional-language/3A39D50DA48F628D17D9A768A1FA39C3 https://www.cambridge.org/core/journals/journal-of-functiona...
    - tome 2y ago
      Sabry's definition of "pure" fails to satisfy me for two reasons: 1. It assumes that the language is "a conservative extension of the simply typed λ-calculus". That's rather high-powered yet also really restrictive! Haskell doesn't satisfy that requirement. It also assumes the language has functions. Expression languages (i.e. ones without functions) are perfectly reasonable languages and it makes sense to ask whether they are pure. 2. It assumes that a language putatively has multiple evaluation orders (which I suppose is a consequence of the assumption "It is a conservative extension of the simply typed λ-calculus"). Haskell doesn't have multiple evaluation orders. It has one! (notwithstanding you can influence it with seq/!) If you unpick the essence of what Sabry's really saying you find you can translate it into the Haskell world through imposing two conditions: C1. soundness of the β-axiom (a.k.a. referential transparency) (this plays the role of Sabry's condition that call by need and call by value have the same result). C2. That let x = <definition of x> in ... gives the same result as let !x = <definition of x> in ... whenever the latter terminates. (This plays the role of Sabry's condition that call by name and call by value have the same result.) I omitted this condition from my original. I probably shouldn't have because technically it's required, but it risks getting into the weeds of strictness versus laziness. So Sabry's definition of "pure" is a long-winded and restricted way saying something that can be much more conveniently expressed by C1 and C2. If you disagree with me, please demonstrate a property of purity that can't be deduced from C1 and C2! > I should note that I agree that, in practice, Haskell is almost always pure and/or referentially transparent. I was just pointing out that technically the GP was correct that it's not perfectly 100% so. OK, fine, but I also said the GP was correct! I am keen to point out, however, that exceptions (including division by zero) do not violate referential transparency (and if someone thinks they violate "purity" that may be a sign that "purity" is ill-defined).

afiori 2y ago

I feel like exceptions where added as a mix of "look we can do that too" and "maybe if so many functions return optional values then it is going to be too much of a pain to use" In hindsight I think few would now regret not having added them in the first place.

fire_lake 2y ago
> maybe if so many functions return optional values then it is going to be too much of a pain to use I strongly believe that there is a point in the PL design space that makes optionals everywhere usable. Maybe Haskell can still be the language that delivers this.
- tome 2y ago
  To plug my own solution, my effect system Bluefin makes exceptions visible in the type, well-scoped, and also freely composable with all other effects: https://hackage.haskell.org/package/bluefin-0.0.3.0/docs/Bluefin-Exception.html https://hackage.haskell.org/package/bluefin-0.0.3.0/docs/Blu...

afiori 2y ago

>It has unsafe IO primitives To be tongue in cheek then it also has the side effect of heating the CPU.

IshKebab 2y ago

It is pure in the same way that Rust is memory safe. That is too say there are a tiny number of exceptions/escape hatches, but they are not meant to be the norm. Every day programming doesn't involve them. Exceptions aren't impure anyway.

nextaccountic 2y ago
Exceptions define an effect. Code with exceptions aren't actually pure in the sense that their return type doesn't fully describe what the code does, so it doesn't just map an input into an output: there is something else going on In some pure functional languages, the pure fragment doesn't have exceptions, and you add exceptions as an effect (or as a monad) (If you reify the effect with a type like Either or Result, then the code becomes pure: but that's just a monad like said above)
- gmfawcett 2y ago
  > in the sense that their return type doesn't fully describe what the code does Sure they do, at least in Haskell. Bottom inhabits all types.
  - nextaccountic 2y ago
    There's a difference between "doesn't return because it has an infinite loop" and "doesn't return because it threw an exception" Haskell can't express the difference, but languages with effects, like Koka and F*, can! The first effect is called div in Koka and the second is called exn, section 2.2 here https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-20.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
    - gmfawcett 2y ago
      It's fine if the poster above me wishes to change languages. Anyone who chooses to stick with Haskell should get comfortable with the notion that functions can diverge, and accept that this is fully consistent with the Haskell type system. The return types may seem unhelpful, but they are accurate.