A law for MonadReader

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

A law for MonadReader

Li-yao Xia-2
Hello Café,

While trying to document laws for mtl classes
(https://github.com/haskell/mtl/issues/5) I have been puzzling over the
subtle logical relationships between a few variants.

Consider the following four possible laws for MonadReader's ask:

(1) (ask >> ask) = ask

(2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r ->
return (r, r))

(3) (ask >> return ()) = return ()

Let

reader :: MonadReader r m => (r -> a) -> m a
reader f = fmap f ask

(4) reader is a monad homomorphism from ((->) r) to m, i.e.:

reader (\_ -> a) = return a
(reader m >>= \x -> reader (k x)) = reader (m >>= k)

Question: which ones imply which ones?

Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2)
say that ask is idempotent ("asking twice is the same as asking once"),
but (3) and (4) imply the stronger property of nullipotence ("ask has no
side effects").

---

Any help with the following conjectures is welcome (we're assuming the
monad laws hold in the first place):

A. (1) and (2) are equivalent.

I can prove that (2) implies (1). However the converse eludes me.

B. (3) and (4) are equivalent.

Again, I can prove that (4) implies (3), but I had no success with the
converse.

C. ((3) or (4)) implies ((1) and (2))

((3) implies (1)), and ((4) implies ((1) and (2))) are straightforward,
but without the above equivalence, the missing bit is ((3) implies (2))

It seems that parametricity plays an important role in the conjectured
implications. I didn't manage to apply free theorems to this problem,
but perhaps you will have better luck.

Regards,
Li-yao
_______________________________________________
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: A law for MonadReader

Benjamin Fox
As far as I can tell, (1) on it's own does not imply (2). I even have a counterexample, assuming no further laws on `ask` and no laws on `local`. Requiring `local` makes things more complicated (as `local` always does) and it may well be that a sufficiently strong law for `local` would rule out cases where (1) and (2) differ. (I'm not sure of that, I'll need to think about it a bit more.)

Here is the counterexample:

instance MonadReader (IORef Int) IO where
    ask = newIORef 0
    local _ = id

This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0. But not (2): (newIORef 0 >>= \r1 -> newIORef 0 >>= \r2 -> return (r1, r2)) (newIORef 0 >>= \r -> return (r, r)). The left side of (2) returns a tuple containing two different IORefs (both containing 0), whereas the right side returns a tuple containing two references to the same IORef.


On Sun, Jun 3, 2018 at 2:19 AM Li-yao Xia <[hidden email]> wrote:
Hello Café,

While trying to document laws for mtl classes
(https://github.com/haskell/mtl/issues/5) I have been puzzling over the
subtle logical relationships between a few variants.

Consider the following four possible laws for MonadReader's ask:

(1) (ask >> ask) = ask

(2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r ->
return (r, r))

(3) (ask >> return ()) = return ()

Let

reader :: MonadReader r m => (r -> a) -> m a
reader f = fmap f ask

(4) reader is a monad homomorphism from ((->) r) to m, i.e.:

reader (\_ -> a) = return a
(reader m >>= \x -> reader (k x)) = reader (m >>= k)

Question: which ones imply which ones?

Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2)
say that ask is idempotent ("asking twice is the same as asking once"),
but (3) and (4) imply the stronger property of nullipotence ("ask has no
side effects").

---

Any help with the following conjectures is welcome (we're assuming the
monad laws hold in the first place):

A. (1) and (2) are equivalent.

I can prove that (2) implies (1). However the converse eludes me.

B. (3) and (4) are equivalent.

Again, I can prove that (4) implies (3), but I had no success with the
converse.

C. ((3) or (4)) implies ((1) and (2))

((3) implies (1)), and ((4) implies ((1) and (2))) are straightforward,
but without the above equivalence, the missing bit is ((3) implies (2))

It seems that parametricity plays an important role in the conjectured
implications. I didn't manage to apply free theorems to this problem,
but perhaps you will have better luck.

Regards,
Li-yao
_______________________________________________
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: A law for MonadReader

Viktor Dukhovni


> On Jun 3, 2018, at 3:32 AM, Benjamin Fox <[hidden email]> wrote:
>
> Here is the counterexample:
>
> instance MonadReader (IORef Int) IO where
>     ask = newIORef 0
>     local _ = id
>
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Can you explain what you mean?

Prelude> :m + Data.IORef
Prelude Data.IORef> let z = 0 :: Int
Prelude Data.IORef> a <- newIORef z
Prelude Data.IORef> b <- newIORef z
Prelude Data.IORef> let c = newIORef z
Prelude Data.IORef> let d = newIORef z
Prelude Data.IORef> a == b
False
Prelude Data.IORef> c == d

<interactive>:8:1: error:
    • No instance for (Eq (IO (IORef Int))) arising from a use of ‘==’
    • In the expression: c == d
      In an equation for ‘it’: it = c == d

--
        Viktor.

_______________________________________________
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: A law for MonadReader

Benjamin Fox
Here, as in general in the definitions of laws, the relevent question is referential transparency, not Eq instances.

(You'll note that generally in the definitions of laws the symbol "=" is used, not "==". Sometimes that's written as "≡", to be even clearer about what it represents, as for instance the Monad Laws page on the Haskell wiki does.)

For some laws, like the "fmap id = id" Functor law, this is obviously the only possible interpretation, as both sides of that equation are necessarily functions, and functions don't have an Eq instance.

So in this case, what the first law is asking for is that "ask >> ask" is the same as "ask", in that any instance of "ask" in a program can be replaced with "ask >> ask", or vice versa, without that changing the program's semantics.


On Sun, Jun 3, 2018 at 9:47 AM Viktor Dukhovni <[hidden email]> wrote:


> On Jun 3, 2018, at 3:32 AM, Benjamin Fox <[hidden email]> wrote:
>
> Here is the counterexample:
>
> instance MonadReader (IORef Int) IO where
>     ask = newIORef 0
>     local _ = id
>
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Can you explain what you mean?

Prelude> :m + Data.IORef
Prelude Data.IORef> let z = 0 :: Int
Prelude Data.IORef> a <- newIORef z
Prelude Data.IORef> b <- newIORef z
Prelude Data.IORef> let c = newIORef z
Prelude Data.IORef> let d = newIORef z
Prelude Data.IORef> a == b
False
Prelude Data.IORef> c == d

<interactive>:8:1: error:
    • No instance for (Eq (IO (IORef Int))) arising from a use of ‘==’
    • In the expression: c == d
      In an equation for ‘it’: it = c == d

--
        Viktor.

_______________________________________________
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: A law for MonadReader

Li-yao Xia-2
In reply to this post by Benjamin Fox
On 06/03/2018 03:32 AM, Benjamin Fox wrote:

> As far as I can tell, (1) on it's own does not imply (2). I even have a
> counterexample, assuming no further laws on `ask` and no laws on
> `local`. Requiring `local` makes things more complicated (as `local`
> always does) and it may well be that a sufficiently strong law for
> `local` would rule out cases where (1) and (2) differ. (I'm not sure of
> that, I'll need to think about it a bit more.)
>
> Here is the counterexample:
>
> instance MonadReader (IORef Int) IO where
>      ask = newIORef 0
>      local _ = id
>
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0. But not
> (2): (newIORef 0 >>= \r1 -> newIORef 0 >>= \r2 -> return (r1, r2))≠
> (newIORef 0 >>= \r -> return (r, r)). The left side of (2) returns a
> tuple containing two different IORefs (both containing 0), whereas the
> right side returns a tuple containing two references to the same IORef.
>

Thanks Benjamin, that's a good counterexample. It also shows that the
other missing implications (((3) => (4)) and ((3) => (2))) do not hold.

Indeed, I had incorrectly assumed that even if we discard the result of
an action, we can reconstruct it by observing the action's effects, and
(1) and (3) were meant to imply that those effects must be trivial, but
newIORef contradicts this because the creation of a new reference is
only made observable by using it.

Li-yao
_______________________________________________
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: A law for MonadReader

Ivan Perez
In reply to this post by Benjamin Fox
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Doesn't this change the state in the IO monad (which is why (2) does not hold for this instance)? If so, would it still be true?

Ivan

On 3 June 2018 at 07:55, Benjamin Fox <[hidden email]> wrote:
Here, as in general in the definitions of laws, the relevent question is referential transparency, not Eq instances.

(You'll note that generally in the definitions of laws the symbol "=" is used, not "==". Sometimes that's written as "≡", to be even clearer about what it represents, as for instance the Monad Laws page on the Haskell wiki does.)

For some laws, like the "fmap id = id" Functor law, this is obviously the only possible interpretation, as both sides of that equation are necessarily functions, and functions don't have an Eq instance.

So in this case, what the first law is asking for is that "ask >> ask" is the same as "ask", in that any instance of "ask" in a program can be replaced with "ask >> ask", or vice versa, without that changing the program's semantics.


On Sun, Jun 3, 2018 at 9:47 AM Viktor Dukhovni <[hidden email]> wrote:


> On Jun 3, 2018, at 3:32 AM, Benjamin Fox <[hidden email]> wrote:
>
> Here is the counterexample:
>
> instance MonadReader (IORef Int) IO where
>     ask = newIORef 0
>     local _ = id
>
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Can you explain what you mean?

Prelude> :m + Data.IORef
Prelude Data.IORef> let z = 0 :: Int
Prelude Data.IORef> a <- newIORef z
Prelude Data.IORef> b <- newIORef z
Prelude Data.IORef> let c = newIORef z
Prelude Data.IORef> let d = newIORef z
Prelude Data.IORef> a == b
False
Prelude Data.IORef> c == d

<interactive>:8:1: error:
    • No instance for (Eq (IO (IORef Int))) arising from a use of ‘==’
    • In the expression: c == d
      In an equation for ‘it’: it = c == d

--
        Viktor.

_______________________________________________
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: A law for MonadReader

Benjamin Fox
No, newIORef does not itself change any state. It returns an IO value because each invocation returns a different IORef, but there isn't any way to tell how many or which IORefs were created. So newIORef 0 >> newIORef 0 doesn't differ in any way from newIORef 0, except in that an additional object being created and then immediately garbage collected. This is exactly the same as how the expression Just 0 >> Just 0 is the equivalent to Just 0, except again with an additional object being created and then garbage collected behind the scenes.

If you'd agree that Just 0 >> Just 0 ≡ Just 0, then I think you have to also agree that newIORef 0 >> newIORef 0 ≡ newIORef 0. In both cases, each side of the equivalence has the exact same semantics (save perhaps for additional allocations, which we generally ignore when doing this kind of analysis). No program which you could write could differentiate between the two sides (again, save by doing some trickery such as benchmarking the program and seeing which allocates more.)


On Sun, Jun 3, 2018 at 6:56 PM Ivan Perez <[hidden email]> wrote:
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Doesn't this change the state in the IO monad (which is why (2) does not hold for this instance)? If so, would it still be true?

Ivan

On 3 June 2018 at 07:55, Benjamin Fox <[hidden email]> wrote:
Here, as in general in the definitions of laws, the relevent question is referential transparency, not Eq instances.

(You'll note that generally in the definitions of laws the symbol "=" is used, not "==". Sometimes that's written as "≡", to be even clearer about what it represents, as for instance the Monad Laws page on the Haskell wiki does.)

For some laws, like the "fmap id = id" Functor law, this is obviously the only possible interpretation, as both sides of that equation are necessarily functions, and functions don't have an Eq instance.

So in this case, what the first law is asking for is that "ask >> ask" is the same as "ask", in that any instance of "ask" in a program can be replaced with "ask >> ask", or vice versa, without that changing the program's semantics.


On Sun, Jun 3, 2018 at 9:47 AM Viktor Dukhovni <[hidden email]> wrote:


> On Jun 3, 2018, at 3:32 AM, Benjamin Fox <[hidden email]> wrote:
>
> Here is the counterexample:
>
> instance MonadReader (IORef Int) IO where
>     ask = newIORef 0
>     local _ = id
>
> This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0.

Can you explain what you mean?

Prelude> :m + Data.IORef
Prelude Data.IORef> let z = 0 :: Int
Prelude Data.IORef> a <- newIORef z
Prelude Data.IORef> b <- newIORef z
Prelude Data.IORef> let c = newIORef z
Prelude Data.IORef> let d = newIORef z
Prelude Data.IORef> a == b
False
Prelude Data.IORef> c == d

<interactive>:8:1: error:
    • No instance for (Eq (IO (IORef Int))) arising from a use of ‘==’
    • In the expression: c == d
      In an equation for ‘it’: it = c == d

--
        Viktor.

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