Feeding a monad into itself

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
16 messages Options
Reply | Threaded
Open this post in threaded view
|

Feeding a monad into itself

Jake
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Rein Henrichs
This is about as good as you can do. The monad-loops package provides a variety of similar combinators, generally implemented in similar ways, but not this specific combinator. The downside of this combinator is that it is partial: it will run forever without producing anything if f never gives a Nothing.

On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Jeff Clites
Also this pattern does seem Maybe-specific, in that for the general Monad case there's not an obvious termination condition.

JEff

On Jul 20, 2017, at 11:03 AM, Rein Henrichs <[hidden email]> wrote:

This is about as good as you can do. The monad-loops package provides a variety of similar combinators, generally implemented in similar ways, but not this specific combinator. The downside of this combinator is that it is partial: it will run forever without producing anything if f never gives a Nothing.

On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

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

Joshua Grosso

On Thu, Jul 20, 2017 at 7:16 PM, Jeff Clites <[hidden email]> wrote:
Also this pattern does seem Maybe-specific, in that for the general Monad case there's not an obvious termination condition.

JEff

On Jul 20, 2017, at 11:03 AM, Rein Henrichs <[hidden email]> wrote:

This is about as good as you can do. The monad-loops package provides a variety of similar combinators, generally implemented in similar ways, but not this specific combinator. The downside of this combinator is that it is partial: it will run forever without producing anything if f never gives a Nothing.

On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Jake

That's what I was thinking, but I couldn't figure out if I wanted MonadPlus, Alternative or maybe Monoid because they all have zero elements.


On Thu, Jul 20, 2017, 21:52 Joshua Grosso <[hidden email]> wrote:
Could MonadPlus (with mzero) or Alternative (with empty) provide the termination condition, if this pattern turned out to be more generally useful?

Joshua Grosso

On Thu, Jul 20, 2017 at 7:16 PM, Jeff Clites <[hidden email]> wrote:
Also this pattern does seem Maybe-specific, in that for the general Monad case there's not an obvious termination condition.

JEff

On Jul 20, 2017, at 11:03 AM, Rein Henrichs <[hidden email]> wrote:

This is about as good as you can do. The monad-loops package provides a variety of similar combinators, generally implemented in similar ways, but not this specific combinator. The downside of this combinator is that it is partial: it will run forever without producing anything if f never gives a Nothing.

On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

David Menendez-2
Another possibility is to use Either for an early exit.

iterateM :: Monad m => (a -> m a) -> a -> m b
iterateM f a = f a >>= iterateM f

exitOnNothing :: (a -> Maybe a) -> a -> Either a a
exitOnNothing f a = maybe (Left a) Right (f a)

Now, your untilNothing is iterateM . exitOnNothing, but you can easily
extend it to use IO or whatever pattern you like.


On Thu, Jul 20, 2017 at 11:17 PM, Jake <[hidden email]> wrote:

> That's what I was thinking, but I couldn't figure out if I wanted MonadPlus,
> Alternative or maybe Monoid because they all have zero elements.
>
>
> On Thu, Jul 20, 2017, 21:52 Joshua Grosso <[hidden email]> wrote:
>>
>> Could MonadPlus (with mzero) or Alternative (with empty) provide the
>> termination condition, if this pattern turned out to be more generally
>> useful?
>>
>> Joshua Grosso
>>
>> On Thu, Jul 20, 2017 at 7:16 PM, Jeff Clites <[hidden email]> wrote:
>>>
>>> Also this pattern does seem Maybe-specific, in that for the general Monad
>>> case there's not an obvious termination condition.
>>>
>>> JEff
>>>
>>> On Jul 20, 2017, at 11:03 AM, Rein Henrichs <[hidden email]>
>>> wrote:
>>>
>>> This is about as good as you can do. The monad-loops package provides a
>>> variety of similar combinators, generally implemented in similar ways, but
>>> not this specific combinator. The downside of this combinator is that it is
>>> partial: it will run forever without producing anything if f never gives a
>>> Nothing.
>>>
>>> On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
>>>>
>>>> I have a function f :: a -> Maybe a that I want to feed into itself with
>>>> some initial input until it returns Nothing.
>>>>
>>>> untilNothing :: (a -> Maybe a) -> a -> a
>>>> untilNothing f x = case f x of
>>>>                             Just x' -> untilNothing f x'
>>>>                             Nothing -> x
>>>>
>>>> Is there a better way to do this? I feel like there is something more
>>>> general going on with Monads being fed into themselves, but maybe I'm wrong.
>>>> Thoughts?
>>>> _______________________________________________
>>>> Haskell-Cafe mailing list
>>>> To (un)subscribe, modify options or view archives go to:
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.



