RULES exploration

[treeowl]

Opening this up to explore some things we might want to smash with RULES.

1. toView (lift m) = m >>= single. I believe this should help lift m <|> n and m <|> lift n.
2. As discussed, toView (fromView m) = m. Among other things, this should improve pure a <|> m and m <|> pure a.

[treeowl]

If lift is inlined, then that first rule I suggested wouldn't be necessary, as the toView . fromView rule will take care of it. However, we might not want to do that, because there are other games we can play with lift when we can see it.

lift m >>= f ==> fromView $ m >>= toView . f

looks promising.

In combination with that, we might want to reassociate binds:

(m >>= n) >>= f ==> m >>= \x -> n x >>= f

The big question is whether we can convince either of these rules to fire. There may also be ways to change the SeqT representation to do this stuff without rules.

[dagit]

My understanding of how RULES would work for this (since almost everything here is a type class method) is that we'll need to provide standalone functions that implement those methods and write the RULES against those.

Phase control might help with some of the ordering of applying the rules. Phases start at some high number and go until phase 0 runs. So you could have a toView . fromView rule run at a lower phase number than the lift m >>= f rule.

I really like these kinds of optimizations but having multiple rules does come at a cost. As you know, when you have multiple rules you have to make sure they are confluent. And they have to respect strictness. So it's not just the normal term equality confluence but I believe it's a stronger version that respects strictness?

[treeowl]

As part of the toView . fromView ==> id and fromView . toView ==> id rules, we probably want to write INLINE wrapper functions that apply toView and fromView and dispatch to (possibly INLINABLE) worker functions. The reason is that we want to be really sure the simplifier can see those collapsible pairs, even when we don't necessarily want to inline the things around them.

[treeowl]

Confluence is a desirable property, but not something we can generally guarantee within the confines of GHC's system. In particular, rules firing can affect inlining decisions and such that may affect whether other rules will fire. Even rules that appear confluent, therefore, may not actually be. I'm guessing you're actually concerned about the much weaker guarantee that rules should not change program meaning. That is very important, yes. I don't think that should really be particularly hard, including with regard to strictness, under the assumption that the underlying Monad instances are strictly lawful. That means we should document that RULES might change the behavior of code written for weird things like Control.Monad.Trans.State.Lazy and Control.Monad.Trans.Tardis. I don't imagine that there's any good reason to apply a logic monad transformer to such beasts anyway, but I could be wrong. Without that assumption, we can't write any useful rules whatsoever.

[dagit]

Confluence is the property mentioned in the papers and documentation. I forget exactly where I read it, but I know I saw confluence and preserving strictness both mentioned.

[treeowl]

Confluence is discussed on the Haskell Wiki. It's mentioned in the GHC documentation, but only in passing. The basic idea is that you should try to avoid writing rules in such a way that the choice of which rule to fire next (when there are multiple choices) will have a dramatic impact on performance.

[treeowl]

And yes, we should be careful to preserve strictness. But as I said above, we can do very little without assuming strictly lawful Monad instances. It's up to you whether to make that assumption. I would suggest doing so, and documenting it in some detail.

[treeowl]

Awkwardly, SeqT itself is not a strictly lawful monad. Note that undefined >>= pure is not undefined, but rather something closer to lift undefined. Can we fix that by, e.g., making >>= strict in its first argument?

[treeowl]

Or do we want to just say that users shouldn't seq on SeqT and should always toView it first?

[treeowl]

I just realized that fromView . toView ==> id is invalid, since it loses laziness. But toView . fromView ==> id, which is much more useful, should be fine.

[treeowl]

I realized we actually can use a slightly more limited rule even without assuming the user's Monad instance is lawful:

toView (fromView m) = m >>= \x -> return x

This is the result of just inlining and reducing. In principle, GHC could do this without a rule, but I don't know if it does.