Newest at the top
| 2025-02-04 21:00:44 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-02-04 21:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-02-04 20:58:24 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-04 20:56:58 +0100 | _ht | (~huub@62.250.52.179) _ht |
| 2025-02-04 20:56:25 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-02-04 20:54:44 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-04 20:51:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-04 20:51:30 +0100 | supercode | (~supercode@user/supercode) supercode |
| 2025-02-04 20:50:31 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-04 20:46:51 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-02-04 20:45:44 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f07d9acb33bf68493bd.dip0.t-ipconnect.de) acidjnk |
| 2025-02-04 20:45:09 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-04 20:44:40 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-02-04 20:41:57 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-04 20:40:47 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-04 20:36:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-04 20:33:50 +0100 | Googulator | (~Googulato@2a01-036d-0106-418c-6daf-e703-6cee-d20f.pool6.digikabel.hu) |
| 2025-02-04 20:33:34 +0100 | Googulator | (~Googulato@2a01-036d-0106-418c-6daf-e703-6cee-d20f.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-02-04 20:32:29 +0100 | <monochrom> | Ah OK right, (s,) is Writer if we just need the functor part. OK I'm happy now, sorry for all the disagreements! |
| 2025-02-04 20:27:01 +0100 | <ncf> | (and let's not forget the comonad that comes from the (r →) ⊣ (r, ) adjunction, the store comonad) |
| 2025-02-04 20:26:26 +0100 | <ncf> | ...on reader or writer. in a sense you could say that state is more fundamental than the reader/writer monads/comonads |
| 2025-02-04 20:25:30 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-04 20:25:22 +0100 | <ncf> | yes the adjunction comes before any monad or comonad structure |
| 2025-02-04 20:25:00 +0100 | <monochrom> | But I guess Moggi said "I told you so". |
| 2025-02-04 20:24:46 +0100 | <monochrom> | But yikes, 2-categories haha (dies inside). |
| 2025-02-04 20:24:06 +0100 | <monochrom> | IIRC the correct pair of adjunction is Reader s and (s,), treating (s,) as just the obvious functor but it doesn't need to be a monad so we don't need s to be a monoid. |
| 2025-02-04 20:21:55 +0100 | <ncf> | (the subtlety is that left adjoint monads are not dual to right adjoint monads in the 1-categorical sense; you have to dualise at the 2-categorical level for this to work out, but it's really the same idea) |
| 2025-02-04 20:21:13 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f074c76d1a444d11045.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-02-04 20:21:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-04 20:21:01 +0100 | <ncf> | ok now i'm sure |
| 2025-02-04 20:19:47 +0100 | <ncf> | but i'm not 100% sure this is true |
| 2025-02-04 20:19:41 +0100 | <ncf> | now i want to claim that this is a left adjoint comonad and thus the right adjoint Reader r has a monad structure, which would be the usual Reader monad |
| 2025-02-04 20:18:13 +0100 | <ncf> | and every object in Hask has a unique trivial comonoid structure for the cartesian monoidal structure, so you get Comonad ((,) r) for any r (this instance https://hackage.haskell.org/package/comonad-5.0.9/docs/src/Control.Comonad.html#line-156) |
| 2025-02-04 20:17:29 +0100 | <ncf> | namely, any *co*monoid object R in a monoidal category has an action *comonad* R ⊗ — |
| 2025-02-04 20:17:00 +0100 | <ncf> | but Reader r is also a monad without assuming that r is a monoid, and this can be explained dually |
| 2025-02-04 20:16:25 +0100 | <ncf> | (this one https://hackage.haskell.org/package/comonad-5.0.9/docs/src/Control.Comonad.html#line-156) |
| 2025-02-04 20:15:50 +0100 | <ncf> | now since Writer m has a right adjoint (Reader m), this is even an *adjoint monad* https://ncatlab.org/nlab/show/adjoint+monad, which automatically makes Reader m a comonad |
| 2025-02-04 20:15:09 +0100 | <ncf> | so Writer m is the action monad of m for the cartesian monoidal structure on Hask |
| 2025-02-04 20:14:44 +0100 | <ncf> | a categorical way to see Writer is the following: given any monoidal category (C, ⊗) and monoid object M in C, there's an action monad M ⊗ — whose multiplication is given by the multiplication of M (and similarly for the unit) |
| 2025-02-04 20:12:22 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-02-04 20:11:42 +0100 | sabathan | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-02-04 20:10:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-02-04 20:10:07 +0100 | jespada | (~jespada@2800:a4:2267:4f00:6988:7c40:be6b:df82) jespada |
| 2025-02-04 20:08:30 +0100 | sabathan | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-02-04 20:06:20 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-04 20:05:46 +0100 | <ncf> | Writer does not come from an adjunction on Hask (at least not obviously) |
| 2025-02-04 20:05:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-04 20:02:14 +0100 | jespada | (~jespada@2800:a4:2267:4f00:6988:7c40:be6b:df82) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-04 20:02:07 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-04 20:00:49 +0100 | <monochrom> | Writer presumes that s is a monoid but State doesn't. How does that adjunction work? |