Wadler 中刻度方程的问题，“函数式编程的 Monads”，第 3 节

Question

在 Wadler 的 Monads for functional programming 中，我正在查看等式

tick ✭ λ().m = m ✭ λ().tick

在第 3 节中（在 State Monad 的上下文中）。据说是

只要 tick 是对 m 内状态的唯一操作，就会保持。

我不明白这是怎么回事。左项的类型不是 m 而右项的类型不是 tick : M ()？而且，如果m的类型不是M()，那么右边的✭操作数的类型不匹配。

我环顾四周，但找不到任何勘误表，同样的公式出现在 2001 年的论文修订版中，所以我肯定遗漏了什么……

Answer 1

在 Haskell 语法中，

tick x  =  ((), x+1)
unitState a x  =  (a, x)
bindState m k  =  uncurry k . m    -- StarOp for State

bindState tick (\() -> m) =
     = uncurry (\() -> m) . (\x -> ((), x+1))
     = (\y -> uncurry (\() -> m) ( (\x -> ((), x+1)) y))
     = (\y -> uncurry (\() -> m)          ((), y+1)    )
     = (\y ->         (\() -> m)           () (y+1)    )
     = (\y ->                 m               (y+1)    )

bindState m (\() -> tick) =
     = uncurry (\() -> tick) . m
     = uncurry (\() -> (\x -> ((), x+1))) . m
     = uncurry (\() x -> ((), x+1)) . m
     = (\y -> uncurry (\() x -> ((), x+1)) (m y))
     = (\y -> let ((),z) = m y in ((), z+1))

这两个只有在m y返回((),z)这样m (y+1)返回((),z+1)时才会相同（即m y只会在初始状态@987654327上增加一些固定数量 @，不依赖于y)。

所以我看不出类型的问题，但是那个英文短语的含义也让我无法理解。

顺便说一下，该论文提出的通过将 unitState 更改为 unitState a x = (a, x+1) 来将“执行计数”添加到其 monadic evaluator 的方式，本质上会使其成为非法 monad，因为这个新的 unitState 不会成为身份。

类型是，

tick :: M ()
bindState :: M a -> (a -> M b) -> M b
(\() -> tick) :: () -> M () 

bindState (tick :: M ()) ((\() -> m) :: () -> M b ) :: M b
bindState (m :: M ()) ((\() -> tick) :: () -> M ()) :: M ()

所以唯一的类型是 m 必须是 m :: M ()，而不是一般的 M b，正如我们已经在上面的扩展中看到的那样。