Syntax extensions: mdo and do...rec

[Levent Erkok]

On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
> > > Don't the laws for loop and mfix justify the transformation?
> >
> > The loop axioms do, but Levent didn't assume right tightening, which
> > corresponds to moving bindings down from a rec, because monads like
> > exceptions don't satisfy it.  The same would go for a loop defined on
> > an exception arrow.  And that's the biggest problem with implicit
> > segmentation: you need to understand what it does to work out the
> > meaning of your program.  Again there's an example in those papers
> > and Levent's thesis.

Given most practical monads don't have mfix's that satisfy right
shrinking, I think segmentation is a must. But as Ross points out, you
need to be careful: It's very practical from a programmers perspective
(just let the compiler figure out minimal segments--I can't think of a
single case where a programmer would want larger blocks, and if he does
there's a way to do that too, just use explicit mfix calls or use the new 
"rec" syntax). On the other hand, if you're reasoning about mdo
expressions you've to be careful in finding the segments yourself. It's
not hard at all, but requires some care. 

> I expected any problems would be like that. I remember hearing about a
> fixpoint operator for the continuation monad that satisfied all the laws
> but right tightening. Well, this would fall under "If it really turns out
> to be frequently necessary".

The closest I know of an mfix for the continuation monad was designed by
Magnus Carlsson. He's implementation relies on a
continuation monad that is built on top of a monad that supports
references. He claimed (proved?) that left-shrinking was not satisfiable
in the presence of callcc. Magnus can provide more details. There's also a
similar argument along those lines in my thesis as well (chapter 5).

Another approach to value recursion was recently given by Sabry and Moggi
in their latest FICS paper: They have an mfix-like operator for
continuations there, but it doesn't satisfy left-shrinking either.
(Their treatment of value recursion is rather different than ours as
well.) See Amr Sabry's papers for details. 

> > BTW, in GHC 6.2 with the -fglasgow-exts -farrows flags, you will be able
> > to use either mdo or do...rec for monads and for arrows, as an experiment.
> > (Maybe "rec" wasn't such a great keyword to take from the identifier
> > space.)

"rec" is nice to have, but I think the "proc" notation also needs a
corresponding "mproc" to do the automatic segmentation. The end
programmers need not worry about extra "recs," it just adds another level
of complexity (just like the let/let rec discussion). Ross: any plans on
implementing that?

-Levent.