krisajenkins / remotedata

Tools for fetching data from remote sources (incl. HTTP).
MIT License
249 stars 23 forks source link

`andThen` is not a lawful Monad #40

Open Fresheyeball opened 3 years ago

Fresheyeball commented 3 years ago

After doing some work porting this to Haskell and I discovered that there is an inconsistency between andMap and andThen.

Specifically it breaks the ap law:

ap mf ma = mf >>= (\f -> ma >>= (\a -> return (f a)))

ap == (<*>)

or in an Elm context

ap ma mf = andThen (\a -> andThen (\f -> Success (f a)) mf) ma

ap == andMap

But this is not the case, given this counter example:

ap     NotAsked Loading = NotAsked
andMap NotAsked Loading = Loading

What you have right now for andMap is a valid Applicative, but the specific Applicative it is does not lead to Monad. The correct Applicative to match andThen would be as follows:

andMap : RemoteData e a -> RemoteData e (a -> b) -> RemoteData e b
andMap wrappedValue wrappedFunction =
    case ( wrappedFunction, wrappedValue ) of
        ( Success f, Success value ) ->
            Success (f value)

        ( _, Failure error ) ->
            Failure error

        ( _, Loading ) ->
            Loading

        ( _, NotAsked ) ->
            NotAsked

        ( Failure error, _ ) ->
            Failure error

        ( Loading, _ ) ->
            Loading

        ( NotAsked, _ ) ->
            NotAsked

Now the counter example is lawful

ap     NotAsked Loading = NotAsked
andMap NotAsked Loading = NotAsked
turboMaCk commented 3 years ago

I think this is correct observation except for the fact that I don't see how this could make current implementation unlawful. This can be due to my lack of understanding for sure but I would like if you can explain what leads to you to such conclusion.

The function ap:

ap mf ma = mf >>= (\f -> ma >>= (\a -> return (f a)))

is correct proof that every monad must be applicative as well. However I'm not aware that ap == (<*>) is some actual law. It kind of makes sense in languages with hierarchy of typeclasses (Haskell, Purescript...) but I don't think it's a law. If anything because Applicative is preceding Monad I would expect it to be one of monad laws if anything but it's not.

This all being said I think logical thing would be to return NotAsked when ever one of the constructors is NotAsked since that would seem the most practical to me. That means even andMap Loading NotAsked == NotAsked