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