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
@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

user3237465 user3237465 · Accepted Answer · 2015-12-21T10:34:03

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 Answers