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

add Applicative and Monad instances for Label #164

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

subttle
Copy link
Contributor

@subttle subttle commented Feb 4, 2019

No description provided.

@snowleopard
Copy link
Owner

Thanks @subttle! While the instances look reasonable, it's not obvious to me that Applicative and Monad laws hold. Could you give some intuition about why you chose this particular implementation, and why it satisfies the expected laws?

@snowleopard
Copy link
Owner

@subttle Strange: I received an email notification with your comment about using QuickCheck, but it doesn't seem to be here. Have you deleted it, or is it a GitHub glitch?

Regarding using QuickCheck: this requires an Eq Label instance, but we don't have one. Which one did you use?

@subttle
Copy link
Contributor Author

subttle commented Feb 4, 2019

Hi! Thank you for considering this PR.

The notification was because I went to shift-enter for a newline but instead entered the comment, doh!

While not a substitute for a proof (I will try to do one which considers the appropriate graph laws), I had done some basic checks with QuickCheck and checkers.

instance (Arbitrary a) => Arbitrary (Label a) where
    -- This particular instance may be large or even not terminate
    arbitrary = oneof [ pure Zero
                      , pure One
                      , fmap Symbol arbitrary
                      , fmap Star arbitrary
                      , liftA2 (:+:) arbitrary arbitrary
                      , liftA2 (:*:) arbitrary arbitrary
                      ]

And also adding a Generic to the derived list for Label, then checking with checkers.

λ> quickBatch $ functor (undefined :: Label (Int, String, Char))

functor:
  identity: +++ OK, passed 500 tests.
  compose:  +++ OK, passed 500 tests.
λ> quickBatch $ applicative (undefined :: Label (Int, String, Char))

applicative:
  identity:     +++ OK, passed 500 tests.
  composition:  +++ OK, passed 500 tests.
  homomorphism: +++ OK, passed 500 tests.
  interchange:  +++ OK, passed 500 tests.
  functor:      +++ OK, passed 500 tests.
λ> quickBatch $ monad (undefined :: Label (Int, String, Char))

monad laws:
  left  identity: +++ OK, passed 500 tests.
  right identity: +++ OK, passed 500 tests.
  associativity:  +++ OK, passed 500 tests.
λ> 

Although, I had only used an instance of EqProp which uses the default eq implementation (I think this is structural equality by default which I'm sure you do not use) so I should try again after updating that accordingly. As far as intuition goes, I think the implementation of pure is the natural one considering the implementation of Functor, and the rest of the implementation I drew inspiration from a tree monad implementation. I will comment again soon when I can try out what I mentioned.

@snowleopard
Copy link
Owner

Thanks @subttle! One simple thing to do to at least resolve the question about the validity of the Applicative instance is to use (<*>) = ap as the implementation. This is required by Applicative-Monad laws anyway, plus makes the implementation simpler.

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

Successfully merging this pull request may close these issues.

2 participants