I'm so looking forward to a language type system expressive enough to do a pushout lattice of <types,operators,laws> theories. So semiring, and everything else, can simply and uniquely exist. Instead of the pervasive "It's unfortunate that they did not include"... so very much. Instantly instantiatable platonic forms, instead of years of proposals, endless discussions, and standardization committee meetings. Dancing math, instead of slathering api glue.
How to put this... The potential design space is larger than is often appreciated?
Suppose I tell you, "here's a programming thing, with api/behavior that's described by some category-theory category... a category over presets". Now preset[1] means you don't get equality testing - you can't even test "set" membership. Making it hard to prove or check much. You just have to take my word for it that I've given you a thing of that category. Which makes mathematicians sad. But as a programmer... that's a better spec than I often get! ;) So there's this design space, where what you can describe, use, check, or prove, with what costs and tradeoffs, is richly varied and intertwined. And historically, it seems we've not been exploring it with great speed or coverage.
http://www.axiom-developer.org/ There's docs at the bottom of http://www.axiom-developer.org/axiom-website/documentation.h... , but http://www.axiom-developer.org/axiom-website/hyperdoc/axbook... is perhaps easier.
[0] http://stedolan.net/research/semirings.pdf