Embeddings, Part Two: Monad --> Thrist

Here comes the second part of my promised embeddings, this time I'll embed any monadic chain (corresponding to the do-syntax in Haskell) into a thrist and provide a semantics. Later I'll try to discuss some convenience features and try my luck with mfix (and the mdo-notation).

As in my post dealing with arrows, we have to define an adapter GADT:

data Monad' :: (* -> *) -> * -> * -> * where
Feed :: Monad m => m b -> Monad' m a b
Digest :: Monad m => (a -> m b) -> Monad' m a b

The semantics is a bit trickier as in the arrow case, but let's find out the type signature first...
Feed sounds like an introduction of a new monadic value, we would like to interpret it as the (>>) connective. Digest on the other hand transforms, and thus corresponds to (>>=). Both expect an already formed monadic value, so we can state:

recoverM :: Monad m => m a -> Thrist (Monad' m) a b -> m b

The effect of an empty thrist is trivial:

recoverM mon Nil = mon

And the other two connectives turn out to be the only sensible way to do it:

recoverM mon (Cons (Feed m) rest) = recoverM (mon >> m) rest
recoverM mon (Cons (Digest f) rest) = recoverM (mon >>= f) rest

Now, we can build up chains:

*Embeddings> :t Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil
Cons (Feed getChar) $ Cons (Digest $ (return . ord)) Nil :: forall a. Thrist (Monad' IO) a Int

and execute them too:

*Embeddings> recoverM getChar (Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil)
Loading package haskell98 ... linking ... done.
GG71

The first 'G' is consumed by the getChar invocation that is given to recoverM, but its result is ignored. The second is having an effect too, and its result is used to obtain the ASCII value. The overall monadic action is then run by ghci, printing the 71.

We have converted >> getChar >>= (return . ord) into a thrist and got it back by means of recoverM! And this works for any monad.

Two shortcuts come to my mind, they can be modelled by adding two simpler variants to the GADT:

Feed' :: Monad m => b -> Monad' m a b
Digest' :: Monad m => (a -> b) -> Monad' m a b

The semantics should be clear, I leave the extension of recoverM to the reader.

Now what about the value fixpoint mfix? Can we dress it in thristy clothes? Frankly, I have no idea, but I would be happy to hear from you. It is late, I need sleep now. Bye.