--
Dave Menendez <[hidden email]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Silvio Frischknecht
In reply to this post by Jake
Well you can usually replace a recursion with a fix and a case Maybe
with a maybe. Then you would get something like this.

untilNothing f = fix (\f' a -> maybe a f' (f a))

But it's really unreadable. Or at least I can't read it. Though it's fun
to think up. Also no connection to monads.

Cheers Silvio
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Kim-Ee Yeoh
Administrator
In reply to this post by Jake
Another perfectly cromulent definition is:

untilNothing f = fromJust . last . takeWhile isJust . iterate (f =<<) . Just

This has 2 advantages:

1. It illustrates the haskellism that "A list is a loop is a list."

2. It composes much-beloved list combinators into a reasonable pipeline.


-- Kim-Ee

On Fri, Jul 21, 2017 at 12:26 AM, Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

MarLinn
On 2017-07-21 17:57, Kim-Ee Yeoh wrote:
Another perfectly cromulent definition is:

untilNothing f = fromJust . last . takeWhile isJust . iterate (f =<<) . Just

This has 2 advantages:

1. It illustrates the haskellism that "A list is a loop is a list."
2. It composes much-beloved list combinators into a reasonable pipeline.

Note that

	fromJust . last . takeWhile isJust . iterate (f =<<) . Just
	≡
	last . catMaybes . takeWhile isJust . iterate (f =<<) . Just

Note further that that with duplicate x = (x,x),

	\initialElement -> catMaybes . takeWhile isJust . iterate (f =<<) . Just $ initialElement
	≡
	\initialElement -> initialElement: unfoldr (fmap duplicate . f) initialElement

In other words, the pipeline is basically equivalent to a simple unfoldr modulo the first step. Therefore,

	untilNothing f initialElement = last $ initialElement : unfoldr (fmap duplicate . f) initialElement

Which reveals the relation to anamorphisms and makes it possible to drop two of the three pain-inducing functions (isJust and fromJust).

This further hints at the fact that loops are a combination of anamorphisms/unfolds (here: unfoldr) and catamorphisms/folds (here: last). As last can easily be replaced with better options like foldMap Last, the search for a "better" implementation should basically consist of a search for a more suitable unfold. A simple hoogle seems to reveal several options.


Cheers,
MarLinn

PS: The relation to lists still remains in my version, but it may be easier to see that the "haskellism" is just an unfortunate result of both their prominence in the standard libraries and the specialised syntax we have for them. That's why it's a "haskellism", and not a universal relation.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Jake

Very interesting! What do you mean by a "better" unfold?


On Fri, Jul 21, 2017, 13:06 MarLinn <[hidden email]> wrote:
On 2017-07-21 17:57, Kim-Ee Yeoh wrote:
Another perfectly cromulent definition is:

untilNothing f = fromJust . last . takeWhile isJust . iterate (f =<<) . Just

This has 2 advantages:

1. It illustrates the haskellism that "A list is a loop is a list."
2. It composes much-beloved list combinators into a reasonable pipeline.

Note that

	fromJust . last . takeWhile isJust . iterate (f =<<) . Just
	≡
	last . catMaybes . takeWhile isJust . iterate (f =<<) . Just

Note further that that with duplicate x = (x,x),

	\initialElement -> catMaybes . takeWhile isJust . iterate (f =<<) . Just $ initialElement
	≡
	\initialElement -> initialElement: unfoldr (fmap duplicate . f) initialElement

In other words, the pipeline is basically equivalent to a simple unfoldr modulo the first step. Therefore,

	untilNothing f initialElement = last $ initialElement : unfoldr (fmap duplicate . f) initialElement

Which reveals the relation to anamorphisms and makes it possible to drop two of the three pain-inducing functions (isJust and fromJust).

