>If (as a human reader of a programme) I see > >do a <- thing1 > <expression> > >and I notice (perhaps after some modifications) that a is >not present in <expression>, then I /really/ don't want a >change to > >do thing1 > <expression> > >to change the meaning of the programme. I think the point that's being missed in this discussion is that a monad is an *abstract* type, and sometimes the natural "equality" on the abstract type is not the same as equality on representations. Of course, we want the left and right hand sides of the monad laws to have the same "meaning", and we want >> to "mean" >>= \_ ->, but this meaning is really up to the abstract equality, not the concrete one. If we can give >> a more efficient implementation, which constructs a better representation than >>= does, that's fine, as long as the two representations "mean" the same thing. To be specific, the application that kicked off this discussion was program generation. In this example, it's not important that >> and >>= generate the same *program text*, the important thing is that they generate equivalent programs. If >> can more easily generate a more efficient program, that's fine. There's another example in QuickCheck, where we use a monad Gen for random value generation -- Gen a is a generator for random values of type a. Gen does not satisfy the monad laws: for example, g and g >>= return will usually generate different values. But viewed as *probability distributions* (which is how we think of them), they are the same. "Morally", Gen is a monad. This is all perfectly respectable, and has to do with the fact that Haskell is a programming language, not mathematics -- so we represent equivalence classes by values chosen from them. For the *language* to rule out constructing different representations for "equivalent" constructions, such as >> and >>=, would be unreasonable. John Hughes
On Tue, 2 Apr 2002 10:00:37 +0200 (MET DST), John Hughes <rjmh@cs.chalmers.se> wrote:
If (as a human reader of a programme) I see
do a <- thing1 <expression>
and I notice (perhaps after some modifications) that a is not present in <expression>, then I /really/ don't want a change to
do thing1 <expression>
to change the meaning of the programme.
I think the point that's being missed in this discussion is that a monad is a n *abstract* type, and sometimes the natural "equality" on the abstract type is not the same as equality on representations. Of course, we want the left and right hand sides of the monad laws to have the same "meaning", and we want >> to "mean" >>= \_ ->, but this meaning is really up to the abstract equality, not the concrete one. If we can give >> a more efficient implementation, whic h constructs a better representation than >>= does, that's fine, as long as the two representations "mean" the same thing.
Point taken, but I remain unconvinced. What comes out of the monad /isn't/ abstract; there's nothing to ensure that subsequent use respects the abstraction.
To be specific, the application that kicked off this discussion was program generation. In this example, it's not important that >> and >>= generate the same *program text*, the important thing is that they generate equivalent programs. If >> can more easily generate a more efficient program, that's fine.
Is it fine though? Since it will be possible to inspect the generated code, it's possible that a change from do {_ <- A; B} to do {A; B} can radically alter the subsequent behaviour of the programme.
There's another example in QuickCheck, where we use a monad Gen for random value generation -- Gen a is a generator for random values of type a. Gen doe s not satisfy the monad laws: for example, g and g >>= return will usually generate different values. But viewed as *probability distributions* (which i s how we think of them), they are the same. "Morally", Gen is a monad.
Well, aren't there cases where generating the /same/ pseudo-random sequences is important? In such a case, making what looks like a semantically neutral change to the programme might invalidate years of stored results.
This is all perfectly respectable, and has to do with the fact that Haskell i s a programming language, not mathematics -- so we represent equivalence classe s by values chosen from them. For the *language* to rule out constructing different representations for "equivalent" constructions, such as >> and >>=, would be unreasonable.
Here's the problem. Your argument sounds very similar to the one against type checking. That /you/ can get it right doesn't encourage me to believe that J Random Hacker isn't going to abuse the facility. It's not as if you couldn't define >!= and >! for something that's nearly a monad, it would just stop you using the do notation, which is, I think fair, since Haskell provides no way of selecting the correct form of equality for do {_ <- A; B} == do {A; B}. Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk 31 Chalmers Road jf@cl.cam.ac.uk Cambridge CB1 3SZ +44 1223 570179 (after 14:00 only, please!)
On Tue, Apr 02, 2002 at 08:48:41PM +0100, Jon Fairbairn wrote:
Point taken, but I remain unconvinced. What comes out of the monad /isn't/ abstract; there's nothing to ensure that subsequent use respects the abstraction.
Sure. That's the programmer's responsibility to keep track of. To me the situation seems entirely analogous to defining a '+' operation that is not associative; if the programmer wants to do it, more power to her. (In fact, the standard '+' on floating point numbers is not associative. Sometimes it matters!) These considerations are the reasons compilers are typically prohibited from taking advantage of such laws, and why the translation from the 'do' notation should be the obvious one (using '>>'). Best, Dylan Thurston
participants (3)
-
Dylan Thurston -
John Hughes -
Jon Fairbairn