5 ms·

Linear Algebra of Types (2019)

115 points by g0xA52A2A 3y ago

yu3zhou4 3y ago
A quite interesting read. It gave me Prolog vibes.
dataflow 3y ago
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.
- eigenket 3y ago
  They mentioned min-plus and the two are essentially identical (specifically they're isomorphic with the isomorphism being x -> (-x))
  - dataflow 3y ago
    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.
    - eigenket 3y ago
      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.
- yau8edq12i 3y ago
  A "max-plus algebra" is just one example of semiring, one which isn't related to the article.
deleted 3y ago
[deleted]
Twey 3y ago
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
- taliesinb 3y ago
  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.

115 points by g0xA52A2A 3y ago

A quite interesting read. It gave me Prolog vibes.

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.

eigenket 3y ago
They mentioned min-plus and the two are essentially identical (specifically they're isomorphic with the isomorphism being x -> (-x))
- dataflow 3y ago
  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.
  - eigenket 3y ago
    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.
yau8edq12i 3y ago
A "max-plus algebra" is just one example of semiring, one which isn't related to the article.

deleted 3y ago

[deleted]

Twey 3y ago

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

taliesinb 3y ago
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.