2025-04-04 00:01:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 00:04:14 +0200 | remexre | (~remexre@user/remexre) (Ping timeout: 252 seconds) |
2025-04-04 00:05:20 +0200 | Eoco | (~ian@128.101.131.218) (Ping timeout: 252 seconds) |
2025-04-04 00:05:25 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 00:06:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 00:10:20 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-04 00:11:44 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 244 seconds) |
2025-04-04 00:13:23 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 252 seconds) |
2025-04-04 00:15:15 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
2025-04-04 00:16:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 00:18:32 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
2025-04-04 00:19:04 +0200 | chewybread | (~chewybrea@c-174-181-7-135.hsd1.pa.comcast.net) |
2025-04-04 00:19:04 +0200 | chewybread | (~chewybrea@c-174-181-7-135.hsd1.pa.comcast.net) (Changing host) |
2025-04-04 00:19:04 +0200 | chewybread | (~chewybrea@user/chewybread) chewybread |
2025-04-04 00:20:42 +0200 | hattckory | (~hattckory@205.189.187.4) |
2025-04-04 00:21:09 +0200 | ph88 | (~ph88@2a02:8109:9e26:c800:2342:51dd:f532:6d25) ph88 |
2025-04-04 00:21:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 00:24:44 +0200 | remexre | (~remexre@user/remexre) remexre |
2025-04-04 00:25:27 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 00:28:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 00:31:13 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 268 seconds) |
2025-04-04 00:31:59 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
2025-04-04 00:32:14 +0200 | Guest57 | (~Guest57@2607:fb90:bd10:58e0:5d0f:841e:976b:4ffd) |
2025-04-04 00:33:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 00:35:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-04 00:44:11 +0200 | chewybread | (~chewybrea@user/chewybread) (Ping timeout: 252 seconds) |
2025-04-04 00:44:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 00:45:36 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 00:49:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 00:49:57 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 248 seconds) |
2025-04-04 00:52:22 +0200 | chewybread | (~chewybrea@c-174-181-7-135.hsd1.pa.comcast.net) |
2025-04-04 00:52:23 +0200 | chewybread | (~chewybrea@c-174-181-7-135.hsd1.pa.comcast.net) (Changing host) |
2025-04-04 00:52:23 +0200 | chewybread | (~chewybrea@user/chewybread) chewybread |
2025-04-04 00:52:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
2025-04-04 00:57:40 +0200 | tavare | (~tavare@150.129.88.189) tavare |
2025-04-04 00:57:40 +0200 | tavare | (~tavare@150.129.88.189) (Changing host) |
2025-04-04 00:57:40 +0200 | tavare | (~tavare@user/tavare) tavare |
2025-04-04 00:57:51 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
2025-04-04 00:59:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 01:00:30 +0200 | Guest57 | (~Guest57@2607:fb90:bd10:58e0:5d0f:841e:976b:4ffd) (Ping timeout: 240 seconds) |
2025-04-04 01:00:31 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 01:04:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 01:05:38 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 01:05:45 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 268 seconds) |
2025-04-04 01:12:38 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
2025-04-04 01:13:00 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 244 seconds) |
2025-04-04 01:15:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 01:17:04 +0200 | <haskellbridge> | <Liamzee> https://medium.com/@trueskawka/haskell-divmod-and-quotrem-450b859b656a |
2025-04-04 01:17:24 +0200 | <haskellbridge> | <Liamzee> is haskell auto-optimizing divmod into quotrem? I tried on apple silicon and couldn't find appreciable differences |
2025-04-04 01:19:04 +0200 | tabemann_ | tabemann |
2025-04-04 01:22:24 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f05c47cfd219ef4d968.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
2025-04-04 01:22:33 +0200 | <Axman6> | There has been work to implement efficient division by known constants but I'm not sure if it ever got merged. I was going to work on it but someone else was on it already (and using a less efficient algorithm afaict) |
2025-04-04 01:22:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-04 01:23:26 +0200 | forell | (~forell@user/forell) (Ping timeout: 252 seconds) |
2025-04-04 01:26:46 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 01:29:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 01:29:48 +0200 | sprotte24 | (~sprotte24@p200300d16f073800ec483cc7828fc8d9.dip0.t-ipconnect.de) (Quit: Leaving) |
2025-04-04 01:30:55 +0200 | <geekosaur> | https://gitlab.haskell.org/ghc/ghc/-/issues/22152 is marked fixed. I'm not immediately finding the buggy constant division optimization that got into 9.12.1 |
2025-04-04 01:34:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 01:38:05 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
2025-04-04 01:38:18 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-04-04 01:44:42 +0200 | <haskellbridge> | <Liamzee> I don't think GHC can figure out in my context that it's always positive thus quotrem introduces no inaccuracy |
2025-04-04 01:44:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 01:45:13 +0200 | <haskellbridge> | <Liamzee> also my benchmark is probably wrong, just forcing the value i'm looking for, without using it, is still causing substantial kernel time |
2025-04-04 01:46:08 +0200 | <Axman6> | quotRem is often faster than divMod, and should be preferred if you're working with only positivie inputs |
2025-04-04 01:46:14 +0200 | <Axman6> | positive* |
2025-04-04 01:47:00 +0200 | <c_wraith> | isn't quotRem what hardware actually gives you, with divMod requiring some fixups? |
2025-04-04 01:47:04 +0200 | <haskellbridge> | <Liamzee> it's not kernel time, i'm just misreading |
2025-04-04 01:47:11 +0200 | <haskellbridge> | <Liamzee> zsh time |
2025-04-04 01:47:12 +0200 | <haskellbridge> | <Liamzee> facepalm |
2025-04-04 01:48:06 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Ping timeout: 240 seconds) |
2025-04-04 01:49:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 01:50:00 +0200 | <Axman6> | I did some of the work to make this _a lot_ faster on aarch64, adding access to the UMULH and UMULL instructions |
2025-04-04 01:50:20 +0200 | <Axman6> | (Which I think got backported to 9.10 not too long ago) |
2025-04-04 01:53:34 +0200 | ph88 | (~ph88@2a02:8109:9e26:c800:2342:51dd:f532:6d25) (Quit: Leaving) |
2025-04-04 01:56:06 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 02:01:17 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-04-04 02:01:24 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2025-04-04 02:08:21 +0200 | otto_s | (~user@p5b044be5.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2025-04-04 02:09:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 02:09:50 +0200 | otto_s | (~user@p5de2ff42.dip0.t-ipconnect.de) |
2025-04-04 02:10:16 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 02:11:27 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-04-04 02:12:07 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 244 seconds) |
2025-04-04 02:13:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 02:15:13 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 244 seconds) |
2025-04-04 02:21:37 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-04-04 02:24:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 02:27:50 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 02:28:01 +0200 | hattckory | (~hattckory@205.189.187.4) (Ping timeout: 248 seconds) |
2025-04-04 02:29:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 02:30:12 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 244 seconds) |
2025-04-04 02:32:43 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-04-04 02:33:07 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 02:38:24 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 246 seconds) |
2025-04-04 02:40:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 02:45:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
2025-04-04 02:48:24 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) |
2025-04-04 02:52:57 +0200 | Square2 | (~Square@user/square) Square |
2025-04-04 02:54:08 +0200 | inca | (~inca@syn-098-011-170-006.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-04-04 02:56:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 02:56:24 +0200 | Square | (~Square4@user/square) (Ping timeout: 260 seconds) |
2025-04-04 03:01:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 03:11:32 +0200 | xff0x | (~xff0x@2405:6580:b080:900:4999:ed25:622a:4144) (Ping timeout: 272 seconds) |
2025-04-04 03:12:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 03:15:28 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) werneta |
2025-04-04 03:17:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 03:21:06 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 246 seconds) |
2025-04-04 03:27:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 03:31:43 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2025-04-04 03:32:03 +0200 | toby-bro | (~toby-bro@user/toby-bro) (Ping timeout: 245 seconds) |
2025-04-04 03:32:09 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
2025-04-04 03:32:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 03:43:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 03:48:35 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
2025-04-04 03:49:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 03:50:00 +0200 | haritz | (~hrtz@user/haritz) (Ping timeout: 276 seconds) |
2025-04-04 03:51:56 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
2025-04-04 03:53:52 +0200 | puke | (~puke@user/puke) (Quit: puke) |
2025-04-04 03:53:56 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-04-04 03:54:06 +0200 | Square2 | (~Square@user/square) (Ping timeout: 268 seconds) |
2025-04-04 03:59:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 04:05:01 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 04:06:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-04 04:06:45 +0200 | thuna` | (~thuna`@user/thuna/x-1480069) (Ping timeout: 248 seconds) |
2025-04-04 04:09:11 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
2025-04-04 04:10:08 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 268 seconds) |
2025-04-04 04:13:06 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 04:15:11 +0200 | chewybread | (~chewybrea@user/chewybread) (Remote host closed the connection) |
2025-04-04 04:16:44 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) |
2025-04-04 04:16:47 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) (Changing host) |
2025-04-04 04:16:47 +0200 | haritz | (~hrtz@user/haritz) haritz |
2025-04-04 04:17:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 04:18:52 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-04 04:20:31 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 265 seconds) |
2025-04-04 04:22:35 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) gabriel_sevecek |
2025-04-04 04:23:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 04:28:49 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 244 seconds) |
2025-04-04 04:33:10 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) |
2025-04-04 04:33:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 04:34:52 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Changing host) |
2025-04-04 04:34:52 +0200 | XZDX | (~xzdx@user/XZDX) XZDX |
2025-04-04 04:36:03 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
2025-04-04 04:36:36 +0200 | mange | (~user@user/mange) mange |
2025-04-04 04:37:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-04 04:41:01 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 04:49:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 04:51:14 +0200 | <haskellbridge> | <Liamzee> thanks Axman6! |
2025-04-04 04:53:31 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 252 seconds) |
2025-04-04 04:53:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-04 04:54:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 04:59:43 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
2025-04-04 05:00:20 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) hackager |
2025-04-04 05:00:20 +0200 | ChanServ | +v haskellbridge |
2025-04-04 05:00:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 05:06:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 05:06:40 +0200 | <haskellbridge> | <Liamzee> that's cool, on apple m3, using time, C is 0.31s user 0.01s system for pidigits |
2025-04-04 05:07:12 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-04 05:09:24 +0200 | <haskellbridge> | <Liamzee> vs cabal run pidigits.hs -- 10000 -N4 0.43s user 0.02s system 95% cpu 0.472 total |
2025-04-04 05:11:18 +0200 | <haskellbridge> | <Liamzee> which is really freaking weird, the "div" outperforms the "quote" |
2025-04-04 05:11:22 +0200 | <haskellbridge> | <Liamzee> erm, "quot" |
2025-04-04 05:12:51 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Read error: Connection reset by peer) |
2025-04-04 05:16:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 05:17:11 +0200 | rstromlund | (~user@user/rstromlund) rstromlund |
2025-04-04 05:21:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 05:21:44 +0200 | rstromlund | (~user@user/rstromlund) (Ping timeout: 244 seconds) |
2025-04-04 05:32:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 05:35:05 +0200 | nitrix | (~nitrix@user/meow/nitrix) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-04-04 05:37:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 05:42:39 +0200 | michalz | (~michalz@185.246.207.215) |
2025-04-04 05:45:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
2025-04-04 05:48:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 05:53:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 05:55:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 06:00:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 06:01:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 06:06:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-04 06:32:18 +0200 | pabs3 | Guest7041 |
2025-04-04 06:32:18 +0200 | Guest7041 | (~pabs3@user/pabs3) (Killed (tantalum.libera.chat (Nickname regained by services))) |
2025-04-04 06:32:43 +0200 | pabs3 | (~pabs3@user/pabs3) pabs3 |
2025-04-04 06:32:47 +0200 | sp1ff | (~user@c-67-160-173-55.hsd1.wa.comcast.net) sp1ff |
2025-04-04 06:33:31 +0200 | <haskellbridge> | <Liamzee> does anyone have an intel system and is willing to help with benchmarks here? |
2025-04-04 06:33:44 +0200 | <haskellbridge> | <Liamzee> https://benchmarksgame-team.pages.debian.net/benchmarksgame/performance/pidigits.html |
2025-04-04 06:34:24 +0200 | <haskellbridge> | <Liamzee> on my system, quot does not introduce any advantages over div, but i'm on apple silicon, but the Haskell on apple silicon is taking 50% more time than the C |
2025-04-04 06:34:50 +0200 | <haskellbridge> | <Liamzee> whereas on their benchmarks, it's roughly 2x the time |
2025-04-04 06:42:23 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
2025-04-04 06:42:24 +0200 | jmcantrell_ | jmcantrell |
2025-04-04 06:47:17 +0200 | tavare | (~tavare@150.129.88.189) |
2025-04-04 06:47:17 +0200 | tavare | (~tavare@150.129.88.189) (Changing host) |
2025-04-04 06:47:17 +0200 | tavare | (~tavare@user/tavare) tavare |
2025-04-04 06:49:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 06:55:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 06:56:07 +0200 | ERR0R157 | (~ERR0R157@user/ERR0R157) ERR0R157 |
2025-04-04 07:01:33 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
2025-04-04 07:05:24 +0200 | <sim590> | I just added the data constructor `Offline` here: https://github.com/sim590/habanga/blob/b965deab3e7a3802c93bcfc6d46df58eabda28d4/src/core/NetworkSt… And I tried using it over here: https://github.com/sim590/habanga/blob/b965deab3e7a3802c93bcfc6d46df58eabda28d4/src/tui/GameView.h… and it compiles correctly according to HLS (Haskell Language Server), but cabal build gives "Not in |
2025-04-04 07:05:26 +0200 | <sim590> | scope: data constructor ‘NS.Offline’". Wtf ? |
2025-04-04 07:05:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 07:05:59 +0200 | <sim590> | It is exported... All types and constructors are exported by that module. So, GHC is wrong here. But I don't get it. |
2025-04-04 07:07:18 +0200 | <sim590> | If I replace `NS.Offline` by `_`, it compiles correctly... |
2025-04-04 07:08:53 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
2025-04-04 07:10:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 07:14:07 +0200 | <c_wraith> | did the habanga-tui component get recompiled? |
2025-04-04 07:14:18 +0200 | <sim590> | I did a full `v2-clean`. |
2025-04-04 07:14:21 +0200 | <sim590> | Then, I recompiled. |
2025-04-04 07:14:24 +0200 | <sim590> | Same error. |
2025-04-04 07:14:48 +0200 | <c_wraith> | Did it actually compile that component during the recompile? |
2025-04-04 07:15:03 +0200 | <sim590> | Oh I see. |
2025-04-04 07:15:06 +0200 | <sim590> | Let me check. |
2025-04-04 07:15:30 +0200 | <sim590> | That would explain. |
2025-04-04 07:16:34 +0200 | <c_wraith> | oh, I had that backwards. -core is the one that might not be recompiling |
2025-04-04 07:16:42 +0200 | <c_wraith> | but I suppose you know what I meant |
2025-04-04 07:16:59 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2025-04-04 07:17:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-04 07:17:40 +0200 | <sim590> | c_wraith: here's what I got: https://paste.debian.net/1367361/ |
2025-04-04 07:17:41 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
2025-04-04 07:17:47 +0200 | <sim590> | it does compile it.. :/ |
2025-04-04 07:17:54 +0200 | <sim590> | It's in NetworkState |
2025-04-04 07:19:12 +0200 | <c_wraith> | Ok, getting into real "just in case" territory - are you sure you've saved the change? |
2025-04-04 07:19:20 +0200 | <sim590> | Yes :D |
2025-04-04 07:19:42 +0200 | <sim590> | Oh. |
2025-04-04 07:19:44 +0200 | <sim590> | Fuc |
2025-04-04 07:20:08 +0200 | <sim590> | I think I was editing the file in the Git staging area. Because of fugitive.vim. |
2025-04-04 07:20:51 +0200 | <c_wraith> | That sounds way more confusing than any time I've saved to the wrong file. |
2025-04-04 07:21:05 +0200 | <c_wraith> | ... which is surprisingly common |
2025-04-04 07:21:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 07:21:57 +0200 | <haskellbridge> | <Liamzee> is there a simpler way to do (unur . move)? |
2025-04-04 07:22:11 +0200 | <sim590> | OK. There's clearly something. I'm not sure what it is yet. The file seems to be OK on disk, but git says it's "untracked". Even though, I committed it... |
2025-04-04 07:22:15 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-04-04 07:24:25 +0200 | <sim590> | Ah gawd. It seems like my Vim decided to save the file in the root directory of the repo instead of it's usual path and I,ve been editing that file since. Damn. |
2025-04-04 07:26:36 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-04 07:28:50 +0200 | ERR0R157 | (~ERR0R157@user/ERR0R157) (Remote host closed the connection) |
2025-04-04 07:29:31 +0200 | <sim590> | It seems like cabal decided to use the wrong NetworkState file in the root directory (that didn't have the constructor) even though `hs-source-dirs:` for `habanga-core` said `src/core`. So like if you have files in subdirectories, it's possible cabal/ghc confuses files in the root directories with files in the subdirectories. Seems like a bug. |
2025-04-04 07:37:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 07:44:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 07:44:36 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2025-04-04 07:55:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 08:00:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-04 08:02:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 08:02:29 +0200 | fp1 | (~Thunderbi@2001:708:20:1406::1370) fp |
2025-04-04 08:07:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 08:08:13 +0200 | ft | (~ft@p508db463.dip0.t-ipconnect.de) (Quit: leaving) |
2025-04-04 08:12:12 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 08:13:43 +0200 | <haskellbridge> | <Liamzee> i guess i love my experience with linear haskell being, every few months: |
2025-04-04 08:13:48 +0200 | <haskellbridge> | <Liamzee> "wow, linear haskell is a wonderful idea" |
2025-04-04 08:13:59 +0200 | <haskellbridge> | <Liamzee> then |
2025-04-04 08:14:12 +0200 | <haskellbridge> | <Liamzee> "developed by people who thought the best part of Rust was fighting with the borrow checker" |
2025-04-04 08:19:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 08:19:24 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-04 08:20:00 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
2025-04-04 08:21:07 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
2025-04-04 08:23:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 08:34:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 08:36:29 +0200 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-04-04 08:38:08 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
2025-04-04 08:38:41 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-04 08:39:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 08:50:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 08:54:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-04 08:56:09 +0200 | ash3en | (~Thunderbi@89.56.182.235) (Ping timeout: 276 seconds) |
2025-04-04 09:00:01 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-04-04 09:00:57 +0200 | caconym | (~caconym@user/caconym) caconym |
2025-04-04 09:01:55 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
2025-04-04 09:03:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 09:05:16 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2025-04-04 09:08:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-04 09:16:38 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
2025-04-04 09:16:40 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 09:16:44 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
2025-04-04 09:18:06 +0200 | Lord_of_Life_ | Lord_of_Life |
2025-04-04 09:18:51 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
2025-04-04 09:18:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 09:21:21 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-04 09:22:18 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f05c0965f70e915e324.dip0.t-ipconnect.de) acidjnk |
2025-04-04 09:23:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 09:25:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 09:26:38 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
2025-04-04 09:43:20 +0200 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-04-04 09:43:57 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2025-04-04 09:44:44 +0200 | nitrix | (~nitrix@user/meow/nitrix) nitrix |
2025-04-04 09:47:05 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 09:51:34 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-04 09:51:46 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) (Ping timeout: 268 seconds) |
2025-04-04 09:54:44 +0200 | sprotte24 | (~sprotte24@p200300d16f176a0098ec2c88260f9eb5.dip0.t-ipconnect.de) |
2025-04-04 10:02:17 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
2025-04-04 10:05:36 +0200 | __monty__ | (~toonn@user/toonn) toonn |
2025-04-04 10:07:48 +0200 | fp1 | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 268 seconds) |
2025-04-04 10:15:35 +0200 | ash3en | (~Thunderbi@89.56.182.235) (Quit: ash3en) |
2025-04-04 10:15:45 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
2025-04-04 10:18:58 +0200 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-04-04 10:20:24 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 10:20:31 +0200 | Guest57 | (~Guest57@2607:fb90:bdc9:4bb1:fc1e:62da:e5b7:17ae) |
2025-04-04 10:20:43 +0200 | Guest27 | (~Guest57@2607:fb90:bdc9:4bb1:fc1e:62da:e5b7:17ae) |
2025-04-04 10:25:51 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
2025-04-04 10:27:28 +0200 | ash3en | (~Thunderbi@89.56.182.235) (Ping timeout: 245 seconds) |
2025-04-04 10:28:01 +0200 | Guest57 | (~Guest57@2607:fb90:bdc9:4bb1:fc1e:62da:e5b7:17ae) (Quit: Client closed) |
2025-04-04 10:33:00 +0200 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-04-04 10:34:06 +0200 | Guest27 | (~Guest57@2607:fb90:bdc9:4bb1:fc1e:62da:e5b7:17ae) (Ping timeout: 240 seconds) |
2025-04-04 10:37:07 +0200 | chele | (~chele@user/chele) chele |
2025-04-04 10:39:35 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 10:44:36 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
2025-04-04 10:45:19 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
2025-04-04 10:46:03 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:818c:f861:24cb:fd10) ubert |
2025-04-04 10:46:40 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) |
2025-04-04 10:48:24 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
2025-04-04 10:49:26 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Client Quit) |
2025-04-04 10:49:57 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-04-04 10:52:49 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-04 11:13:33 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2025-04-04 11:15:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-04 11:24:13 +0200 | ash3en | (~Thunderbi@89.56.182.235) (Quit: ash3en) |
2025-04-04 11:27:27 +0200 | Digitteknohippie | (~user@user/digit) Digit |
2025-04-04 11:27:42 +0200 | hughjfchen | (~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3) |
2025-04-04 11:27:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 11:28:13 +0200 | hughjfchen | (~hughjfche@vmi2417424.contaboserver.net) hughjfchen |
2025-04-04 11:28:18 +0200 | Digit | (~user@user/digit) (Ping timeout: 245 seconds) |
2025-04-04 11:29:30 +0200 | <hellwolf> | I am a believer of LinearTypes. We need more people writing about it including practical use cases of it. |
2025-04-04 11:29:37 +0200 | dhil | (~dhil@2a0c:b381:52e:3600:d846:130d:349b:6b56) dhil |
2025-04-04 11:30:30 +0200 | ash3en | (~Thunderbi@89.56.182.235) ash3en |
2025-04-04 11:31:12 +0200 | hughjfchen | (~hughjfche@vmi2417424.contaboserver.net) (Client Quit) |
2025-04-04 11:32:55 +0200 | hughjfchen | (~hughjfche@vmi2417424.contaboserver.net) hughjfchen |
2025-04-04 11:34:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 11:35:29 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-04 11:35:33 +0200 | <hellwolf> | IMO, LinearTypes, linearity on arrows, is more versatile, e.g.: 1) LT can type correctly the protocol of resource accessing (memory management, e.g.), 2.) LT can safely versioning of the data, so that you don't use outdated data and cause losses in financial applications, 3.) model concurrency better than overly-sequential monadically, see "motivation" part of the lineartypes proposal. |
2025-04-04 11:36:23 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Remote host closed the connection) |
2025-04-04 11:36:44 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-04 11:41:51 +0200 | <haskellbridge> | <Morj> How's the ghc optimization of linear values progressed? Last I checked (ughh how many years ago) it was still worse than unboxing vectors and values and using ST |
2025-04-04 11:43:15 +0200 | <haskellbridge> | <Morj> Quick googling shows that it's still not as good, sad https://0xd34df00d.me/posts/2024/09/naive-nfas.html#linear-vectors |
2025-04-04 11:46:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 11:48:29 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 11:52:37 +0200 | hseg | (~gesh@46.120.20.180) |
2025-04-04 11:57:39 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
2025-04-04 11:57:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-04 11:58:01 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
2025-04-04 12:00:56 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
2025-04-04 12:01:15 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
2025-04-04 12:03:35 +0200 | <kqr> | Is there a conduit function for splitting Text up into words, and running the conduit for each word? I found Data.Conduit.Text.lines so I could probably mirror that implementation in my own words function, but it would be even more convenient if there was something ready-made I'm missing. |
2025-04-04 12:04:07 +0200 | <kqr> | I have thought about first splitting into lines, and then splitting the line into words with regular Text functions, and then re-yielding each word. Is that a reasonable approach? |
2025-04-04 12:04:33 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-04 12:10:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 12:11:19 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
2025-04-04 12:17:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 12:18:24 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds) |
2025-04-04 12:19:13 +0200 | Square2 | (~Square@user/square) Square |
2025-04-04 12:23:01 +0200 | <hseg> | int-e: Turns out 9.10.1 is an option -- hlint supports it already |
2025-04-04 12:24:08 +0200 | <hseg> | So while I put "report ghc-lib-parser is also affected by https://gitlab.haskell.org/ghc/ghc/-/issues/25576" on my todo list, I now have a workaround for the meantime |
2025-04-04 12:30:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 12:31:46 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
2025-04-04 12:33:44 +0200 | img | (~img@user/img) img |
2025-04-04 12:34:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
2025-04-04 12:37:18 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Remote host closed the connection) |
2025-04-04 12:37:41 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-04 12:41:59 +0200 | <haskellbridge> | <hellwolf> Morj: I am not sure. |
2025-04-04 12:41:59 +0200 | <haskellbridge> | But I will say is, there should be more to sell than performance, is it not? Otherwise people will rather stick to C/C++ or Rust. |
2025-04-04 12:44:47 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
2025-04-04 12:45:01 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) szkl |
2025-04-04 12:46:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 12:50:10 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 12:54:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-04 12:56:12 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2025-04-04 12:58:27 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
2025-04-04 12:59:12 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2025-04-04 13:01:55 +0200 | hseg | (~gesh@46.120.20.180) (Quit: WeeChat 4.6.0) |
2025-04-04 13:05:34 +0200 | <kqr> | Unrelated to the above: what would it take to derive semigroup and monoid? GHC suggests DeriveAnyClass but I have a vague memory that would be overkill. |
2025-04-04 13:06:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 13:06:26 +0200 | forell | (~forell@user/forell) forell |
2025-04-04 13:16:34 +0200 | tv | (~tv@user/tv) (Quit: derp) |
2025-04-04 13:18:30 +0200 | tv | (~tv@user/tv) tv |
2025-04-04 13:42:34 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-04 13:54:56 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:818c:f861:24cb:fd10) (Remote host closed the connection) |
2025-04-04 13:55:09 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:988a:cdd2:ae2a:2121) ubert |
2025-04-04 14:05:52 +0200 | xff0x | (~xff0x@2405:6580:b080:900:c94:b4ca:3e28:1c70) |
2025-04-04 14:07:47 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-04 14:11:07 +0200 | tremon | (~tremon@83.80.159.219) tremon |
2025-04-04 14:12:54 +0200 | dyniec | (~dyniec@dybiec.info) (Remote host closed the connection) |
2025-04-04 14:13:15 +0200 | dyniec | (~dyniec@dybiec.info) |
2025-04-04 14:16:56 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f05c0965f70e915e324.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
2025-04-04 14:20:27 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-04 14:22:26 +0200 | Digitteknohippie | Digit |
2025-04-04 14:28:34 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) |
2025-04-04 14:30:00 +0200 | fp1 | (~Thunderbi@2001:708:20:1406::1370) fp |
2025-04-04 14:31:08 +0200 | mange | (~user@user/mange) (Quit: Zzz...) |
2025-04-04 14:32:03 +0200 | Inst | (~Inst@user/Inst) Inst |
2025-04-04 14:32:10 +0200 | <Inst> | this just feels wrong |
2025-04-04 14:32:12 +0200 | <Inst> | https://paste.tomsmeding.com/1BYeLvRm |
2025-04-04 14:32:47 +0200 | <Inst> | this is an expanded for clarity version of Gordon Goodsman's solution here |
2025-04-04 14:32:50 +0200 | <Inst> | https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/pidigits-ghc-6.html |
2025-04-04 14:32:53 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 14:33:05 +0200 | <Inst> | the integer is intentional |
2025-04-04 14:33:40 +0200 | <Inst> | But Gordon's version is the best performing right now |
2025-04-04 14:37:37 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-04 14:38:07 +0200 | <Inst> | i mean, i could change it to ST, I tried a version with linear types that got blown up by poor support for integer in linear base |
2025-04-04 14:44:49 +0200 | ft | (~ft@p508db463.dip0.t-ipconnect.de) ft |
2025-04-04 14:45:40 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) |
2025-04-04 14:51:58 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:c0fa:b50a:3031:4dce) |
2025-04-04 14:55:01 +0200 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) smalltalkman |
2025-04-04 14:57:25 +0200 | Inst | (~Inst@user/Inst) (Remote host closed the connection) |
2025-04-04 15:04:58 +0200 | <haskellbridge> | <Morj> hellwolf: The good part about haskell is that you can get high performance and still use a good language with safety guarantees and pretty APIs. Linear types make the second even better, and if they did the first it would be incredible |
2025-04-04 15:07:25 +0200 | Square | (~Square4@user/square) Square |
2025-04-04 15:08:25 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2025-04-04 15:08:34 +0200 | <haskellbridge> | <hellwolf> It would be ideal. Yes. But I must admit I overlooked a lot Haskell's performance side of things in my use cases so far.. |
2025-04-04 15:09:25 +0200 | <haskellbridge> | <hellwolf> And I admit that it could improve a lot of its adoption if we had both safety and performance. It's probably too obvious :) |
2025-04-04 15:10:28 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 15:10:30 +0200 | <haskellbridge> | <hellwolf> I hope there is no such a trilemma exist: syntax (ergonomics), performance and safety. |
2025-04-04 15:13:36 +0200 | <haskellbridge> | <Morj> I'm usually happy with the performance of the regular code, especially compared to something like python or typescript. I've also for several years worked on a project where we were writing video decoders in haskell and cared about performance a lot, and it we were able to go very far with it |
2025-04-04 15:14:31 +0200 | <haskellbridge> | <Morj> I'm also always surprised by the fact that haskell TUIs are mostly faster than rust ones, somehow |
2025-04-04 15:23:24 +0200 | <haskellbridge> | <hellwolf> Morj: Nice read. |
2025-04-04 15:23:24 +0200 | <haskellbridge> | Is that your blog? |
2025-04-04 15:23:29 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-04 15:23:49 +0200 | <haskellbridge> | <Morj> Nope, some guy I follow |
2025-04-04 15:32:38 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-04-04 15:36:27 +0200 | Square | (~Square4@user/square) (Ping timeout: 246 seconds) |
2025-04-04 15:39:10 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) acidjnk |
2025-04-04 15:39:22 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) |
2025-04-04 15:39:47 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-04-04 15:40:43 +0200 | sprotte24 | (~sprotte24@p200300d16f176a0098ec2c88260f9eb5.dip0.t-ipconnect.de) (Quit: Leaving) |
2025-04-04 15:42:53 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-04 15:43:35 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) (Ping timeout: 244 seconds) |
2025-04-04 15:44:41 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) |
2025-04-04 15:50:14 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) (Ping timeout: 265 seconds) |
2025-04-04 15:51:25 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) |
2025-04-04 15:53:24 +0200 | Square2 | (~Square@user/square) (Ping timeout: 260 seconds) |
2025-04-04 15:57:41 +0200 | bezik | (~bezik@wikipedia/bezik) bezik |
2025-04-04 15:58:41 +0200 | toby-bro | (~toby-bro@user/toby-bro) toby-bro |
2025-04-04 15:58:58 +0200 | aman | (~aman@user/aman) aman |
2025-04-04 16:01:18 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-04-04 16:05:04 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) (Ping timeout: 260 seconds) |
2025-04-04 16:05:47 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) |
2025-04-04 16:08:26 +0200 | <haskellbridge> | <Liamzee> hmmm, just built a version under ST array, seems to lose about 2% speed compared to accum parameter :( |
2025-04-04 16:10:26 +0200 | <haskellbridge> | <Liamzee> plus side, at least I've had a legitimate use for unsafeInterleaveST for the first time in my life |
2025-04-04 16:11:47 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
2025-04-04 16:11:48 +0200 | inca | (~inca@syn-172-100-032-197.res.spectrum.com) (Ping timeout: 272 seconds) |
2025-04-04 16:14:50 +0200 | <EvanR> | pure functional for the win |
2025-04-04 16:15:20 +0200 | <EvanR> | yes ST is purely functional but the mutation will have a GC cost |
2025-04-04 16:15:36 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2025-04-04 16:16:57 +0200 | <EvanR> | "haskell TUIs are faster than rust TUIs" how do you even measure the airspeed speed velocity of a TUI |
2025-04-04 16:18:50 +0200 | <EvanR> | s/speed speed/speed/ |
2025-04-04 16:25:31 +0200 | <darkling> | Well, first you get an unladen swallow, and... |
2025-04-04 16:28:16 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) |
2025-04-04 16:40:06 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-04 16:40:54 +0200 | Digit | (~user@user/digit) (Ping timeout: 276 seconds) |
2025-04-04 16:41:50 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
2025-04-04 16:52:30 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:988a:cdd2:ae2a:2121) (Quit: ubert) |
2025-04-04 16:58:12 +0200 | <EvanR> | if a^3 < b^3 then a < b because cube root is a monotonic function and can be applied to both sides. But if a and b are rational and you only have the laws of rational numbers... I'm having a hard time proving this |
2025-04-04 16:59:03 +0200 | <EvanR> | similar to if (assuming a and b are > 0) a^2 < b^2 then a < b. Not sure which is simpler. I can't do either |
2025-04-04 16:59:14 +0200 | <int-e> | you can prove the contrapositive |
2025-04-04 16:59:33 +0200 | <haskellbridge> | <Morj> > how do you even measure the airspeed speed velocity of a TUIMore responsive to button presses, you know. I haven't measured it with a stopwatch, but it's noticeable how fast ghcup is for example |
2025-04-04 17:00:03 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
2025-04-04 17:00:54 +0200 | <EvanR> | int-e, that would seem to prove "it can't not be true" |
2025-04-04 17:01:19 +0200 | <EvanR> | this is from a book that is supposedly "a constructive approach" and the hint is also suggesting an indirect proof |
2025-04-04 17:01:26 +0200 | <int-e> | good enough for me |
2025-04-04 17:01:44 +0200 | <int-e> | (I default to classical logic) |
2025-04-04 17:01:58 +0200 | <EvanR> | it might not be classical logic since we're talking about rationals |
2025-04-04 17:02:11 +0200 | <EvanR> | I mean, just classical |
2025-04-04 17:02:18 +0200 | <haskellbridge> | <Morj> You don't need any laws of rational numbers here though |
2025-04-04 17:03:24 +0200 | <EvanR> | if you only have the laws of rational numbers, then you either need them or you can do it with nothing |
2025-04-04 17:03:47 +0200 | <EvanR> | (or it's impossible) |
2025-04-04 17:04:43 +0200 | <haskellbridge> | <Morj> You only need the statement "forall a, b: a > b ==> a^3 > b^3" and the laws of the "<" relation as usual, with them you can prove the opposite direction as well |
2025-04-04 17:04:53 +0200 | <haskellbridge> | <Morj> This works for rational, whole or natural numbers |
2025-04-04 17:04:59 +0200 | <haskellbridge> | <Morj> Uhh s/whole/integer/ |
2025-04-04 17:05:17 +0200 | <EvanR> | I can get if a < b then a^2 < b^2, but I'm not sure how that helps |
2025-04-04 17:05:25 +0200 | <EvanR> | I couldn't get if a < b then a^3 < b^3 |
2025-04-04 17:05:38 +0200 | <EvanR> | but either way that's the wrong direction |
2025-04-04 17:05:56 +0200 | <int-e> | your comparisons are decidable; you have trichotomy. |
2025-04-04 17:06:02 +0200 | <EvanR> | ? |
2025-04-04 17:06:10 +0200 | <EvanR> | sure |
2025-04-04 17:06:15 +0200 | <haskellbridge> | <Morj> Wait, come again, what are you trying to prove from what? |
2025-04-04 17:06:23 +0200 | <EvanR> | if a^3 < b^3 then a < b |
2025-04-04 17:06:38 +0200 | <haskellbridge> | <Morj> And what facts are given? |
2025-04-04 17:06:48 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
2025-04-04 17:06:53 +0200 | <EvanR> | rational numbers |
2025-04-04 17:07:15 +0200 | <int-e> | This will still follow from "if a >= b then a^3 >= b^3" by case analysis on the comparison a < b. |
2025-04-04 17:07:16 +0200 | <EvanR> | ok, a and b exist and are rational |
2025-04-04 17:07:18 +0200 | <haskellbridge> | <Morj> Rational numbers, depending on your class, might not have an "<" associated :D |
2025-04-04 17:07:35 +0200 | <EvanR> | they do, obviously |
2025-04-04 17:07:57 +0200 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-04-04 17:07:58 +0200 | TheCoffeMaker_ | (~TheCoffeM@186.136.173.70) |
2025-04-04 17:08:32 +0200 | <EvanR> | alright case analysis on a < b |
2025-04-04 17:08:39 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 260 seconds) |
2025-04-04 17:08:47 +0200 | <EvanR> | you use "if a < b then a^3 < b^3" but I couldn't prove this xD |
2025-04-04 17:09:07 +0200 | <int-e> | comparing a and b you get three cases: a < b and a^3 < b^3; a = b an a^3 = b^3; a > b and a^3 > b^3. |
2025-04-04 17:09:09 +0200 | <EvanR> | but also you'd have to dispatch the no, actually b < a case |
2025-04-04 17:09:25 +0200 | <EvanR> | you went from a < b to a^3 < b^3 |
2025-04-04 17:09:31 +0200 | <EvanR> | how |
2025-04-04 17:10:26 +0200 | <int-e> | if 0 <= a < b then a^3 <= a^2b <= ab^2 < b^3. The case a < b <= 0 is similar, and a <= 0 <= b and a < b falls to looking at signs |
2025-04-04 17:10:40 +0200 | <int-e> | by the laws of an ordered field |
2025-04-04 17:10:52 +0200 | <EvanR> | wait |
2025-04-04 17:11:16 +0200 | <EvanR> | yes I got a^3 < a^2b and ab^2 < b^3 separately |
2025-04-04 17:11:29 +0200 | dolio | (~dolio@130.44.140.168) dolio |
2025-04-04 17:11:38 +0200 | <EvanR> | how did you get a^2b < ab^2 |
2025-04-04 17:12:05 +0200 | <int-e> | you multiply a < b by a from the left and by b from the right |
2025-04-04 17:12:27 +0200 | <EvanR> | that's ab < ab |
2025-04-04 17:12:27 +0200 | <int-e> | it's just <= because a = 0 is a possibility |
2025-04-04 17:12:30 +0200 | dolio | (~dolio@130.44.140.168) (Client Quit) |
2025-04-04 17:12:35 +0200 | <EvanR> | er |
2025-04-04 17:13:03 +0200 | EvanR | recapitulates |
2025-04-04 17:13:18 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) (Remote host closed the connection) |
2025-04-04 17:13:34 +0200 | dolio | (~dolio@130.44.140.168) dolio |
2025-04-04 17:15:31 +0200 | <int-e> | TBH the funny part of this is that you were (apparently) willing to accept that the cube root function is strictly monotonic. |
2025-04-04 17:16:08 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
2025-04-04 17:16:12 +0200 | <EvanR> | well that's a fact about real numbers right |
2025-04-04 17:16:47 +0200 | <int-e> | well it's not if you apply the same level of skepticism that you're currently applying to the strict monotonicity of f(x) = x^3 in the rationals |
2025-04-04 17:18:32 +0200 | <EvanR> | I don't understand, I'm not skeptical. I'm trying to go from certain assumptions to a conclusion |
2025-04-04 17:18:58 +0200 | <int-e> | well, f(x) = x^3 being monotonic is a fact about rational number.s |
2025-04-04 17:19:05 +0200 | <EvanR> | not absolute truths, or "doesn't matter somebody somewhere has already done this one" |
2025-04-04 17:19:05 +0200 | int-e | shrugs |
2025-04-04 17:19:36 +0200 | <EvanR> | it might be but I didn't get there |
2025-04-04 17:19:56 +0200 | <int-e> | so how did you get there for the cube root in the reals? |
2025-04-04 17:19:56 +0200 | <EvanR> | but we just proved that |
2025-04-04 17:20:04 +0200 | <EvanR> | I didn't that's the point |
2025-04-04 17:20:28 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:c0fa:b50a:3031:4dce) (Quit: Leaving) |
2025-04-04 17:20:56 +0200 | <EvanR> | also it wouldn't even help, are you going to apply a function coded for real numbers to rationals? xD |
2025-04-04 17:21:10 +0200 | <int-e> | the rationals are a subfield of the reals |
2025-04-04 17:21:29 +0200 | <int-e> | (another fact) |
2025-04-04 17:21:30 +0200 | <EvanR> | this is "real anaylsis: a constructive approach" |
2025-04-04 17:21:38 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-04-04 17:21:46 +0200 | <EvanR> | so I can't solve chapter 1 by using chapter 17 from the other book |
2025-04-04 17:21:51 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
2025-04-04 17:22:15 +0200 | <EvanR> | again, the task to is to reason from what's assumed and not from "any argument whatever" |
2025-04-04 17:24:00 +0200 | fp1 | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 272 seconds) |
2025-04-04 17:24:24 +0200 | <EvanR> | maybe in chapter 17 there will be a thing to prove that any monotonic functions on reals can be downgraded to a monotonic function on rationals |
2025-04-04 17:25:14 +0200 | <EvanR> | somehow |
2025-04-04 17:32:33 +0200 | <EvanR> | a < b? yes, then you're done. Or a == b, then a^3==b^3 contradicting a^3 < b^3. Or b < a, using the above, b^3 < a^3, also contradicting. |
2025-04-04 17:32:39 +0200 | <EvanR> | cool |
2025-04-04 17:35:15 +0200 | <EvanR> | that means I don't have to solve this using the "hint use an indirect proof": Show that family of intervals [a,b] where a^3 <= 2 and 2 <= b^3 is consistent (any interval in the family intersects all the others) |
2025-04-04 17:41:40 +0200 | <kuribas> | You could prove that (a*a*a)/(b*b*b) < (c*c*c*)/(d*d*d) then a/b < c/d |
2025-04-04 17:41:52 +0200 | <kuribas> | For integral values of a, b, c, and d. |
2025-04-04 17:42:26 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
2025-04-04 17:43:30 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2025-04-04 17:45:39 +0200 | <EvanR> | if aaa / (bbb) < ccc / (ddd) then a/b < c/d? |
2025-04-04 17:45:50 +0200 | <EvanR> | just cancel 4 things? |
2025-04-04 17:45:53 +0200 | <EvanR> | wait |
2025-04-04 17:45:59 +0200 | <EvanR> | nvm |
2025-04-04 17:46:35 +0200 | <EvanR> | oh this is the same question. Well I tried that too and couldn't figure it out |
2025-04-04 17:46:49 +0200 | <kuribas> | Where do you get stuck? |
2025-04-04 17:47:19 +0200 | <EvanR> | immediately |
2025-04-04 17:48:39 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds) |
2025-04-04 17:49:35 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) |
2025-04-04 17:49:57 +0200 | <kuribas> | It's easy for naturals no? |
2025-04-04 17:51:14 +0200 | <EvanR> | what is |
2025-04-04 17:51:20 +0200 | <kuribas> | The formula? |
2025-04-04 17:51:32 +0200 | <EvanR> | nope |
2025-04-04 17:51:38 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 245 seconds) |
2025-04-04 17:51:56 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-04 17:52:13 +0200 | <EvanR> | aaaddd < bbbccc |
2025-04-04 17:52:34 +0200 | <EvanR> | 1 < bbbccc / (aaaddd) |
2025-04-04 17:52:49 +0200 | <EvanR> | aaaddd / (bbbccc) < 1 |
2025-04-04 17:54:39 +0200 | <kuribas> | a < b -> a*c < b*d if c < d and a < b |
2025-04-04 17:54:59 +0200 | <kuribas> | Easy proof by induction |
2025-04-04 17:55:04 +0200 | <EvanR> | you know what's easy, drawing two squares of different sizes aligned to corners, and extending one edge to map the other edge onto the larger side, and it's obviously shorter xD |
2025-04-04 17:55:23 +0200 | <EvanR> | or the cube version where you can extend a diagonal from the smaller cube onto larger cubes side |
2025-04-04 17:56:08 +0200 | <EvanR> | but this book is all about "no pictures!" |
2025-04-04 17:56:56 +0200 | <kuribas> | Anyway, I think "aaa < bbb -> a < b " is easy to prove by induction for naturals. |
2025-04-04 17:57:27 +0200 | <EvanR> | kuribas, a < b -> a*c < b*d ... ok I'm not seeing the connection. So that requires a < b, which we are trying to prove |
2025-04-04 17:57:43 +0200 | <kuribas> | right, that's the wrong direction. |
2025-04-04 17:58:13 +0200 | <EvanR> | I'll try that induction |
2025-04-04 17:58:37 +0200 | <int-e> | a*c < b*d if c < d and a < b is most elegantly split into two steps, a*c < b*c < b*d or a*c < a*d < b*d. |
2025-04-04 17:58:46 +0200 | <EvanR> | double induction 😱 |
2025-04-04 17:59:13 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
2025-04-04 17:59:31 +0200 | <int-e> | err the first comparison in either chain should be <= if 0 is allowed |
2025-04-04 18:00:51 +0200 | <haskellbridge> | <sm> Morj: Morj, really ? This surprises me |
2025-04-04 18:01:32 +0200 | <sm> | ("haskell TUIs are always faster than rust ones") |
2025-04-04 18:02:20 +0200 | <EvanR> | after thinking about it, I now see that your two "either or" formulas are not the "two steps" xD |
2025-04-04 18:03:10 +0200 | <kuribas> | aaa < a*a*a+n for some positive n. Also a*a*a+n = (a+m)(a+m)(a+m) for some m where b = a+m. Prove that m is positive. |
2025-04-04 18:03:13 +0200 | <EvanR> | ac < bc and bc < bd gets ac < bd, and other other thing was another route |
2025-04-04 18:04:15 +0200 | Digit | (~user@user/digit) Digit |
2025-04-04 18:04:28 +0200 | <EvanR> | aaa+n = (a+m)(a+m)(a+m) for some m ? |
2025-04-04 18:04:43 +0200 | <EvanR> | seems like a leap to me |
2025-04-04 18:05:17 +0200 | <kuribas> | EvanR: definition of `<` and `b` |
2025-04-04 18:05:31 +0200 | <EvanR> | that's an equal sign |
2025-04-04 18:06:06 +0200 | <EvanR> | ok, multiply out all the a+m and you get one aaa term |
2025-04-04 18:06:12 +0200 | <EvanR> | now I get it |
2025-04-04 18:06:59 +0200 | <kuribas> | We have the premise aaa < bbb, which means exists m such that "bbb = aaa + m" |
2025-04-04 18:07:06 +0200 | <kuribas> | It's the definition of < for naturals. |
2025-04-04 18:07:34 +0200 | <EvanR> | yeah it's just that I'm only considering your actual messages xD |
2025-04-04 18:07:46 +0200 | <kuribas> | sorry, I used n above. |
2025-04-04 18:08:05 +0200 | <EvanR> | since I have no idea what I'm doing |
2025-04-04 18:08:14 +0200 | <EvanR> | it's not a case of already know it |
2025-04-04 18:08:53 +0200 | <EvanR> | sm, yes... sounds like something else was slow in the apples to oranges comparison |
2025-04-04 18:10:23 +0200 | <kuribas> | gtg |
2025-04-04 18:10:31 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
2025-04-04 18:11:46 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
2025-04-04 18:21:33 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
2025-04-04 18:22:26 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2025-04-04 18:23:21 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) |
2025-04-04 18:33:18 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) (Ping timeout: 240 seconds) |
2025-04-04 18:36:19 +0200 | Digitteknohippie | (~user@user/digit) Digit |
2025-04-04 18:36:53 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) |
2025-04-04 18:38:54 +0200 | Digit | (~user@user/digit) (Ping timeout: 252 seconds) |
2025-04-04 18:39:59 +0200 | tromp | (~textual@2001:1c00:3487:1b00:5ca9:4add:c07a:f3a) |
2025-04-04 18:45:38 +0200 | Square2 | (~Square@user/square) Square |
2025-04-04 18:46:02 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
2025-04-04 18:46:44 +0200 | rvalue | (~rvalue@user/rvalue) rvalue |
2025-04-04 18:49:09 +0200 | Digitteknohippie | (~user@user/digit) (Ping timeout: 252 seconds) |
2025-04-04 18:58:38 +0200 | Digit | (~user@user/digit) Digit |
2025-04-04 18:59:32 +0200 | nitrix | (~nitrix@user/meow/nitrix) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-04-04 19:05:39 +0200 | Digitteknohippie | (~user@user/digit) Digit |
2025-04-04 19:06:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-04 19:07:40 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds) |
2025-04-04 19:10:15 +0200 | Digitteknohippie | digitteknohippie |
2025-04-04 19:10:20 +0200 | digitteknohippie | Digitteknohippie |
2025-04-04 19:11:47 +0200 | Digit | (~user@user/digit) (Quit: sorting out accidental double login) |
2025-04-04 19:12:01 +0200 | Digitteknohippie | Digit |
2025-04-04 19:12:30 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
2025-04-04 19:15:54 +0200 | dhil | (~dhil@2a0c:b381:52e:3600:d846:130d:349b:6b56) (Ping timeout: 246 seconds) |
2025-04-04 19:17:36 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 19:18:30 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) (Ping timeout: 240 seconds) |
2025-04-04 19:20:57 +0200 | sprotte24 | (~sprotte24@p200300d16f176a0098ec2c88260f9eb5.dip0.t-ipconnect.de) |
2025-04-04 19:21:42 +0200 | rit | (~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) |
2025-04-04 19:24:07 +0200 | tromp | (~textual@2001:1c00:3487:1b00:5ca9:4add:c07a:f3a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2025-04-04 19:24:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-04 19:36:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-04 19:37:24 +0200 | SethTisue | (sid14912@id-14912.ilkley.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-04 19:38:19 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2025-04-04 19:39:36 +0200 | mud | (~mud@user/kadoban) (Quit: quit) |
2025-04-04 19:43:58 +0200 | haritz | (~hrtz@user/haritz) (Ping timeout: 272 seconds) |
2025-04-04 19:44:23 +0200 | mud | (~mud@user/kadoban) kadoban |
2025-04-04 19:46:30 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f050cb0d6601d636238.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2025-04-04 19:50:30 +0200 | manwithluck | (~manwithlu@2a09:bac5:5085:2dc::49:221) manwithluck |