Another approach to value recursion was recently given by Sabry and Moggi in their latest FICS paper: They have an mfix-like operator for continuations there, but it doesn't satisfy left-shrinking either.

The paper in question is available at: http://www.cs.indiana.edu/~sabry/papers/valuerecursion_extended.ps

(Their treatment of value recursion is rather different than ours as well.) See Amr Sabry's papers for details.

The typing of mfix given in our paper is: (m a -> m a) -> m a; by changing the (ret e) to e in rule M.2 you get exactly the same mfix of Erkok/Launchbury. The paper also shows why left-shrinking cannot hold in general and gives an example for the continuation monad. --Amr