">>" and "do" notation

John Hughes rjmh@cs.chalmers.se
Tue, 2 Apr 2002 10:00:37 +0200 (MET DST)


	>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