This further hints at the fact that loops are a combination of anamorphisms/unfolds (here: unfoldr) and catamorphisms/folds (here: last). As last can easily be replaced with better options like foldMap Last, the search for a "better" implementation should basically consist of a search for a more suitable unfold. A simple hoogle seems to reveal several options.


Cheers,
MarLinn

PS: The relation to lists still remains in my version, but it may be easier to see that the "haskellism" is just an unfortunate result of both their prominence in the standard libraries and the specialised syntax we have for them. That's why it's a "haskellism", and not a universal relation.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

MarLinn

> Very interesting! What do you mean by a "better" unfold?
>
Well you asked the original question, so I'll leave that up to you to
define. ;)

Your original version is relatively specialised, but simple and
efficient. The one I adapted uses quite a bit of intermediate wrapping
and unwrapping and needs to move parts around on every iteration. Only
because of list fusion does it have a chance to compete. It's also quite
indirect and uses up cognitive energy when trying to understand it. So
yours is "better" in several ways.

Maybe there's a general unfold that is easier to understand. Or more
efficient. Or easier to adapt to more situations. It depends highly on
what your actual goals are…

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Jeff Clites
In reply to this post by Jake
Another interesting thought: although all of those give you a way to obtain a zero, I don't think any give you a way to test whether something is that zero. Hmm.

JEff

On Jul 20, 2017, at 8:17 PM, Jake <[hidden email]> wrote:

That's what I was thinking, but I couldn't figure out if I wanted MonadPlus, Alternative or maybe Monoid because they all have zero elements.


On Thu, Jul 20, 2017, 21:52 Joshua Grosso <[hidden email]> wrote:
Could MonadPlus (with mzero) or Alternative (with empty) provide the termination condition, if this pattern turned out to be more generally useful?

Joshua Grosso

On Thu, Jul 20, 2017 at 7:16 PM, Jeff Clites <[hidden email]> wrote:
Also this pattern does seem Maybe-specific, in that for the general Monad case there's not an obvious termination condition.

JEff

On Jul 20, 2017, at 11:03 AM, Rein Henrichs <[hidden email]> wrote:

This is about as good as you can do. The monad-loops package provides a variety of similar combinators, generally implemented in similar ways, but not this specific combinator. The downside of this combinator is that it is partial: it will run forever without producing anything if f never gives a Nothing.

On Thu, Jul 20, 2017 at 10:27 AM Jake <[hidden email]> wrote:
I have a function f :: a -> Maybe a that I want to feed into itself with some initial input until it returns Nothing.

untilNothing :: (a -> Maybe a) -> a -> a
untilNothing f x = case f x of
                            Just x' -> untilNothing f x'
                            Nothing -> x

Is there a better way to do this? I feel like there is something more general going on with Monads being fed into themselves, but maybe I'm wrong. Thoughts?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

MarLinn
On 2017-07-21 23:33, Jeff Clites wrote:
> Another interesting thought: although all of those give you a way to
> obtain a zero, I don't think any give you a way to test whether
> something is that zero. Hmm.

Well you could always use Eq. Or Foldable's null. That would generalize
the loop to all foldable monads. Is that useful? I doubt it, but it's
interesting.

Cheers.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Olaf Klinke
In reply to this post by Jake

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-Distribution-Finite.html
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

MarLinn
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Feeding a monad into itself

Olaf Klinke
In reply to this post by Jake
MarLinn,

you observed well, I swept something under the carpet. So here are the definitions in full glory. Apologies to all the not-so mathematically minded in Haskell-Cafe, the mail has grown rather long.

A partially ordered set is a type X together with a function
(≤) :: X -> X -> Bool
obeying three laws.
∀ x. x ≤ x
x ≤ y and y ≤ z implies x ≤ z
x ≤ y and y ≤ x implies x == y

Note that total orders, like the Ord typeclass, require that either x ≤ y or y ≤ x hold, but not so partial orders.
Now suppose you have two partially ordered types, say X and A. By abuse of notation we use ≤ for each of the orders.
Suppose we have functions
f :: X -> A
g :: A -> X
Suppose further that f and g are order-preserving, that is
x ≤ x' implies f x ≤ f x'
a ≤ a' implies g a ≤ g a'.
Then f is said to be left adjoint to y if for all x :: X and a :: A,
f x ≤ a precisely when x ≤ g a.

