4 ms·

I don't object to purity, I want to know what it means. I didn't realise that this is not a well-understood concept. (I mentioned Sabry's definition of purity

by mafribe 11y ago

I don't object to purity, I want to know what it means. I didn't realise that this is not a well-understood concept. (I mentioned Sabry's definition of purity which I found surprising.) The original discussion started because somebody complained that Haskell programmers often appear unable to transliterate imperative algorithms. I assume that this complaint was about transliteration into pure Haskell (whatever that may mean exactly). Clearly transliteration into full Haskell with actual mutability is possible. I mentioned Pippenger's article to bring to the debate the idea that the question whether such transliteration is always possible is an open research problem.

tome 11y ago
I don't think anyone knows a solid definition of purity. It certainly refers to at least two things (1. independence of order of evaluation, 2. no side effects) and informally speaking we often "know" what it is in a particular context, but writing down a formal definition is very hard. I'm certainly not satisfied with Sabry's definition. I don't like the idea that you have to have both a strict and a non-strict evaluation for your language.
- mafribe 11y ago
  If nobody knows what purity means, then what are all those tortured discussions on whether Haskell is pure or not about? ... Anyway, I'm a bit unhappy about the requirement of full evaluation order independence, because even the purest of pure languages (e.g. the untyped lambda-calculus or PCF) don't have full evaluation order independence. I guess you mean evaluation order independence modulo termination? My intuition is that pure means that all language expressions M can always be evaluated locally by just looking at the meaning of all subterms of M. In terms of Hoare logic (for total correctness) that would mean that the pre-condition speaks only about the termination of the free variables of M (sorry for being so terse, I think this can be made formal).
  - dllthomas 11y ago
    Usually this is the way words work - we notice a regularity in the environment we wish to refer to; we build a sense of it, usually motivated by some examples and counterexamples; we give it a handle; and we then try to find a definition that matches our intuition. There certainly seem to be regularities that "pure" is intended to point at in this context, but it definitely seems that we've not settled on a definition, and we may not even agree on examples. The notions of purity I was pointing at was any that entailed the restrictions in the paper you'd linked. There are restrictions of Haskell that are pure in those senses, but Haskell taken as a whole is not, even without invoking anything unsafe.
  - tome 11y ago
    > If nobody knows what purity means, then what are all those tortured discussions on whether Haskell is pure or not about? ... They're about what purity means!
dllthomas 11y ago
"I assume that this complaint was about transliteration into pure Haskell (whatever that may mean exactly). Clearly transliteration into full Haskell with actual mutability is possible." Ah, if you'd made that assumption explicit I would not have objected. I don't see anywhere the querent suggesting that his translation demand invoked any notion of purity. If it did, then certainly he was asking a harder question than he presented, although even in that case a naive translation could have trivially produced an O(m n lg(n)) solution and O(m^n) should quite reasonably be considered failure. I think the issue in the main is that relatively novice Haskell developers are likely to be the most eager to try and translate arbitrary code on demand in #haskell.

by mafribe 11y ago

tome 11y ago

I don't think anyone knows a solid definition of purity. It certainly refers to at least two things (1. independence of order of evaluation, 2. no side effects) and informally speaking we often "know" what it is in a particular context, but writing down a formal definition is very hard. I'm certainly not satisfied with Sabry's definition. I don't like the idea that you have to have both a strict and a non-strict evaluation for your language.

mafribe 11y ago
If nobody knows what purity means, then what are all those tortured discussions on whether Haskell is pure or not about? ... Anyway, I'm a bit unhappy about the requirement of full evaluation order independence, because even the purest of pure languages (e.g. the untyped lambda-calculus or PCF) don't have full evaluation order independence. I guess you mean evaluation order independence modulo termination? My intuition is that pure means that all language expressions M can always be evaluated locally by just looking at the meaning of all subterms of M. In terms of Hoare logic (for total correctness) that would mean that the pre-condition speaks only about the termination of the free variables of M (sorry for being so terse, I think this can be made formal).
- dllthomas 11y ago
  Usually this is the way words work - we notice a regularity in the environment we wish to refer to; we build a sense of it, usually motivated by some examples and counterexamples; we give it a handle; and we then try to find a definition that matches our intuition. There certainly seem to be regularities that "pure" is intended to point at in this context, but it definitely seems that we've not settled on a definition, and we may not even agree on examples. The notions of purity I was pointing at was any that entailed the restrictions in the paper you'd linked. There are restrictions of Haskell that are pure in those senses, but Haskell taken as a whole is not, even without invoking anything unsafe.
- tome 11y ago
  > If nobody knows what purity means, then what are all those tortured discussions on whether Haskell is pure or not about? ... They're about what purity means!

dllthomas 11y ago

"I assume that this complaint was about transliteration into pure Haskell (whatever that may mean exactly). Clearly transliteration into full Haskell with actual mutability is possible." Ah, if you'd made that assumption explicit I would not have objected. I don't see anywhere the querent suggesting that his translation demand invoked any notion of purity. If it did, then certainly he was asking a harder question than he presented, although even in that case a naive translation could have trivially produced an O(m n lg(n)) solution and O(m^n) should quite reasonably be considered failure. I think the issue in the main is that relatively novice Haskell developers are likely to be the most eager to try and translate arbitrary code on demand in #haskell.