How to encode actions that take monadic arguments with free (or freer) monads?

Question

Most monadic functions take pure arguments and return a monadic value. But there are a few that need also monadic arguments, for example:

mplus :: (MonadPlus m) => m a -> m a -> m a

finally :: IO a -> IO b -> IO a

forkIO :: m () -> m ThreadId

-- | From Control.Monad.Parallel
forkExec :: m a -> m (m a)

Each of them seems to bring up a different problem and I can't get a grasp of a generic way how to encode such actions using free monads.

• In both finally and forkIO the problem is that the monadic argument is of a different type than the result. But for free one would need them to be of the same type, as IO a gets replaced by the type variable of the encoding type, like data MyFunctor x = Finally x x x, which would only encode IO a -> IO a -> IO a.

  In From zero to cooperative threads in 33 lines of Haskell code the author uses Fork next next to fist implement

  cFork :: (Monad m) => Thread m Bool
  cFork = liftF (Fork False True)
  

  and then uses it to implement

  fork :: (Monad m) => Thread m a -> Thread m ()
  

  where the input and output have different types. But I don't understand if this was derived using some process or just an ad-hoc idea that works for this particular purpose.

• mplus is in particular confusing: a naive encoding as

  data F b = MZero | MPlus b b
  

  distributes over >>= and a suggested better implementation is more complicated. And also a native implementation of a free MonadPlus was removed from free.

  In freer it's implemented by adding

  data NonDetEff a where
    MZero :: NonDetEff a
    MPlus :: NonDetEff Bool
  

  Why is MPlus NonDetEff Bool instead of NonDetEff a a? And is there a way how to make it work with Free, where we need the data type to be a functor, other than using the CoYoneda functor?

• For forkExec I have no idea how to proceed at all.

Answer 1

I'll answer only about the Freer monad part. Recall the definition:

data Freer f b where
    Pure :: b -> Freer f b
    Roll :: f a -> (a -> Freer f b) -> Freer f b

Now with

data NonDetEff a where
  MZero :: NonDetEff a
  MPlus :: NonDetEff Bool

we can define

type NonDetComp = Freer NonDetEff

When Roll is applied to MPlus, a is unified with Bool and the type of the second argument is Bool -> NonDetEff b which is basically a tuple:

tuplify :: (Bool -> a) -> (a, a)
tuplify f = (f True, f False)

untuplify :: (a, a) -> (Bool -> a)
untuplify (x, y) True  = x
untuplify (x, y) False = y

As an example:

ex :: NonDetComp Int
ex = Roll MPlus $ Pure . untuplify (1, 2)

So we can define a MonadPlus instance for non-deterministic computations

instance MonadPlus NonDetComp where
    mzero       = Roll MZero Pure
    a `mplus` b = Roll MPlus $ untuplify (a, b)

and run them

run :: NonDetComp a -> [a]
run (Pure x)       = [x]
run (Roll MZero f) = []
run (Roll MPlus f) = let (a, b) = tuplify f in run a ++ run b