`Sum Natural` is not a lawful `Group` instance.

[jonathanknowles]

Hi there!

First of all, thank you for creating and maintaining this library—I really appreciate the work that has gone into it!

While experimenting, I happened to notice that Sum Natural is an instance of Group, which caught me by surprise. Since the natural numbers under addition don’t form a group, I was curious about the reasoning behind this instance.

Looking at the laws stated in this library, the law a <> invert a == mempty doesn’t hold for any non-zero value of Sum Natural, since applying invert to a non-zero value results in an arithmetic underflow exception. That behaviour is understandable given that, for historical reasons, base defines Natural as an instance of Num, and that the Group instance for Sum a is currently defined as:

instance Num a => Group (Sum a) where
  invert = Sum . negate . getSum

One could argue that the decision (presumably made long ago!) to make Natural an instance of Num was questionable, since this means the Num laws can’t always be strictly relied upon. Though given the mathematical focus of the groups library, I wonder whether maintaining this behaviour is the best approach?

Some other libraries have made a choice to avoid relying on the customary Num laws always holding. For example, in monoid-subclasses, Sum Natural is an instance of PositiveMonoid, but Sum Integer is not.

Perhaps a similar approach could be taken here? I suppose that one solution might be to introduce a helper class, such as:

class Num a => SumGroup a

instance SumGroup Int
instance SumGroup Int8
instance SumGroup Int16
instance SumGroup Int32
instance SumGroup Int64
instance SumGroup Integer
...

Then, the constraints for the Group instance of Sum a could be strengthened:

instance SumGroup a => Group (Sum a)

This would have the advantage of allowing types to be added on a case-by-case basis (and giving downstream users the flexibility to take the same measured approach for their own types). The downside, of course, is that making this change would require some caution to avoid breaking existing code.

I’d love to hear your thoughts on this. Thanks again for all your work on this library.

Best regards,
Jonathan

[Taneb]

Hi! Thanks for this issue. It's something I did think about. The big cost to your suggestion is that I can't make instances for number types I don't know about, ones that (hypothetically) get added to base in the future, or ones in other packages. I don't think that cost is worth it. I will consider adding documentation to the instance saying that it doesn't work as expected for Natural.

[jonathanknowles]

Hi! Thanks for this issue. It's something I did think about. The big cost to your suggestion is that I can't make instances for number types I don't know about, ones that (hypothetically) get added to base in the future, or ones in other packages. I don't think that cost is worth it. I will consider adding documentation to the instance saying that it doesn't work as expected for Natural.

Hi! Thanks for the response—I really appreciate you taking the time to consider this.

I understand your concern about not being able to define instances for unknown future types, and I can emphasise with the maintenance trade-off involved. However, I hope it's still okay to share a few thoughts with you:

Regarding unknown future types

You mention the concern that restricting the Group (Sum a) instance would mean we can’t define instances for number types that don’t yet exist. Am I right in thinking that your main concern relates to the maintenance overhead?

If so, would one possible mitigation be that users of the library would likely notice when a particular instance they need (for a type in base) is missing and submit a PR to add it? (Hope I've not misunderstood your argument here.) In my case, I'd be happy to submit PRs like this if you're open to that.

In the case of monoid-subclasses, I think this cautious approach has been used to good effect to incorporate new instances. For example: blamario/monoid-subclasses#55

Though I can appreciate that this "adding instances for new types as they appear in base" approach would require ongoing maintenance work.

One downside though of the current approach means that any new Num instance will automatically get a Group (Sum a) instance, even if it doesn’t actually satisfy the group laws. This seems like a bigger risk, since it could silently introduce and help propagate invalid instances into the ecosystem.

Regarding customary laws

In the case of Sum Natural, most of the methods of Num still work correctly—it’s just negate that doesn’t work as expected, which is annoying, but arguably doesn't negate (apologies for the pun 😄) the overall usefulness of Num for those types. People have become accustomed to the fact (over time) that the Num laws are customary, which is not ideal, but of course hard to change due to the nature of base being a core library.

However, in Group, invert is the primary operation, meaning the core functionality of the instance is problematic in the case of Sum Natural. A type that only partially satisfies Num can often still be useful, but a Group instance that always fails on its main method (except for mempty) seems more problematic.

Regarding documentation

I agree with you that documenting the issue is a strict improvement over the status quo! But I do worry that it doesn’t prevent incorrect behaviour from propagating, mainly because the compiler isn't aware of documentation, and developers using downstream libraries may not even be aware that that particular piece of documentation exists.

Which brings me to:

Downstream libraries

Here's a concrete example of an issue this causes in practice:

I maintain a package called monoidmap, which defines the MonoidMap k v type, which maps keys to non-null monoidal values. The key requirement is that v must be an instance of MonoidNull (which implies Monoid). I also define a Group instance as follows:

instance Group v => Group (MonoidMap k v) where
    invert m = MonoidMap.map invert m

This definition rests on the idea that if v is a valid Group, then MonoidMap k v is also a valid Group. However, because Sum Natural is currently an instance of Group, this means MonoidMap k (Sum Natural) is also automatically a Group—which is clearly incorrect, as invert (the primary operation of Group) is not properly defined for Sum Natural.

Although this is a trivial example, I think this isn't just a theoretical concern—it means that any downstream library or user relying on Group (Sum v) could unintentionally end up releasing even more invalid Group instances into the ecosystem (like the MonoidMap example above).

Anyway, I just wanted to share these thoughts with you. I understand that on balance you may still opt to keep the current design (after all, Natural is a bit of an outlier here). If so, I respect your decision and appreciate all the work you've put into this. If you'd like to discuss further, would be happy to.

All the best
Jonathan