5 ms·

The field needs better foundations. CT is pretty good.

KRAKRISMOTT 4y ago
No. It won't make a significant (if any at all) difference to effectiveness. Rewriting Pytorch in Haskell won't magically get you AGI.
- adamnemecek 4y ago
  It's not about rewriting things in Haskell but about using CT to reason about architectures.
- solomonb 4y ago
  No one was suggesting rewriting anything in Haskell afaict..
- bawolff 4y ago
  You wouldn't expect improved foundations to increase effectiveness in the short term. And AGI is totally irrelavent here.
hgsgm 4y ago
Why? How? The OP GitHub site doesn't promote any material that introduces the concepts at all. The "survey" paper at the top is nigh-impenetrable. I'm sure the category theorists are having fun modelling machine learning, but it doesn't show how machine learning benefits from the category theory.
- adamnemecek 4y ago
  Residual connection serves as a feedback/trace a la trace in traced monoidal categories. That is one insight I have gleaned from CT.
  - resource0x 4y ago
    You beat me to this. Indeed, of all categories the monoidal ones are the most potent. Look how nicely they fit in crypto ledgers: https://www.cl.cam.ac.uk/events/syco/3/slides/Nester.pdf https://www.cl.cam.ac.uk/events/syco/3/slides/Nester.pdf \s
- Yoric 4y ago
  Category Theory (just as all mathematical models for programming or subsets thereof) are building blocks for reasoning on what we build. Past applications of such mathematical models include: - programming languages with semantics that are better adapted to specific problems (e.g. Rust's ownership); - better compilers (see e.g. Haskell's supercompiler, which puts to shame `constexpr`-style features); - better static analyzers (e.g. better type systems, abstract interpretation, model checkers). In the case of Machine Learning, it might some day help us create Machine Learning that we can understand and trust better. Or it might fail. Or it might help us invent something different entirely, in 30 years.
  - riku_iki 4y ago
    why those approaches never picked up outside of some academia projects?..
    - Yoric 4y ago
      These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD. I suspect that Apple is also using model-checking at various layers, but I have no proof :)
      - riku_iki 4y ago
        and how does it work? Do they write drivers in some verifiable subset of C?
        Yoric 4y ago
        That's how I understand it. I haven't checked the details.
  - anfelor 4y ago
    Intuition from category theory has certainly been useful for some programming language features (eg. algebraic effects, modal types or lenses), but I don't think it has helped with the things you cite. Rusts ownership model was created with little formal, academic understanding - or do you mean more foundational stuff like linear logic? And I don't think that Haskell does supercompilation today? It does optimize a whole lot but that is more due to laziness and other optimizations. But neither these optimizations nor supercompilation have much to do with category theory as far as I am aware.
- bgavran 4y ago
  There's a well-articulated essay from Christopher Olah that captures the undercurrent, and perhaps even the motivation of many of these papers https://colah.github.io/posts/2015-09-NN-Types-FP/ https://colah.github.io/posts/2015-09-NN-Types-FP/ You're completely right that the repo doesn't promote any introductory material. CT is notoriously difficult to get into, and this repository wasn't meant to be a pedagogical one, but rather a list of all the relevant papers. Though, I'll see about remedying this. I have a different repository that curates a list of (what I consider to be, as a CS major) relatively approachable CT introductory materials https://github.com/bgavran/Category_Theory_Resources https://github.com/bgavran/Category_Theory_Resources and it might be a good idea to add a pointer to it.
  - hgsgm 4y ago
    Olah's blog entry is about types and algebra. We've had types and algebra for a long time distinct Category Theory, which is a further abstraction over algebraic structures. A lot of computer programmers who never studied Abstract Algebra or Type Theory before think that all of that is Category Theory because Haskell is their first exposure to all that, and Category Theory is a big meme in Haskell, thanks to Monad.

No. It won't make a significant (if any at all) difference to effectiveness. Rewriting Pytorch in Haskell won't magically get you AGI.

adamnemecek 4y ago
It's not about rewriting things in Haskell but about using CT to reason about architectures.
solomonb 4y ago
No one was suggesting rewriting anything in Haskell afaict..
bawolff 4y ago
You wouldn't expect improved foundations to increase effectiveness in the short term. And AGI is totally irrelavent here.

hgsgm 4y ago

Why? How? The OP GitHub site doesn't promote any material that introduces the concepts at all. The "survey" paper at the top is nigh-impenetrable. I'm sure the category theorists are having fun modelling machine learning, but it doesn't show how machine learning benefits from the category theory.

adamnemecek 4y ago
Residual connection serves as a feedback/trace a la trace in traced monoidal categories. That is one insight I have gleaned from CT.
- resource0x 4y ago
  You beat me to this. Indeed, of all categories the monoidal ones are the most potent. Look how nicely they fit in crypto ledgers: https://www.cl.cam.ac.uk/events/syco/3/slides/Nester.pdf https://www.cl.cam.ac.uk/events/syco/3/slides/Nester.pdf \s
Yoric 4y ago
Category Theory (just as all mathematical models for programming or subsets thereof) are building blocks for reasoning on what we build. Past applications of such mathematical models include: - programming languages with semantics that are better adapted to specific problems (e.g. Rust's ownership); - better compilers (see e.g. Haskell's supercompiler, which puts to shame `constexpr`-style features); - better static analyzers (e.g. better type systems, abstract interpretation, model checkers). In the case of Machine Learning, it might some day help us create Machine Learning that we can understand and trust better. Or it might fail. Or it might help us invent something different entirely, in 30 years.
- riku_iki 4y ago
  why those approaches never picked up outside of some academia projects?..
  - Yoric 4y ago
    These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD. I suspect that Apple is also using model-checking at various layers, but I have no proof :)
    - riku_iki 4y ago
      and how does it work? Do they write drivers in some verifiable subset of C?
      - Yoric 4y ago
        That's how I understand it. I haven't checked the details.
- anfelor 4y ago
  Intuition from category theory has certainly been useful for some programming language features (eg. algebraic effects, modal types or lenses), but I don't think it has helped with the things you cite. Rusts ownership model was created with little formal, academic understanding - or do you mean more foundational stuff like linear logic? And I don't think that Haskell does supercompilation today? It does optimize a whole lot but that is more due to laziness and other optimizations. But neither these optimizations nor supercompilation have much to do with category theory as far as I am aware.
bgavran 4y ago
There's a well-articulated essay from Christopher Olah that captures the undercurrent, and perhaps even the motivation of many of these papers https://colah.github.io/posts/2015-09-NN-Types-FP/ https://colah.github.io/posts/2015-09-NN-Types-FP/ You're completely right that the repo doesn't promote any introductory material. CT is notoriously difficult to get into, and this repository wasn't meant to be a pedagogical one, but rather a list of all the relevant papers. Though, I'll see about remedying this. I have a different repository that curates a list of (what I consider to be, as a CS major) relatively approachable CT introductory materials https://github.com/bgavran/Category_Theory_Resources https://github.com/bgavran/Category_Theory_Resources and it might be a good idea to add a pointer to it.
- hgsgm 4y ago
  Olah's blog entry is about types and algebra. We've had types and algebra for a long time distinct Category Theory, which is a further abstraction over algebraic structures. A lot of computer programmers who never studied Abstract Algebra or Type Theory before think that all of that is Category Theory because Haskell is their first exposure to all that, and Category Theory is a big meme in Haskell, thanks to Monad.