[Haskell-cafe] A law for MonadReader

[Ivan Perez]

 > 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 <foxbenjaminfox at gmail.com> 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
> <https://wiki.haskell.org/Monad_laws> 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 <ietf-dane at dukhovni.org>
> wrote:
>
>>
>>
>> > On Jun 3, 2018, at 3:32 AM, Benjamin Fox <foxbenjaminfox at gmail.com>
>> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180603/70ddc188/attachment.html>