Newest at the top
| 2025-01-15 16:42:39 +0100 | <pounce> | tomsmeding: original |
| 2025-01-15 16:42:33 +0100 | <pounce> | i think type systems should be linear and m >> m shouldn't be allowed >_> |
| 2025-01-15 16:42:16 +0100 | <tomsmeding> | of the original or of your fork? |
| 2025-01-15 16:42:12 +0100 | swistak | (~swistak@185.21.216.141) |
| 2025-01-15 16:42:00 +0100 | pounce | is now maintainer of this codebase |
| 2025-01-15 16:41:42 +0100 | <pounce> | buh |
| 2025-01-15 16:41:18 +0100 | <Leary> | s/In short,/E.g./ |
| 2025-01-15 16:40:08 +0100 | <Leary> | In short, `withAgda` could get cleanup code added to it later, and the change would only need to be made in the definition of `withAgda`, nowhere else. |
| 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) |