Open hdgarrood opened 5 years ago
@paf31, @cryogenian I’d be interested to hear your thoughts on this.
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.
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.
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 Σ.
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)
.
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
.
Haha, I just saw your comment.
Yes, that's quite a nice way of constructing it :)
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
If this is what is desired, perhaps a better encoding would be
or a newtype over this.