tag:blogger.com,1999:blog-8068466035875589791.post5123629018832636827..comments2024-03-26T00:37:39.585-07:00Comments on Semantic Domain: Category Theory in PL researchNeel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-8068466035875589791.post-63018608476954395822018-08-07T03:13:36.244-07:002018-08-07T03:13:36.244-07:00Hi Max, of course I don't want to say that sop...Hi Max, of course I don't want to say that sophisticated categorical techniques are bad! <br /><br />Your own work is a nice example of this -- there's an immediate, obvious analogy between contracts and dynamic typing (my favorite early example is Nick Benton's pearl <a href="" rel="nofollow"><em>Undoing Dynamic Typing</em></a>), but before your work it was an analogy, not a theorem. Sure, it would be nice if you could get the same results with less work, but if wishes were horses...!<br /><br />Instead, my point is that there's a lot of value even in "low-tech" applications of category theory. Sets with structure are as basic as it gets, but there's still a lot of mileage to be had. Eventually you may want a more sophisticated approach, but for exploratory purposes having a simple model in hand is a really good thing. (Eg, to handle the empty type in our FRP language, we eventually moved to using functor category semantics.)<br /><br />Strength is actually a nice example of this. Its usual formulation is indeed slightly odd, but in a closed category a functor F being strong is equivalent to having a family of maps σ : (A ⇒ B) → (FA ⇒ FB), where double-arrow A ⇒ B is the exponential and single-arrow X → Y are morphisms. This asserts a totally sensible relationship between the internal and external homs, which shouldn't frighten anyone. Indeed, it should guide you to looking at the enriched view (since closed categories are self-enriched), but IMO even the starting point is a nice one.Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-74125446863406872902018-08-06T17:41:07.077-07:002018-08-06T17:41:07.077-07:00Hi Neel, very nice post.
I don't really want t...Hi Neel, very nice post.<br />I don't really want to make a big deal out of this but I want to make 2 points to clarify what I meant.<br /><br />1. First, I would say that what you're talking about here is *denotational semantics*, and you are saying that category theory is useful for clarifying the basic notions (object, morphism, monoidal structure etc.) and the interpretation of the syntax in the models. This is all great stuff, but I think my preferred use of category theory is to go slightly further into what I would call *categorical logic* which is distinguished from denotational semantics in that while in denotational semantics we are interested in interpreting the syntax in a particular category and justifying program equivalences that way, in categorical logic we are interested in defining the class of all models and proving in addition a *completeness* theorem, and any time you have an interesting new judgment you end up needing more "exotic" theory to describe it properly.<br /><br />2. If you look at my next tweet, you'll see that the first example I provided was Moggi talking about how the notion of *strong monad* requires moving beyond the 2-category of categories. I expect this would surprise some people because strong monad doesn't seem to be a particularly sophisticated notion to a PL person (probably because it's one of the first category theory applications they learn). After all a strong monad is just a monad with some extra natural transformation. However I think that definition would be viewed with suspicion by a category theorist until you establish that it is equivalent to saying that a monad is strong is equivalent to it being enriched (and similarly another definition using fibred cats). To me it is the latter kind of definition that motivates me to use category theory: discover the right "doctrine" and the constructions become obvious.<br /><br />Finally the context for the tweet was my own experience with working on the semantics of gradual typing where my main conceptual leap thus far has been to use double categories/equipments, which is invariably met with extreme skepticism because it's so "exotic". It gave me the impression that there was something wrong with my approach, but the more I read the literature I realized that internal/enriched/fibred/multi-category theory comes up basically any time you move beyond simple types and cartesian closed categories, and if it doesn't it might actually improve the presentation to use it.Max S. Newhttps://www.blogger.com/profile/06397739710418207929noreply@blogger.com