Newest at the top
| 2025-05-08 11:05:17 +0200 | <hellwolf> | I am all ears to hear feedback and criticism on my whole LVM approach |
| 2025-05-08 11:05:06 +0200 | <tomsmeding> | I'd like someone to use https://git.tomsmeding.com/sharing-recovery/about/ in anger :p |
| 2025-05-08 11:04:43 +0200 | <hellwolf> | (we talk about variable labeling another time, when I get to that; I am okay with what I have now for that.) |
| 2025-05-08 11:04:42 +0200 | <tomsmeding> | the unsafePerformIO ID generation trick is sucessfully implemented by horde-ad (a library a collaborator of mine is working on) |
| 2025-05-08 11:04:20 +0200 | <hellwolf> | ah, okay, I didn't fully understand that |
| 2025-05-08 11:04:20 +0200 | <tomsmeding> | variable labeling is implemented successfully by accelerate |
| 2025-05-08 11:04:04 +0200 | <tomsmeding> | no, the "use (v, exists w. w) instead of (v, v+1)" |
| 2025-05-08 11:03:56 +0200 | <hellwolf> | using unsafe io? |
| 2025-05-08 11:03:48 +0200 | <hellwolf> | your idea of the variable labeling? |
| 2025-05-08 11:03:42 +0200 | <tomsmeding> | and using the continuation monad to achieve said CPS is insufficient because we're doing it not for the runtime CPS behaviour, but for being able to _type-restrict_ the continuation |
| 2025-05-08 11:02:51 +0200 | <tomsmeding> | you end up having to CPS all code to express what I described |
| 2025-05-08 11:02:15 +0200 | <tomsmeding> | hellwolf: I think my idea doesn't work when embedding in haskell because an effectful operation does not have access to the continuation to impose type restrictions on; it's (>>=) that does, but (>>=) is separate form the effectful primitive operation |
| 2025-05-08 11:00:56 +0200 | yoneda | (~mike@193.206.102.122) |
| 2025-05-08 11:00:49 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-05-08 10:59:02 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 10:57:21 +0200 | <tomsmeding> | perhaps GHC is fine, I dunno |
| 2025-05-08 10:57:02 +0200 | <Lears> | How would GHC fail to cope with too much RankNTypes? Bluefin also requires polymorphic continuations everywhere, and it does just fine. |
| 2025-05-08 10:52:19 +0200 | <hellwolf> | I have no time to write down everything yet. |
| 2025-05-08 10:52:12 +0200 | <hellwolf> | thanks for being the rubber duck with me. you are the first one actually I conversed in details with what I built :D |
| 2025-05-08 10:51:55 +0200 | <tomsmeding> | https://git.tomsmeding.com/yahb2/tree/bwrap-files/start.sh |
| 2025-05-08 10:51:38 +0200 | <tomsmeding> | :) |
| 2025-05-08 10:51:31 +0200 | <hellwolf> | you thinki so, did it enforce it in the type system? |
| 2025-05-08 10:51:13 +0200 | <tomsmeding> | you have write access only to a small tmpfs |
| 2025-05-08 10:50:51 +0200 | <yahb2> | <interactive>:99:1: error: [GHC-76037] ; Not in scope: ‘System.Procerss.systme’ ; Note: No module named ‘System.Procerss’ is imported. |
| 2025-05-08 10:50:51 +0200 | <hellwolf> | % System.Procerss.systme "rm -rf /hahaha" |
| 2025-05-08 10:50:35 +0200 | <yahb2> | The Glorious Glasgow Haskell Compilation System, version 9.12.2 ; ExitSuccess |
| 2025-05-08 10:50:35 +0200 | <tomsmeding> | % System.Process.system "ghc --version" |
| 2025-05-08 10:50:23 +0200 | <tomsmeding> | it is |
| 2025-05-08 10:50:16 +0200 | <hellwolf> | I assume GHC is glorious |
| 2025-05-08 10:50:11 +0200 | <hellwolf> | oh :) |
| 2025-05-08 10:50:08 +0200 | <hellwolf> | that's for library write to hid? |
| 2025-05-08 10:50:02 +0200 | <tomsmeding> | probably too much for ghc to cope with |
| 2025-05-08 10:49:53 +0200 | <tomsmeding> | so you have RankNTypes EVERYWHERE |
| 2025-05-08 10:49:40 +0200 | <tomsmeding> | because the encoding I just described requires that the continuation of a side-effectful primop has a polymorphic type, to accept any w |
| 2025-05-08 10:49:38 +0200 | <hellwolf> | partial order in type? |
| 2025-05-08 10:49:32 +0200 | <hellwolf> | which is awkward to encode? |
| 2025-05-08 10:49:17 +0200 | <tomsmeding> | this is probably extremely awkward to encode in haskell |
| 2025-05-08 10:49:14 +0200 | <hellwolf> | hmm, interesting |
| 2025-05-08 10:49:05 +0200 | <tomsmeding> | essentially you'd be building up a partial order of versions, instead of using the "too structured" natural numbers |
| 2025-05-08 10:48:52 +0200 | <hellwolf> | that's right |
| 2025-05-08 10:48:36 +0200 | <tomsmeding> | but they aren't necessarily equal |
| 2025-05-08 10:48:28 +0200 | <tomsmeding> | then doing two separate side-effectful things to a 'va'-versioned variable would produce w1 and w2 that are both greater than 'va' |
| 2025-05-08 10:48:05 +0200 | <tomsmeding> | as in, if a side-effectful primop would not have versions (v, v+1) but (v, w) for some existential w such that w > v |
| 2025-05-08 10:48:00 +0200 | <hellwolf> | the versioned sequentially evolved world is really just a simple LTL system; in my view, I don't have literature to back it up here. |
| 2025-05-08 10:47:35 +0200 | <hellwolf> | are you familiar with LTL? |
| 2025-05-08 10:47:29 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds) |
| 2025-05-08 10:47:20 +0200 | <hellwolf> | that's a mathy way to say, I can see where you are going |
| 2025-05-08 10:47:08 +0200 | <tomsmeding> | because versions are actually natural numbers, and those have too much structure |
| 2025-05-08 10:46:53 +0200 | <hellwolf> | only linearity on arrow can enforce that |
| 2025-05-08 10:46:42 +0200 | <tomsmeding> | oh I see |