">>" and "do" notation

[John Hughes]

	> 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. ... If we can give >> a more efficient
	> implementation, which constructs a better representation
	> than >>=3D 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.

That's true, of course. But *should* we insist that the programming language
guarantee that abstractions are always respected? i.e. equivalent
representations are always treated equivalently? We don't always in other
contexts. To take an example, consider a bag datatype with a bagFold operator
and an Eq instance that implements bag equality. Then

    xBag =3D=3D yBag

doesn't necessarily imply

    bagFold op z xBag =3D=3D bagFold op z yBag

We rely on the programmer to use bagFold properly, i.e. supply an AC op with
unit z. If he doesn't, the abstraction is broken.

	> 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 >>=3D, 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 >!=3D 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} =3D=3D do {A; B}.

	  J=F3n

This is a much bigger cost than you make out. Making something into a monad
allows not only the use of the do syntax, it allows the use of a large number
of generic monad operations, the application of monad transformers, etc
etc. It's a big deal.

I agree there's an analogy here with type-checking here. Indeed, there's a
tradeoff where typechecking is concerned too: we give up some flexibility for
greater safety. We accept that nowadays, because the flexibility we give up
with Hindley-Milner typing is not so great, and the gain in safety is
considerable. But would you argue that we should prohibit programs which
potentially break an abstraction?  I.e. prohibit bagFold, or alternatively
allow it only for operators which the compiler can *decide* are AC? Would you
want to prohibit monad instances which the compiler cannot decide satisfy the
monad laws? I know you would want to prohibit monad instances where the
compiler cannot decide that >> and >>=3D are properly related.

The trouble is that prohibiting bagFold, separate definitions of >>,
etc. altogether is quite a big cost: such things are very useful! Yet we lack
the analogue of the Hindley-Milner type system -- a way for the compiler to
*decide* that a monad instance, an ADT definition, or whatever, is OK, which
is *proven* sufficiently flexible to handle almost all practical cases. In its
absence, the analogy with type-checking is not compelling. If all we had was a
monomorphic type system, then I would be against imposing type-checking too.

Perhaps there's an interesting research direction here for somebody...

John