Add Grothendieck group

[hrb90]

So we have an Abelian type and a Commutative typeclass, right? And categorically there's a forgetful functor from abelian groups to commutative monoids --- and that functor has a left adjoint, which is the Grothendieck group. We already have one free construction in the library, why not another? :wink:

I kind of doubt this would be actually useful to anybody, but I also think of purescript-group as partially a vehicle to teach functional programmers about groups so they have more mental models for category theory, and this would accomplish that nicely.

[hdgarrood]

I’ve yet to come across a good way of representing equivalence classes in code; the best I’ve been able come up with is some canonicalisation type class like this:

class (Commutative a, Monoid a) <= GrothendieckCanonical a where
  canonicalise :: Tuple a a -> Tuple a a

which should designate one element as the ‘canonical’ representative for each equivalence class, and then send any element of any class to the canonical representative for its class. I’d be interested to see if you have some alternative idea in mind.

[morganthomas]

I'm not opposed to including this. In general I would like to avoid bloating the lib with mathematical constructions that will not have practical applications, to increase the signal to noise ratio for most users of the library docs. On the other hand I also see the educational/research value of exploring and documenting pure math in PureScript. So I'm not of the opinion that all constructions in the library must have known practical applications. In this particular instance I wouldn't object to including the construction. I bet my general opinion here is similar to where others are at, but I'd be interested in hearing about any diversity of opinion on this topic that exists among us.

[hrb90]

@hdgarrood Yep, that's more or less the approach I was thinking of as well, and it's similar to what we're doing with the free group.