Fair conjunction. Similarly to the previous function, consider
the distributivity law, naturally expected from
MonadPlus:
(a <|> b) >>= k = (a >>= k) <|> (b >>= k)
If
a >>= k can backtrack arbitrarily
many times,
b >>= k may never be
considered. In logic statements, "backtracking" is the process of
discarding the current possible solution value and returning to a
previous decision point where a new value can be obtained and tried.
For example:
>>> do { x <- pure 0 <|> pure 1 <|> pure 2; if even x then pure x else empty } :: [Int]
[0,2]
Here, the
x value can be produced three times, where
<|> represents the decision points of that production.
The subsequent
if statement specifies
empty (fail) if
x is odd, causing it to be discarded and a return to an
<|> decision point to get the next
x.
The statement "
a >>= k can backtrack
arbitrarily many times" means that the computation is resulting in
empty and that
a has an infinite number of
<|> applications to return to. This is called a
conjunctive computation because the logic for
a and
k must both succeed (i.e.
pure a value instead of
empty).
Similar to the way
interleave allows both branches of a
disjunctive computation, the
>>- operator takes care to
consider both branches of a conjunctive computation.
Consider the operation:
odds = pure 1 <|> fmap (2 +) odds
oddsPlus n = odds >>= \a -> pure (a + n)
g = do x <- (pure 0 <|> pure 1) >>= oddsPlus
if even x then pure x else empty
>>> observeMany 3 g
...never completes...
This will never produce any value because all values produced by the
do program come from the
pure 1 driven
operation (adding one to the sequence of odd values, resulting in the
even values that are allowed by the test in the second line), but the
pure 0 input to
oddsPlus generates an
infinite number of
empty failures so the even values generated
by the
pure 1 alternative are never seen. Using
interleave here instead of
<|> does not help due
to the aforementioned distributivity law.
Also note that the
do notation desugars to
>>=
bind operations, so the following would also fail:
do a <- pure 0 <|> pure 1
x <- oddsPlus a
if even x then pure x else empty
The solution is to use the
>>- in place of the normal
monadic bind operation
>>= when fairness between
alternative productions is needed in a conjunction of statements
(rules):
h = do x <- (pure 0 <|> pure 1) >>- oddsPlus
if even x then pure x else empty
>>> observeMany 3 h
[2,4,6]
However, a bit of care is needed when using
>>- because,
unlike
>>=, it is not associative. For example:
>>> let m = [2,7] :: [Int]
>>> let k x = [x, x + 1]
>>> let h x = [x, x * 2]
>>> m >>= (\x -> k x >>= h)
[2,4,3,6,7,14,8,16]
>>> (m >>= k) >>= h -- same as above
[2,4,3,6,7,14,8,16]
>>> m >>- (\x -> k x >>- h)
[2,7,3,8,4,14,6,16]
>>> (m >>- k) >>- h -- central elements are different
[2,7,4,3,14,8,6,16]
This means that the following will be productive:
(pure 0 <|> pure 1) >>-
oddsPlus >>-
\x -> if even x then pure x else empty
Which is equivalent to
((pure 0 <|> pure 1) >>- oddsPlus) >>-
(\x -> if even x then pure x else empty)
But the following will
not be productive:
(pure 0 <|> pure 1) >>-
(\a -> (oddsPlus a >>- \x -> if even x then pure x else empty))
Since do notation desugaring results in the latter, the
RebindableSyntax language pragma cannot easily be used
either. Instead, it is recommended to carefully use explicit
>>- only when needed.