3 ms·

So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this i

So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this is correct then category theory is a theory of programming.

sesm 1y ago
You don't need category theory to connect dots with arrows, graph theory is enough for this.
- Twey 1y ago
  Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.
  - sesm 1y ago
    But what's the utility of this definition? Does it help solve or prove something?
    - deleted 1y ago
      [deleted]
    - Twey 1y ago
      It helps you build an intuition for categories, if you're used to graphs :) If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.
      - sesm 1y ago
        IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).
        Twey 1y ago
        Rephrasing things is useful when it allows you to draw equivalences with other things that might have results or insights that translate across, which is something a lot of people use CT for. As with most maths the payoffs aren't always immediate, though, which leads to a lot of frustration with from programmers who expect immediate results from their insights. From a programming perspective, though, a fair few important things have (by now) turned out to be useful that have come as a result of rephrasing programming in mathematical terms. Some top contenders are monads (directly from CT — think Haskell, but also LINQ, JavaScript Thenables, async/await, Rust Option/Result combinators, parser combinators), proof assistants and modern approaches to type systems, linear/substructural logic (think Rust or C++ move semantics), functional programming (which is now embraced at least to some extent by all mainstream programming languages), functional reactive programming (the core ideas behind things like React), et cetera.
- griffzhowl 1y ago
  If you allowed infinite graphs maybe. How would you define a functor or natural transformation in graph theory? Seems like you would need to construct a conceptual system that is just equivalent to category theory
- xanderlewis 1y ago
  No, but if you want to talk about composing those arrows (and a sensible notion of composition should probably be associative, and perhaps have a unit) you eventually end up reinventing category theory.
ihm 1y ago
It can very much be. Here’s one example of this phenomenon (there are many others but this is the most famous): https://wiki.haskell.org/Curry-Howard-Lambek_correspondence https://wiki.haskell.org/Curry-Howard-Lambek_correspondence

sesm 1y ago

You don't need category theory to connect dots with arrows, graph theory is enough for this.

Twey 1y ago
Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.
- sesm 1y ago
  But what's the utility of this definition? Does it help solve or prove something?
  - deleted 1y ago
    [deleted]
  - Twey 1y ago
    It helps you build an intuition for categories, if you're used to graphs :) If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.
    - sesm 1y ago
      IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).
      - Twey 1y ago
        Rephrasing things is useful when it allows you to draw equivalences with other things that might have results or insights that translate across, which is something a lot of people use CT for. As with most maths the payoffs aren't always immediate, though, which leads to a lot of frustration with from programmers who expect immediate results from their insights. From a programming perspective, though, a fair few important things have (by now) turned out to be useful that have come as a result of rephrasing programming in mathematical terms. Some top contenders are monads (directly from CT — think Haskell, but also LINQ, JavaScript Thenables, async/await, Rust Option/Result combinators, parser combinators), proof assistants and modern approaches to type systems, linear/substructural logic (think Rust or C++ move semantics), functional programming (which is now embraced at least to some extent by all mainstream programming languages), functional reactive programming (the core ideas behind things like React), et cetera.
griffzhowl 1y ago
If you allowed infinite graphs maybe. How would you define a functor or natural transformation in graph theory? Seems like you would need to construct a conceptual system that is just equivalent to category theory
xanderlewis 1y ago
No, but if you want to talk about composing those arrows (and a sensible notion of composition should probably be associative, and perhaps have a unit) you eventually end up reinventing category theory.

ihm 1y ago

It can very much be. Here’s one example of this phenomenon (there are many others but this is the most famous): https://wiki.haskell.org/Curry-Howard-Lambek_correspondence https://wiki.haskell.org/Curry-Howard-Lambek_correspondence