4 ms·

I am not aware that it does on its own, but I am not an expert in category theory, so I might be wrong. Many (most?) applications of category theory are just t

I am not aware that it does on its own, but I am not an expert in category theory, so I might be wrong. Many (most?) applications of category theory are just that—they tend to elegantly marshall disparate theories into a more general framework. For a very round-about answer, however—since Brouwer, we have understood that a computable function corresponds to a continuous function; continuity has a nice characterization in category theory in terms of sheaves; therefore category theory provides a basis for understanding computability. Or: the syntax of (some, but not all) computable functions is the internal language of an elementary topos. I could go on and on... The pattern here is that we could have done all this without category theory (and in fact we did!): but it provides a unifying and enriching perspective as one of the three cornerstones of computer science: logic, type theory and category theory. (See Bob Harper's amusing post on the topic for more: http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ http://existentialtype.wordpress.com/2011/03/27/the-holy-tri...)

cousin_it 12y ago
OK, I see. I'm a bit skeptical of anything that claims to be an enriching perspective but doesn't yield interesting results. This is similar to functional programming, which also feels beautiful and enriching to those who study it, but hard to show that it's superior in any measurable way. I mean, I like Curry-Howard-Lambek as much as the next guy, but typed computation is mostly about constraining computation to make some things impossible, and I'd like the unifying perspective to be more about making new things possible. Somehow, the type stuff just feels boring and lifeless to me, in a way that e.g. algorithm design doesn't.
- jonsterling 12y ago
  There are two lenses through which you can looked at typed computation, intrinsic and extrinsic. From the extrinsic perspective (which I actually prefer for semantical reasons), you are classifying the terms of a computation system which are already endowed with an operational semantics; in this sense, you are constraining computation. But I prefer to use the term "classify" rather than "constrain"; in systems built on this kind of theory, like Nuprl, for instance, you can give a type to any kind of computation you want, even the kinds that are typically ruled out in type theory (such as partiality). The intrinsic perspective is where the computations and the types are inextricably linked. This is the proof-theoretic, gentzen-style way to look at it. In this case, it is harder to say that you are constraining computation; and in many systems in the intrinsic typing tradition, it is a lot more about inferring computation than constraining it. However, do not go and think that the extrinsic perspective is "lifeless". I would say that it is the opposite, since this is the result of taking seriously the realizability-style semantics which underly the entire intuitionistic notion of Truth as understood by Brouwer and others. I consider the Curry-Howard Correspondence (the identification of program with proof) to be lifeless, in the sense that nothing is really happening there, since the programs are literally proofs of judgement in a formal system; but the Brouwer-Heyting-Kolmogorov correspondence, which is similar, is much more interesting--this is the classification of computations as witnesses/realizers for propositions. Intensional type theory is a theory of formal proof, where the terms are literally proofs of judgement: it's pretty dead in there. Type theory based on realizability, though, is more interesting, since the computations exist on their own and we categorize them as the essential computational content of propositions. Once you go down the rabbit hole, what seems lifeless now may not then. Though based on what you have said about algorithm design, it is entirely possible that we simply have very different aesthetics for theories. If you are interested in reading further, I wrote something here: http://www.jonmsterling.com/posts/2014-10-29-proof-term-assignments-and-intuitionistic-truth.html http://www.jonmsterling.com/posts/2014-10-29-proof-term-assi.... And follow the links which I give, since those are better than what I wrote!
  - cousin_it 12y ago
    Many thanks for writing that out! I can't parse most of it yet, but it looks like I have some nice pointers for further study :-)
    - jonsterling 12y ago
      Sure, no problem. Feel free to email me (jon at jonmsterling dot com) if you have any questions.

cousin_it 12y ago

OK, I see. I'm a bit skeptical of anything that claims to be an enriching perspective but doesn't yield interesting results. This is similar to functional programming, which also feels beautiful and enriching to those who study it, but hard to show that it's superior in any measurable way. I mean, I like Curry-Howard-Lambek as much as the next guy, but typed computation is mostly about constraining computation to make some things impossible, and I'd like the unifying perspective to be more about making new things possible. Somehow, the type stuff just feels boring and lifeless to me, in a way that e.g. algorithm design doesn't.

jonsterling 12y ago
There are two lenses through which you can looked at typed computation, intrinsic and extrinsic. From the extrinsic perspective (which I actually prefer for semantical reasons), you are classifying the terms of a computation system which are already endowed with an operational semantics; in this sense, you are constraining computation. But I prefer to use the term "classify" rather than "constrain"; in systems built on this kind of theory, like Nuprl, for instance, you can give a type to any kind of computation you want, even the kinds that are typically ruled out in type theory (such as partiality). The intrinsic perspective is where the computations and the types are inextricably linked. This is the proof-theoretic, gentzen-style way to look at it. In this case, it is harder to say that you are constraining computation; and in many systems in the intrinsic typing tradition, it is a lot more about inferring computation than constraining it. However, do not go and think that the extrinsic perspective is "lifeless". I would say that it is the opposite, since this is the result of taking seriously the realizability-style semantics which underly the entire intuitionistic notion of Truth as understood by Brouwer and others. I consider the Curry-Howard Correspondence (the identification of program with proof) to be lifeless, in the sense that nothing is really happening there, since the programs are literally proofs of judgement in a formal system; but the Brouwer-Heyting-Kolmogorov correspondence, which is similar, is much more interesting--this is the classification of computations as witnesses/realizers for propositions. Intensional type theory is a theory of formal proof, where the terms are literally proofs of judgement: it's pretty dead in there. Type theory based on realizability, though, is more interesting, since the computations exist on their own and we categorize them as the essential computational content of propositions. Once you go down the rabbit hole, what seems lifeless now may not then. Though based on what you have said about algorithm design, it is entirely possible that we simply have very different aesthetics for theories. If you are interested in reading further, I wrote something here: http://www.jonmsterling.com/posts/2014-10-29-proof-term-assignments-and-intuitionistic-truth.html http://www.jonmsterling.com/posts/2014-10-29-proof-term-assi.... And follow the links which I give, since those are better than what I wrote!
- cousin_it 12y ago
  Many thanks for writing that out! I can't parse most of it yet, but it looks like I have some nice pointers for further study :-)
  - jonsterling 12y ago
    Sure, no problem. Feel free to email me (jon at jonmsterling dot com) if you have any questions.