7 ms·

Well, that paper escalated quickly! I've dabbled in enough category theory to have some inkling of the meaning of this, but not much. I've kind of given up on

Well, that paper escalated quickly! I've dabbled in enough category theory to have some inkling of the meaning of this, but not much. I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice in any short period of time, but I'm still tempted by the feeling that the big revelation is just a couple concepts away.

roenxi 6y ago
It seems unlikely that there will be any profound insights from category theory on how to write code, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things. Category theory is likely to contribute by giving specialists a language they can use to communicate, and it seems likely to me that at some point general tools rooted in category theory will have some sort of interesting implication for testing and debugging. Taking Haskell for example; the language isn't anything to write home about but the type checking in the tooling enabled a big improvement in writing bug free code. So there is a probably a lot on offer for the sort of people who write tooling, and less on offer for everyone else.
- pgustafs 6y ago
  “It seems unlikely that there will be any profound insights from logic on how to compute, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things.“
  - roenxi 6y ago
    It would be helpful if you fleshed that out a little, I'm curious about how you think insights from logic helps people program. I don't think I could deduce whether a developer knew or was ignorant of formal logic in a code review. Unless they give it away with a rather direct comment. Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.
    - pgustafs 6y ago
      I was referring to the fact that computers themselves are the descendants of logicians — Church, Turing, von Neumann. Your argument above could have just as easily been used to attack Turing machines before the invention of the general purpose computer.
    - calhoun137 6y ago
      +1 for the request for a rephrasing. When Faraday was asked about what the practical use of his discovery of electromagnetic induction was, he famously replied, "what is the use of a newborn baby?" Which is how I read the OP
      - pgustafs 6y ago
        Here’s another great quote along the same lines: “No one has yet discovered any warlike purpose to be served by the theory of numbers or relativity, and it seems unlikely that anyone will do so for many years.” GH Hardy 1941
- GregarianChild 6y ago
  Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads neatly generalise many similar ideas in programming. (Moggi/Plotkin should have won a Goedel award for this!) This led to a great deal of activity towards generalising this to other forms of computation, in particular parallel computing (key problem: generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding). In my opinion, this has comprehensively failed to date, in the sense that (A) while you can express some parallelism in a way that can be read as a generalisation of cut-elimination / category theory, that is not surprising since (simplifying a great deal for brevity) category theory is a foundation of mathematics; but (B) when you express non purely functional computation categorically, you get extremely complicated formal systems that obscure the fundamental simplicity of what they abstract from and generally have only what they abstract from as actual model of the abstraction. Let's take Example 47 from the Native Type Theory paper: what exactly is the formal property the typing system induces? (The paper makes vague allusions to a "foreign function interface" with rho-calculus, but there is no published understanding of even the equational theory of rho-calculus. Why should I trust this paper?) What is the logic that the paper promises ("Native Type Theory gives provides a shared framework of reasoning")? What are the proof rules, so I can type them into Lean or Coq? Show me that they are better than the simple logics I get from looking at lambda-calculus operationally. Each abstraction has costs and benefits. As of 2021, the costs of categorical methods outside of pure functional languages outweigh their benefits. I worked in categorical methods for programming and changed the field, when I realised this.
  - siraben 6y ago
    > generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reduction to cut-elimination and parallel composition, and what is meant by hiding here? I would be curious to know of relevant work in the area.
    - 6y ago
- specialist 6y ago
  > profound insights from category theory on how to write code Sure. But as u/feniv hinted upthread, I'm also optimistic about the impact on language design (noodling). I too have a hobby toy language. For the type system, I just want to use the best available science. Hopefully something practical, easy to explain, simple to use, with good enough ergonomics. While type theory is really important, it's just not my area of interest, and I'd like to defer to the experts.
- calhoun137 6y ago
  > It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "unlikely", quite the opposite. The reason I feel so strongly about this is that computer science is a subset of pure mathematics, its the part that deals with algorithms and computation. There are many questions in computer science which cannot be answered without an appeal to pure math (e.g., what is the best possible compression algorithm) All of computer science began as a result of the work of Hilbert on the foundations of logic[1]. This is what led to Turing's paper on Turing Machines. Since that time, mathematicians have done a lot of exciting work on foundations. Category theory has completely transformed the way we think about abstract mathematical objects; and type theory is very exciting in that it brings mathematics closer to a programming language which is compiled in the human brain and is done with pen and paper. It's seems to me very likely that in the future, code writing standards will change and get better, and will not remain the same. Towards that end, it makes sense that improvements will come from a better understanding of foundations, since that is where it all started. Curious for your thoughts? [1] https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:text=The%20system%20Hilbert%20asked%20for,than%20first%2Dorder%20Peano%20arithmetic.&text=Thus%20a%20satisfactory%20answer%20to,already%20believe%20PA%20is%20consistent https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:....
  - threatofrain 6y ago
    What has been your interest in category theory? How has category theory empowered your work?
    - calhoun137 6y ago
      My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
      - feanaro 6y ago
        I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.
