Newest at the top
| 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) |
| 2026-03-07 15:48:25 +0100 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) (Read error: Connection reset by peer) |
| 2026-03-07 15:48:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-07 15:47:53 +0100 | GdeVolpi1 | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2026-03-07 15:43:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-07 15:32:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-03-07 15:28:35 +0100 | simpleshun | (~simpleshu@user/SimpleShun) SimpleShun |
| 2026-03-07 15:25:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-07 15:16:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-03-07 15:12:06 +0100 | <Guest89> | oh damn, strict data actually massively improved the runtime on larger inputs |
| 2026-03-07 15:11:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-07 15:08:00 +0100 | <Guest89> | exa do you have a reference description of the data structure? |
| 2026-03-07 15:07:26 +0100 | <Guest89> | well the point is more that the data structures should be limited to trees and lists |