RE: Syntax extensions: mdo and do...rec
I agree with this. We'll move GHC to implement any consensus. My own opinion is that expr :: = ... | do { stmts } stmts :: = .. | rec { stmts } is the cleanest story. I guess that we should ensure that do rec { stmts } means what it looks like. Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of | nilsson@cs.yale.edu | Sent: 16 September 2003 18:09 | To: haskell@haskell.org | Subject: Syntax extensions: mdo and do...rec | | Dear Haskellers, | | A questions. | | The do-notation has been extended to support recursive bindings by using | the "mdo" keyword. The do-notation has also been extended (through Ross | Patterson's preprocessor, and now also GHC) to support programming | with arrows. In that context, a different syntax, using the keyword "rec", | is used to enable recursive bindings. | | It seems somewhat confusing to have distinct syntax for what appears | to be very closely related purposes. Would it be possible have just a | single syntactic extension to enable recursive bindings in either context? | (Presumably the "rec" version is a bit more flexible in that it can be | applied to a subset of the bindings in a do-construct.) | | Best regards, | | /Henrik | | -- | Henrik Nilsson | Yale University | Department of Computer Science | nilsson@cs.yale.edu | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
hello, i have no strong feelings about that either way, however since in haskell we do not have "let" vs "let rec" distinctions, perhaps we should not have "do" vs "do rec" distinction. this of course would break programs relying on shadowing (and at least i write quite a few of those, but that is mostly habit). i doubt that this will cause many backward compatability problems, as one can compile old modules (not using recursive do) without the flag enabling recursive dos. bye iavor Simon Peyton-Jones wrote:
I agree with this. We'll move GHC to implement any consensus.
My own opinion is that expr :: = ... | do { stmts }
stmts :: = .. | rec { stmts }
is the cleanest story. I guess that we should ensure that
do rec { stmts }
means what it looks like.
Simon
| -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of | nilsson@cs.yale.edu | Sent: 16 September 2003 18:09 | To: haskell@haskell.org | Subject: Syntax extensions: mdo and do...rec | | Dear Haskellers, | | A questions. | | The do-notation has been extended to support recursive bindings by using | the "mdo" keyword. The do-notation has also been extended (through Ross | Patterson's preprocessor, and now also GHC) to support programming | with arrows. In that context, a different syntax, using the keyword "rec", | is used to enable recursive bindings. | | It seems somewhat confusing to have distinct syntax for what appears | to be very closely related purposes. Would it be possible have just a | single syntactic extension to enable recursive bindings in either context? | (Presumably the "rec" version is a bit more flexible in that it can be | applied to a subset of the bindings in a do-construct.) | | Best regards, | | /Henrik | | -- | Henrik Nilsson | Yale University | Department of Computer Science | nilsson@cs.yale.edu | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
-- ================================================== | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | ==================================================
hello,
i have no strong feelings about that either way, however since in haskell we do not have "let" vs "let rec" distinctions, perhaps we should not have "do" vs "do rec" distinction. this of course would break programs relying on shadowing (and at least i write quite a few of those, but that is mostly habit). i doubt that this will cause many backward compatability problems, as one can compile old modules (not using recursive do) without the flag enabling recursive dos.
I think you have a great idea here. The problem with that is that not all monads support recursive bindings. We can deal with that, but the desuagring of a do statement wouldn't be so trivial any more. The most sensible approach I can think of is to analyze the bindings and generate a translation involving mfix if the bindings are recursive, and a translation without if they are not. I don't like complicating the translation, but at least it is still purely syntactic. I'm also worried about making the typing of a statement depend on the binding structure, rather than just the types of subexpressions and how they are used. It's probably a bit simpler than the normal mental typechecking we do, but it is different. If we do this we should try for nice warnings about recursively defined variables if failures to staisfy the MonadFix constraint suggest the do statement was wrong. In any case, I don't see the need for explicit rec groups. Can't GHC just find the strongly connected components like it already does with let bindings? Don't the laws for loop and mfix justify the transformation? If you really need to specify the binding groups (or at least provide an upper bound on their size) you can use explicit nested mdo statements. I don't think we should force the programmer to explicitly identify groups of recursive bindings. It's probably not even worth providing synatx beyond nested mdo statements uness is is frequently necessary. I agree with Iavor that we should try for simplicity and consistency. Are there any gaping holes in my musings on his proposal? Brandon
The arguments being made here can all be found in the recursive monad bindings papers and Levent's thesis. On Wed, Sep 17, 2003 at 11:41:24AM -0700, Brandon Michael Moore wrote:
In any case, I don't see the need for explicit rec groups. Can't GHC just find the strongly connected components like it already does with let bindings?
That's what GHC and Hugs do now for mdo (actually segments rather than components, because actions can't be rearranged).
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. 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.)
On Thu, 18 Sep 2003, Ross Paterson wrote:
The arguments being made here can all be found in the recursive monad bindings papers and Levent's thesis.
I don't remember anything about finding smaller binding groups in the mdo paper. I don't think I've read Levent's thesis.
On Wed, Sep 17, 2003 at 11:41:24AM -0700, Brandon Michael Moore wrote:
In any case, I don't see the need for explicit rec groups. Can't GHC just find the strongly connected components like it already does with let bindings?
That's what GHC and Hugs do now for mdo (actually segments rather than components, because actions can't be rearranged).
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.
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".
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.)
When can we expect 6.2? Brandon
Sorry, I forgot the main question I was raising. Even if we need something other than mdo, do we need to make a distinction between do and mdo? If left tightening is satisfied then do and mdo are equivalent for nonrecursive blocks. If we are willing to give up shadowing a compiler could translate recursive blocks with mfix and non-recursive blocks without. Personally I don't like shadowing, and especially don't like reursive bindings some places and shadowing in others. On the necessity of rec syntax, how is a statement like do rec binds1 rec binds2 stmts different from do BV1 <- mdo binds1 return BV1 BV2 <- mdo binds2 return BV2 stmts where BVn is a tuple of all the variables bound in bindsn. Brandon
On the necessity of rec syntax, how is a statement like do rec binds1 rec binds2 stmts different from do BV1 <- mdo binds1 return BV1 BV2 <- mdo binds2 return BV2 stmts where BVn is a tuple of all the variables bound in bindsn.
These two expressions are semantically different if your mfix doesn't satisfy the right shrinking property. (Note that right shrinking is not an assumed property for value recursion operators.) Examples: IO/Maybe/Strict-state/Lists and many others don't satisfy right-shrinking. (On the other hand more "well-behaved" monads like: Environments/Lazy State/Identity etc satisfy right-shrinking). There's a theorem stating that (roughly) any monad based on a disjoint sum with more than one constructor will fail this property. The problem is that in the first expression "rec binds1" and "rec binds2" might fail to terminate while the "mdo" forms in the second expression can terminate due to segmentation. If your mfix satisfies right-shrinking, then they are provably equivalent. Note that rec means "just wrap mfix" around these binders, while "mdo" means perform segmentation and find minimum "rec" blocks. This stuff is all explained in the Haskell Workshop paper, or chapter 7 of my thesis, all available at: http://www.cse.ogi.edu/pacsoft/projects/rmb (The thesis is more up-to-date with respect to terminology. Also the "rec" keyword is not mentioned anywhere in those papers since that was a last minute addition by Simon PJ inspired by Ross's arrow notation.) -Levent.
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.
On Mon, Sep 29, 2003 at 07:31:33AM -0700, Levent Erkok wrote:
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?
It's in the bit you re-quoted (not "mproc" but "mdo" inside "proc").
On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
The problem with that is that not all monads support recursive bindings. We can deal with that, but the desuagring of a do statement wouldn't be so trivial any more. The most sensible approach I can think of is to analyze the bindings and generate a translation involving mfix if the bindings are recursive, and a translation without if they are not. I don't like complicating the translation, but at least it is still purely syntactic.
I'm also worried about making the typing of a statement depend on the binding structure, rather than just the types of subexpressions and how they are used. It's probably a bit simpler than the normal mental typechecking we do, but it is different. If we do this we should try for nice warnings about recursively defined variables if failures to staisfy the MonadFix constraint suggest the do statement was wrong.
In any case, I don't see the need for explicit rec groups. Can't GHC just find the strongly connected components like it already does with let bindings? Don't the laws for loop and mfix justify the transformation? If you really need to specify the binding groups (or at least provide an upper bound on their size) you can use explicit nested mdo statements.
I don't think we should force the programmer to explicitly identify groups of recursive bindings. It's probably not even worth providing synatx beyond nested mdo statements uness is is frequently necessary. I agree with Iavor that we should try for simplicity and consistency. Are there any gaping holes in my musings on his proposal?
We were rooting for a single "do" construct that'll capture recursion automatically from the start. However, there are a couple of issues: 1. Shadowing (you've already pointed that out.) 2. Polymorphic let bindings inside the do notation, when they are used in a prior statement. (This complicates things quite a bit from type-checking perspective.) 3. The need for automatic segmentation to overcome right-shrinking issues. (Not a real problem in reality, but at least "mdo" makes it obvious that something different is going on.) After much discussion, the consensus was to keep recursive-do separate at least for the time being. Maybe Haskell-2 can incorporate it right away without the need for "mdo." Again, all this stuff is discussed in chapter 7 of the thesis (especially section 7.2), available at: http://www.cse.ogi.edu/pacsoft/projects/rmb -Levent.
participants (5)
-
Brandon Michael Moore -
Iavor Diatchki -
Levent Erkok -
Ross Paterson -
Simon Peyton-Jones