| 2024-11-07 00:00:01 +0100 | wryishly | (~wryish@216.246.119.62) (Ping timeout: 248 seconds) |
| 2024-11-07 00:00:04 +0100 | rune_ | (sid21167@id-21167.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-11-07 00:00:04 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-11-07 00:00:27 +0100 | jjhoo | (~jahakala@user/jjhoo) jjhoo |
| 2024-11-07 00:00:29 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru |
| 2024-11-07 00:00:29 +0100 | hacklschorsch | (~flo@2a01:4f9:3a:2296::2) |
| 2024-11-07 00:00:45 +0100 | s4msung | (~s4msung@user/s4msung) s4msung |
| 2024-11-07 00:00:51 +0100 | NiKaN | (sid385034@id-385034.helmsley.irccloud.com) NiKaN |
| 2024-11-07 00:00:54 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) snek |
| 2024-11-07 00:00:55 +0100 | rune_ | (sid21167@id-21167.ilkley.irccloud.com) |
| 2024-11-07 00:01:11 +0100 | Techcable | (sid534393@user/Techcable) Techcable |
| 2024-11-07 00:01:11 +0100 | tritlo | (sid58727@id-58727.hampstead.irccloud.com) |
| 2024-11-07 00:01:24 +0100 | aristid | (sid1599@id-1599.uxbridge.irccloud.com) |
| 2024-11-07 00:01:49 +0100 | thaumavorio | (~thaumavor@thaumavor.io) thaumavorio |
| 2024-11-07 00:01:54 +0100 | notzmv | (~daniel@user/notzmv) (Ping timeout: 246 seconds) |
| 2024-11-07 00:04:14 +0100 | <probie> | When did Haskell get the IO type? ~1996? |
| 2024-11-07 00:04:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 00:04:41 +0100 | Square2 | (~Square4@user/square) Square |
| 2024-11-07 00:04:51 +0100 | alexherbo2 | (~alexherbo@2a02-8440-341a-456e-a8d1-f94d-35c3-2d26.rev.sfr.net) alexherbo2 |
| 2024-11-07 00:05:44 +0100 | <Rembane> | Yeah, it's a bit older, 1993ish. https://ncatlab.org/nlab/show/IO-monad |
| 2024-11-07 00:05:47 +0100 | <Rembane> | https://dl.acm.org/doi/10.1145/158511.158524 |
| 2024-11-07 00:06:03 +0100 | <EvanR> | uniqueness types? |
| 2024-11-07 00:07:28 +0100 | Square | (~Square@user/square) (Ping timeout: 245 seconds) |
| 2024-11-07 00:07:30 +0100 | <dolio> | 1.3 is the first report with it. |
| 2024-11-07 00:07:44 +0100 | Square2 | Square |
| 2024-11-07 00:08:56 +0100 | <dolio> | The 1993 citation is dated 1992 if you click on it. :þ |
| 2024-11-07 00:09:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-11-07 00:09:27 +0100 | <Rembane> | Good stuff :D |
| 2024-11-07 00:09:38 +0100 | <Rembane> | This is why I don't trust time |
| 2024-11-07 00:10:03 +0100 | <EvanR> | the researcher was merlin, who famously experienced time backwards |
| 2024-11-07 00:10:12 +0100 | <dolio> | Ah, of course. |
| 2024-11-07 00:12:20 +0100 | <Rembane> | It must've been a real trip to talk to him |
| 2024-11-07 00:13:59 +0100 | <dolio> | Even the 1.0 report has the continuation based I/O which, if you looked at it today, you might figure out it could be factored into a monad. |
| 2024-11-07 00:15:10 +0100 | <dolio> | It's like every IO operation has (>>=) stuck onto it already, and maybe catch. |
| 2024-11-07 00:16:02 +0100 | <Inst> | Clean predates Haskell, interestingly enough. |
| 2024-11-07 00:17:21 +0100 | unlucy | (sid572875@user/unlucy) unlucy |
| 2024-11-07 00:17:46 +0100 | <Rembane> | How does Clean before Haskell handle IO? |
| 2024-11-07 00:19:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 00:22:12 +0100 | <int-e> | "Consequently, a Clean program consists of a set of rewrite rules." -- 1987 Clean was a language for expressing graph rewriting systems. |
| 2024-11-07 00:22:41 +0100 | <int-e> | cf. https://wiki.clean.cs.ru.nl/Publications#1987 |
| 2024-11-07 00:23:16 +0100 | visilii | (~visilii@85.172.77.90) (Quit: ZNC - https://znc.in) |
| 2024-11-07 00:23:34 +0100 | visilii | (~visilii@85.172.77.90) |
| 2024-11-07 00:23:48 +0100 | <probie> | https://www.mbsd.cs.ru.nl/publications/papers/1992/achp92-HighLevelIO.pdf 1992 seems to be where IO appears in Clear |
| 2024-11-07 00:24:20 +0100 | <int-e> | stdin was provided as a list of newline-terminated lines. So it's the main :: [String] -> [String] type of I/O. |
| 2024-11-07 00:24:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 00:24:54 +0100 | <Rembane> | Isn't that how very early Haskell did I/O? |
| 2024-11-07 00:25:20 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-11-07 00:25:22 +0100 | <dolio> | Sort of. But the types are more complex, I think. |
| 2024-11-07 00:25:44 +0100 | <dolio> | Not just strings. |
| 2024-11-07 00:25:57 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2024-11-07 00:26:12 +0100 | <int-e> | Hmm 1988 has a related language called LEAN? Hehe. |
| 2024-11-07 00:26:36 +0100 | <Rembane> | I need the languages EAN, AN and N too. |
| 2024-11-07 00:26:42 +0100 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2024-11-07 00:26:52 +0100 | CrunchyFlakes | (~CrunchyFl@31.19.233.78) |
| 2024-11-07 00:27:18 +0100 | Everything | (~Everythin@178-133-140-206.mobile.vf-ua.net) (Remote host closed the connection) |
| 2024-11-07 00:27:38 +0100 | <probie> | I think `UNQ` in early Clean appears slightly before monadic IO in early Haskell, since the first monadic IO paper that's been found so far references the Clean one. |
| 2024-11-07 00:27:43 +0100 | visilii | (~visilii@85.172.77.90) (Client Quit) |
| 2024-11-07 00:28:36 +0100 | visilii | (~visilii@85.172.77.90) |
| 2024-11-07 00:30:40 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2024-11-07 00:31:22 +0100 | <Inst> | I think you can consider IO in Haskell a very primitive / early effect system, but I don't think you can say the same for Clean's uniqueness types, which seem to be a more of linearity |
| 2024-11-07 00:31:51 +0100 | <Inst> | so then you can argue that Haskell had the first effect system |
| 2024-11-07 00:35:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 00:38:09 +0100 | kstatz12 | (~karl@user/kstatz12) kstatz12 |
| 2024-11-07 00:38:12 +0100 | <int-e> | 1992 CLEAN still had rules, 1994 CLEAN started to look more like Haskell. |
| 2024-11-07 00:38:14 +0100 | int-e | shrugs |
| 2024-11-07 00:38:42 +0100 | <int-e> | Anyway, the lesson here is that languages evolve, so dates of conception can be misleading. |
| 2024-11-07 00:38:54 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2024-11-07 00:39:31 +0100 | <dolio> | I'm curious what Miranda did, but I can't find my copy of the manual. |
| 2024-11-07 00:39:52 +0100 | kstatz12 | (~karl@user/kstatz12) (Client Quit) |
| 2024-11-07 00:40:33 +0100 | <haskellbridge> | <Bowuigi> Miranda has a sys_message ADT, main uses a list of that |
| 2024-11-07 00:40:56 +0100 | <sshine> | Inst, I understand that IO came to Haskell at some later point. |
| 2024-11-07 00:41:00 +0100 | <dolio> | In '85, though? |
| 2024-11-07 00:41:13 +0100 | <sshine> | I was born that year! |
| 2024-11-07 00:41:44 +0100 | <dolio> | I mean, that would make somse sense, because Haskell was essentially Miranda with a few tweaks. |
| 2024-11-07 00:42:07 +0100 | <int-e> | sshine: so how do you feel about turning ancient next year *runs* |
| 2024-11-07 00:42:12 +0100 | <sshine> | https://okmij.org/ftp/Computation/IO-monad-history.html |
| 2024-11-07 00:42:23 +0100 | <sshine> | apparently I'm not as ancient as the IO monad after all |
| 2024-11-07 00:42:24 +0100 | acidjnk | (~acidjnk@p200300d6e7283f63c008ff7276864804.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-11-07 00:44:17 +0100 | <sshine> | well, it ain't 0x20 or 0x30, but it's a pretty number. :) |
| 2024-11-07 00:47:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-11-07 00:51:33 +0100 | hueso | (~root@user/hueso) (Quit: hueso) |
| 2024-11-07 00:57:37 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-11-07 00:58:00 +0100 | Versality | (~Versality@user/Versality) (Remote host closed the connection) |
| 2024-11-07 00:58:14 +0100 | Versality | (~Versality@84.237.180.62) |
| 2024-11-07 00:58:14 +0100 | Versality | (~Versality@84.237.180.62) (Changing host) |
| 2024-11-07 00:58:14 +0100 | Versality | (~Versality@user/Versality) Versality |
| 2024-11-07 01:00:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 01:04:51 +0100 | hueso | (~root@user/hueso) hueso |
| 2024-11-07 01:05:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 01:06:18 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-11-07 01:12:02 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-11-07 01:14:10 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2024-11-07 01:14:10 +0100 | ljdarj1 | ljdarj |
| 2024-11-07 01:14:57 +0100 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-11-07 01:15:32 +0100 | sprotte24 | (~sprotte24@p200300d16f45f60044d2f8c33ad18940.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2024-11-07 01:15:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 01:20:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-11-07 01:22:12 +0100 | xff0x | (~xff0x@2405:6580:b080:900:3e16:56e8:fa8f:748e) (Ping timeout: 276 seconds) |
| 2024-11-07 01:23:04 +0100 | <monochrom> | Haha so there is opportunity for saying "Lean 88"?! :) |
| 2024-11-07 01:27:25 +0100 | <monochrom> | But I disagree with Oleg in thinking of () as world state. Instead, it is more honest without sacrificing pragmatics to adopt that in "() -> Codomain" the -> is a Kleisli arrow. |
| 2024-11-07 01:28:38 +0100 | TonyStone | (~TonyStone@user/TonyStone) (Quit: Leaving) |
| 2024-11-07 01:28:54 +0100 | TonyStone | (~TonyStone@user/TonyStone) TonyStone |
| 2024-11-07 01:31:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 01:33:10 +0100 | <haskellbridge> | <zwro> would we be better off without undefined and error and other bottoms? could we guarantee totality (modulo termination)? |
| 2024-11-07 01:34:07 +0100 | <geekosaur> | no, because there are other ways to get bottoms any time there are external inputs |
| 2024-11-07 01:35:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-11-07 01:36:06 +0100 | <geekosaur> | too many bottoms, thanks to whoever thought it was a brilliant idea to throw an exception (which is a bottom) on file not found etc. |
| 2024-11-07 01:39:46 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-11-07 01:43:16 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-11-07 01:46:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 01:51:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 01:51:44 +0100 | troojg | (~troojg@user/troojg) troojg |
| 2024-11-07 01:56:23 +0100 | alexherbo2 | (~alexherbo@2a02-8440-341a-456e-a8d1-f94d-35c3-2d26.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 02:00:18 +0100 | <haskellbridge> | <zwro> can't those exceptions be "caught" with something like `readFile :: IO (Either Exception FileContents)` ? |
| 2024-11-07 02:00:56 +0100 | <haskellbridge> | <zwro> (pseudocode) |
| 2024-11-07 02:01:54 +0100 | LainExperiments | (~LainExper@user/LainExperiments) LainExperiments |
| 2024-11-07 02:02:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 02:07:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 02:09:42 +0100 | KaitoDaumoto | (~Unity3D@user/kaitodaumoto) (Remote host closed the connection) |
| 2024-11-07 02:09:58 +0100 | <haskellbridge> | <zwro> maybe i want to explore liquid haskell? |
| 2024-11-07 02:14:08 +0100 | jero98772 | (~jero98772@2800:484:1d7c:cc00::3) |
| 2024-11-07 02:14:13 +0100 | jero98772 | (~jero98772@2800:484:1d7c:cc00::3) (Client Quit) |
| 2024-11-07 02:15:05 +0100 | notzmv | (~daniel@user/notzmv) notzmv |
| 2024-11-07 02:15:09 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-11-07 02:16:08 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2024-11-07 02:17:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 02:20:06 +0100 | <geekosaur> | no, they're actual exceptions that must be caught in `IO` with `catch` or `handle` etc. |
| 2024-11-07 02:21:01 +0100 | <dolio> | Well, you could restructure everything to return explicit failures. However, the problem is that that isn't necessarily a good idea. |
| 2024-11-07 02:22:40 +0100 | <geekosaur> | as long as exceptions are a trainwreck, I can't see it being worse |
| 2024-11-07 02:23:48 +0100 | <dolio> | That's very naive. |
| 2024-11-07 02:24:54 +0100 | <geekosaur> | https://mail.haskell.org/pipermail/libraries/2014-September/023675.html |
| 2024-11-07 02:25:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 02:25:11 +0100 | <geekosaur> | you're likely to leak with any exception |
| 2024-11-07 02:25:25 +0100 | <geekosaur> | synchronous exceptions were a fundamental mistake |
| 2024-11-07 02:26:35 +0100 | LainExperiments | (~LainExper@user/LainExperiments) (Quit: Client closed) |
| 2024-11-07 02:29:41 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-11-07 02:29:46 +0100 | LainExperiments | (~LainExper@user/LainExperiments) LainExperiments |
| 2024-11-07 02:35:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 02:38:52 +0100 | <dolio> | If you mean asynchronous exceptions, then you are unnecessarily conflating that with other aspects of the exception API. |
| 2024-11-07 02:39:52 +0100 | <dolio> | E.G. if you don't want to locally handle an explicit `Either` result, then you need to use a monad transformer or something. |
| 2024-11-07 02:40:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 02:42:02 +0100 | <dolio> | Which is possible, but then you probably have a lot of lifting and lowering to do. And also, the transformer will probably have abysmal performance characteristics, because it will repeatedly be building and inspecting Either values for the expected common case of not having an exception. |
| 2024-11-07 02:46:40 +0100 | <dolio> | For scenarios where exceptions are actually exceptional, you want an alternate implementation, like continuations for algebraic effects, so that you just install a handler once and you only jump out to it when there actually is an exception. It's technically the same 'type,' but one implementation is far superior for how it will likely be used. |
| 2024-11-07 02:49:39 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2024-11-07 02:49:58 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-11-07 02:51:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 02:54:18 +0100 | <Leary> | We could (and imo should) have unchecked panics (anywhere) and statically checked exceptions (IO/ST only) with `IO/ST :: [Exception] -> Type -> Type` uniting exception sets in `<*>`/`>>=` while `try`/`catch` delete one and `main :: IO [] (); runST :: (forall s. ST [] a) -> a`. Interruptible operations would necessarily include async exceptions in the type-level list of exceptions they might throw. The actual implementation would be essentially unchanged |
| 2024-11-07 02:54:18 +0100 | <Leary> | , the interface would just be more strongly typed. |
| 2024-11-07 02:55:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 03:02:03 +0100 | LainExperiments | (~LainExper@user/LainExperiments) (Ping timeout: 256 seconds) |
| 2024-11-07 03:02:30 +0100 | califax_ | (~califax@user/califx) califx |
| 2024-11-07 03:03:01 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-11-07 03:03:14 +0100 | TonyStone | (~TonyStone@user/TonyStone) (Ping timeout: 260 seconds) |
| 2024-11-07 03:03:36 +0100 | califax | (~califax@user/califx) (Ping timeout: 260 seconds) |
| 2024-11-07 03:03:36 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 2024-11-07 03:03:50 +0100 | califax_ | califax |
| 2024-11-07 03:05:11 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2024-11-07 03:05:27 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2024-11-07 03:06:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 03:10:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-11-07 03:12:01 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 2024-11-07 03:14:40 +0100 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-11-07 03:18:08 +0100 | TonyStone | (~TonyStone@user/TonyStone) TonyStone |
| 2024-11-07 03:21:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 03:23:46 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2024-11-07 03:26:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 03:32:31 +0100 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) ryanbooker |
| 2024-11-07 03:35:29 +0100 | troojg | (~troojg@user/troojg) (Ping timeout: 248 seconds) |
| 2024-11-07 03:37:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 03:39:26 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-11-07 03:42:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 03:48:50 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-11-07 03:54:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 04:01:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-11-07 04:10:48 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 245 seconds) |
| 2024-11-07 04:12:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 04:12:45 +0100 | blover | (~arthur@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) blover |
| 2024-11-07 04:13:50 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-11-07 04:17:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 04:20:03 +0100 | blover | (~arthur@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) (Remote host closed the connection) |
| 2024-11-07 04:20:38 +0100 | blover | (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) blover |
| 2024-11-07 04:27:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 04:32:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-11-07 04:33:29 +0100 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) (Ping timeout: 260 seconds) |
| 2024-11-07 04:40:10 +0100 | <Axman6> | I wrote something to do that years ago, which used indexed monads to list the possible expections, and handlers would remove them from the list |
| 2024-11-07 04:40:52 +0100 | blover | (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | gmg | (~user@user/gehmehgeh) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | califax | (~califax@user/califx) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (*.net *.split) |
| 2024-11-07 04:40:52 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (*.net *.split) |
| 2024-11-07 04:42:59 +0100 | <Axman6> | https://gist.github.com/axman6/19adc08a809d919a2efb |
| 2024-11-07 04:43:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 04:43:25 +0100 | <Axman6> | (From back in the day when we didn't have most of those type level functions on lists defined for us) |
| 2024-11-07 04:46:33 +0100 | califax | (~califax@user/califx) califx |
| 2024-11-07 04:46:34 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) stiell |
| 2024-11-07 04:46:36 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-11-07 04:47:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 04:50:15 +0100 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) TimWolla |
| 2024-11-07 04:50:50 +0100 | Inst_ | (~Inst@user/Inst) Inst |
| 2024-11-07 04:50:51 +0100 | td_ | (~td@i53870906.versanet.de) (Ping timeout: 276 seconds) |
| 2024-11-07 04:51:02 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2024-11-07 04:51:19 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2024-11-07 04:52:23 +0100 | td_ | (~td@i5387092D.versanet.de) |
| 2024-11-07 04:53:21 +0100 | Inst | (~Inst@user/Inst) (Ping timeout: 248 seconds) |
| 2024-11-07 04:54:23 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2024-11-07 05:01:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 05:05:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-11-07 05:11:24 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 05:12:16 +0100 | <Leary> | Axman6: The Atkey parameterised monad isn't ideal for this; you want a graded(?) monad: `class Graded (m :: k -> Type -> Type) where { type E m :: k; type Ap m (g1 :: k) (g2 :: k) :: k; pure :: a -> m (E m) a; (>>=) :: m g1 a -> (a -> m g2 b) -> m (Ap m g1 g2) b }`, with the obvious monoidal properties at both levels. |
| 2024-11-07 05:16:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 05:17:46 +0100 | <Axman6> | Not sure I follow how that works, I thik I'd need to see the instances |
| 2024-11-07 05:21:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 05:31:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 05:37:49 +0100 | Inst_ | (~Inst@user/Inst) (Ping timeout: 260 seconds) |
| 2024-11-07 05:38:00 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-11-07 05:38:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-11-07 05:42:19 +0100 | <jackdk> | Does anyone have a favourite rank2classes-style library that provides a class for HKD representables? I'm specifically looking for a class to associate a record with a GADT namings its fields (like a total DMap) and a FRepresentable sounds like it would fit the bill. I don't need a rank-2 tabulate, if that makes the search easier. The FIndexable in Ed's distributive library looks right but never made it from GitHub to Hackage. |
| 2024-11-07 05:45:38 +0100 | aforemny_ | (~aforemny@i59F4C67C.versanet.de) aforemny |
| 2024-11-07 05:46:34 +0100 | aforemny | (~aforemny@i577B13E8.versanet.de) (Ping timeout: 260 seconds) |
| 2024-11-07 05:50:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 05:55:46 +0100 | Square | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2024-11-07 05:58:31 +0100 | <Leary> | Axman6: https://gist.github.com/LSLeary/4484fb6bc4d96e59092d48592c162b9f |
| 2024-11-07 06:00:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-11-07 06:07:57 +0100 | famubu | (~famubu@user/famubu) famubu |
| 2024-11-07 06:09:26 +0100 | <famubu> | Hi. I was trying to do the example shown in the FRACTRAN wikipedia article: https://en.wikipedia.org/wiki/FRACTRAN |
| 2024-11-07 06:09:36 +0100 | <famubu> | This is what I did: https://bpa.st/2FVCW |
| 2024-11-07 06:09:51 +0100 | <famubu> | It gets the first few numbers right, but then goes wrong. |
| 2024-11-07 06:09:57 +0100 | <famubu> | Any idea how to fix it? |
| 2024-11-07 06:10:08 +0100 | <famubu> | This is my first time using Data.Ratio |
| 2024-11-07 06:10:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 06:11:37 +0100 | <famubu> | Could be the `isInt` function? |
| 2024-11-07 06:11:51 +0100 | <monochrom> | Is it actually safe to use Int and Ratio Int for this? Will you get integers too big for Int? |
| 2024-11-07 06:13:15 +0100 | <famubu> | I was doing it under the assumption that it won't go beyond Int. Maybe I should change it? |
| 2024-11-07 06:14:05 +0100 | <famubu> | Doing Int instead of Integer made it necessary to convert between Int and Integer too. |
| 2024-11-07 06:14:26 +0100 | <Leary> | Axman6: (refresh to see improvements, if you already opened that link) |
| 2024-11-07 06:15:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-11-07 06:18:41 +0100 | <famubu> | Made a version using Integer instead of Int: https://bpa.st/WT4TU |
| 2024-11-07 06:18:51 +0100 | <famubu> | Result is still incorrect though.. |
| 2024-11-07 06:19:09 +0100 | <famubu> | It's giving [2,15,825,725,1925,2275,425,25 |
| 2024-11-07 06:19:23 +0100 | <famubu> | should've been [2,15,825,725,1925,2275,425,390, |
| 2024-11-07 06:25:55 +0100 | <probie> | Why are you roundtripping via `Float`? Surely `isInt` could be more easily defined as `isInt x = denominator x == 1`. With that (and removing `fromRational`) I get correct answers with your code |
| 2024-11-07 06:26:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 06:28:29 +0100 | <EvanR> | was just musing with this bog standard python code for 36028797018963968 `div` 5... which is apparently int(36028797018963968 / 5), which round trips through float and gets the wrong answer xD |
| 2024-11-07 06:29:02 +0100 | <EvanR> | there is a // operator for integer division but it is doing the equivalent of `quot` instead of div |
| 2024-11-07 06:29:45 +0100 | <EvanR> | floats... so alluring... so deadly |
| 2024-11-07 06:30:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-11-07 06:32:17 +0100 | <famubu> | probie: Oh yeah.. Thanks! |
| 2024-11-07 06:32:23 +0100 | <famubu> | Modified it to https://bpa.st/HQC4O |
| 2024-11-07 06:32:26 +0100 | <famubu> | It works. |
| 2024-11-07 06:34:06 +0100 | <famubu> | The `foo` function feels a bit messy. Any suggestions to make it better? More readable? |
| 2024-11-07 06:39:09 +0100 | <Axman6> | Leary: nice, definitely simpler than the index monad version |
| 2024-11-07 06:40:57 +0100 | <probie> | fambu: Perhaps something like https://paste.tomsmeding.com/oA1DYLzQ |
| 2024-11-07 06:41:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 06:42:03 +0100 | <Axman6> | famubu: you can make multiple definitions inside a let block: let mfn = ...\n bs = ...\n bb = ...\nin |
| 2024-11-07 06:44:53 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-11-07 06:45:34 +0100 | <famubu> | probie: Thanks. :) |
| 2024-11-07 06:45:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 06:46:26 +0100 | <famubu> | Axman6: Oh.. didn't know that. Will keep that in mind. |
| 2024-11-07 06:49:39 +0100 | <Axman6> | famubu: some things worth noting from probie's code, functions like null, head, tail etc. are often better replaced by case statements which allow you to perform the check (null) and also name the values you want (the head of the list) in one, efficient statement |
| 2024-11-07 06:51:31 +0100 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-11-07 06:51:32 +0100 | <Axman6> | not sure how I feel about the use of round, I feel like it's likely to be doing more than just numerator would, which we know is the right value |
| 2024-11-07 06:51:38 +0100 | pavonia | (~user@user/siracusa) (Read error: Connection reset by peer) |
| 2024-11-07 06:51:53 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-11-07 06:51:57 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2024-11-07 06:52:16 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) stiell |
| 2024-11-07 06:52:43 +0100 | michalz | (~michalz@185.246.207.221) |
| 2024-11-07 06:56:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 06:57:10 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-11-07 06:57:27 +0100 | califax | (~califax@user/califx) califx |
| 2024-11-07 06:58:06 +0100 | <famubu> | Axman6: +1 |
| 2024-11-07 07:00:19 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-11-07 07:01:02 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2024-11-07 07:01:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 07:09:05 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-11-07 07:09:41 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2024-11-07 07:12:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 07:15:45 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Read error: Connection reset by peer) |
| 2024-11-07 07:16:03 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 07:17:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 07:17:56 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-11-07 07:25:14 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 252 seconds) |
| 2024-11-07 07:26:08 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-11-07 07:28:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 07:31:38 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 255 seconds) |
| 2024-11-07 07:31:48 +0100 | euleritian | (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) |
| 2024-11-07 07:33:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-11-07 07:43:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 07:43:28 +0100 | euleritian | (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-11-07 07:44:36 +0100 | euleritian | (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) |
| 2024-11-07 07:48:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-11-07 07:55:11 +0100 | acidjnk | (~acidjnk@p200300d6e7283f9509f155732eb456c8.dip0.t-ipconnect.de) acidjnk |
| 2024-11-07 07:57:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 08:02:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 08:07:39 +0100 | jco | (~jco@78-70-217-44-no600.tbcn.telia.com) jco |
| 2024-11-07 08:07:46 +0100 | alp | (~alp@2001:861:e3d6:8f80:4549:4578:5f94:9afe) |
| 2024-11-07 08:10:31 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-11-07 08:13:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 08:13:51 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2024-11-07 08:15:12 +0100 | dolio | (~dolio@130.44.140.168) (Ping timeout: 252 seconds) |
| 2024-11-07 08:17:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-11-07 08:18:16 +0100 | dolio | (~dolio@130.44.140.168) dolio |
| 2024-11-07 08:22:34 +0100 | jco | (~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving) |
| 2024-11-07 08:28:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 08:33:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 08:34:13 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 08:38:27 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-11-07 08:44:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 08:47:25 +0100 | ft | (~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-11-07 08:48:12 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-11-07 08:48:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-11-07 08:50:14 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-11-07 08:51:10 +0100 | briandaed | (~root@185.234.210.211) |
| 2024-11-07 08:51:11 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-11-07 08:51:27 +0100 | misterfish | (~misterfis@h239071.upc-h.chello.nl) misterfish |
| 2024-11-07 08:52:27 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2024-11-07 08:55:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 09:00:01 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-11-07 09:00:39 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-11-07 09:03:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 09:11:19 +0100 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 260 seconds) |
| 2024-11-07 09:13:24 +0100 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-11-07 09:15:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-11-07 09:18:09 +0100 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 260 seconds) |
| 2024-11-07 09:19:18 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 276 seconds) |
| 2024-11-07 09:19:29 +0100 | sourcetarius | (~sourcetar@user/sourcetarius) sourcetarius |
| 2024-11-07 09:20:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-11-07 09:20:42 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 09:29:19 +0100 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-11-07 09:31:39 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2024-11-07 09:33:36 +0100 | notzmv | (~daniel@user/notzmv) (Ping timeout: 276 seconds) |
| 2024-11-07 09:35:20 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2024-11-07 09:35:33 +0100 | euleritian | (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 2024-11-07 09:36:09 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-11-07 09:36:17 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 255 seconds) |
| 2024-11-07 09:41:11 +0100 | rvalue- | rvalue |
| 2024-11-07 09:43:54 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2024-11-07 09:44:42 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-11-07 09:44:55 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 252 seconds) |
| 2024-11-07 09:46:28 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 09:54:50 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-11-07 09:56:09 +0100 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-11-07 09:57:57 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-11-07 09:59:06 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 272 seconds) |
| 2024-11-07 10:00:26 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 10:01:25 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 10:03:31 +0100 | supercode | (~supercode@user/supercode) supercode |
| 2024-11-07 10:03:58 +0100 | ubert | (~Thunderbi@77.119.163.56.wireless.dyn.drei.com) ubert |
| 2024-11-07 10:05:18 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 246 seconds) |
| 2024-11-07 10:06:05 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 10:16:49 +0100 | hgolden__ | (~hgolden@146.70.173.229) hgolden |
| 2024-11-07 10:19:24 +0100 | hgolden_ | (~hgolden@169.150.203.10) (Ping timeout: 252 seconds) |
| 2024-11-07 10:21:15 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 10:21:53 +0100 | misterfish | (~misterfis@h239071.upc-h.chello.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 10:28:55 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-11-07 10:31:37 +0100 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 10:31:49 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 10:32:42 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-11-07 10:37:26 +0100 | <kuribas> | Which proof assistants have good automation? |
| 2024-11-07 10:37:56 +0100 | <kuribas> | Is it true that dependently typed proof assistants (agda, coq, idris) have worse automation than HOL based (isabella)? |
| 2024-11-07 10:38:48 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-11-07 10:40:10 +0100 | <tomsmeding> | Coq has fairly good automation, not familiar with HOL; Agda has ~absent automation |
| 2024-11-07 10:40:30 +0100 | <tomsmeding> | but contrary to Coq, Agda has readable syntax |
| 2024-11-07 10:41:11 +0100 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-11-07 10:46:24 +0100 | Versality | (~Versality@user/Versality) (Remote host closed the connection) |
| 2024-11-07 10:46:37 +0100 | Versality | (~Versality@user/Versality) Versality |
| 2024-11-07 10:49:47 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 10:51:18 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 10:55:40 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2024-11-07 10:58:38 +0100 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-11-07 11:00:32 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 11:00:52 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 11:01:48 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 11:05:50 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 255 seconds) |
| 2024-11-07 11:09:03 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2024-11-07 11:13:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 11:13:38 +0100 | xdminsy | (~xdminsy@117.147.71.147) xdminsy |
| 2024-11-07 11:16:59 +0100 | sroso | (~sroso@user/SrOso) SrOso |
| 2024-11-07 11:18:04 +0100 | xdminsy | (~xdminsy@117.147.71.147) (Client Quit) |
| 2024-11-07 11:19:39 +0100 | <kuribas> | tomsmeding: what about this? https://agda.readthedocs.io/en/latest/tools/auto.html |
| 2024-11-07 11:20:39 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 260 seconds) |
| 2024-11-07 11:23:00 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-11-07 11:24:21 +0100 | xdminsy | (~xdminsy@117.147.71.147) xdminsy |
| 2024-11-07 11:26:27 +0100 | <kuribas> | tomsmeding: did you mean there is no automation, or that "absent" is an automation feature? |
| 2024-11-07 11:28:43 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 11:29:36 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-11-07 11:32:16 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 11:32:45 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) kritzefitz |
| 2024-11-07 11:39:42 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Ping timeout: 276 seconds) |
| 2024-11-07 11:43:09 +0100 | notzmv | (~daniel@user/notzmv) notzmv |
| 2024-11-07 11:43:16 +0100 | <tomsmeding> | kuribas: I meant "no automation", but that's indeed not strictly true. 'auto' is useful for constructing simple lambda calculus terms, but it's multiple leagues below e.g. coq's 'omega' which just solves integer arithmetic stuff for you |
| 2024-11-07 11:43:53 +0100 | <tomsmeding> | and 'omega' is not considered "fancy" in coq world |
| 2024-11-07 11:44:42 +0100 | <kuribas> | ah right :) |
| 2024-11-07 11:44:49 +0100 | <tomsmeding> | there is an integer _equality_ solver in agda-stdlib, but you have to explicitly write out the equality that you want it to solve |
| 2024-11-07 11:44:58 +0100 | <tomsmeding> | and for inequalities, well, you're on your own with the basic lemmas |
| 2024-11-07 11:45:23 +0100 | <tomsmeding> | agda-presburger can do it but it's doubly-exponential so it runs out of memory once you have 8 variables in your formula |
| 2024-11-07 11:46:17 +0100 | <kuribas> | idris has a proof search algorithm, but it's also fragile. |
| 2024-11-07 11:46:28 +0100 | tomsmeding | doesn't know much about idris |
| 2024-11-07 11:49:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 11:52:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 11:53:02 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) (Quit: ZNC - http://znc.in) |
| 2024-11-07 11:53:24 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) mulk |
| 2024-11-07 11:57:31 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-11-07 11:57:35 +0100 | Digit | (~user@user/digit) (Ping timeout: 255 seconds) |
| 2024-11-07 12:00:42 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2024-11-07 12:05:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-11-07 12:10:02 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 12:11:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 12:13:11 +0100 | xff0x | (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) |
| 2024-11-07 12:20:53 +0100 | Digitteknohippie | Digit |
| 2024-11-07 12:23:47 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 12:25:58 +0100 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-11-07 12:27:21 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 12:30:53 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-11-07 12:31:22 +0100 | pavonia | (~user@user/siracusa) (Read error: Connection reset by peer) |
| 2024-11-07 12:32:05 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2024-11-07 12:37:07 +0100 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-11-07 12:38:53 +0100 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-11-07 12:42:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 12:47:12 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2024-11-07 12:52:11 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds) |
| 2024-11-07 12:52:21 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-11-07 12:52:21 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-11-07 12:54:50 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-11-07 12:56:24 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-11-07 12:59:40 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 13:00:04 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-11-07 13:01:37 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2024-11-07 13:02:11 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-11-07 13:04:43 +0100 | longlongdouble | (~longlongd@117.234.149.253) |
| 2024-11-07 13:17:17 +0100 | Inst | (~Inst@user/Inst) Inst |
| 2024-11-07 13:17:23 +0100 | <Inst> | don't ask to ask, applicative laws? |
| 2024-11-07 13:17:27 +0100 | longlongdouble | (~longlongd@117.234.149.253) (Read error: Connection reset by peer) |
| 2024-11-07 13:18:06 +0100 | <Inst> | composition -> associativity of monoids, other three laws = identity quality of pure |
| 2024-11-07 13:18:33 +0100 | longlongdouble | (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) |
| 2024-11-07 13:24:39 +0100 | CoolMa7 | (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) CoolMa7 |
| 2024-11-07 13:27:59 +0100 | longlongdouble | (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) (Ping timeout: 260 seconds) |
| 2024-11-07 13:29:23 +0100 | longlongdouble | (~longlongd@117.234.149.253) |
| 2024-11-07 13:30:26 +0100 | <Leary> | Inst: Identity === /left/ identity; Interchange === /symmetry/ of identity (hence /right/ identity). Homomorphism is redundant, following from parametricity. |
| 2024-11-07 13:31:14 +0100 | <Inst> | thanks leary |
| 2024-11-07 13:31:28 +0100 | <Inst> | didn't figure out on my own to compartmentalize them into left and right identity |
| 2024-11-07 13:32:01 +0100 | <Inst> | just a strong lax monoidal functor, what's the problem? ツ |
| 2024-11-07 13:39:12 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-11-07 13:42:21 +0100 | <kuribas> | tomsmeding: you mean coq has the best proof solving among dependently typed proof systems? |
| 2024-11-07 13:42:34 +0100 | <kuribas> | tomsmeding: But the tactics are separate from the language, right? |
| 2024-11-07 13:43:09 +0100 | famubu | (~famubu@user/famubu) (Ping timeout: 260 seconds) |
| 2024-11-07 13:48:35 +0100 | <haskellbridge> | <zwro> i'm playing around with the ghcitui and haskeline packages. i wonder if it's impossible to stream the output of, say, `let a = 1 : a in a` instead of waiting (in vain) for it to complete |
| 2024-11-07 13:50:05 +0100 | <geekosaur> | _if_ ghci is being run in a pty and buffering is disabled, streaming should work |
| 2024-11-07 13:50:54 +0100 | <geekosaur> | without the former, you get output in (I think 8kb on Linux) chunks; without the latter you get line buffering, but it's all one line so you again end up getting chunks when the line overflows the buffer |
| 2024-11-07 13:52:31 +0100 | <Inst> | leary: is this the best intro to parametricity? |
| 2024-11-07 13:52:33 +0100 | <Inst> | https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf |
| 2024-11-07 13:52:49 +0100 | hgolden__ | (~hgolden@146.70.173.229) (Ping timeout: 244 seconds) |
| 2024-11-07 13:52:51 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 13:53:10 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 13:53:44 +0100 | <geekosaur> | (note that, if it's not in a pty, you would have to rewrite ghci to disable output buffering; GNU stdbuf only works with GNU libc's stdio, not Haskell's) |
| 2024-11-07 13:54:35 +0100 | <geekosaur> | hm, that may mean you still can't get it to stream because in a pty it'll use `LineBuffering` and you can't tell it otherwise) |
| 2024-11-07 13:54:54 +0100 | <geekosaur> | so yeh, custom ghci build would be needed |
| 2024-11-07 13:55:03 +0100 | <haskellbridge> | <zwro> geekosaur: strangely, if i don't hFlush or i disable buffering, the process explodes and consumes all my cpu+memory |
| 2024-11-07 13:55:29 +0100 | <geekosaur> | that sounds like a ghcitui problem |
| 2024-11-07 13:55:39 +0100 | <haskellbridge> | <zwro> yes |
| 2024-11-07 13:55:43 +0100 | <geekosaur> | presumably you'd have to rewrite it to stream instead of reading the output all at once |
| 2024-11-07 13:56:00 +0100 | <geekosaur> | not impossible, just requires some work |
| 2024-11-07 13:56:22 +0100 | <geekosaur> | (getting it all as a single chunk is the lazy-programmer way 🙂 ) |
| 2024-11-07 13:58:12 +0100 | <geekosaur> | also I suspect you will run into the problems I described f you do change ghcitui to stream instead of trying to read it all at once |
| 2024-11-07 13:58:13 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-11-07 14:01:33 +0100 | <Leary> | Inst: That's the most notable paper on the subject, but try <http://www.vex.net/~trebla/haskell/abs-type-param.html> first. |
| 2024-11-07 14:01:43 +0100 | hgolden | (~hgolden@23.162.40.28) hgolden |
| 2024-11-07 14:01:56 +0100 | <Inst> | i hope monochrom doesn't have vex.net/~trebla on highlight? |
| 2024-11-07 14:03:04 +0100 | <geekosaur> | at most the last part, I suspect, but I have this feeling it would be egoboo 😛 |
| 2024-11-07 14:03:54 +0100 | CoolMa7 | (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2024-11-07 14:04:20 +0100 | CoolMa7 | (~CoolMa7@95.91.137.87) CoolMa7 |
| 2024-11-07 14:05:24 +0100 | housemate | (~housemate@146.70.66.228) housemate |
| 2024-11-07 14:07:36 +0100 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 14:11:09 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-11-07 14:11:44 +0100 | pavonia_ | (~user@user/siracusa) siracusa |
| 2024-11-07 14:13:04 +0100 | CoolMa7 | (~CoolMa7@95.91.137.87) (Ping timeout: 272 seconds) |
| 2024-11-07 14:13:22 +0100 | <Inst> | well it's deserved, his article's good |
| 2024-11-07 14:14:02 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-11-07 14:14:27 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2024-11-07 14:15:49 +0100 | longlongdouble | (~longlongd@117.234.149.253) (Ping timeout: 260 seconds) |
| 2024-11-07 14:15:49 +0100 | pavonia | (~user@user/siracusa) (Ping timeout: 260 seconds) |
| 2024-11-07 14:15:54 +0100 | pavonia_ | pavonia |
| 2024-11-07 14:15:57 +0100 | longlongdouble | (~longlongd@117.234.146.164) |
| 2024-11-07 14:16:11 +0100 | housemate | (~housemate@146.70.66.228) (Read error: Connection reset by peer) |
| 2024-11-07 14:24:56 +0100 | housemate | (~housemate@146.70.66.228) housemate |
| 2024-11-07 14:30:17 +0100 | CoolMa7 | (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) CoolMa7 |
| 2024-11-07 14:30:18 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 252 seconds) |
| 2024-11-07 14:31:18 +0100 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |