Timeline for What non-monoidal functors on monoidal categories are used "in nature"?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 24, 2012 at 18:45 | comment | added | Neel Krishnaswami | I should add that Wadler's comments about "single-threadedness" are exactly about requiring a functor to be non-monoidal as part of accurately model computation. | |
| Mar 24, 2012 at 18:44 | comment | added | Neel Krishnaswami | Yes, it's the same thing. If you want a nice collection of examples, see Philip Wadler's notes "Monads for Functional Programming" <homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf>. These notes will probably seem slow-paced to you, but there were (and still are) a lot of programming language researchers who don't know much category theory. | |
| Mar 24, 2012 at 16:58 | comment | added | Erik Wennstrom | I've only ever encountered CS monads in passing before. Is the exception monad the same as the "maybe" monad? If not, could you point me at a good place to read up on it? | |
| Mar 22, 2012 at 15:43 | comment | added | Erik Wennstrom | (That "\mathsection" is supposed to be the section symbol, by the way. I wish you could preview comments.) <br> Of course, you can get these easily if you pick trivial versions. If $T$ is monoidal, then you end up with a model for elementary linear logic (by just ignoring $S$). And if in addition you've got a symmetric (lax) monoidal comonad, you get a model for non-light (heavy?) linear logic. <br> So that's why I'm looking for a specifically non-monoidal endofunctor. Most of the rest of the requirements are pretty ordinary, but I've never really worked with non-monoidal functors before. | |
| Mar 22, 2012 at 15:35 | comment | added | Erik Wennstrom | You're right; $T$ represents the restricted $!$ exponential of LLL and $S$ is the neutral $\mathsection$ exponential ("paragraph"). I kind of hinted at it above, but here it is explicitly: All I need to model intuitionist multiplicative light linear logic is a symmetric monoidal closed category equipped with a (not necessarily monoidal) endofunctor $T$, a monoidal endofunctor $S$, and natural transformations $d_A: TA\to TA\otimes TA$, $e_A: TA\to 1$, and $l_A: TA\to SA$ such that for every object $A$, $(TA,d_A,e_A)$ forms a commutative comonoid. | |
| Mar 22, 2012 at 14:08 | history | answered | Neel Krishnaswami | CC BY-SA 3.0 |