If X is partially ordered, so is each function space (as you suggested correctly), namely pointwise.
Define for f, g :: Z -> X
f ≤ g when ∀ z. f z ≤ g z

If you like, (->) Z is an applicative functor and the ≤ function for the type Z -> X is built using liftA2 (≤).

A bounded lattice is a partially ordered type L that has two nullary and two binary operations:
least :: L
greatest :: L
min :: L -> L -> L
max :: L -> L -> L
subject to the following laws.
∀ x. least ≤ x
∀ x. x ≤ greatest
z ≤ x and z ≤ y precisely when z ≤ min x y
x ≤ z and y ≤ z precisely when max x y ≤ z

An example is the type Bool where False ≤ True, least = False, greatest = True, min = (&&) and max = (||).
Observe that for each x :: L, the partial application (min x) is a monotone function of type L -> L.
Hence we can ask when each such function has a right adjoint. If each such right adjoint exists, we call L a Heyting algebra and denote the right adjoint to (min x) by (-->) x.

For every MonadPlus m, we can embed Bool into m () using the function Control.Monad.guard.
In this reading, False is represented by Nothing and True is represented by Just ().
We thus obtain partial orders on Maybe () as well as on any function type X -> Maybe ().
Recall that my (/\) function had type
m a -> (a -> m ()) -> m a
Specialising to a = () we obtain

meet = \x y -> x /\ (const y) :: m () -> m () -> m ()

which you can convince yourself produces the (&&) operator in case of Maybe () == Bool.
Likewise, my arrow (-->) has type
m a -> m a -> a -> m ()
from which we can build

impl = \x y -> (x --> y) () :: m () -> m () -> m ()

Now, in the bounded distributive lattice Bool the right adjoint to (&&) x is the logical implication (→) x and we check

ghci> guard True `impl` guard True :: Maybe ()
Just ()
ghci> guard True `impl` guard False :: Maybe ()
Nothing
ghci> guard False `impl` guard False :: Maybe ()
Just ()
ghci> guard False `impl` guard True :: Maybe ()
Just ()

Summarising, for some MonadPlus monads m, the type m () looks like a bounded lattice with
least = mzero
greatest = return ()
max = mplus
min = meet
and for a subclass of these monads, including m = Maybe, m () is a Heyting algebra with the right adjoint to min defined as the impl function above.

On to a more complicated example. Let R = [0,∞] denote the type of non-negative real numbers, including positive infinity, (totally) ordered by the obvious ≤ relation. Observe that for each r :: R, the multiplication function
(*) r :: R -> R
is order-preserving if we define 0 * ∞ = 0. Hence we can ask for its right adjoint, which will be a function of type R -> R as well. Exercise: Prove that the right adjoint is division (/) of real numbers, with boundary cases
r / 0 = ∞ = ∞ / x for all r and x.
This demonstrates the parallels between logical implication and divison: They are both right adjoints in a certain sense. Is there a monad m with m () = R? Yes: The monad G of measures, a.k.a. the Giry monad. Is is not a Haskell monad, though. There is no Haskell type which has R as denotational semantics. But let's pretend. Let's pretend all sets are finite and of Eq class. Then a measure on X can be encoded by a list of type [(X,R)]. It is what packages like probable do.
What is (/\) for this monad of measures? Look at the type:
(/\) :: G a -> (a -> R) -> G a
It modifies a measure by a real-valued function. If x :: X previously had the weight r, then the new weight is r * (f x). Obviously, for each measure dx the operator \f -> dx /\ f is order-preserving, since multiplication is monotone. Hence we can ask for a right adjoint. It must be a function of type
G a -> G a -> (a -> R)
associating a real-valued function to a pair of measures. For a = () we already know the answer: It is division. For all other types, the right adjoint is known as the Radon-Nikodym derivative [*]. It is an important gadget in machine learning because it can be used to build conditional probabilites. Intuitively, you can see the connection: For a conditional probability, you first filter the list [(X,R)] for all the allowed x, then divide by the sum of all remaining weights to make the total weight 1 again. Hence without division there is no conditional probability.

Moral of the story: Logical implication and conditional probabilities are both instances of the same problem, only for different monads.

-- Olaf

[*] Again, I am sweeping stuff under the carpet. On function space (X -> R), the order ≤ is defined up to sets of measure zero.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.