threatofrain 6y ago
But category theory is very foundational theory. It would similarly be like learning set theory without further goals, which would be fine if you think of it as alternative Sudoku. As a foundational language it’s there to formalize mathematical objects, but that doesn’t mean people think in either set or category theory, as opposed to higher level objects in their domain.
- acjohnson55 6y ago
  Totally agree. Just musing on my desire to fully understand this paper, but with the knowledge that all the steps to get there probably won't do much for me outside their own satisfaction. Which, admittedly, might be fun.
calhoun137 6y ago
> I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice Same. It makes me kind of sad that pure math is not more helpful here! I think its possible that coding standards today are really high quality, and that any improvements are going to require a revolutionary paradigm shift in how we think about programming at an extreme level of generality. That's where pure math comes in, its a good place to shop around for new ideas, since we are kind of at a local maximum now in terms of best practices, imo. This is how I use math while coding: Instead of tinkering with numbers, just calculate the thing and get all the numbers right the first time. When trying to solve a problem, it's super helpful to have spent years proving theorems in pure math, it helped me compile programs in my head. When I am suuuuuuper stuck and need to figure out if what I am trying to do has already been done in math somewhere. When constructing an overall plan for a project, using abstract concepts in mathematics to properly anticipate the limits of what various implementations will be in order to pick the best one.
- tsss 6y ago
  Unfortunately, I think quality simply isn't needed for all the web shops and trivial CRUD applications that most programmers work on.
proc0 6y ago
CT helps advance Denotational Semantics, so syntax is written closer to math syntax, which I think is approaching computation in a much more stricter way and therefore leveraging the "magic" of math. Of course the price is paid in complexity of the theory and learning curve to understand it, which kills its practicality.
carapace 6y ago
Have you seen "Compiling to categories"? > It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

roenxi 6y ago

It seems unlikely that there will be any profound insights from category theory on how to write code, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things. Category theory is likely to contribute by giving specialists a language they can use to communicate, and it seems likely to me that at some point general tools rooted in category theory will have some sort of interesting implication for testing and debugging. Taking Haskell for example; the language isn't anything to write home about but the type checking in the tooling enabled a big improvement in writing bug free code. So there is a probably a lot on offer for the sort of people who write tooling, and less on offer for everyone else.

pgustafs 6y ago
“It seems unlikely that there will be any profound insights from logic on how to compute, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things.“
- roenxi 6y ago
  It would be helpful if you fleshed that out a little, I'm curious about how you think insights from logic helps people program. I don't think I could deduce whether a developer knew or was ignorant of formal logic in a code review. Unless they give it away with a rather direct comment. Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.
  - pgustafs 6y ago
    I was referring to the fact that computers themselves are the descendants of logicians — Church, Turing, von Neumann. Your argument above could have just as easily been used to attack Turing machines before the invention of the general purpose computer.
  - calhoun137 6y ago
    +1 for the request for a rephrasing. When Faraday was asked about what the practical use of his discovery of electromagnetic induction was, he famously replied, "what is the use of a newborn baby?" Which is how I read the OP
    - pgustafs 6y ago
      Here’s another great quote along the same lines: “No one has yet discovered any warlike purpose to be served by the theory of numbers or relativity, and it seems unlikely that anyone will do so for many years.” GH Hardy 1941
