[Haskell-cafe] 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.

[1] http://leventerkok.github.io/papers/erkok-thesis.pdf
[2] https://hackage.haskell.org/package/mtl

On Thu, Oct 25, 2018 at 7:43 AM Benjamin Redelings <
benjamin.redelings at gmail.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181025/5f30ab4a/attachment.html>