Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: applications of categorical logic

Leopold Schlicht (May 05 2021 at 12:33):

Does categorical logic have some real applications in theoretical computer science?
Lambek and Scott's equivalence between the category of cartesian closed categories and the category of theories in the $\lambda$-calculus (which can be seen as a functional programming language!) comes to mind. I think there are also similar correspondences concerned with adding a concept of polymorphism to the $\lambda$-calculus, which is also feature of programming languages. But I don't know if these are just nice and appealing correspondences to have or if they have any concrete application in computer science.

Nick Hu (May 05 2021 at 13:36):

It's the foundation of categorical (denotational) semantics of programming languages. That is, you might write a factorial function in Haskell

factorial :: Integer -> Integer
factorial 0 = 1
factorial n = n * (factorial (n - 1))

but to what extent can this be identified with the mathematical function $(-)!\colon \mathbb{N} \to \mathbb{N}$?

The answer according to this is that types are identified with objects in a CCC, terms are identified with morphisms, and with that we can make the bridge.

Thibaut Benjamin (May 05 2021 at 14:37):

The question is kind of vague, so I can't really give you a super precise answer, but here are some pointers of things that might be of interest for you:

• You could use the correspondence between CCC and $\lambda$-calculi to obtain "for free" a programming language dedicated to working with any CCC. Say you want to work with a mathematical concept, and it so happens that this concept defines a CCC, then you can go through this correspondence, to get a $\lambda$-calculus, and implement it as a programming language. That way you can manipulate some mathematical concepts directly with your computer, with a dedicated language.
• Going a bit further, you might be interested in Martin-Löf type theory (the underlying type theory of proof assistants like Coq and Agda). These have a lot of interesting categorical descriptions, as locally cartesian closed category (doesn't work perfectly, but that's a good start), or as category with attributes, categories with families, see https://ncatlab.org/nlab/show/categorical+model+of+dependent+types.
• Inside Agda for instance, you can define the type of integer as an inductive type

data N : Set where
  O : N
  S : N -> N

To justify that this definition makes sense, and give a semantics to it, the usual method is to construct it as the initial algebra of the polynomial X\mapsto 1+X. For this one example, you would not need the concept of initial algebra, but if you want to give semantics for every inductive types and not just a particular one, then I think it's pretty necessary.

• You can modify the rules of the logic to get other flavors of type theory, like linear type theory. Those also correspond to categorical devices, and it's quite useful to understand this correspondence to get the full picture.
• The very concept of monads in Haskell directly comes from category theory.

These are just a few places, categorical logic really is everywhere in computer science, if you look at it from the right point of view. Often times it's not the only way to understand things, and substantial amount of work can be done without categories, but it always bring something try and see things from a categorical perspective.

John Baez (May 05 2021 at 14:53):

@Leopold Schlicht - you asked for "real applications in theoretical computer science", which is a somewhat ambiguous question, since "theoretical" and "applied" are often treated as antonyms.

I'm not the right person to answer this, but I'll just say:

Lots of theoretical computer science takes the equivalence between cartesian closed categories and $\lambda$-theories as fundamental and builds on it in various directions. It's an enormous body of work. Among other things, it's led to the creation of programming languages such as OCaml, which seek to be mathematically principled. This little webpage is a nice explanation of that:

• OCaml’s Categorical Origins.

John Baez (May 05 2021 at 14:57):

The "Cam" in "OCaml" means "categorical abstract machine", and you might like a look at this paper:

• G. Cousineau, P.-L. Curien, M. Mauny, The categorical abstract machine, 1987.

Leopold Schlicht (May 05 2021 at 16:51):

Thank you all!
I see, it's almost impossible to tease out when some piece of computer science really is an application of category theory or categorical logic, and even theoretical computer science seems to be interested in theoretical ideas (involving categories) that don't have direct applications.
I have to admit, to me it seems there isn't much category theory used in The categorical abstract machine (both "functor" and "natural transformation" don't occuring even once!), but it's nice to hear that it at least inspired the inventors. :-)

John Baez (May 05 2021 at 17:24):

Of course, the categorical abstract machine was created in 1987 before categorical computer science really caught on. A lot has been done since then!

