Newest at the top
2025-02-04 00:50:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-02-04 00:48:59 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
2025-02-04 00:45:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
2025-02-04 00:44:07 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-04 00:43:36 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-04 00:41:01 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-04 00:40:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-02-04 00:40:01 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
2025-02-04 00:39:43 +0100 | euleritian | (~euleritia@dynamic-176-006-140-194.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2025-02-04 00:39:21 +0100 | euleritian | (~euleritia@dynamic-176-006-140-194.176.6.pool.telefonica.de) |
2025-02-04 00:39:13 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2025-02-04 00:37:47 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
2025-02-04 00:37:12 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2025-02-04 00:36:18 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2025-02-04 00:35:14 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
2025-02-04 00:34:57 +0100 | euleritian | (~euleritia@dynamic-176-006-140-194.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2025-02-04 00:34:50 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-02-04 00:33:56 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-04 00:33:25 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-04 00:23:50 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-02-04 00:23:45 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-04 00:23:14 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-04 00:19:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-02-04 00:19:15 +0100 | euleritian | (~euleritia@dynamic-176-006-140-194.176.6.pool.telefonica.de) |
2025-02-04 00:18:58 +0100 | euleritian | (~euleritia@dynamic-176-006-140-194.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2025-02-04 00:13:35 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-04 00:13:03 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-04 00:11:00 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
2025-02-04 00:04:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-02-04 00:03:41 +0100 | byte | (~mu@user/byte) (Quit: Leaving) |
2025-02-04 00:03:23 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-04 00:02:52 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-03 23:59:08 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-02-03 23:57:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-02-03 23:55:36 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-03 23:53:12 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-02-03 23:52:57 +0100 | <ncf> | you can also emulate local using state (just update the state before and restore it after), so i guess there's a bit more structure here |
2025-02-03 23:52:41 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-02-03 23:51:27 +0100 | <ncf> | (well, "m is a submonad of n" = "m embeds into n") |
2025-02-03 23:51:17 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-03 23:50:37 +0100 | <ncf> | oh no the definition just says monic, so embedding = submonad |
2025-02-03 23:49:32 +0100 | <ncf> | "state retracts onto reader" i guess |
2025-02-03 23:49:06 +0100 | <ncf> | i guess they mean something different; they also require a left inverse |
2025-02-03 23:47:52 +0100 | <ncf> | https://leventerkok.github.io/papers/erkok-thesis.pdf says embeddings instead of proper submonads (see ยง4.6) |
2025-02-03 23:47:07 +0100 | <tomsmeding> | oh right, preservation of pure and join is sufficient, then you automatically preserve equations on the monad operations in the domain |
2025-02-03 23:46:32 +0100 | <ncf> | https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html |
2025-02-03 23:46:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
2025-02-03 23:46:18 +0100 | <ncf> | yes (well i just mean it's not invertible) |
2025-02-03 23:45:56 +0100 | <ncf> | preserves the operations (pure and join) |
2025-02-03 23:45:54 +0100 | <tomsmeding> | and does the "proper" in "proper submonad" mean that said monad morphism is not surjective? |