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 typ

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