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.
Max New (Aug 19 2022 at 21:25):Hi, I keep coming back to the following question and I can't seem to find good references.
Given a monad T, there are some well known conditions (necessary and sufficient, I think) on the monad to let you interpret its category of algebras in various type theories:
Strong monad -> Moggi's monadic metalanguage/Call-by-push-value
Commutative monad -> Symmetric monoidal categories/linear logic w/ just exchange
And furthermore if T is the monad from an algebraic theory there are conditions on the theory that are equivalent to the conditions on the monad:
Strong monad -> any theory
Commutative monad -> commutative theory (all operations commute)
Can anyone help me find a reference for the two intermediate notions:
?? theory -> ?? monad -> semicartesian monoidal category/affine logic (linear logic + weakening)
?? theory -> ?? monad -> relevance monoidal category/relevance logic (linear logic + contraction)
I could have sworn I've seen them before, but I am coming up empty. I'd like to put them on nlab so I don't lose them again.
Sam Staton (Aug 20 2022 at 05:44):Hi Max, I think they're usually called relevant and affine monads, already in Bart Jacobs' Semantics of Weakening and Contraction, where there's more discussion of the history. Bart and others have written more about it since too, of course.
An affine theory is one where f(x,x,x...) = x for all f. These are sometimes called "modes", and include the theory of convex sets.
In programming languages we also talk about "discardable" and "copyable" effects, which are related similarly, as you probably know.
Does that help?
Max New (Aug 20 2022 at 18:28):Very helpful, thanks. I started a table on this page: https://ncatlab.org/nlab/show/side+effect I should probably add a column for the discardable/copyable/central/thunkable stuff.
Sam Staton (Aug 21 2022 at 15:38):Nice. Reminds me a bit of the table in @Ohad Kammar 's paper thesis work, e.g. POPL 2012 or his thesis page 255.
Max New (Sep 20 2022 at 19:46):Oh this table is great! Exactly what I was looking for thanks