Newest at the top
| 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) |
| 2025-01-15 14:23:42 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-01-15 14:21:21 +0100 | paotsaq | (~paotsaq@127.209.37.188.rev.vodafone.pt) |