Newest at the top
| 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) |
| 2026-03-07 15:57:25 +0100 | AlexNoo_ | (~AlexNoo@178.34.150.243) |
| 2026-03-07 15:57:22 +0100 | AlexNoo__ | (~AlexNoo@178.34.150.243) (Ping timeout: 248 seconds) |
| 2026-03-07 15:56:50 +0100 | AlexNoo_ | (~AlexNoo@178.34.150.243) (Ping timeout: 248 seconds) |
| 2026-03-07 15:56:42 +0100 | AlexNoo | (~AlexNoo@178.34.150.243) |
| 2026-03-07 15:56:09 +0100 | <Guest89> | I may have to investigate more specialized data structures depending on whether or not I am brave enough to try to make the implementation work on the disk |
| 2026-03-07 15:55:35 +0100 | AlexNoo | (~AlexNoo@178.34.150.243) (Ping timeout: 245 seconds) |
| 2026-03-07 15:55:22 +0100 | <Guest89> | Data.Set is probably a fine compromise for the moment |
| 2026-03-07 15:55:10 +0100 | <[exa]> | anyway if that's the case, Data.Set is pure and should be quite fast too. |
| 2026-03-07 15:54:52 +0100 | <[exa]> | I kinda thought that this is the implementation of the system where you're proving stuff |
| 2026-03-07 15:54:46 +0100 | <Guest89> | yes |
| 2026-03-07 15:54:33 +0100 | <[exa]> | wait why not (you're proving that something can be done purely?) |
| 2026-03-07 15:53:29 +0100 | <Guest89> | I think for the purposes of my thesis it's invalid because I theoretically can't rely on random access |
| 2026-03-07 15:53:12 +0100 | <[exa]> | Guest89: the structure is a completely normal binary heap in array, makeHeap and related stuff is on wiki |
| 2026-03-07 15:53:07 +0100 | AlexNoo__ | (~AlexNoo@178.34.150.243) |
| 2026-03-07 15:52:42 +0100 | <[exa]> | Guest89: oh great :) |
| 2026-03-07 15:52:21 +0100 | AlexNoo_ | (~AlexNoo@178.34.150.243) |