[Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:21 AM, Conal Elliott wrote:

> 
> And I also raised a more fundamental question than whether this claim of sameness is true, namely what is equality on IO? Without a precise & consistent definition of equality, the claims like "f 42 == f (43 - 1)" are even defined, let alone true. And since the conversation is about Haskell IO, I'm looking for a definition that applies to all of IO, not just some relatively well-behaved subset like putchar/getchar+IORefs+threads.

Well, you'll no doubt be glad to know I think I've said about all I need to say on this topic, but I'll add one more thing.  Threads like this I often find useful even when I disagree vehemently with various parties.  In this case an old idea I'd forgotten about was suddenly dislodged by the discussion.  A few years ago - the last time I got involved in a discussion on Haskell semantics - I spent some time sketching out ideas for using random variables to provide definitions (or at least notation) for stuff like IO.  I'm not sure I could even find the notes now, but my recollection is that it seemed like a promising approach.  One advantage is that this eliminates the kind of informal language (like "user input") that seems unavoidable in talking about IO.  Instead of defining e.g. readChar or the like as an "action" that does something and returns an char (or however standard Haskell idiom puts it), you can just say that readChar is a random char variable and be done with it.  The notion of "doing an action" goes away.  The side-effect of actually reading the input or the like can be defined generically by saying that evaluating a random variable always has some side-effect; what specifically the side effect is does not matter.  I mention this as a possible approach for anybody looking for a better way of accounting for IO in Haskell.

Cheers,

Gregg