Newest at the top
| 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: |
| 2025-05-08 10:36:29 +0200 | <hellwolf> | newtype P'x (eff :: PortEffect) r a = MkP'x (P (YulCat LinearEffectX) r a) |
| 2025-05-08 10:36:29 +0200 | <hellwolf> | -- | Yul port with the port effect kind, aka. yul ports. |
| 2025-05-08 10:36:25 +0200 | <hellwolf> | type P'V v = P'x (VersionedPort v) |
| 2025-05-08 10:36:24 +0200 | <hellwolf> | -- | Yul port with linearly versioned data, aka. versioned yul ports. |
| 2025-05-08 10:36:03 +0200 | <hellwolf> | "P k r a" was the original API |
| 2025-05-08 10:35:41 +0200 | <hellwolf> | haha, well how else, you do it. P is not my api, P'v is a newtype wrapper where I shove the version into |
| 2025-05-08 10:35:22 +0200 | <tomsmeding> | "P'v v r a" |
| 2025-05-08 10:35:16 +0200 | <hellwolf> | :) what I just said, or the code related to P? |
| 2025-05-08 10:34:37 +0200 | <tomsmeding> | reads like klingon |
| 2025-05-08 10:34:24 +0200 | <tomsmeding> | sure |
| 2025-05-08 10:34:14 +0200 | <hellwolf> | e.g. Ur or (), or this type of thing doesn't carry such a version information |
| 2025-05-08 10:34:04 +0200 | <hellwolf> | not all @a@ has to be |
| 2025-05-08 10:34:01 +0200 | <hellwolf> | right, to be precise, @a@ has a chance to be versioned at @va@ |
| 2025-05-08 10:33:39 +0200 | <tomsmeding> | hence me not yet understanding what va is used for |
| 2025-05-08 10:33:20 +0200 | <tomsmeding> | what I'm naively expecting is that a variable reference has a specific version, and you can only _refer_ to such a variable if its version is equal to the current vb |
| 2025-05-08 10:33:13 +0200 | <hellwolf> | so all data are versioned |
| 2025-05-08 10:33:10 +0200 | <hellwolf> | data uses the "port api" from linear-smc library |
| 2025-05-08 10:32:59 +0200 | <hellwolf> | sput'l :: forall. VersionThread r ⊸ P'V v r a ⊸ P'V v r b ⊸ (VersionThread r, P'V (v + 1) r ()) |
| 2025-05-08 10:32:53 +0200 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl-linear-smc/src/YulDSL/Has… |
| 2025-05-08 10:32:44 +0200 | <tomsmeding> | sure |
| 2025-05-08 10:32:38 +0200 | <hellwolf> | since @a@ has no injectivty to @va@ |
| 2025-05-08 10:32:30 +0200 | <hellwolf> | let me show you, it's not obvious, if you only look at LVM definitinop |
| 2025-05-08 10:32:05 +0200 | <tomsmeding> | so I thought I'd look at variables, but I haven't found what I'm looking for yet |
| 2025-05-08 10:31:52 +0200 | <tomsmeding> | I'm looking for something that shows me how using a non-fresh reference will result in a type error |
| 2025-05-08 10:31:24 +0200 | <hellwolf> | okay, thanks, I will fix |
| 2025-05-08 10:31:10 +0200 | <tomsmeding> | LVMVar.hs |