[HN Gopher] Linear Algebra of Types (2019)
       ___________________________________________________________________
        
       Linear Algebra of Types (2019)
        
       Author : g0xA52A2A
       Score  : 96 points
       Date   : 2024-03-30 11:14 UTC (1 days ago)
        
 (HTM) web link (www.philipzucker.com)
 (TXT) w3m dump (www.philipzucker.com)
        
       | yu3zhou4 wrote:
       | A quite interesting read. It gave me Prolog vibes.
        
       | dataflow wrote:
       | 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 wrote:
         | They mentioned min-plus and the two are essentially identical
         | (specifically they're isomorphic with the isomorphism being x
         | -> (-x))
        
           | dataflow wrote:
           | 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 wrote:
             | 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 wrote:
         | A "max-plus algebra" is just one example of semiring, one which
         | isn't related to the article.
        
       | Twey wrote:
       | 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 a 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
        
       ___________________________________________________________________
       (page generated 2024-03-31 23:01 UTC)