[Haskell-cafe] On the purity of Haskell

[David Sabel]

A perhaps acceptable notion of the property we want (purity etc.) is
that all the extensions of the purely functional core language of Haskell
(say the lazy lambda calculus extended with data constructors, etc) are
_conservative_, that is all the equations that hold
in the pure core language still hold in the extended language.

For a part of Concurrent Haskell such a conservativity result is shown in
  D.Sabel , M. Schmidt-Schauß. On conservativity of Concurrent Haskell. 
Frank report 47, 2011.
http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-47.pdf
It also shows that with arbitrary use of unsafeInterleaveIO 
conservativity does not hold.

And of course the result does not capture any IO-operation (only 
takeMVar, putMVar and spawning threads are considered),
but it may be extended to more operations ...

Just my two cents,
  David

On 30.12.2011 02:07, Conal Elliott wrote:
> I wrote that post to point out the fuzziness that fuels many 
> discussion threads like this one. See also 
> http://conal.net/blog/posts/notions-of-purity-in-haskell/ and the 
> comments.
>
> I almost never find value in discussion about whether language X is 
> "functional", "pure", or even "referentially transparent", mainly 
> because those terms are used so imprecisely. In the notions-of-purity 
> post, I suggest another framing, as whether or not a language and/or 
> collection of data types is/are "denotative", to use Peter Landin's 
> recommended replacement for "functional", "declarative", etc. I 
> included some quotes and a link in that post. so people can track down 
> what "denotative" means. In my understanding, Haskell-with-IO is not 
> denotative, simply because we do not have a (precise/mathematical) 
> model for IO. And this lack is by design, as explained in the "toxic 
> avenger" remarks in a comment on that post.
>
> I often hear explanations of what IO means (world-passing etc), but I 
> don't hear any consistent with Haskell's actual IO, which includes 
> nondeterministic concurrency. Perhaps the difficulties could be 
> addressed, but I doubt it, and I haven't seen claims pursued far 
> enough to find out.
>
>   - Conal
>
> On Thu, Dec 29, 2011 at 4:42 PM, Steve Horne 
> <sh006d3592 at blueyonder.co.uk <mailto:sh006d3592 at blueyonder.co.uk>> wrote:
>
>     On 30/12/2011 00:16, Sebastien Zany wrote:
>>     Steve Horne wrote:
>>
>>         I haven't seen this view explicitly articulated anywhere before
>>
>>
>>     See Conal Elliott's blog post The C language is purely functional
>>     <http://conal.net/blog/posts/the-c-language-is-purely-functional>.
>     Thanks - yes, that's basically the same point. More concise - so
>     clearer, but not going into all the same issues - but still the
>     same theme.
>
>     _______________________________________________________
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120102/411952f0/attachment.htm>