In Wadler's Monads for functional programming I'm looking at the equation
tick ✭ λ().m = m ✭ λ().tick
in section 3 (in the context of State Monad). It is claimed that it
holds so long as tick is the only action on state within m.
I fail to understand how this can be the case. Doesn't the left term have the type of m while the right term has the type of tick : M ()? Moreover, if the type of m isn't M (), the types of the operands of ✭ are mismatched on the right-hand side.
I looked around but couldn't find any errata, and the same equation appears in the revised version of the paper from 2001, so there must clearly be something I'm missing…
In Haskell syntax,
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))
These two will only be the same if m y returns ((),z) such that m (y+1) returns ((),z+1) (i.e. m y only adds some fixed amount to the initial state y, which does not depend on y).
So I don't see the problem with the types, but that English phrase's meaning eludes me too.
By the way the paper's proposed way of adding "execution counts" to its monadic evaluator by changing this unitState into unitState a x = (a, x+1), essentially, would make it an illegal monad because this new unitState won't be an identity.
The types are,
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 ()
So the only thing with the types is that m must be m :: M (), not the general M b, as we already saw with the expansions above.