Free is not a Semiring

[hdgarrood]

A Semiring requires commutative addition, but the addition operation for Free is list concatenation, which is not commutative.

It looks like Free is an encoding of the idea described in the wikipedia article on Semirings

• Given an alphabet (finite set) Σ, the set of formal languages over Σ (subsets of Σ∗) is a semiring with product induced by string concatenation and addition as the union of languages (i.e. simply union as sets). The zero of this semiring is the empty set (empty language) and the semiring's unit is the language containing as its sole element the empty string.[12]
• Generalising the previous example (by viewing Σ∗ as the free monoid over Σ), take M to be any monoid; the power set P M of all subsets of M forms a semiring under set-theoretic union as addition and set-wise multiplication.

If this is what is desired, perhaps a better encoding would be

instance Monoid m => Semiring (Set m) where
  zero = Set.empty
  add = Set.union
  one = Set.singleton mempty 
  mul x y = Set.fromFoldable $ lift2 (<>) (Set.toUnfoldable x) (Set.toUnfoldable y :: Array m)

or a newtype over this.

[hdgarrood]

@paf31, @cryogenian I’d be interested to hear your thoughts on this.

[cryogenian]

I don't like the idea of having Ord constraint, but if there is no way to work without it or Eq to preserve semiring laws I'm OK with such change.

[paf31]

Yes, the additive bit really ought to use a Set, but the original intent was to avoid that so as to avoid pulling in all of ordered-containers, with the understanding that the constructed values should be used in such a way as to respect commutativity.

I don't think Set on its own is the free semiring though, right? Indeed Wikipedia also says

N[x], polynomials with natural number coefficients form a commutative semiring

is the free commutative semiring, and adding more relations can't make the free object bigger.

Maybe I need to go through this again, and write down my working in comments. It might have been incorrect originally.

[hdgarrood]

Yes - that's something I was also meaning to ask: is this semiring really the free semiring? It's not clear to me that there even is such a thing. The free commutative semiring won't be the same as the free semiring (if the latter exists) either, right? Free certainly isn't commutative, since the multiplication operation is based on the (also non-commutative) free monoid on Σ.

[paf31]

Well, consider all expressions buildable out of elements of a given type a, and also 0, 1, +, and *, subject to only the semiring laws. We can rewrite these by distributing additions outside of multiplications, removing any 0-additions, and 0-or-1-multiplications. 1-additions can be expanded out into multiple terms, so we end up with expressions which are sums of products of various values of type a. The sums are (as you observed) unordered since terms which are equivalent up to reordering terms of a product must be considered equal, but the products are ordered, giving us a representation of Set (List a).

[hdgarrood]

Okay, having done some working I have persuaded myself that there is a free functor F : Set → Semiring which is the composite of the free functors ∗ : Set → Mon (the free monoid functor) and 𝒫 : Mon → Semiring (the 'semiring-from-a-monoid' version of the covariant power set functor), where 𝒫 equips a monoid with a semiring structure as given by my example code above. So we could define

newtype Free a = Free (Set (List a))
derive newtype instance freeSemiring :: Semiring (Free a)

given the above instance for Set.

[hdgarrood]

Haha, I just saw your comment.

[paf31]

Yes, that's quite a nice way of constructing it :)