[HN Gopher] Catgrad: A categorical deep learning compiler
       ___________________________________________________________________
        
       Catgrad: A categorical deep learning compiler
        
       Author : remexre
       Score  : 63 points
       Date   : 2025-02-03 07:44 UTC (2 days ago)
        
 (HTM) web link (catgrad.com)
 (TXT) w3m dump (catgrad.com)
        
       | abeppu wrote:
       | So, learning about the categorical structure is interesting, but
       | is there a specific advantage to seeing these concepts directly
       | informing the implementation vs as a post-hoc way of explaining
       | what autodiff is doing? E.g. Tensorflow is creating and
       | transforming graphs of computation. Despite being written before
       | most of the categorical work cited was done, isn't it doing the
       | "same" thing, but we just wouldn't find names or comments in the
       | code that closely align with the categorical work?
        
       | tripplyons wrote:
       | How does this compare to the XLA's ability to compile full
       | training steps from JAX?
        
       | bguberfain wrote:
       | It remembers me Theano [0].
       | 
       | [0] https://en.wikipedia.org/wiki/Theano_(software)
        
       | catgary wrote:
       | This is a nice project, but "You only linearize once" is more-or-
       | less the type theory version of "Reverse Derivative Categories",
       | so JAX really does this already.
        
         | statusfailed wrote:
         | (author here) the goals of catgrad are a bit different to JAX -
         | first of all, the "autodiff" algorithm is really a general
         | approach to composing _optics_ , of which autodiff is just a
         | special case. Among other things, this means you can "plug your
         | own language" into the syntax library to get a "free" autodiff
         | algorithm. Second, catgrad itself is more like an IR right now
         | - we're using it at hellas.ai to serve as a serverless runtime
         | for models.
         | 
         | More philosophically, the motto is "write programs as morphisms
         | directly". Rather than writing a term in some type theory which
         | you then (maybe) give a categorical semantics, why not just
         | work directly in a category?
         | 
         | Long term, the goal is to have a compiler which is a stack of
         | categories with functors as compiler passes. The idea being
         | that in contrast to typical compilers where you are "stuck" at
         | a given abstraction level, this would allow you to view your
         | code at various levels of abstractions. So for example, you
         | could write a program, then write an x86-specific optimization
         | for one function which you can then prove correct with respect
         | to the more abstract program specification.
        
           | nh23423fefe wrote:
           | can you expand on "write programs as morphisms directly"
           | 
           | I'm someone super interested in category theory and ITT, but
           | I can't quite parse what you are trying to convey even though
           | I think I have the prereqs to understand the answer.
        
       | cyanydeez wrote:
       | i always find it fascinating when projects like these can seem to
       | find a proper overview for the AI curious non-PhD students.
        
       ___________________________________________________________________
       (page generated 2025-02-05 23:01 UTC)