为什么 "let" 语句强制 "applicative do" 块需要 monad 约束？

Question

考虑这个例子：

{-# 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'

看起来不错！但是没有：

[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.

即使这样也失败了：

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

因此，引入任何 let 语句都会从 "applicative do" 中删除 "applicative"。为什么？

Answer 1

您想将此脱糖到什么应用表达式？ monadic 表达式是一系列链式作用域，因此 let 引入一个扩展到所有剩余作用域的绑定是有意义的，但是对于 applicative 来说，各种表达式不能真正相互依赖，所以有没有将 let 脱糖到

有意义的范围

Answer 2

它将转化为

let unrelated = 1 in return $ Tuple x y'

没有 return <something> 的形式，应用 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.

如果你看一下https://gitlab.haskell.org/ghc/ghc/wikis/applicative-do中关于脱糖的描述，它也不支持let任何方式。

为什么 "let" 语句强制 "applicative do" 块需要 monad 约束？

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

haskell

monads

ghc

applicative

do-notation