Newest at the top
| 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 |
| 2025-05-08 10:18:41 +0200 | <hellwolf> | yea, linear-type is for "data freshness" |
| 2025-05-08 10:18:24 +0200 | <tomsmeding> | no need for linear types to make sharing visible |
| 2025-05-08 10:18:15 +0200 | <tomsmeding> | but if you'd be writing your own language, with a separate parser and typechecker, then you have an AST of the user-written program immediately, and you can see all sharing because you're the only one who might break it |
| 2025-05-08 10:17:40 +0200 | <tomsmeding> | it's a technique to make the sharing explicit _in an embedding in haskell_ |
| 2025-05-08 10:17:29 +0200 | <tomsmeding> | then I actually question whether you _need_ linear types for this |
| 2025-05-08 10:17:13 +0200 | <hellwolf> | it's jsut for evaluator (the codegen most importantlh) |
| 2025-05-08 10:17:04 +0200 | <tomsmeding> | then this works |
| 2025-05-08 10:16:56 +0200 | <hellwolf> | tomsmeding: yep, variable duplication is not a runtime thing! |
| 2025-05-08 10:16:38 +0200 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/2b39ca47cb55324cab4eda36c0546ea1fb3d7aca/hs-pkgs… see runYLVM |
| 2025-05-08 10:16:16 +0200 | <tomsmeding> | there's no performance cost associated with duplication? |
| 2025-05-08 10:16:09 +0200 | <tomsmeding> | right, so apparently it doesn't matter in your application domain that variables are duplicated more often than strictly necessary? |
| 2025-05-08 10:15:29 +0200 | <lambdabot> | do you ensure the variable is dropped |
| 2025-05-08 10:15:29 +0200 | <lambdabot> | Unexpected do block in function application: |
| 2025-05-08 10:15:29 +0200 | <lambdabot> | error: |
| 2025-05-08 10:15:27 +0200 | <hellwolf> | the monad runner as a "cleanup block" that cleanup the variable references in the end. |
| 2025-05-08 10:15:27 +0200 | <hellwolf> | > but how do you ensure the variable is dropped |
| 2025-05-08 10:14:56 +0200 | <hellwolf> | yea, template haskell is unsound. I should read into your approach |