[Haskell-cafe] Re: An interesting monad: "Prompt"

[apfelmus]

Derek Elkins wrote:
> Ryan Ingram wrote:
>> apfelmus wrote: 
>>         A context passing implementation (yielding the ContT monad
>>         transformer)
>>         will remedy this.
>>  
>> Wait, are you saying that if you apply ContT to any monad that has the
>> "left recursion on >>= takes quadratic time" problem, and represent
>> all primitive operations via lift (never using >>= within "lift"),
>> that you will get a new monad that doesn't have that problem?
>>  
>> If so, that's pretty cool.
>>  
>> To be clear, by ContT I mean this monad:
>> newtype ContT m a = ContT { runContT :: forall b. (a -> m b) -> m b }
>>  
>> instance Monad m => Monad (ContT m) where
>>     return x = ContT $ \c -> c x
>>     m >>= f  = ContT $ \c -> runContT m $ \a -> runContT (f a) c
>>     fail     = lift . fail
>>  
>> instance MonadTrans ContT where
>>     lift m   = ContT $ \c -> m >>= c
>>  
>> evalContT :: Monad m => ContT m a -> m a
>> evalContT m = runContT m return

Yes, that's the case because the only way to use >>= from the old monad 
is via lift. Since only primitive operations are being lifted into the 
left of >>=, it's only nested in a right-associative fashion. The 
remaining thing to prove is that ContT itself doesn't have the 
left-associativity problem or any other similar problem. It's pretty 
intuitive, but unfortunately, I currently don't know how to prove or 
even specify that exactly. The problem is that expressions with >>= 
contain arbitrary unapplied lambda abstractions and mixed types but the 
types shouldn't be much a minor problem.

> Indeed this was discussed on #haskell a few weeks ago.  That information
> has been put on the wiki at
> http://www.haskell.org/haskellwiki/Performance/Monads
> and refers to a blog post http://r6.ca/blog/20071028T162529Z.html that
> describes it in action.

Note that the crux of the Maybe example on the wiki page is not curing a 
left-associativity problem, Maybe doesn't have one. The key point here 
is that continuation passing style allows us to inline the liftings

   (Just x  >>=) = \f -> f x
   (Nothing >>=) = \_ -> Nothing

and thus eliminate lots of case analysis. (Btw, this is exactly the 
behavior of exceptions in an imperative language.)

(Concerning the blog post, it looks like this inlining brings speed. But 
Data.Sequence is not to be underestimated, it may well be responsible 
for the meat of the speedup.)

> I'm fairly confident, though I'd have to actually work through it, that
> the Unimo work, http://web.cecs.pdx.edu/~cklin/  could benefit from
> this.  In fact, I think this does much of what Unimo does and could
> capture many of the same things.

Well, Unimo doesn't have the left-associativity problem in the first 
place, so the "only" motive for using  ContT Prompt  instead is to 
eliminate the  Bind  constructor and implied case analyses.

But there's a slight yet important difference between  Unimo p a  and 
Unimo' p a = ContT (Prompt p) a , namely the ability the run the 
continuation in the "outer" monad. Let me explain: in the original 
Unimo, we have a helper function

   observe_monad :: (a -> v)
                 -> (forall b . p (Unimo p) b -> (b -> Unimo p a) -> v)
                 -> (Unimo p a -> v)

for running a monad. For simplicity and to match with Ryan's prompt, 
we'll drop the fact that  p  can be parametrized on the "outer" monad, 
i.e. we consider

   observe_monad :: (a -> v)
                 -> (forall b . p b -> (b -> Unimo p a) -> v)
                 -> (Unimo p a -> v)

This is just the case expression for the data type

   data PromptU p a where
     Return     :: a -> PromptU p a
     BindEffect :: p b -> (b -> Unimo p a) -> PromptU p a

   observe_monad :: (PromptU p a -> v) -> (Unimo p a -> v)

The difference I'm after is that the second argument to  BindEffect  is 
free to return an Unimo and not only another PromptU! This is quite 
handy for writing monads.

In contrast, things for  Unimo' p a = ContT (Prompt p) a  are as follows:

   data Prompt p a where
     Return     :: a -> Prompt p a
     BindEffect :: p b -> (b -> Prompt p a) -> Prompt p a

   observe :: (Prompt p a -> v) -> (Unimo' p a -> v)
   observe f m = f (runCont m Return)

Here, we don't have access to the "outer" monad  Unimo' p a  when 
defining an argument  f  to observe. I don't think we can fix that by 
allowing the second argument of  BindEffect  to return an  Unimo' p a 
since in this case,

   lift :: p a -> Unimo' p a
   lift x = Cont $ BindEffect x

won't work anymore.

Of course, the question now is whether this can be fixed. Put 
differently, this is the question I keep asking: does it allow  Unimo 
to implement strictly more monads than  ContT = Unimo'  or is the latter 
enough? I.e. can every monad be implemented with ContT?


Regards,
apfelmus