Newest at the top
| 2026-03-07 16:31:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-07 16:30:13 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2026-03-07 16:26:35 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2026-03-07 16:26:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-07 16:20:30 +0100 | Guest89 | (~Guest89@185.45.21.144) |
| 2026-03-07 16:19:17 +0100 | tromp | (~textual@2001:1c00:3487:1b00:e975:d7be:a717:768f) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-03-07 16:15:40 +0100 | qqq | (~qqq@185.54.23.93) |
| 2026-03-07 16:14:28 +0100 | Guest89 | (~Guest89@185.45.21.144) (Ping timeout: 240 seconds) |
| 2026-03-07 16:10:16 +0100 | <[exa]> | btw stay around until like monday, more people active by then |
| 2026-03-07 16:10:02 +0100 | <Guest89> | thanks a bunch for the feedback |
| 2026-03-07 16:09:53 +0100 | <Guest89> | otherwise compacting or ghc-dup (which I haven't tried yet and has its own limitations) is my goto |
| 2026-03-07 16:09:51 +0100 | <[exa]> | I've got to go btw, have good luck |
| 2026-03-07 16:09:43 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-03-07 16:09:25 +0100 | <[exa]> | well, yeah. |
| 2026-03-07 16:09:00 +0100 | <Guest89> | but one restriction that I *theoretically* have is the need for deep copying, which koka seems to have built in |
| 2026-03-07 16:08:37 +0100 | <Guest89> | I've actually spoken to one of the contributors before but they're not involved with the I/O algorithm part of it |
| 2026-03-07 16:08:09 +0100 | <Guest89> | I just didn't want to commit to a "clean" version before I had settled things like the type definitions |
| 2026-03-07 16:08:07 +0100 | <[exa]> | koka ain't bad, maybe ask the authors for opinion, maybe they'd have some bright ideas on what to do there |
| 2026-03-07 16:07:53 +0100 | <Guest89> | that's also not a bad idea, I was going to use quickcheck down the line anyway |
| 2026-03-07 16:07:32 +0100 | <[exa]> | which "proves" it ;) |
| 2026-03-07 16:07:26 +0100 | <[exa]> | you can make a quickcheck for equivalence |
| 2026-03-07 16:07:23 +0100 | <Guest89> | hmm maybe |
| 2026-03-07 16:07:14 +0100 | <Guest89> | the best candidate for a performant implementation would be in koka if you know the language but it's not mature at all |
| 2026-03-07 16:07:10 +0100 | <[exa]> | in the benchmarking version you change only this newtype and handling functions, and plug in anything that is fast |
| 2026-03-07 16:06:52 +0100 | <[exa]> | make yourself a newtype for list and call it "priority queue" |
| 2026-03-07 16:06:40 +0100 | <[exa]> | tbh I'd recommend splitting of a "clean" version and a "provably same but fast" version, like you suggested before |
| 2026-03-07 16:05:00 +0100 | <[exa]> | okay now it makes sense |
| 2026-03-07 16:04:53 +0100 | <[exa]> | ahhhhhhhhhhh |
| 2026-03-07 16:04:15 +0100 | <Guest89> | (and then there's laziness as we've discussed) |
| 2026-03-07 16:04:09 +0100 | <Guest89> | but haskell is a good candidate for *specification* template because it's got a very presentable syntax and it has a decent compromise between being very close to total functional/proof assistant syntax while still having very mature libraries and performance |
| 2026-03-07 16:03:47 +0100 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2026-03-07 16:03:02 +0100 | m_a_r_k | (~m_a_r_k@archlinux/support/mark) (Read error: Connection reset by peer) |
| 2026-03-07 16:02:42 +0100 | AlexNoo__ | (~AlexNoo@178.34.150.243) (Ping timeout: 248 seconds) |
| 2026-03-07 16:02:38 +0100 | <Guest89> | and hopefully also demonstrate that the bounds are the same in either paradigm (i.e. compared to imperative) |
| 2026-03-07 16:02:00 +0100 | <Guest89> | basically I'm trying make the first purely functional implementation of an I/O-efficient algorithm |
| 2026-03-07 16:01:39 +0100 | <Guest89> | I'm not a proof guy, I just wanted the best tools to support the limitations provided by the paper I linked |
| 2026-03-07 16:01:38 +0100 | AlexNoo_ | (~AlexNoo@178.34.150.243) (Ping timeout: 248 seconds) |
| 2026-03-07 16:01:20 +0100 | <Guest89> | and https://ssoelvsten.github.io/adiar/ |
| 2026-03-07 16:01:06 +0100 | AlexNoo | (~AlexNoo@178.34.150.243) (Ping timeout: 248 seconds) |
| 2026-03-07 16:00:55 +0100 | <[exa]> | (kinda curious, because it looks like you're proving something directly on the haskell code) |
| 2026-03-07 16:00:52 +0100 | <Guest89> | https://dl.acm.org/doi/10.1145/2429069.2429077 |
| 2026-03-07 16:00:37 +0100 | <[exa]> | btw what's the whole thing about? |
| 2026-03-07 16:00:31 +0100 | <Guest89> | would be nice to have constant time lookup at least though |
| 2026-03-07 15:59:52 +0100 | <Guest89> | so either I need to take the (relatively small) performance loss or invent a whole new kind of wheel in the process |
| 2026-03-07 15:59:36 +0100 | <Guest89> | ideally I need a purely functional and I/O-efficient at the same time but that has never been described in any literature |
| 2026-03-07 15:59:17 +0100 | <[exa]> | well I should finally find time to read that one in full |
| 2026-03-07 15:59:04 +0100 | <Guest89> | including a binomial heap |
| 2026-03-07 15:58:59 +0100 | <Guest89> | Chris Okasaki's book has a few examples |
| 2026-03-07 15:58:14 +0100 | <[exa]> | iirc there's some way to make a functionally-friendly heap but I don't recall any ATM... probably some version of the binomial one should behave nicely |
| 2026-03-07 15:58:09 +0100 | AlexNoo__ | (~AlexNoo@178.34.150.243) |