Newest at the top
| 2025-01-15 16:38:49 +0100 | <Leary> | It's more powerful. That's a bad thing in the sense that function signatures should be restrictive for ease of reasoning, but if you expect to actually need that power at some point, you can then use it without needing to refactor other code. |
| 2025-01-15 16:38:38 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-01-15 16:36:46 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 265 seconds) |
| 2025-01-15 16:35:21 +0100 | <pounce> | why manually taking kleisli arrows instead of composing them normally |
| 2025-01-15 16:34:53 +0100 | <pounce> | instead of `foo >>= \a -> b` it's `foo (\a -> b)` where `foo f = bar >>= f` |
| 2025-01-15 16:33:56 +0100 | <pounce> | this is all over this codebase though |
| 2025-01-15 16:29:37 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-15 16:27:50 +0100 | <tomsmeding> | perhaps there was some cleanup code in an earlier version? |
| 2025-01-15 16:26:59 +0100 | <pounce> | so i think it's weird for it to have that definition |
| 2025-01-15 16:26:55 +0100 | <pounce> | in any case this function doesn't |
| 2025-01-15 16:26:33 +0100 | <pounce> | ah right |
| 2025-01-15 16:26:21 +0100 | <lambdabot> | Monad m => m b -> m b |
| 2025-01-15 16:26:20 +0100 | <tomsmeding> | :t \m -> m >> m >> m |
| 2025-01-15 16:26:16 +0100 | <tomsmeding> | pounce: the M a |
| 2025-01-15 16:26:15 +0100 | <tomsmeding> | Axman6: https://github.com/treblacy/hasdoc |
| 2025-01-15 16:26:15 +0100 | <pounce> | which action? |
| 2025-01-15 16:25:25 +0100 | <tomsmeding> | that |
| 2025-01-15 16:25:17 +0100 | <Leary> | The function could use its argument any number of times, interleaved with any number of other actions. |
| 2025-01-15 16:25:04 +0100 | <tomsmeding> | pounce: the former could run the monadic action multiple times |
| 2025-01-15 16:24:06 +0100 | <Leary> | (no) |
| 2025-01-15 16:23:40 +0100 | alexherbo2 | (~alexherbo@2a02-8440-350c-e8f4-5419-f1db-9c83-bf9d.rev.sfr.net) (Ping timeout: 240 seconds) |
| 2025-01-15 16:21:31 +0100 | <pounce> | by monad laws / parametricity `forall a . M a -> M a` and `M ()` are equivalent... no? |
| 2025-01-15 16:19:38 +0100 | <pounce> | it always returns `m` anyway, so why call `withAgda m` when you could just `withAgda' >> m` |
| 2025-01-15 16:19:07 +0100 | <pounce> | this: https://github.com/agda/cornelis/blob/master/src/Cornelis/Agda.hs#L118 |
| 2025-01-15 16:17:20 +0100 | <enikar> | pounce: which code? |
| 2025-01-15 16:15:43 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-15 16:11:25 +0100 | <pounce> | :? |
| 2025-01-15 16:11:10 +0100 | paotsaq | (~paotsaq@127.209.37.188.rev.vodafone.pt) paotsaq |
| 2025-01-15 16:08:41 +0100 | <lambdabot> | • Variable not in scope: code |
| 2025-01-15 16:08:41 +0100 | <lambdabot> | error: |
| 2025-01-15 16:08:41 +0100 | <lambdabot> | error: Variable not in scope: this :: t0 -> t |
| 2025-01-15 16:08:41 +0100 | <int-e> | :t this code |
| 2025-01-15 16:07:00 +0100 | <pounce> | why the heck is this code `M a -> M a` instead of `M ()` :/ |
| 2025-01-15 15:52:38 +0100 | euleritian | (~euleritia@dynamic-176-006-134-015.176.6.pool.telefonica.de) |
| 2025-01-15 15:51:52 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-01-15 15:45:05 +0100 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2025-01-15 15:39:00 +0100 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2025-01-15 15:24:23 +0100 | housemate | (~housemate@146.70.66.228) (Quit: Nothing to see here. I wasn't there. I take IRC seriously. I do not work for any body DIRECTLY although I do represent BOT NET.) |
| 2025-01-15 15:22:48 +0100 | paotsaq | (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 252 seconds) |
| 2025-01-15 15:20:57 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: ColinRobinson) |
| 2025-01-15 15:14:08 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f02edd754543fe6660f.dip0.t-ipconnect.de) acidjnk |
| 2025-01-15 15:05:46 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f02edd754543fe6660f.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-01-15 15:03:03 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-01-15 15:02:27 +0100 | JuanDaugherty | ColinRobinson |
| 2025-01-15 15:00:54 +0100 | cayley5 | (~cayley5@user/phileasfogg) (Ping timeout: 260 seconds) |
| 2025-01-15 14:50:41 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-15 14:43:49 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-01-15 14:43:47 +0100 | housemate | (~housemate@146.70.66.228) housemate |
| 2025-01-15 14:41:50 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-15 14:30:25 +0100 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |