[Haskell-cafe] Could someone teach me why we use Data.Monoid?

[wren ng thornton]

Stephen Tetley wrote:
> Hi Edward
> 
> Many thanks.
> 
> I've mostly used groupoid for 'string concatenation' on types that I
> don't consider to have useful empty (e.g PostScript paths, bars of
> music...), as string concatenation is associative it would have been
> better if I'd used semigroup in the first place (bounding box union
> certainly looks associative to me as well).
> 
> Are magma and semigroup exclusive, i.e. in the presence of both a
> Magma class and a Semigroup class would it be correct  that Magma
> represents only 'magma-op' where op isn't associative and Semigroup
> represents 'semigroup-op' where the op is associative?


     Magma     = exists S : Set
               , exists _*_ : (S,S)->S

     Semigroup = exists (S,*) : Magma
               , forall a b c:S. a*(b*c) = (a*b)*c

     Monoid    = exists (S,*,assoc) : Semigroup
               , exists e:S. forall a:S. e*a = a = a*e

     Group     = exists (S,*,assoc,e) : Monoid
               , forall a:S. exists a':S. a'*a = e = a*a'

Personally, I don't think magmas are worth a type class. They have no 
structure and obey no laws which aren't already encoded in the type of 
the binop. As such, I'd just pass the binop around. There are far too 
many magmas to warrant making them implicit arguments and trying to 
deduce which one to use based only on the type of the carrier IMO.

But if we did have such a class, then yes the (Magma s) constraint would 
only imply the existence of a binary operator which s is closed under, 
whereas the (Semigroup s) constraint would add an additional implication 
that the binary operator is associative. And we should have Semigroup 
depend on Magma since every semigroup is a magma. Unfortunately, 
Haskell's type classes don't have any general mechanism for stating laws 
as part of the class definition nor providing proofs as part of the 
instance.


> When I decided to use a Groupoid class, I was being a bit lazy-minded
> and felt it could represent a general binary op that _doesn't have to
> be_ associative but potentially could be.

But groupoids do have to be associative (when defined). They're just 
like groups, except that the binop can be a partial function, and 
instead of a neutral element they have the weaker identity criterion (if 
a*b is defined then a*b*b' = a and a'*a*b = b).

Groupoids don't make a lot of sense to me as "string concatenation"-like 
because of the inversion operator. Some types will support the idea of 
"negative letters" without supporting empty strings, but I can't think 
of any compelling examples off-hand. Then again, I deal with a lot of 
monoids which aren't groups and a lot of semirings which aren't rings, 
so I don't see a lot of inversion outside of the canonical examples.

-- 
Live well,
~wren