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.