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.<p>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.<p>[0]: <a href="https://pavpanchekha.com/blog/zippers/derivative.html" rel="nofollow">https://pavpanchekha.com/blog/zippers/derivative.html</a>
[1]: <a href="https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=389fd378c9fe9b17af2756eb484bb562fa7d638a" rel="nofollow">https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d...</a>
[2]: <a href="https://dl.acm.org/doi/abs/10.1145/3434290" rel="nofollow">https://dl.acm.org/doi/abs/10.1145/3434290</a>
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.