Hacker News new | past | comments | ask | show | jobs | submit login
Linear Algebra of Types (2019) (philipzucker.com)
115 points by g0xA52A2A 10 months ago | hide | past | favorite | 8 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.


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


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 quite interesting read. It gave me Prolog vibes.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: