Newest at the top
2025-03-25 14:21:23 +0100 | <tomsmeding> | see, if you just write out `s -> IO (a, s)` all is clear |
2025-03-25 14:20:59 +0100 | <lambdabot> | s -> IO (a, s) |
2025-03-25 14:20:59 +0100 | <tomsmeding> | @unmtl StateT s IO a |
2025-03-25 14:20:55 +0100 | <tomsmeding> | EvanR: case in point why burritos are not appropriate here: if you have StateT s IO a, then even though IO is arguably the "inner" monad here, it's actually the IO burrito that contains the State burrito |
2025-03-25 14:20:14 +0100 | <haskellbridge> | <Liamzee> actually, StateT case is sort of confused, no? |
2025-03-25 14:16:51 +0100 | <Leary> | Yes, it's just a little higher-order tweak on the same idea. |
2025-03-25 14:16:14 +0100 | <int-e> | each value can come with its own m |
2025-03-25 14:15:58 +0100 | <int-e> | oh nm |
2025-03-25 14:15:46 +0100 | <EvanR> | the innermost layer of burritos can't be reset |
2025-03-25 14:15:21 +0100 | <tomsmeding> | okay that last was "inner" |
2025-03-25 14:15:10 +0100 | <tomsmeding> | oh I see |
2025-03-25 14:14:57 +0100 | <EvanR> | scroll up lol |
2025-03-25 14:14:55 +0100 | <int-e> | Leary: but I see what you mean |
2025-03-25 14:14:53 +0100 | <tomsmeding> | EvanR: no one said "last" here |
2025-03-25 14:14:52 +0100 | <EvanR> | "innermost" |
2025-03-25 14:14:46 +0100 | <int-e> | Leary: hmm the example looks dubious (where does m come from?) |
2025-03-25 14:14:46 +0100 | <EvanR> | yes but what is last |
2025-03-25 14:14:37 +0100 | <tomsmeding> | I think that's fairly unambiguous |
2025-03-25 14:14:29 +0100 | <tomsmeding> | where StateT is the outer and IO is the inner |
2025-03-25 14:14:27 +0100 | <EvanR> | ok now that's a burrito |
2025-03-25 14:14:17 +0100 | <tomsmeding> | the "inner" and "outer" here referred to monad transformer stacks like StateT s (ExceptT e IO) a |
2025-03-25 14:14:08 +0100 | <EvanR> | due to your interpretation function producing the opposite order of instructions and LTR RTL language issues |
2025-03-25 14:13:39 +0100 | <EvanR> | "last in the stack" could mean anything |
2025-03-25 14:13:32 +0100 | <EvanR> | and in light of yesterday's discussion of stacks |
2025-03-25 14:12:54 +0100 | <tomsmeding> | everyone who seriously suggests burritos are a good monad intuition are actually burritos themselves |
2025-03-25 14:12:30 +0100 | <EvanR> | burritos |
2025-03-25 14:12:27 +0100 | <EvanR> | I have another rule of thumb |
2025-03-25 14:12:20 +0100 | <EvanR> | inner and outer "things"? |
2025-03-25 14:11:08 +0100 | kh0d | (~kh0d@212.200.247.164) |
2025-03-25 14:10:07 +0100 | <Leary> | Some effect systems like 'effectful' are also effectively reviving these "GADT API"; e.g. https://hackage.haskell.org/package/effectful-core-2.5.1.0/docs/Effectful-Dispatch-Dynamic.html |
2025-03-25 14:08:31 +0100 | kh0d | (~kh0d@212.200.247.164) (Remote host closed the connection) |
2025-03-25 14:06:01 +0100 | <int-e> | alexfmpe: Oh, nice :) |
2025-03-25 14:05:20 +0100 | <haskellbridge> | <alexfmpe> (specialized for reflex-dom, just pointing out gadt api isn't quite forgotten) |
2025-03-25 14:05:18 +0100 | <tomsmeding> | [exa]: I like |
2025-03-25 14:05:10 +0100 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-03-25 14:04:23 +0100 | <haskellbridge> | <alexfmpe> int-e: https://hackage.haskell.org/package/reflex-gadt-api |
2025-03-25 14:04:15 +0100 | <tomsmeding> | [exa]: NT M a runs into M (N a), so AT (BT (CT M)) a in the end runs in M |
2025-03-25 14:04:05 +0100 | <[exa]> | tomsmeding: roughly. |
2025-03-25 14:03:23 +0100 | <Leary> | int-e: AKA `Coyoneda P`. |
2025-03-25 14:03:21 +0100 | <tomsmeding> | [exa]: so inner things can run outer things strangely (reset, run multiple times, etc.) but outer things cannot influence inner things? |
2025-03-25 14:03:19 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-03-25 14:02:46 +0100 | <tomsmeding> | lol |
2025-03-25 14:02:44 +0100 | <[exa]> | tomsmeding: "you can't reset IO", which is why IO is always the last thing in stack |
2025-03-25 14:02:44 +0100 | <tomsmeding> | s/outputs/inputs/ |
2025-03-25 14:02:28 +0100 | <[exa]> | tomsmeding: ohhhhhhhhhhhh I found a rule of thumb! |
2025-03-25 14:02:25 +0100 | <tomsmeding> | the values in the P constructors are the outputs of the effect, the type index is the input for its continuation (the reply) |
2025-03-25 14:01:58 +0100 | <int-e> | The danger of trying to remember things :-) |
2025-03-25 14:01:56 +0100 | <tomsmeding> | I was having doubts but I wasn't sure how to fix it |
2025-03-25 14:01:45 +0100 | <tomsmeding> | that feels better, yeah |
2025-03-25 14:01:28 +0100 | <int-e> | It's `F b = forall a. (P a, a -> b)` |