Opened 2 years ago

Last modified 9 months ago

#13906 new bug

ApplicativeDo doesn't handle existentials as well as it could

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.0.1
Keywords: ApplicativeDo Cc: simonmar
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

ApplicativeDo doesn't work nicely with existentials or GADTs. This was first considered in #13242, but I think it's worth reconsidering in light of #13875. In particular, we no longer need to think specially about whether a particular pattern match reveals evidence, as any pattern match that does so must necessarily be strict. Simon Marlow explains (in revised, I-think-unmerged, documentation) that

    data T where A :: forall a . Eq a => a -> T

    test = do
      A x <- undefined
      _ <- return 'a'
      _ <- return 'b'
      return (x == x)

will not typecheck because it is first rearranged to

    test =
      (\x _ -> x == x)
        <$> do A x <- undefined; _ <- return 'a'; return x
        <*> return 'b'

This is weird! The more human-obvious rearrangement would work just fine:

    test = do
      A x <- undefined
      (\_ _ -> x == x) <$> return 'a' <*> return 'b'

How can we get there? I think it's actually easy. Suppose we have

  do
    p1 <- e1
    p2 <- e2
    p3 <- e3
    p4 <- e4
    p5 <- e5
    e6

Before starting the detailed dependency analysis and such, let's look just at which patterns are strict. If a pattern is strict, then every following action must be seen as depending on it, and therefore its bindings and evidence can scope over everything else. Let's say that p3 is strict. Then we can immediately transform the expression to

  do
    p1 <- e1
    p2 <- e2
    e3 >>= \case
              p3 -> do
                      p4 <- e4
                      p5 <- e5
                      e6
              -- if refutable
              _ -> fail ...

and then continue the process in the inner do block.

If this is done as an initial pass, then further rearrangement doesn't need to consider the possibility of strict patterns; there won't be any.

Change History (8)

comment:1 Changed 2 years ago by simonmar

Well ok, but we're a bit down in the weeds here! Some other more important improvements we could make to ApplicativeDo are e.g. #10892 and #10976.

comment:2 Changed 2 years ago by dfeuer

Copied from Phab:D3691:

simonmar:

But the proposal in Trac #13906 loses some opportunities for parallelism. e.g.

do
  T x1 <- A
  x2 <- B[x1]
  T x2 <- C
  x4 <- D[x2]
  return (x2,x4)

and we want to get (A;B) | (C;D), not (A; (B|C); D)


dfeuer:

We do? I think we don't. Suppose we have

do
  () <- m
  n

Surely we only want to perform n if m successfully produces non-bottom (). The dependency is implicit. To get the parallelism, you need to eliminate the strict binding.

comment:3 Changed 2 years ago by simonmar

Right, but we only need to ensure that a strict pattern match is bound by a >>=. In my example:

do
  T x1 <- a
  x2 <- b x1
  T x2 <- c
  x4 <- d x2
  return (x2,x4)

we can safely translate this to:

(\x2 x4 -> (x2,x4)) <$> (a >>= \(T x1) -> b x1) <*> (c >>= \(T x2) -> d x2)

and this has the correct strictness behaviour. I won't write it all out here, but I'm sure you can see that if you expand out using <*> = ap and apply some other laws then you'll get the right sequence of binds here.

This translation is better (i.e. has lower cost, in the terminology of the ApplicativeDo paper) than the one we'd get if we just started by breaking up the original sequence at every strict pattern match.

comment:4 Changed 2 years ago by simonpj

Doesn't #13875 make all this moot? All patterns binding existentils are srtrict, so (in my imperfect undersatnding) we have to do a monadic bind, at the expense of parallelism, but making it straightforward to keep existentials in scope.

I'm beginning to think that an update of the paper, covering strict patterns and existentials in the vocabulary and notation of the paper, would be a good investment. I'm getting lost!

comment:5 in reply to:  3 Changed 2 years ago by dfeuer

Replying to simonmar:

Right, but we only need to ensure that a strict pattern match is bound by a >>=.

Ah, now I see what you're saying! I was misled by the fact that b and d are applied to x1 and x2. What you were getting at is that by simply making the very next action "dependent" on a strict pattern match, you propagate strictness from the result level to the action level and rely on the fact that strict monads have undefined *> a = undefined. Does that hold up for reader, for example? It doesn't for lazy State, but the latter isn't strictly law-abiding, so you're in the clear there.

comment:6 Changed 20 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:7 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed by GHC 8.6.

comment:8 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.