Newest at the top
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 |
2025-05-08 10:31:05 +0200 | <hellwolf> | where did you see that? |
2025-05-08 10:30:39 +0200 | <tomsmeding> | or perhaps "referrable" |
2025-05-08 10:30:27 +0200 | <tomsmeding> | (it's spelled "referentiable", not "referenciable") |
2025-05-08 10:29:29 +0200 | <hellwolf> | corect |
2025-05-08 10:29:29 +0200 | <hellwolf> | 05-08 11:28 <tomsmeding> presumably the idea is that pure primitive LVM operations have va=vb, and side-effectful primitive LVM operations have va < vb? |
2025-05-08 10:29:07 +0200 | <hellwolf> | I would not see version independently, it's all about the >>= |
2025-05-08 10:28:46 +0200 | <hellwolf> | (_ :: m ctx va vb a) >>= (_ :: a -> m ctx vb vc b) ? |
2025-05-08 10:28:41 +0200 | <tomsmeding> | presumably the idea is that pure primitive LVM operations have va=vb, and side-effectful primitive LVM operations have va < vb? |
2025-05-08 10:28:00 +0200 | <hellwolf> | it's more about what you can be bound with |
2025-05-08 10:27:56 +0200 | <tomsmeding> | is there anything at version 'va'? |
2025-05-08 10:27:49 +0200 | <hellwolf> | not sure I would say ctx having a version, per se. |
2025-05-08 10:27:30 +0200 | <hellwolf> | hmm in a way, I guess. a is the output type at version @vb@. |
2025-05-08 10:27:01 +0200 | <tomsmeding> | the input ctx, that is |
2025-05-08 10:26:49 +0200 | <tomsmeding> | is it the idea that ctx is at version va, and that a is at version vb? |
2025-05-08 10:24:24 +0200 | <tomsmeding> | yes I found it :) |
2025-05-08 10:24:19 +0200 | <hellwolf> | here |
2025-05-08 10:24:19 +0200 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl-linear-smc/internal/lvm/C… |
2025-05-08 10:24:14 +0200 | <hellwolf> | excuse moi, that's my own sh*t |
2025-05-08 10:23:58 +0200 | tomsmeding | is looking at the LVM definition |
2025-05-08 10:23:50 +0200 | <tomsmeding> | yes it does |
2025-05-08 10:23:39 +0200 | <hellwolf> | but does that program example make sense? |
2025-05-08 10:22:40 +0200 | Boarders_____ | (sid425905@id-425905.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-05-08 10:22:22 +0200 | <tomsmeding> | :D |
2025-05-08 10:22:19 +0200 | <hellwolf> | bad habit. |
2025-05-08 10:22:16 +0200 | <hellwolf> | tomsmeding: haha, sorry, it's just sometimes I need to say things to peopel giving money |
2025-05-08 10:21:59 +0200 | <hellwolf> | I am all ears. I am an engineer, so I am here just to assemble solutions. |
2025-05-08 10:21:54 +0200 | <tomsmeding> | you don't need to shout large numbers to convince me that it's interesting to care about software correctness ;) |
2025-05-08 10:21:42 +0200 | <hellwolf> | can you enforce it in type safety in other means? |
2025-05-08 10:21:12 +0200 | <hellwolf> | there were millions lost due to this kind of bugs. |
2025-05-08 10:20:53 +0200 | <hellwolf> | it's a type error if you use dated data |
2025-05-08 10:20:45 +0200 | <hellwolf> | yea, I use linear types ot create a type safe way to encode that |
2025-05-08 10:20:29 +0200 | <hellwolf> | in a open financial API system, that creates a vulnerability |
2025-05-08 10:20:26 +0200 | <tomsmeding> | that sounds like the versioning, not the linear types |
2025-05-08 10:20:17 +0200 | <hellwolf> | you then do something again, with the assumption that the balance of beforeBalanceA is still valid |
2025-05-08 10:19:58 +0200 | <hellwolf> | you read the balance of account A -> beforeBalanceA; you invoke some side effects |
2025-05-08 10:19:21 +0200 | <hellwolf> | so, say, you write such a program: |
2025-05-08 10:19:05 +0200 | <hellwolf> | yea, it's domain specific. let me see if I can explain |
2025-05-08 10:18:50 +0200 | tomsmeding | has no clue what that means |