blamario / monoid-subclasses

Subclasses of Monoid with a solid theoretical foundation and practical purposes
BSD 3-Clause "New" or "Revised" License
33 stars 9 forks source link

Suspected unlawful `Monus` instance for `Maybe`. #38

Closed jonathanknowles closed 1 year ago

jonathanknowles commented 1 year ago

Hi @blamario

I think I've discovered a counterexample to the Monus laws for Maybe.

I tested against the latest version of monoid-subclasses in this repository: 9255072c640f590c92c9ebc9ddc153555501dad7

Counterexample

First some imports:

> import Data.Monoid (Sum (Sum))
> import Data.Monoid.GCD (OverlappingGCDMonoid (..))
> import Data.Monoid.Monus (Monus (..))
> import Numeric.Natural (Natural)

Then define the counterexample arguments:

> a = Just (Sum (0 :: Natural))
> b = Just (Sum (0 :: Natural))

The laws stated in the documentation are as follows (source):

When we test these laws with the example arguments, it seems that the laws are not satisfied:

> (<\>) a b == flip stripPrefixOverlap a b
False
> (<\>) a b == flip stripSuffixOverlap a b
False

If we evaluate just the LHS, we get:

> (<\>) a b
Just (Sum {getSum = 0})

If we evaluate just the RHS, we get:

> flip stripPrefixOverlap a b
Nothing
> flip stripSuffixOverlap a b
Nothing

Perhaps I've interpreted the laws incorrectly?

Many thanks!

Jonathan

jonathanknowles commented 1 year ago

This might actually be a problem with the Monus instance for Maybe, rather than being specific to Maybe (Sum Natural).

I can also reproduce the issue when testing with values of Maybe ():

> a = Just ()
> b = Just ()
> (<\>) a b == flip stripPrefixOverlap a b
False
> (<\>) a b == flip stripSuffixOverlap a b
False
> (<\>) a b
Just ()
> flip stripPrefixOverlap a b
Nothing
> flip stripSuffixOverlap a b
Nothing
jonathanknowles commented 1 year ago

I believe I've found a fix for this issue here https://github.com/blamario/monoid-subclasses/pull/39.

blamario commented 1 year ago

Fixed by @jonathanknowles