> f (x then k) = x then (f . k) (*)
> = x then (\y -> f (k y))
>
> where, of course, f is an adequate polymorphic function i.e.
> f : M a -> M a for any type $a$.
You really want here f : M a -> M b.
> It is easy to see that for the identity monad, this equation (*) becomes
> simply the definition of composition:
>
> f (k x) = (f . k) x
>
> In the case of the list monad (M a = [a]), equation (*)
> holds only if $f$ is a morphism over the concat operator
> i.e. f (u ++ v) = (f u) ++ (f v)
This is the clue. The equation doesn't really depend on the monad,
it depends on f. If the monad is a mathematical monad (satisfying
the usual coherence equations for "return" and "then") then your equation
holds if f is of the form map g for some function g, where 'map'
is the monad functor, expressible in terms of return and then as
map f x = x then (return . f)
> I am wandering if the equation (*) is true (and for which conditions
> for $f$) in the case of the State monad.
Again, if f is of the above form then the equation is true, because
the state monad is a 'true' monad (provided we define 'then' with
irrefutable patterns). So, the question it boils down to is:
Is every function of type (M a->M b) for the state monad of the form
map g for some function g: a->b?
The answer is "No!".
The function 'map' for the state monad (M a = s->(a,s)) is:
map h x s = (h a,t) where (a,t)=x s
We could write our counter-exampling f as follows:
f x s = (g a,s) where (a,t)=x s
This f is almost like (map g), except that it throws away the new state
and returns the old one.
Stefan Kahrs
