#4148: improve new recursive do syntax
---------------------------------+------------------------------------------
Reporter: guest | Owner:
Type: feature request | Status: new
Priority: low | Milestone: 7.6.1
Component: Compiler | Version: 6.12.3
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Comment(by lerkok):
Apologies for the rather long comment below. It's my personal view and I'm
probably a bit biased towards the very original translation of mdo-
expressions for historical reasons. I'm hoping others will find it useful
in shedding some light onto at least the original motivations for the
segmentation aspect of mdo, which seems to be the main source of
discontent here..
Segmentation was part of the very original transformation proposed for mdo
expressions for a very simple reason: The right-shrinking property of mfix
only holds for very few monads of practical interest. Without right-
shrinking, the knot-tying loop implied by mfix cannot be loosened on the
right without changing termination properties. This aspect is well studied
in the literature: In fact, there's a very generic theorem stating that no
monad based on a disjoint sum type admits a value recursion operator that
satisfies the right-shrinking property. (See proposition 3.1.6 of
http://goo.gl/Dj6CO, for instance.) A similar concern arises in the
context of traces over premonoidal categories, as found in Nick Benton's
work, and also in Ross Patterson's arrow-fix axiomatization; for instance
when one considers the fixed-point operator for he Kleisli arrow of a
monad, as derived from the mfix of the underlying monad.
The question then becomes what is the user intended meaning of such
expressions, when used with a monad that doesn't satisfy the right-
shrinking property? There's a rough analogy here with typing of recursive
binding groups: When a recursive binding group is typed (i.e., a let/where
expression), Haskell says that recursively dependent groups must be
identified and typed separately. This improves polymorphism. If you don't
do the grouping, then you'll get less polymorphic types. Not doing this
would be confusing for the user, since seemingly irrelevant bindings in a
group shouldn't change what types are assigned to other bindings. If you
don't do this "segmentation" during typing, then you'll get less
polymorphic types, which would be arguably not what the user wanted in the
first place.
We (John Launchbury and myself) had precisely the same motivation when the
original mdo was designed: If there's a recursive binding group, then the
"knot" should be tied over the minimal segment necessary to resolve the
recursive binding. If you do not do this, then textually irrelevant
recursive bindings can change the meaning of one another, which can be
quite confusing for the user. (There's a simple example of this in Section
7.2.2 of
http://goo.gl/Dj6CO.) So, in this sense, grouping of recursive
bindings for typing purposes in ordinary let/where expressions and
grouping of recursive segments in an mdo-expression serve the same purpose
of capturing the alleged user intent as closely as possible.
One valid argument against the above claim could be that the polymorphic
type improvement is a change to the static semantics, while the
segmentation in mdo is a change to the dynamic semantics. This is true.
However, the point remains that language constructs should reflect what
the user intends to say.
Furthermore, I see no reason why an mdo expression should say that all the
bindings should be in one big knot-tying loop; Just like I wouldn't expect
GHC to wrap around one big call to "fix" around any purely recursive group
of definitions. Recall that the good old "fix" is *the* mfix for the
identity monad, and when we write a recursive "let" binding, we can
consider it as an mdo-binding over the identity monad. Just like we'd
fully expect to see separate fix'es around different recursive bindings
when we write code in the identity monad implicitly provided by let/where
bindings, I'd expect to see separate fix'es (i.e., mfix calls) when I
happen to use some other monad. That is, I don't see why other monads
should be discriminated, as compared to the identity monad.
(The same line of thought would also say we should have just one "do"
expression that handles both recursive and non-recursive variants, just
like we do not have separate let/letrec expressions in Haskell. However, I
think changing "do" into a construct that also handles recursion is
unrealistic for practical reasons. In particular, due to shadowing, the
change wouldn't be backwards compatible.)
One possible compromise might have been the following: Keep both mdo-
expressions (which will do segmentation), and "rec" segments, which will
not do segmentation. Unfortunately, mdo was removed from GHC a while ago
as Simon commented above; so bringing it back is probably out of question.
Given that, I'd think we should simply let "rec" do the segmentation as it
does currently, giving us the rough equivalence that we can replace "mdo"
with "do rec" (modulo the issue with the last expression has to be
indented appropriately), and keep the segmentation semantics present as
implied by the original mdo. If the user really wants to control where
recursion takes place, then he/she can insert explicit calls to mfix as
appropriate. In other words, if "rec" doesn't do segmentation, then
writing the corresponding "mfix" is probably not asking too much either,
so we should maybe completely drop the whole "rec" business and just live
with explicit mfix calls.
Having said all this, I also think that most of this discussion is rather
moot as well. I'm yet to see anyone bitten by whether mdo (or rec) does
segmentation or not. I believe that segmentation is rather necessary
purely from a language design point of view for doing the right thing,
i.e., matching the user intended semantics. But it's not the end of the
world if we go the other way. Bringing back the good old "mdo" expresions
would make me happy, but I can't say that it's a high priority by any
means.
Again, apologies for the long post and thanks for reading through my
personal account of the matter. To state my position on this matter, I
think the best solution would be to bring back mdo-expressions with full
segmentation, and keep "rec" as well, which doesn't do any segmentation.
However, it sounds like bringing "mdo" back in GHC is quite unlikely, so I
think "rec" should keep doing segmentation so we have at least the rough
correspondence "mdo = do rec".
--
Ticket URL: <
http://hackage.haskell.org/trac/ghc/ticket/4148#comment:11>
GHC <
http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Locked
