mfix for a nested monad

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

mfix for a nested monad

Benjamin Redelings
Hi,

I'm trying to implement mfix for a monad that is nested inside another
monad.  I came up with the following logic for how to implement this,
but I suspect there are some things I'm missing. My conclusion is that I
want

interpret (MFix f) = mfix (interpret.f)

Does this seem right?  Has this situation been discussed somewhere?

-BenRI


P.S. Here's what I mean by the monad being nested in another monad. 
Let's say that the monad M2 has interpreter i2, with type

i2 :: M2 a -> M1 a

and then M1 is the other monad, and has interpreter i1:

i1 :: M1a -> a

I suppose that the nesting is really a nesting of interpreters.



P.P.S. I came up with some equational reasoning for how to treat mfix in
the i2 interpreter.

(a) For some interpreters `i`, it makes sense to require

     i (mfix f) = let x = (i . f) x in x

(b) I want the composition of interpreters (i1.i2) to act like (a) above:

     (i1 . i2) (mfix f) = let x = (i1 . i2 . f) x in x

(c) Rearranging, and then substituting using (a):

     i1 (i2 (mfix f)) = let x = i1 . (i2 . f) x in x
                            = i1 (mfix (i2 . f))

(d) Therefore, we could set

     i2 (mfix f) = mfix (i2 . f)

I'm probably going to make a `data` declaration for M2 so I could
actually write

     i2 (Mfix f) = mfix (i2 . f)

-BenRI

_______________________________________________
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: mfix for a nested monad

Levent Erkok
Hi Benjamin,

It's impossible to answer your question without precisely pinning down what you mean by an "embedding." For each monad it is defined for, mfix is required to satisfy three laws: Strictness, Purity, and Left-Shrinking. If you can show that your "embedded" definitions satisfy those, then yes; you do have a valid value-recursion operator. You can find a description of these laws in Chapter 2 of [1]. Since you haven't specified what properties your "embedding" has, it's not possible to say anything in isolation.

More traditionally, adding "new" effects to old monads in Haskell is achieved by using monad transformers [2]. Perhaps that's what you have in mind? If that's the case, then Section 4.9 of [1] lays out how mfix from the base monad can be lifted through a monad transformer stack while preserving the properties. If you can cast your design in terms of MTL style transformers, this would be the way to go. And if you do use the MTL package, then you'll have your MonadFix instances for free, since the library already defines them via the usual instance mechanism.

Cheers,

-Levent.


On Thu, Oct 25, 2018 at 7:43 AM Benjamin Redelings <[hidden email]> wrote:
Hi,

I'm trying to implement mfix for a monad that is nested inside another
monad.  I came up with the following logic for how to implement this,
but I suspect there are some things I'm missing. My conclusion is that I
want

interpret (MFix f) = mfix (interpret.f)

Does this seem right?  Has this situation been discussed somewhere?

-BenRI


P.S. Here's what I mean by the monad being nested in another monad. 
Let's say that the monad M2 has interpreter i2, with type

i2 :: M2 a -> M1 a

and then M1 is the other monad, and has interpreter i1:

i1 :: M1a -> a

I suppose that the nesting is really a nesting of interpreters.



P.P.S. I came up with some equational reasoning for how to treat mfix in
the i2 interpreter.

(a) For some interpreters `i`, it makes sense to require

     i (mfix f) = let x = (i . f) x in x

(b) I want the composition of interpreters (i1.i2) to act like (a) above:

     (i1 . i2) (mfix f) = let x = (i1 . i2 . f) x in x

(c) Rearranging, and then substituting using (a):

     i1 (i2 (mfix f)) = let x = i1 . (i2 . f) x in x
                            = i1 (mfix (i2 . f))

(d) Therefore, we could set

     i2 (mfix f) = mfix (i2 . f)

I'm probably going to make a `data` declaration for M2 so I could
actually write

     i2 (Mfix f) = mfix (i2 . f)

-BenRI

_______________________________________________
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.