Newest at the top
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 |
2025-05-08 10:46:38 +0200 | <hellwolf> | you have two data that has @vb, but they don't aggree with the timeline! |
2025-05-08 10:46:24 +0200 | <hellwolf> | va >>= vb in one monad, and va >>= vb in another monad |
2025-05-08 10:46:06 +0200 | <hellwolf> | think of diamond-shaped path |
2025-05-08 10:45:58 +0200 | <tomsmeding> | sure, unsafe APIs are for living dangerously, we're talking about the safe APIs |
2025-05-08 10:45:38 +0200 | <tomsmeding> | then I still don't see the problem |
2025-05-08 10:45:35 +0200 | <hellwolf> | there is unsafe api for building other safe API |
2025-05-08 10:45:25 +0200 | <hellwolf> | not safely |
2025-05-08 10:45:18 +0200 | <tomsmeding> | can you "upgrade" the version of a variable? |
2025-05-08 10:45:16 +0200 | <hellwolf> | I have drew on paper, but I just don't have a actual "paper" to check if I was right about my hunch |
2025-05-08 10:44:49 +0200 | <hellwolf> | you produce future version of the data of the same version but not from the same "course" |
2025-05-08 10:44:29 +0200 | <hellwolf> | but then you can diverge from the same version to other course of actions |
2025-05-08 10:44:27 +0200 | <tomsmeding> | and you still can't use it at version v+1, which is the freshness restriction |
2025-05-08 10:44:19 +0200 | <hellwolf> | it is the same version |
2025-05-08 10:44:13 +0200 | <tomsmeding> | even if you copy data at version v, the copy will still be at version v |
2025-05-08 10:44:03 +0200 | <tomsmeding> | but it will retain the same version, surely? |
2025-05-08 10:44:01 +0200 | <hellwolf> | it will be "unsound"; I dont' use this word too rigoursly, so don't quote me |
2025-05-08 10:43:45 +0200 | <hellwolf> | you can copy a versioned data too freely without type system knowing |
2025-05-08 10:43:29 +0200 | <hellwolf> | the thing without linearity on arrow is that |
2025-05-08 10:42:53 +0200 | <tomsmeding> | me neither |
2025-05-08 10:42:49 +0200 | <hellwolf> | but I am not a theoretician by trade |
2025-05-08 10:42:32 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2025-05-08 10:42:30 +0200 | <hellwolf> | and I consider this a special case of LTL |
2025-05-08 10:42:26 +0200 | <hellwolf> | but the hunch is that without linearity on arrows, you can't build LTL |
2025-05-08 10:42:15 +0200 | <hellwolf> | I dont' have a full theoretical survey about this problem |
2025-05-08 10:42:06 +0200 | <hellwolf> | my hunch is you cannot do without linear types |
2025-05-08 10:41:59 +0200 | <hellwolf> | yep, happy to continue the discussion |
2025-05-08 10:41:42 +0200 | <tomsmeding> | I may be wrong |
2025-05-08 10:41:38 +0200 | <tomsmeding> | I'm probably not seeing everything, but I have the feeling the goal of requiring freshness of variables can be achieved more simply |
2025-05-08 10:40:23 +0200 | <tomsmeding> | and `sget` produces a computation with va=v and vb=v |
2025-05-08 10:40:08 +0200 | <tomsmeding> | right, I see that an Rv indeed has a single 'v' version |
2025-05-08 10:39:33 +0200 | <hellwolf> | *use |
2025-05-08 10:39:08 +0200 | <hellwolf> | the type is built to be conservative, and assume it will and forbid you to sue the data again |
2025-05-08 10:38:50 +0200 | <hellwolf> | you get a type error, because onTokenMinted might render data stale |
2025-05-08 10:38:38 +0200 | <hellwolf> | if you swap the onTokenMinted and sputs |
2025-05-08 10:38:28 +0200 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/examples/demo/src/ERC20.hs mint function |
2025-05-08 10:38:15 +0200 | <hellwolf> | the example actually shows such a data version type safety in action, is here: |