Why does a "let" statement force an "applicative do" block into requiring a monad constraint?

Question

Consider this example:

{-# language ApplicativeDo #-}

module X where

data Tuple a b = Tuple a b deriving Show

instance Functor (Tuple a) where
    fmap f (Tuple x y) = Tuple x (f y)

instance Foldable (Tuple a) where
    foldr f z (Tuple _ y) = f y z

instance Traversable (Tuple a) where
    traverse f (Tuple x y) = do
        y' <- f y
        let t' = Tuple x y'
        return $ t'

Looks nice! But no:

[1 of 1] Compiling X                ( X.hs, interpreted )

X.hs:15:9: error:
    • Could not deduce (Monad f) arising from a do statement
      from the context: Applicative f
        bound by the type signature for:
                   traverse :: forall (f :: * -> *) a1 b.
                               Applicative f =>
                               (a1 -> f b) -> Tuple a a1 -> f (Tuple a b)
        at X.hs:14:5-12
      Possible fix:
        add (Monad f) to the context of
          the type signature for:
            traverse :: forall (f :: * -> *) a1 b.
                        Applicative f =>
                        (a1 -> f b) -> Tuple a a1 -> f (Tuple a b)
    • In a stmt of a 'do' block: y' <- f y
      In the expression:
        do y' <- f y
           let t' = Tuple x y'
           return $ t'
      In an equation for ‘traverse’:
          traverse f (Tuple x y)
            = do y' <- f y
                 let t' = ...
                 return $ t'
   |
15 |         y' <- f y
   |         ^^^^^^^^^
Failed, no modules loaded.

Even this fails:

instance Traversable (Tuple a) where
    traverse f (Tuple x y) = do
        y' <- f y
        let unrelated = 1
        return $ Tuple x y'

So, introducing any let statement removes the "applicative" from the "applicative do". Why?

Innocent

Before reading the answers here, I thought this was because of the call to return. So, for future readers, I think it’s worthwhile noting that this still gives an error even when pure is used instead of return. – Spinney

Answer 1

It would translate into

let unrelated = 1 in return $ Tuple x y'

which doesn't have the form return <something>, and applicative do requires the last statement to be a return or pure:

In general, the rule for when a do statement incurs a Monad constraint is as follows. If the do-expression has the following form:

do p1 <- E1; ...; pn <- En; return E

where none of the variables defined by p1...pn are mentioned in E1...En, and p1...pn are all variables or lazy patterns, then the expression will only require Applicative. Otherwise, the expression will require Monad. The block may return a pure expression E depending upon the results p1...pn with either return or pure.

Note: the final statement must match one of these patterns exactly:

return E
return $ E
pure E
pure $ E

otherwise GHC cannot recognise it as a return statement, and the transformation to use <$> that we saw above does not apply. In particular, slight variations such as return . Just $ x or let x = e in return x would not be recognised.

If you look at the description of desugaring in https://gitlab.haskell.org/ghc/ghc/wikis/applicative-do, it also doesn't support let in any way.

Oys

Answer 2

What applicative expression would you like this to desugar to? A monadic expression is a series of chained scopes, so it makes sense for a let to introduce a binding that extends over all the remaining scopes, but with applicative the various expressions can't really depend on each other, so there's no scope that it makes sense to desugar the let into.

Donadonadee

In principle, do x1 <- e1; ... ; xn <- en ; let y = eY ; return eR could desugar to do x1 <- e1; ... ; xn <- en ; return (let y = eY in eR) and from there to applicative notation (when possible). We could also do that for let y=eY; xi <- ei part, but we would need to require that eY does not use x(i-1),.... A lot of constraints on "what can be used where" would need to be required, which could be confusing. Hence, it does not look as a very convenient feature. – Squarerigger

Isn't this the same as desugaring to a let around the entire do expression, since the variable being bound can't depend on any of the previous bindings, and can't be used by any following bindings? – Donadonadee

I think so, except for the final return, where you can use the previous bindings. – Squarerigger

@Squarerigger Actually when I was writing this example, I thought like, duh, of course it should desugar into a let ... in ... expression. I am still not sure why not. – Innocent

@IgnatInsarov But what specific let/in expression? For the straw man of unrelated, of course you can put it anywhere, but that's not very interesting. For the version with t' there is no obvious let/in expression with the same meaning. The closest is (\y' -> let t' = Tuple x y' in t') <$> f y, which I guess seems reasonable for this simple case but doesn't generalize well, as chi explains. – Donadonadee