John Baez (May 05 2021 at 17:30):

I mentioned it mainly to set the stage for comments by people who know more about categorical computer science - e.g. most people here.

Leopold Schlicht (May 05 2021 at 17:42):

Either way, OCaml was worth mentioning! I appreciate your help. :-)

Jon Sterling (May 05 2021 at 18:13):

John Baez said:

Of course, the categorical abstract machine was created in 1987 before categorical computer science really caught on. A lot has been done since then!

I would say that CAM was in the tail-end of the hey-day of categorical computer science, before it became almost forbidden to use category theory seriously in computer science in many areas. In the past several years, we are seeing a return to "allowing people to use categories" (at least as measured by one's ability to write papers that mention categories and not have them auto-rejected by major conferences), but it is still somewhat perilous. Which is why those of us who like categories in CS have a big responsiblity to make sure that our applications are significant and not too superficial...

John Baez (May 05 2021 at 18:47):

Jonathan Sterling said:

I would say that CAM was in the tail-end of the hey-day of categorical computer science, before it became almost forbidden to use category theory seriously in computer science in many areas. In the past several years, we are seeing a return to "allowing people to use categories" (at least as measured by one's ability to write papers that mention categories and not have them auto-rejected by major conferences), but it is still somewhat perilous.

Okay, that's interesting. I only became interested in category theory around 1990, and after I did some work on n-categories I got invited to a computer science conference (much to my surprise), and interest in categories among computer scientists seems to be steadily increasing. So I must have missed the first heyday: I thought now was the heyday.

Jon Sterling (May 05 2021 at 18:49):

I hope this heydey turns out better than the last one ;-) A lot of cool stuff was done in First Generation categorical CS, but much of it is forgotten now (except in certain European groups)... It's been shocking and amazing to start getting conference reviews in the past few years that demonstrate some comfort with categories, and I really hope we can continue to nurture this trend.

Jon Sterling (May 05 2021 at 18:51):

I think in part, HoTT has been helpful because many computer scientists have some vague idea that it is "cool" even if they don't know it, and so some room has been made in the community for those who wish to study things using mathematical techniques. It didn't hurt that the mathematical techniques got immensely stronger in the years during which computer scientists swore them off...

John Baez (May 05 2021 at 18:53):

Some examples of why I thought the heyday was now: now programmers are paying to take courses on category theory from Statebox, and @Bartosz Milewski's book Category Theory for Programmers seems fairly popular, and he's writing a book with Brendan Fong called Programming with Categories, and the Topos Institute, carefully placed within range of Silicon Valley, is planning to teach category theory to computer scientists and programmers....

John Baez (May 05 2021 at 18:54):

But of course I live in a bubble! Compared to the overall scope of computer science, all these activities are microscopic.

Jon Sterling (May 05 2021 at 18:57):

Well I think all the things you are mentioning point to the fact that we are likely entering a new hey-day :) And this one seems likely to be bigger. The old one basically only involved the subfield of programming languages, but that seems not really to be the focus of ACT -- which seems much broader and very different to me.

Mike Shulman (May 05 2021 at 20:13):

Why did the first heydey end?

FH (May 05 2021 at 22:14):

One aspect could be the broader shift which occurred from logical to statistical methods.

FH (May 05 2021 at 22:17):

Programming language theory was much bigger back in the 80s and that’s where CT was applicable whereas when the ‘statistical revolution’ arrived in the 90s, there wasn’t really a place for CT

FH (May 05 2021 at 22:17):

That seems to be changing now with the much larger scope of ACT as Jonathan mentioned

Nick Smith (May 06 2021 at 06:59):

From my perspective as a software engineer, the respect for mathematics in computing might have been severely supressed by the Internet Boom and Silicon Valley startup mania that began in the 90s. A lot of research started focusing on solving concrete problems: app usability, security, data compression, search engines, advertising, data analytics... My uninformed guess is that research groups started applying for lots of grants to solve these immediate problems and the more theoretical stuff got left in the dust :sweat_smile: . And at the same time, I'd wager a greater proportion of college students started aiming for industry jobs instead of research, due to lucrative salaries fueled by a shortage of talented software engineers. There's no money in basic research :sweat_smile:

