Is `evaluate` safe compared to `seq`?

Question

As shown in this answer, seq combined with undefined does very strange things when it comes to equational reasoning, for example it can make any monad fail. Another example is in this question.

Recently I stumbled upon evaluate :: a -> IO a that does a similar thing - it evaluates its argument to WHNF but only when the IO action is evaluated. This seems to be much safer, as one expects that "in IO we can do everything". Of course it cannot be used everywhere, but often the need to evaluate an expression is connected somehow with an IO operation (like to force a producing thread to evaluate a computation instead of a consuming thread when working with MVars).

So I'd like to ask, how safe is evaluate? Is it possible to create examples (involve IO of course) where it breaks reasoning about code like seq does? Or can I consider it as a safe replacement of seq (if it's possible for a particular program)?

Answer 1

No, you still get the same issues caused by the seq command, in that any monad used in the first argument of evaluate will have its monad rules broken. Basing it off the rule in ertes's answer:

In the Kleisli category the monad gives rise to return is the identity morphism and (<=<) is composition. So return must be an identity for (<=<):

return <=< x = x

This means you should be able to replace return <=< x with x with any valid monad without changing the operation of the program.

Using that with the evaluate function...

evaluate (return <=< undefined :: a -> Identity b) >> putStrLn "hello"

outputs hello. Using what should be an equivalent statement by replacing return <=< undefined with undefined:

evaluate (undefined :: a -> Identity b) >> putStrLn "hello"

instead causes an Prelude.undefined exception.

This only happens with the evaluate function. Notice that return has exactly the same type signature as evaluate. If you replace evaluate with return in the above commands, the resulting action for both commands is the same (they output hello).