GregarianChild 6y ago
Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads neatly generalise many similar ideas in programming. (Moggi/Plotkin should have won a Goedel award for this!) This led to a great deal of activity towards generalising this to other forms of computation, in particular parallel computing (key problem: generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding). In my opinion, this has comprehensively failed to date, in the sense that (A) while you can express some parallelism in a way that can be read as a generalisation of cut-elimination / category theory, that is not surprising since (simplifying a great deal for brevity) category theory is a foundation of mathematics; but (B) when you express non purely functional computation categorically, you get extremely complicated formal systems that obscure the fundamental simplicity of what they abstract from and generally have only what they abstract from as actual model of the abstraction. Let's take Example 47 from the Native Type Theory paper: what exactly is the formal property the typing system induces? (The paper makes vague allusions to a "foreign function interface" with rho-calculus, but there is no published understanding of even the equational theory of rho-calculus. Why should I trust this paper?) What is the logic that the paper promises ("Native Type Theory gives provides a shared framework of reasoning")? What are the proof rules, so I can type them into Lean or Coq? Show me that they are better than the simple logics I get from looking at lambda-calculus operationally. Each abstraction has costs and benefits. As of 2021, the costs of categorical methods outside of pure functional languages outweigh their benefits. I worked in categorical methods for programming and changed the field, when I realised this.
- siraben 6y ago
  > generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reduction to cut-elimination and parallel composition, and what is meant by hiding here? I would be curious to know of relevant work in the area.
  - 6y ago
specialist 6y ago
> profound insights from category theory on how to write code Sure. But as u/feniv hinted upthread, I'm also optimistic about the impact on language design (noodling). I too have a hobby toy language. For the type system, I just want to use the best available science. Hopefully something practical, easy to explain, simple to use, with good enough ergonomics. While type theory is really important, it's just not my area of interest, and I'd like to defer to the experts.
calhoun137 6y ago
> It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "unlikely", quite the opposite. The reason I feel so strongly about this is that computer science is a subset of pure mathematics, its the part that deals with algorithms and computation. There are many questions in computer science which cannot be answered without an appeal to pure math (e.g., what is the best possible compression algorithm) All of computer science began as a result of the work of Hilbert on the foundations of logic[1]. This is what led to Turing's paper on Turing Machines. Since that time, mathematicians have done a lot of exciting work on foundations. Category theory has completely transformed the way we think about abstract mathematical objects; and type theory is very exciting in that it brings mathematics closer to a programming language which is compiled in the human brain and is done with pen and paper. It's seems to me very likely that in the future, code writing standards will change and get better, and will not remain the same. Towards that end, it makes sense that improvements will come from a better understanding of foundations, since that is where it all started. Curious for your thoughts? [1] https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:text=The%20system%20Hilbert%20asked%20for,than%20first%2Dorder%20Peano%20arithmetic.&text=Thus%20a%20satisfactory%20answer%20to,already%20believe%20PA%20is%20consistent https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:....
- threatofrain 6y ago
  What has been your interest in category theory? How has category theory empowered your work?
  - calhoun137 6y ago
    My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
    - feanaro 6y ago
      I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.

threatofrain 6y ago

But category theory is very foundational theory. It would similarly be like learning set theory without further goals, which would be fine if you think of it as alternative Sudoku. As a foundational language it’s there to formalize mathematical objects, but that doesn’t mean people think in either set or category theory, as opposed to higher level objects in their domain.

acjohnson55 6y ago
Totally agree. Just musing on my desire to fully understand this paper, but with the knowledge that all the steps to get there probably won't do much for me outside their own satisfaction. Which, admittedly, might be fun.

calhoun137 6y ago

> I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice Same. It makes me kind of sad that pure math is not more helpful here! I think its possible that coding standards today are really high quality, and that any improvements are going to require a revolutionary paradigm shift in how we think about programming at an extreme level of generality. That's where pure math comes in, its a good place to shop around for new ideas, since we are kind of at a local maximum now in terms of best practices, imo. This is how I use math while coding: Instead of tinkering with numbers, just calculate the thing and get all the numbers right the first time. When trying to solve a problem, it's super helpful to have spent years proving theorems in pure math, it helped me compile programs in my head. When I am suuuuuuper stuck and need to figure out if what I am trying to do has already been done in math somewhere. When constructing an overall plan for a project, using abstract concepts in mathematics to properly anticipate the limits of what various implementations will be in order to pick the best one.

tsss 6y ago
Unfortunately, I think quality simply isn't needed for all the web shops and trivial CRUD applications that most programmers work on.

proc0 6y ago

CT helps advance Denotational Semantics, so syntax is written closer to math syntax, which I think is approaching computation in a much more stricter way and therefore leveraging the "magic" of math. Of course the price is paid in complexity of the theory and learning curve to understand it, which kills its practicality.

carapace 6y ago

Have you seen "Compiling to categories"? > It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/