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

[Derek Elkins]

On Sat, 2007-11-24 at 11:10 +0100, apfelmus wrote:
> 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.

I agree, hence the fact that that is massively understated.  However,
while Maybe may not have a problem on the same order, there is
definitely a potential inefficiency.
(Nothing >>= f) >>= g expands to 
case (case Nothing of Nothing -> Nothing; Just x -> f x) of 
    Nothing -> Nothing
    Just y -> g y 

This tests that original Nothing twice.  This can be arbitrarily deep.
The right associative version would expand to
case Nothing of
    Nothing -> Nothing
    Just x -> f x >>= g

>  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.)

Indeed, avoiding case analyses and achieving "exactly the behaviour of
exceptions" was the motivation.

> 
> (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 not quite sure what all is being compared to what, but Russell
O'Connor did say that using continuations passing style did lead to a
significant percentage speed up.

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

As I said, I need to work through this stuff first.