Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why is this applicative instance unlawful?

I was reading about monad transformers and found this apparently well known article - A Gentle Introduction to Monad Transformers. What caught my attention was the part where the author describes an applicative instance for a makeshift ExceptT transformer, but leaves a warning mentioning that that instance is unlawful.

Here's the code:

data EitherIO e a = EitherIO {
    runEitherIO :: IO (Either e a)
}

instance Functor (EitherIO e) where
    fmap f = EitherIO . fmap (fmap f) . runEitherIO

instance Applicative (EitherIO e) where
    pure    = EitherIO . return . Right
    f <*> x = EitherIO $
        liftA2 (<*>)
            (runEitherIO f)
            (runEitherIO x)

And the warning:

Warning: A very sharp-sighted reader has pointed out to me that this applicative instance is unlawful. Specifically, it executes the side effects of the right-hand side unconditionally. The expectation of a lawful instance is that it should only execute the side-effects of the right-hand side if the left-hand side was a successful operation.

I am assuming that specifically the implementation of <*> is the problem.

So my main question is: which laws exactly does this instance not satisfy?

From what I can see, the four applicative laws are satisfied (I might be wrong of course). The author says that the problem is that side effects on the right (I am assuming, to the right of <*>) are executed even if the left-hand side was not a successful operation (I am assuming, "successful operation" means that the IO action would yield a Right value when executed).

While I can see that it makes sense from a usage standpoint, it would still be enlightening to see which laws exactly are not satisfied here, and why.

Also, the explanation of why the instance is unlawful mentions side-effects, which makes the reasoning kind of apply only for the IO monad? But at the end of the text, as a finishing move, we change the IO monad to a general monad and make it a parameter of the described data type. This leads me to another question: if we imagine that I was writing this monad transformer myself, what kind of reasoning would I need to apply, to notice that the described applicative instance is indeed unlawful, without resorting to thinking about specific monads that could be used with this transformer?

like image 867
Dmitry Avatar asked Jan 06 '19 03:01

Dmitry


1 Answers

The Applicative instance is lawful. In fact, it's the same instance as Compose IO (Either e). Compositions of applicative functors are applicative (this is one of the very nice things that applicatives have that monads don't).

However, the following is also listed in the laws section of the documentation:

If f is also a Monad, it should satisfy

pure = return
(<*>) = ap
(*>) = (>>)

And this is where the problem is, since there can be no monad that corresponds to the given applicative (this is where the comment about conditional execution of the RHS comes into play). So the Applicative and Monad instances, while each in isolation is lawful, do not agree, and that is punishable by death.

like image 132
luqui Avatar answered Sep 27 '22 18:09

luqui