Also, my CS degree didn't even teach type theory or lambda calculus, and nobody ever told me that programming languages could be defined mathematically. In industry, programming language design is essentially considered a "creative art"... often some Messiah comes along and pulls a new programming language out of nowhere, and explains that "this language is better than its competitors" because it adds features X and Y, and abolishes feature Z. No mention of mathematics. Most people in industry still see OCaml and Haskell (the "categorical" programming languages) as arcane and not useful for writing "real apps".

Nick Smith (May 06 2021 at 07:07):

All that said, I'm not really sure of the extent that industry influenced academia in the 90s-00s :innocent: This is just a speculation.

Bob Atkey (May 06 2021 at 12:05):

My feeling on why the "heyday" ended (or became less mainstream anyway) is that categorical techniques in PL were somewhat tied to domain theoretic denotational semantics. In the late 90s people wanted to prove that their type systems were "sound" and the options were either denotational models, like in Milner's "well typed programs don't go wrong", or the Wright and Felleisen progress+preservation technique. The nice things about progress+preservation were that it was pretty elementary, it seems to scale to anything you can write down a small step operational semantics for, and the notion of "soundness" falls out of your operational semantics, so you don't have to think too hard about what "wrong" means. It is difficult to imagine Benjamin Pierce's TAPL being as successful if it were written using domain theory.

Of course, categorical techniques in PL never really went away. In the late 90s and early 2000s, Monads took off in Haskell, as did initial algebra semantics for datatypes (under the name "two level types"). Plotkin and Power started algebraic effects. Martin Hofmann used category theory to do semantics of type theory and implicit computational complexity. Hyland and Ong's and Abramsky's game semantics were explicitly formulated in the setting of categorical models of Linear Logic. Separation Logic started out from O'Hearn's investigations of Interference Controlled Algol using sheaves, and worked with Pym on categorical semantics of Bunched Implications. Some of this is documented in From Categorical Logic to Facebook Engineering.

This is from a UK and specifically Edinburgh perspective though, I'm not sure what it looked like in the US or elsewhere.

John Baez (May 06 2021 at 16:56):

In the US I think theoretical computer science focuses more on computational complexity, and a lot of researchers in that subject express disinterest in the semantic issues you just listed - disinterest verging sometimes on contempt.

John Baez (May 06 2021 at 16:56):

For example, they might say "I'd be interested if you could use these ideas to reduce our bounds on the complexity of some problem from $O(N^3)$ to $O(N^2)$."

John Baez (May 06 2021 at 16:58):

Another US attitude, connected to the dotcom boom, is "we're too busy writing software that's changing the world to worry about these arcane theoretical issues".

Leopold Schlicht (May 08 2021 at 17:55):

Interesting to read.
Another question I asked myself: What role do domains, complete partial orders, and continuous lattices play in applications to computer science? And what's their relationship to categorical logic?

Alex Gryzlov (May 08 2021 at 20:34):

Denotational semantics of PLs is usually used as a basis for various static analysis tools (i.e. model checkers) and compiler optimizations, however the classical domain theory is considered pretty much outdated at this point and people use game semantics or things like interaction trees

Olli (May 09 2021 at 10:40):

What are the reasons for why classical domain theory is considered outdated these days?

Kenji Maillard (May 09 2021 at 11:30):

I'm actually quite surprised by the claim that it is outdated (hence the reaction). Working a lot with the Coq Proof assistant I see important bits of domain theory underlying quite a lot of large development in computer science: interaction trees are a clever implementation of ideas stemming from domain theory, they are organized to work in hand with the paco library which reuses plenty of domain theory; the Iris framework (upon which large developments such as rustbelt flourish) is also based at its very foundation on domain theory; more generally, a lot of formalization of a non-terminating languages have a small domain theory library lurking around. On the theoretical side I think @Tom de Jong has some interesting results about domain theory in univalent foundations. On the more practical side, there have been a serie of paper by @Max New and his coauthors relating domain theory with gradual typing.

So maybe I'm missing to see what is the "classical" bit that @Alex Gryzlov mentions, but domain theory seems to me to be still quite present in modern CS. What is however true is that I never really had any in depth lectures on domain theory (tackling its technical part in particular) during my studies in France this last decade.

