Re: [Haskell-cafe] Feeding a monad into itself

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. [2] https://hackage.haskell.org/package/probable-0.1.2/docs/Math-Probable-Distri...

This sounds very interesting, thank you. So if I understand correctly, (––>) is supposed to mean “something like implication”? So far so good, but I fail to grasp that in a more precise way because the law makes no sense to me yet. Or rather, something seems to be missing? I suppose it's because I don't have the mathematical perspective to get that part. Even such common things like “Left Adjoints” fail to click in my head, so they're missing on my side… So the operations have the types (∧) ∷ Monad m ⇒ m a → (a → m ()) → m a (≤) ∷ SetLike m ⇒ m a → m a → Bool -- implicitely (––>) ∷ (Eq a) ⇒ m a → m a → a → m () Because (≤) returns something non-monadic, the only way the law makes sense is if it's bracketed like this: (x ∧ f) ≤ y iff f ≤ (x ––> y) Because of the left side, f must have type (a → m ()). That makes sense because (x ––> y) has that same type. But now (≤) has to be defined over this type of functor. In other words you seem to claim this type of functors is “set-like”? I assume the definition is something like f ≤ g iff ∀ x.f x ≤ g x ? I'm still not sure what that would mean for the law, but it seems like the first step towards understanding it a bit. Cheers, MarLinn
participants (2)
-
MarLinn
-
Olaf Klinke