Fri Jul 21 22:30:13 UTC 2017

```Joshua Grosso wrote:

>Could MonadPlus (with mzero) or Alternative (with empty) provide the
>termination condition, if this pattern turned out to be more generally
>useful?

MonadPlus and Alternative provide a way to put the zero into the monad, but no way to check for zeroness. In the Maybe type you have the isNothing function, but the MonadPlus and Alternative classes don't require such a thing, and probably shouldn't.

In the following I present a class that allows to do stuff conditional on mzero. The starting observation is that in logic, False => anything == True. Hence the implication arrow is a (binary) function that turns nothing into something.

Consider the following binary operation. (Logicians: think conjunction)

(/\) :: Monad m => m a -> (a -> m ()) -> m a
ma /\ f = (\a -> liftM (const a) (f a)) =<< ma

It's a bit like Control.Monad.mfilter but deletes stuff by mapping it to mzero instead of False. For example,

ghci> [0,1,2,3] /\ (\n -> replicate n ())
[1,2,2,3,3,3]

Some MonadPlus monads are set-like. Think of Nothing as the empty set, Just x as the singleton set {x} and think of the list [x,y,z] as the finite set {x,y,z}, disregarding muliplicities. For such monads m, the types m a have a preorder ≤ which is set inclusion under the "set interpretation". For example,
Nothing ≤ Just ()
[1,2,3] ≤ [1,2,3,4]
but not [1,2] ≤ [1,4].

Now consider the following type class.

class (Monad m) => Heyting m where
(-->) :: (Eq a) => m a -> m a -> a -> m ()

We reqire that for all x, y and f

x /\ f ≤ y
if and only if
f ≤ x --> y

That is, (x /\) is left adjoint to (x -->), which reminds the logician of the Heyting implication arrow.
For MonadPlus instances, we suggest that

(mzero -->) == const (const (return ()))

Here are some instances:

instance Heyting [] where
ys --> xs = \a -> if (a `notElem` ys) || (a `elem` xs)
then [()]
else []
instance Heyting Maybe where
y --> x = listToMaybe.((maybeToList y) --> (maybeToList x))

Without the Eq constraint, I couldn't have used the elem function, hence the Heyting class carries that constraint.
(There is also a Heyting instance for the monad of finite distributions [1], see the package probable [2]
and its siblings.) Heyting monads have a sort of negation, turning mzero into something:

neg :: (MonadPlus m, Heyting m) => m a -> m ()
neg x = ((liftM (const ()) x) --> mzero) ()

Using neg, we can do stuff on mzero:
ghci> neg Nothing
Just ()
ghci> neg (Just ())
Nothing
ghci> neg [1,2,3]
[]
ghci> neg []
[()]

Finally we implement Jake's function, but more general.

untilMZero :: (Heyting m, MonadPlus m) =>  (a -> m a) -> a -> m a
untilMZero f x = (liftM (const x) (neg (f x))) `mplus` ((f x) >>= (untilMZero f))

ghci> untilMZero (\n -> if n > 5 then Nothing else Just (n+1)) 0
Just 6
ghci> untilMZero (\n -> if n > 5 then [] else [n+1,2*n]) 1
[6,10,8,6,6,10,8,6,10,8,6,6,10,8]

-- Olaf

[1] For the Giry monad, --> computes the Radon-Nikodym derivative. It type-checks.