Haskell State Monad代码：验证mlabel函数展开逻辑正确性

核心代码定义 #

instance Monad ST where
   --return :: a -> ST a
   return x = S (\s -> (x,s))

   --(>>=) :: ST a -> (a -> ST b) -> ST b
   st >>= f = S (\s -> let (x, s') = app st s
                            in app (f x) s')

type State = Int
newtype ST a = S (State -> (a, State))

data Tree a = Leaf a | Node (Tree a) (Tree a) deriving (Show)

app :: ST a -> State -> (a, State)
app (S st) s = st s

mlabel函数实现 #

mlabel :: Tree a -> ST (Tree Int)
mlabel (Leaf _) = fresh >>= (\n -> return (Leaf n))
mlabel (Node l r) = mlabel l >>= (\l ->
                    mlabel r >>= (\r ->
                    return (Node l r)))

fresh函数定义 #

fresh :: ST Int
fresh = S (\n -> (n , n +1))

输入为Leaf 'a'时的推导过程（原文翻译+修正） #

当输入为Leaf 'a'时，mlabel等价于fresh >>= (\n -> return (Leaf n))，以下是展开推导：

fresh >>= (\n -> return (Leaf n))
= S (\n -> (n, n+1)) >>= (\n -> return (Leaf n))
= S (\s -> let (x, s') = app (S (\n -> (n, n+1))) s
               -- 计算app结果：app (S st) s = st s，因此x=s，s'=s+1
               (x, s') = (s, s+1)
           in app ((\n -> return (Leaf n)) x) s')
= app (return (Leaf s)) s'  -- 代入x=s
= app (S (\s'' -> (Leaf s, s''))) s'  -- 展开return的定义
= (Leaf s, s')  -- 计算app结果
= (Leaf s, s+1)  -- 代入s'=s+1

推导逻辑验证 #

原文推导存在几处错误：

• 符号错误：将>>=误写为>>==；
• return定义混淆：return (Leaf x)的正确展开是S (\s'' -> (Leaf x, s''))，原文错误地写成了S (\x -> (Leaf x, x+1))，混淆了值参数和状态参数；
• 最终结果错误：正确结果应为(Leaf s, s+1)，而非(Leaf s+1, (s+1)+1)。

正确的逻辑是：从初始状态s出发，fresh取出当前状态值s作为标记，同时将状态更新为s+1；随后return将标记为s的叶子节点包装，且不改变已更新的状态，最终得到带标记的叶子节点和自增后的状态。因此原文推导逻辑不正确，核心问题是对return的Monad实现理解偏差。

内容的提问来源于stack exchange，提问作者Rifat Ahmed