Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

andThen is not a lawful Monad #40

Open
Fresheyeball opened this issue Jan 5, 2021 · 1 comment
Open

andThen is not a lawful Monad #40

Fresheyeball opened this issue Jan 5, 2021 · 1 comment

Comments

@Fresheyeball
Copy link

Fresheyeball commented Jan 5, 2021

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
Copy link

turboMaCk commented Oct 8, 2021

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants