Linear Algebra of Types (2019) | Hacker News Reader

Linear Algebra of Types (2019)

philipzucker.com

115 pointsg0xA52A2A8 comments

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

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.

They mentioned min-plus and the two are essentially identical (specifically they're isomorphic with the isomorphism being x -> (-x))

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.

I guess? I mean they linked to the wiki page which mentions both versions and explicitly says they're isomorphic.

They could mention it explicitly in the blog as well but its clearly not the focus of this post.

A "max-plus algebra" is just one example of semiring, one which isn't related to the article.

A quite interesting read. It gave me Prolog vibes.

Reply on news.ycombinator.com