You can take this idea further by trying to find computational analogues of more complex algebra structures and operations. For example, the derivative of a type function gives the type of ‘one-hole contexts’ of that type[0], which gives rise to the work on zippers for context-preserving transformation in functional data structures, things like Rust's `Entry` API for maps.
Amr Sabry has been doing work on extending this kind of ‘type algebra’ to negatives and fractions, with applications to reversible programming à la Kanren and quantum programming languages where breaking reversibility is an important effect, and I'm always kind of captivated by it when I see it. His original paper on it[1] is from 2012; he's produced a new paper[2] more recently that is more sophisticated but perhaps a bit harder to follow without a category-theory background.
Hey there, a bit late but I've read your other comments and I'd like to get in touch. I happen to be very focused on type derivatives, in the context of applying category theory to AI, having just discovered Conor's original papers. Your comment was extremely helpful. Please email me at tali@tali.link if you see this.
I'm not sure if they were unaware of it or just failed to mention it by this name, but "max-plus algebra" is a common term in the literature of systems here.
That (subtly) misses my point. They mentioned min-plus algebra and linked it to "tropical semiring", but that only focuses on the mathematical concept, not the application. To give an analogy: it's akin to discussing "objective functions" and "derivatives" and how machine learning makes use of them (while linking to the "mathematical optimization" Wikipedia article), while failing to mention the keywords "gradient descent" and "loss function".
The minus sign might seem insignificant to a mathematician, but the discussion fails to communicate (or even acknowledge) that one of those terms is the canonical one that comes up in that field/application. This introduces a bit of an extra hurdle for those seeking more literature in the area.
Amr Sabry has been doing work on extending this kind of ‘type algebra’ to negatives and fractions, with applications to reversible programming à la Kanren and quantum programming languages where breaking reversibility is an important effect, and I'm always kind of captivated by it when I see it. His original paper on it[1] is from 2012; he's produced a new paper[2] more recently that is more sophisticated but perhaps a bit harder to follow without a category-theory background.
[0]: https://pavpanchekha.com/blog/zippers/derivative.html [1]: https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... [2]: https://dl.acm.org/doi/abs/10.1145/3434290