On Fri, 2011-12-30 at 12:45 -0600, Gregg Reynolds wrote:
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.
Isn't this just another way of saying the same thing that's been said already? It's just that you're saying "random variable" instead of "I/O action". But you don't really mean random variable, because there's all this stuff about side effects thrown in which certainly isn't part of any idea of random variables that anyone else uses. What you really mean is, apparently, I/O action, and you're still left with all the actual issues that have been discussed here, such as when two I/O actions (aka random variables) are the same. There is one difference, and it's that you're still using the term "evaluation" to mean performing an action. That's still a mistake. Evaluation is an idea from operational semantics, and it has nothing to do with performing effects. The tying of effects to evaluation is precisely why it's so hard to reason about programs in, say, C denotationally, because once there is no such thing as an evaluation process, modeling the meaning of terms becomes much more complex and amounts to reinventing operational semantics in denotational clothing)\. I'd submit that it is NOT an advantage to any approach that the notion of doing an action goes away. That notion is *precisely* what programs are trying to accomplish, and obscuring it inside functions and evaluation rather than having a way to talk about it is handicapping yourself from a denotational perspective. Rather, what would be an advantage (but also rather hopeless) would be to define the notion of doing an action more precisely. -- Chris Smith