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.

It seems to me that the implementation depends not on the type of the function but on its semantics. "But I don't understand if this was derived using some process" I think the 'process' here is simply modelling your domain properly. For example, I think that the encoding of `finally` would be more obvious if you first try to encode the "most general" exception functions (`throw`, `catch`?). The type of `finally` is the same as `<*`.. so you theoretically there is no reason a function of this type can't be encoded (maybe just not directly..). — user2407038, Dec 21 '15 at 05:00
@user2407038 I understand what you mean. But I'm interested in the approach "mechanically encode the whole interface and let the interpreter worry about the implementation details". — Petr, Dec 26 '15 at 13:36

score 3 · Answer 1 · answered Dec 21 '15 at 10:34

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

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

1 Answers1