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

data Monad' :: (* -> *) -> * -> * -> * whereThe semantics is a bit trickier as in the arrow case, but let's find out the type signature first...

Feed :: Monad m => m b -> Monad' m a b

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

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 bThe effect of an empty thrist is trivial:

recoverM mon Nil = monAnd the other two connectives turn out to be the only sensible way to do it:

recoverM mon (Cons (Feed m) rest) = recoverM (mon >> m) restNow, we can build up chains:

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

*Embeddings> :t Cons (Feed getChar) $ Cons (Digest (return . ord)) Niland execute them too:

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

*Embeddings> recoverM getChar (Cons (Feed getChar) $ Cons (Digest (return . ord)) Nil)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.

Loading package haskell98 ... linking ... done.

GG71

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 bThe semantics should be clear, I leave the extension of recoverM to the reader.

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

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.

## No comments:

Post a Comment