John Baez (May 09 2021 at 15:49):

Sometimes branches of math or science become "outdated" when they succeed in their goals and there aren't tons of open questions that people find exciting. An example is general topology, also called "point set topology". Few people do PhD theses in general topology nowadays, and it would be hard to get a job in it. But it's widely used throughout math and it underlies a lot of other work on topology.

I have no idea, but maybe "classical domain theory" was so successful that few people feel there's not a lot of important open questions left. @Kenji Maillard makes it sound like classical domain theory underlies interaction trees and a lot of very practical work in computer science.

John Baez (May 09 2021 at 15:51):

When I was a grad student at MIT in 1986-1989 I was told that "homotopy theory is dead", because the work of Adams and Sullivan and Quillen and Segal and May and others had settled all the really big open questions, like the relationship between topological, smooth and PL manifolds in high dimensions.

John Baez (May 09 2021 at 15:51):

Ironically this was just when homotopy theory was getting ready to invade the rest of mathematics!

Jon Sterling (May 10 2021 at 02:58):

Kenji Maillard said:

I'm actually quite surprised by the claim that it is outdated (hence the reaction). Working a lot with the Coq Proof assistant I see important bits of domain theory underlying quite a lot of large development in computer science: interaction trees are a clever implementation of ideas stemming from domain theory, they are organized to work in hand with the paco library which reuses plenty of domain theory; the Iris framework (upon which large developments such as rustbelt flourish) is also based at its very foundation on domain theory; more generally, a lot of formalization of a non-terminating languages have a small domain theory library lurking around. On the theoretical side I think Tom de Jong has some interesting results about domain theory in univalent foundations. On the more practical side, there have been a serie of paper by Max New and his coauthors relating domain theory with gradual typing.

So maybe I'm missing to see what is the "classical" bit that Alex Gryzlov mentions, but domain theory seems to me to be still quite present in modern CS. What is however true is that I never really had any in depth lectures on domain theory (tackling its technical part in particular) during my studies in France this last decade.

You bring up Iris, but this is actually the perfect example of something that is using a domain theory that is not classic domain theory --- to answer your question as to what the "classic" part means, I would suggest that people like me are using it to distinguish from guarded domain theory, which has very different properties.

To me, domain theory is immortal --- no matter what we do, we are going to keep coming back to ideas that were formulated as part of the program of domain theory. I am utterly convinced of this. But it is one thing to say this, and another to treat the present-day inheritors of domain theory as if they are the same as classic domain theory.

Jon Sterling (May 10 2021 at 03:07):

Domain theory in the sense of Dana's agenda is not, I would say, one of those fields that succeeded in its goals and has no open questions. My impression is that there are many questions and they are way too hard to solve without changing some definitions. Dana's own conclusion was that domain theory had to be re-done in order to make progress. Roughly what happened is that domain theory got increasingly arcane, so Scott, Hyland, as well as a number of other excellent scientists attempted to tame the situation by developing a topos-theoretic abstraction called synthetic domain theory. Synthetic domain theory is actually an excellent idea that contains many very very deep insights, but it truly never caught on (not even a little bit!).

Recently these things are coming back! But I don't think that the classic CPOs, etc. will ever come back in full force, and I'm ok with that.

About a decade ago, Birkedal, Møgelberg, Schwinghammer and Støvring introduced what they called synthetic guarded domain theory (SGDT). This has several very important technical differences from the old domain theory (both analytic and synthetic); in the guarded domain theory, one does not work with true fixed points but with 'guarded' fixed points where the recursive part is underneath a certain modality. In return, you have a general fixed point combinator that works on _any_ object of the topos, in contrast to synthetic domain theory where you can solve fixed points only on certain objects that have some cool properties relative to the classifier of semidecidable propositions. While computer scientists have been reluctant to actually phrase their work in the language of SGDT (they are more comfortable working with natural numbers by hand), it would not be an exaggeration to say that an immense proportion of the last 10 years of work in programming languages is using ideas from SGDT.

And this month, a new paper came out on ArXiv working in the style of classic synthetic domain theory in a really cool way, which I was delighted to see.

Alex Gryzlov (May 10 2021 at 11:49):

