4 ms·

This library is cool and I may end up cribbing some of its design. It's unfortunate that they did not include semirings directly, which have many interesting al

This library is cool and I may end up cribbing some of its design. It's unfortunate that they did not include semirings directly, which have many interesting algebraic uses. [0] [0] http://stedolan.net/research/semirings.pdf http://stedolan.net/research/semirings.pdf

mncharity 7y ago
> It's unfortunate that they did not include [...] 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.
- caleb-allen 7y ago
  Is this something dependent types could do? Genuinely curious, this sounds interesting.
  - mncharity 7y ago
    They could help, but dealing with them well is still an active research area... 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. [1] https://ncatlab.org/nlab/show/preset https://ncatlab.org/nlab/show/preset
- joppy 7y ago
  Have you looked at Axiom, a computer algebra system?
  - mncharity 7y ago
    If so, not in many years. http://www.axiom-developer.org/ http://www.axiom-developer.org/ There's docs at the bottom of http://www.axiom-developer.org/axiom-website/documentation.html http://www.axiom-developer.org/axiom-website/documentation.h... , but http://www.axiom-developer.org/axiom-website/hyperdoc/axbook/book-contents.xhtml http://www.axiom-developer.org/axiom-website/hyperdoc/axbook... is perhaps easier.
- epatters 7y ago
  Within the Julia ecosystem, you might be interested in Catlab (https://github.com/epatters/Catlab.jl https://github.com/epatters/Catlab.jl), as we are actively working to build something very much along these lines. We already have in place a system for describing generalized algebraic theories (GATs) in Julia and generating symbolic expressions for them. In the future, we intend to implement pushouts of GATs as an algebraic approach to theory fusion. We are currently in the planning stage of this part of the project and hope to get something working this year.
  - mncharity 7y ago
    Nifty. Perhaps add a copy of the documentation link[1] to the top of the README? Friction minimization... [1] https://epatters.github.io/Catlab.jl/latest/ https://epatters.github.io/Catlab.jl/latest/

mncharity 7y ago

> It's unfortunate that they did not include [...] 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.

caleb-allen 7y ago
Is this something dependent types could do? Genuinely curious, this sounds interesting.
- mncharity 7y ago
  They could help, but dealing with them well is still an active research area... 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. [1] https://ncatlab.org/nlab/show/preset https://ncatlab.org/nlab/show/preset
joppy 7y ago
Have you looked at Axiom, a computer algebra system?
- mncharity 7y ago
  If so, not in many years. http://www.axiom-developer.org/ http://www.axiom-developer.org/ There's docs at the bottom of http://www.axiom-developer.org/axiom-website/documentation.html http://www.axiom-developer.org/axiom-website/documentation.h... , but http://www.axiom-developer.org/axiom-website/hyperdoc/axbook/book-contents.xhtml http://www.axiom-developer.org/axiom-website/hyperdoc/axbook... is perhaps easier.
epatters 7y ago
Within the Julia ecosystem, you might be interested in Catlab (https://github.com/epatters/Catlab.jl https://github.com/epatters/Catlab.jl), as we are actively working to build something very much along these lines. We already have in place a system for describing generalized algebraic theories (GATs) in Julia and generating symbolic expressions for them. In the future, we intend to implement pushouts of GATs as an algebraic approach to theory fusion. We are currently in the planning stage of this part of the project and hope to get something working this year.
- mncharity 7y ago
  Nifty. Perhaps add a copy of the documentation link[1] to the top of the README? Friction minimization... [1] https://epatters.github.io/Catlab.jl/latest/ https://epatters.github.io/Catlab.jl/latest/