3 ms·
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 th
by 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 agoUsually 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!