To add a bit to Jon's great answer, I think in practice the two main stumbling blocks for classic domain theory were the problem of full abstraction (i.e., finding semantics without "junk" in it) which was already an issue for PCF (probably the simplest possible functional PL) and the ever-increasing need to model concurrent features (AFAIK no one has figured out how to properly work with powerdomains for that).

Jon Sterling (May 10 2021 at 12:49):

Ironically, the new paper I linked to pertains to full abstraction for PCF...

But more broadly speaking I think that a big problem with the old school work on denotational semantics was methodological: at the time (and now!), people were trying to understand what kinds of equational reasoning are justified with regard to actual programs, and many people felt that one way to come up with the set of equations was to interpret into a domain model, and then check what equations hold. So long as your model is non-trivial, this method can be used to show that two programs behave the same way when you run them in any execution context (that they are "observationally equivalent"): if they are interpreted to the same object in the model, there can be no definable program context that distinguishes them, because that too would have an interpretation in the model. On the other hand, absent full abstraction, this approach cannot be used to find _all_ the observational equivalences --- indeed, in most cases the domain interpretation will contain contexts that lie outside the image of the interpretation that are able to make additional distinctions, meaning that two programs might behave the same but not be identified.

I think this was considered a big problem at the time because people wanted to think of the domain models as definitions of the behavior of a programming language, and people were very concerned that the obvious models did not model all observational equivalences. So this set off an immense amount of work to study various restrictions of the semantic domains and their morphisms, in order to investigate questions like full abstraction.

While a lot of great stuff came out of that process (like Berry's stable domains), I personally feel that some of the motivations were a bit misguided. I think of the models, including domain models, as tools that can be used to prove specific theorems, and I personally have use for many different such models; therefore it is strange, from my viewpoint, to want to have a single model that captures every observational equivalence. Moreover, because observational equivalences in a programming language will not be preserved by adding new features to the language, it is really totally bizarre from my point of view to want observational equivalence to define the equational theory of a language --- because this would be a totally degenerate kind of "theory" that cannot be extended in a non-trivial way! The category of such "theories" would be very pitiful indeed...

From this perspective, it is much easier to make peace with the lack of full abstraction and proceed with semantics in a way that is more inspired by categorical algebra than by the (to my view) very old-fashioned style of thinking about "intended semantics", etc.

Mike Shulman (May 10 2021 at 14:35):

Hear hear!!

Olli (May 10 2021 at 16:39):

Thanks everyone for your insightful replies!

CB Wells (May 10 2021 at 18:56):

I don't have the background to contribute here, but @Mike Stay and I just wrote Native-Type-Theory.pdf, a method to enhance languages using the internal logic of their presheaf toposes.

This is probably one of the simplest possible applications of categorical logic; we are surprised to find that it has not yet really been explored and implemented.

Jon Sterling (May 10 2021 at 21:03):

@Christian Williams I liked the part of your paper that involved including rewrite rules in the base theory, and generating some kind of program logic from this. I think this is indeed a new and under-explored perspective...

In general the idea of using a category of presheaves to enhance a language has seen quite a bit of application in type theory, but very little so far in PL until your draft and my recent draft with Bob Harper ("Logical Relations As Types"). It's a good idea, and I hope that more people will start applying it.

CB Wells (May 10 2021 at 21:59):

Thanks! Yeah, I've been very happy to realize that with finite limits, we can internalize most common forms of structural operational semantics.

CB Wells (May 10 2021 at 22:02):

You probably saw the application toward the end, where we construct the type of bisimilar processes. Though apparently this type is not decidable, I'm sure there are benefits to expressing it as a type in this way, e.g. reasoning up to bisimilarity.

CB Wells (May 10 2021 at 22:07):

I haven't yet understood your Logical Relations as Types; it has a lot of CS terminology and intuitions that I am not yet familiar with.

Jon Sterling (May 10 2021 at 23:28):

By the way, Bob and I just finished a pretty substantial revision of our paper, now uploaded here: http://www.jonmsterling.com/pdfs/lrat.pdf

The main changes are revamping the discussion of related work, and providing more background and explicit computations in the section on topoi. And fixing zillions of typos.