| 2025-05-08 00:00:02 +0200 | <hellwolf> | 05-08 00:59 <tomsmeding> your users whose program now takes ages, will care |
| 2025-05-08 00:00:02 +0200 | <hellwolf> | heh, yea, my domain happens to have small programs; safety is more important there, which I am trying to sell |
| 2025-05-08 00:00:13 +0200 | <tomsmeding> | I'd rather say that every constructor in your GADT gets an additional field: the label |
| 2025-05-08 00:00:27 +0200 | <hellwolf> | that's an interesting idea |
| 2025-05-08 00:00:38 +0200 | <hellwolf> | could be a next step in next version. |
| 2025-05-08 00:01:07 +0200 | <hellwolf> | so, I try to use linear-types only for effectful stuff |
| 2025-05-08 00:01:10 +0200 | <hellwolf> | there you can't duplicate |
| 2025-05-08 00:01:18 +0200 | <hellwolf> | otherwise storage or external messages sent twice |
| 2025-05-08 00:01:20 +0200 | <hellwolf> | that's incorrect |
| 2025-05-08 00:01:23 +0200 | <hellwolf> | semantics |
| 2025-05-08 00:01:25 +0200 | <tomsmeding> | or alternatively, and more neatly, you write your AST as a base functor, and have two "fixpoint combinators" on top of that: the usual one (newtype Fix f = In (f (Fix f))) _after_ sharing recovery, and a labeled one (data Labeled f = Lab Int (f (Labeled f))) before sharing recovery |
| 2025-05-08 00:01:37 +0200 | <tomsmeding> | right |
| 2025-05-08 00:01:40 +0200 | <hellwolf> | and linear types solvs the sharing completely |
| 2025-05-08 00:01:51 +0200 | <hellwolf> | and I developed a technical of using linear types very ergonomically |
| 2025-05-08 00:01:53 +0200 | <hellwolf> | I can talk another time |
| 2025-05-08 00:02:00 +0200 | <hellwolf> | it's too exciting for me, I need to sleep to :D |
| 2025-05-08 00:02:09 +0200 | <tomsmeding> | :p |
| 2025-05-08 00:02:20 +0200 | <tomsmeding> | sleep well |
| 2025-05-08 00:02:34 +0200 | <hellwolf> | | let z = a + b * c in dup'l z & uncurry (*) |
| 2025-05-08 00:02:40 +0200 | <hellwolf> | this is linear-type version of working with pure diagrams |
| 2025-05-08 00:02:46 +0200 | <hellwolf> | | let z = a + b * c in z * z |
| 2025-05-08 00:02:55 +0200 | <hellwolf> | this is the non-linear-type version with diagram duplication |
| 2025-05-08 00:03:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 00:03:27 +0200 | <hellwolf> | I can repl codegen and live demo :) |
| 2025-05-08 00:03:36 +0200 | <hellwolf> | that's what I will be working on until the conferenc.e |
| 2025-05-08 00:04:42 +0200 | <hellwolf> | I have Category/Monoidal/Cartesian/Cartesian Closed standard categorical "verbs" |
| 2025-05-08 00:05:39 +0200 | <hellwolf> | special constructors/"verbs" are: MapHask, Switch, Jmp (jump to named function or built-in), Call (external messages), SGet/SPut (storage) |
| 2025-05-08 00:06:12 +0200 | <hellwolf> | I am very judicious of adding special verb, unless I can't find a categorical verb. |
| 2025-05-08 00:06:41 +0200 | <hellwolf> | usually it's particular to the domain, or a special control structure |
| 2025-05-08 00:07:22 +0200 | <hellwolf> | I can't do infinite recursion stuff in this domain, I don't even have heap (I can emulate, but I dont' want to go there), so I need a special verb for tight-loop |
| 2025-05-08 00:07:26 +0200 | <hellwolf> | to implement Foldable. |
| 2025-05-08 00:07:47 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-05-08 00:07:54 +0200 | <hellwolf> | so, the tight-loop is the special control flow |
| 2025-05-08 00:08:03 +0200 | <hellwolf> | another one is Switch control flow |
| 2025-05-08 00:08:34 +0200 | <hellwolf> | which I solved the sharing problem there, by having special functions that build the diagram "delicately" |
| 2025-05-08 00:08:44 +0200 | <hellwolf> | with the help of the special verb. |
| 2025-05-08 00:08:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 00:08:54 +0200 | <hellwolf> | but that's the entire language |
| 2025-05-08 00:09:08 +0200 | <hellwolf> | it's not a lambda based language. I still lambda from Haskell. |
| 2025-05-08 00:09:10 +0200 | <hellwolf> | *steal |
| 2025-05-08 00:09:32 +0200 | <hellwolf> | alright, that's all for today :) |
| 2025-05-08 00:10:33 +0200 | <hellwolf> | maybe the final one is the end-to-end example: https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/examples/demo/src/ERC20.hs This is in linear-types, in fact, my special linear-versioned-monad, which is definitely something I haven't seen prior art with my limited search |
| 2025-05-08 00:12:36 +0200 | <hellwolf> | I know it's gonna be exciting for me to keep talking and not shut up. One last thing for labeling: |
| 2025-05-08 00:13:16 +0200 | <hellwolf> | to solves the ergonomics of not having to manually label |
| 2025-05-08 00:13:29 +0200 | <hellwolf> | I have used template haskell to generate unique id |
| 2025-05-08 00:13:39 +0200 | <hellwolf> | based on module name and src loc |
| 2025-05-08 00:13:44 +0200 | <hellwolf> | here: https://github.com/yolc-dev/yul-dsl-monorepo/blob/2b39ca47cb55324cab4eda36c0546ea1fb3d7aca/hs-pkgs… |
| 2025-05-08 00:14:25 +0200 | <hellwolf> | I don't use that for all diagrams, but your suggestion of making labeling part of the GADT type is a good one, I think I will use that eventually. |
| 2025-05-08 00:14:41 +0200 | <hellwolf> | but that might involve too much template haskell dotted everywhere |
| 2025-05-08 00:14:52 +0200 | <hellwolf> | I still care about ergonomics, so I will be still judicious about it. |
| 2025-05-08 00:19:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 00:20:13 +0200 | hellwolf | duck. good night. |
| 2025-05-08 00:22:27 +0200 | xff0x | (~xff0x@2405:6580:b080:900:c380:f27a:d8a3:29c7) (Ping timeout: 252 seconds) |
| 2025-05-08 00:23:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 00:24:02 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-05-08 00:30:24 +0200 | tromp | (~textual@2001:1c00:3487:1b00:d43:3b62:1503:cb84) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 00:34:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 00:38:14 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 2025-05-08 00:38:45 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-05-08 00:40:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-05-08 00:41:59 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-05-08 00:49:20 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 00:50:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 00:53:09 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f51b11b7fbde7c758e1.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-05-08 00:55:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 00:56:32 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-05-08 01:04:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 01:08:36 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 264 seconds) |
| 2025-05-08 01:08:45 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-05-08 01:11:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 01:11:16 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-05-08 01:12:32 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 01:13:01 +0200 | sprotte24 | (~sprotte24@p200300d16f3ca800283c8f0415b7b94b.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-05-08 01:13:52 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-08 01:14:25 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-05-08 01:21:43 +0200 | Kaladin | (~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) (Quit: Leaving) |
| 2025-05-08 01:22:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 01:26:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 01:28:19 +0200 | shapr | (~user@2600:4040:5c49:5600:cacf:8e54:c9ac:25) (Remote host closed the connection) |
| 2025-05-08 01:30:40 +0200 | Kaladin | (~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) Kaladin |
| 2025-05-08 01:33:49 +0200 | Guest84 | (~Guest84@host-95-237-69-25.retail.telecomitalia.it) |
| 2025-05-08 01:37:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 01:42:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 01:45:20 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2025-05-08 01:56:01 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 248 seconds) |
| 2025-05-08 02:00:57 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-05-08 02:04:31 +0200 | jespada | (~jespada@179.26.249.126) (Ping timeout: 244 seconds) |
| 2025-05-08 02:04:33 +0200 | hiredman | (~hiredman@frontier1.downey.family) (Ping timeout: 248 seconds) |
| 2025-05-08 02:07:18 +0200 | hiredman | (~hiredman@frontier1.downey.family) hiredman |
| 2025-05-08 02:09:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 02:12:05 +0200 | Guest84 | (~Guest84@host-95-237-69-25.retail.telecomitalia.it) (Quit: Client closed) |
| 2025-05-08 02:12:07 +0200 | Kaladin | (~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) (Quit: Leaving) |
| 2025-05-08 02:14:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 02:20:51 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 02:25:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 02:26:25 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 2025-05-08 02:27:14 +0200 | Axma13761 | (~Axman6@user/axman6) Axman6 |
| 2025-05-08 02:28:47 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-08 02:29:33 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 250 seconds) |
| 2025-05-08 02:30:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 02:30:28 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-08 02:30:31 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-08 02:32:39 +0200 | Natch | (~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 260 seconds) |
| 2025-05-08 02:35:59 +0200 | Natch | (~natch@c-92-34-7-158.bbcust.telenor.se) Natch |
| 2025-05-08 02:40:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 02:46:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-05-08 02:56:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 02:58:19 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2025-05-08 02:58:25 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 2025-05-08 03:01:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-05-08 03:02:39 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-05-08 03:09:04 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000::2) |
| 2025-05-08 03:10:29 +0200 | sajenim | (~sajenim@user/sajenim) sajenim |
| 2025-05-08 03:10:49 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000::2) (Changing host) |
| 2025-05-08 03:10:49 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-05-08 03:12:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 03:17:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-05-08 03:28:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 03:33:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 03:38:15 +0200 | pointlessslippe1 | (~pointless@62.106.85.17) (Read error: Connection reset by peer) |
| 2025-05-08 03:41:41 +0200 | pointlessslippe1 | (~pointless@62.106.85.17) pointlessslippe1 |
| 2025-05-08 03:44:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 03:46:01 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-05-08 03:48:55 +0200 | img | (~img@user/img) img |
| 2025-05-08 03:51:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-05-08 04:02:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 04:04:37 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) |
| 2025-05-08 04:06:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 04:15:41 +0200 | tavare | (~tavare@user/tavare) tavare |
| 2025-05-08 04:17:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 04:19:57 +0200 | chewybread | (~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70) |
| 2025-05-08 04:19:57 +0200 | chewybread | (~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70) (Changing host) |
| 2025-05-08 04:19:57 +0200 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2025-05-08 04:22:01 +0200 | td_ | (~td@i5387091E.versanet.de) (Ping timeout: 252 seconds) |
| 2025-05-08 04:22:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 04:22:48 +0200 | Square | (~Square@user/square) Square |
| 2025-05-08 04:23:00 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 2025-05-08 04:23:48 +0200 | td_ | (~td@i53870937.versanet.de) |
| 2025-05-08 04:29:22 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-05-08 04:33:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 04:39:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 04:45:36 +0200 | chewybread | (~chewybrea@user/chewybread) (Remote host closed the connection) |
| 2025-05-08 04:49:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 04:54:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 04:58:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 05:03:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 05:10:29 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-05-08 05:12:00 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-05-08 05:13:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 05:16:24 +0200 | <monochrom> | No one can steal lambda from Haskell without also stealing purity, laziness, preferring currying, ... |
| 2025-05-08 05:19:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-05-08 05:21:40 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 2025-05-08 05:23:46 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 05:29:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 05:34:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-05-08 05:44:02 +0200 | aforemny_ | (~aforemny@i59F4C598.versanet.de) aforemny |
| 2025-05-08 05:45:19 +0200 | aforemny | (~aforemny@2001:9e8:6ce9:2000:c495:2bb2:ad61:d989) (Ping timeout: 265 seconds) |
| 2025-05-08 05:45:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 05:50:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 06:01:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 06:06:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-05-08 06:10:25 +0200 | Square | (~Square@user/square) (Ping timeout: 248 seconds) |
| 2025-05-08 06:17:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 06:21:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-05-08 06:35:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 06:37:14 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 06:38:28 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 2025-05-08 06:41:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 06:49:27 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-05-08 06:52:48 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-05-08 06:53:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 06:54:09 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 2025-05-08 07:04:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 07:06:45 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-05-08 07:09:39 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) (Read error: Connection reset by peer) |
| 2025-05-08 07:10:08 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-05-08 07:14:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 07:19:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 07:27:13 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-08 07:27:32 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-08 07:28:13 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 07:30:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 07:32:41 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-05-08 07:35:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-05-08 07:46:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 07:51:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-05-08 07:51:33 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2025-05-08 08:00:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 08:05:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 08:08:48 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 08:10:19 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 2025-05-08 08:15:49 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) internatetional |
| 2025-05-08 08:15:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 08:20:55 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) (Ping timeout: 276 seconds) |
| 2025-05-08 08:21:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 08:31:20 +0200 | <haskellbridge> | <hellwolf> morning thought to continue... |
| 2025-05-08 08:31:20 +0200 | <haskellbridge> | Using exponential objects (aka. a -> b or b^a) to express the desire explicitly that "a" as an output of an unknown diagram may be used by the exponential object any number of times is the alternative to regular "let" for an embedding language. |
| 2025-05-08 08:31:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 08:32:25 +0200 | <haskellbridge> | <hellwolf> It intends to solve the "exponentially growing diagrams" issue, similar to what let var sharing solves. |
| 2025-05-08 08:32:42 +0200 | <haskellbridge> | <hellwolf> The word "exponential" appears twice seems an interesting coincidence. |
| 2025-05-08 08:33:37 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 08:34:17 +0200 | <haskellbridge> | <hellwolf> Furthermore, LinearTypes offers another alternative: force you to express sharing using combinators such as "dup" |
| 2025-05-08 08:34:47 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-05-08 08:36:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-08 08:37:07 +0200 | <haskellbridge> | <hellwolf> Furthermore furthermore, I have developed a special "lmonad" for LinearTypes which makes that chore of duplication invisible. In brief, m VarRef, and each time you use the var you get a duplication. |
| 2025-05-08 08:37:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-05-08 08:37:31 +0200 | <haskellbridge> | <hellwolf> It's a trade-off again: now, you need to program in a monad |
| 2025-05-08 08:41:20 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-05-08 08:41:53 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-08 08:42:31 +0200 | <haskellbridge> | <hellwolf> further further furthermore, while using monad and LinrarTypes seems to defeat the benefits of using LinrarTypes to express "parallelizable branches", |
| 2025-05-08 08:44:02 +0200 | <haskellbridge> | <hellwolf> by that I mean, thanks to LinearTypes, it's very clear that branches of linear paths can be evaluated in parallel with side effects, since any sharing is explicit with "dup". |
| 2025-05-08 08:45:31 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f49a8c9e3402b4ffa7d.dip0.t-ipconnect.de) acidjnk |
| 2025-05-08 08:46:55 +0200 | <haskellbridge> | <hellwolf> but that benefit can be recouped by versioning the global state, where versioned monad within the same "version" can be evaluated in parallel, but the monad of the next version must wait all those to finish first. |
| 2025-05-08 08:47:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-05-08 08:48:28 +0200 | <haskellbridge> | <hellwolf> this construction may seems ad-hoc, but I think if i try to generalize further, maybe a 2026 endeavour of me..., this is essentially building up to a monadic way of encoding linear-time temporal logic in Haskell. |
| 2025-05-08 08:49:20 +0200 | <haskellbridge> | <hellwolf> linear-versioned monad that I build for yolc is a rather special case of LTL |
| 2025-05-08 08:49:53 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-05-08 08:50:58 +0200 | <haskellbridge> | <hellwolf> there is domain-specific benefit to linearly versioning data, namely to financial application security through this programming language safety, but I will skip here. |
| 2025-05-08 08:51:05 +0200 | <haskellbridge> | <hellwolf> alright. fin. |
| 2025-05-08 08:51:28 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 2025-05-08 08:52:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-05-08 08:53:24 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-05-08 08:54:45 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 2025-05-08 08:56:57 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 09:00:03 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-08 09:00:45 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-08 09:06:41 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-08 09:14:41 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 09:19:10 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-05-08 09:20:36 +0200 | Guest44 | (~Guest44@91-154-214-151.elisa-laajakaista.fi) |
| 2025-05-08 09:29:25 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-05-08 09:29:28 +0200 | YoungFrog | (~youngfrog@2a02:a03f:c9db:fc00:93c8:3aef:156:8fed) (Ping timeout: 272 seconds) |
| 2025-05-08 09:33:14 +0200 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog |
| 2025-05-08 09:34:42 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 09:36:00 +0200 | Frostillicus_1 | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 2025-05-08 09:43:45 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-05-08 09:44:43 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-05-08 09:56:37 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-05-08 09:56:43 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2025-05-08 10:07:33 +0200 | <tomsmeding> | hellwolf: haven't read further in your monologue here, but generating IDs for sharing recovery using template haskell is unsound |
| 2025-05-08 10:07:51 +0200 | <tomsmeding> | the same haskell term at the very same place in the diagram might produce distinct, non-unifiable nodes in the diagram |
| 2025-05-08 10:08:35 +0200 | <tomsmeding> | `let f = \x -> x + x in f a + f b` in haskell |
| 2025-05-08 10:09:05 +0200 | <tomsmeding> | a user can write that, and the resulting yolc diagram, lacking lambda, must have 3 separate (+) nodes, two of which are generated by the exact same (+) operation in the source file |
| 2025-05-08 10:09:49 +0200 | <tomsmeding> | the sharing that you can recover is not _lexical_ identity of the variables in question, but _runtime_ heap pointer identity |
| 2025-05-08 10:09:54 +0200 | <tomsmeding> | or something that approximates the latter |
| 2025-05-08 10:11:18 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-05-08 10:12:12 +0200 | <tomsmeding> | hellwolf: "m VarRef and every time you use it you get a duplication" sounds good, but how do you ensure the variable is dropped (as in `consume`) exactly once? Or is the linearity really _only_ for duplication detection and is it fine to duplicate too many times and drop some of the leftovers? |
| 2025-05-08 10:14:15 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-05-08 10:14:17 +0200 | Guest44 | (~Guest44@91-154-214-151.elisa-laajakaista.fi) (Quit: Client closed) |
| 2025-05-08 10:14:56 +0200 | <hellwolf> | yea, template haskell is unsound. I should read into your approach |
| 2025-05-08 10:15:27 +0200 | <hellwolf> | > but how do you ensure the variable is dropped |
| 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:29 +0200 | <lambdabot> | error: |
| 2025-05-08 10:15:29 +0200 | <lambdabot> | Unexpected do block in function application: |
| 2025-05-08 10:15:29 +0200 | <lambdabot> | do you ensure the variable is dropped |
| 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:16:16 +0200 | <tomsmeding> | there's no performance cost associated with duplication? |
| 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:56 +0200 | <hellwolf> | tomsmeding: yep, variable duplication is not a runtime thing! |
| 2025-05-08 10:17:04 +0200 | <tomsmeding> | then this works |
| 2025-05-08 10:17:13 +0200 | <hellwolf> | it's jsut for evaluator (the codegen most importantlh) |
| 2025-05-08 10:17:29 +0200 | <tomsmeding> | then I actually question whether you _need_ linear types for this |
| 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: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:18:24 +0200 | <tomsmeding> | no need for linear types to make sharing visible |
| 2025-05-08 10:18:41 +0200 | <hellwolf> | yea, linear-type is for "data freshness" |
| 2025-05-08 10:18:50 +0200 | tomsmeding | has no clue what that means |
| 2025-05-08 10:19:05 +0200 | <hellwolf> | yea, it's domain specific. let me see if I can explain |
| 2025-05-08 10:19:21 +0200 | <hellwolf> | so, say, you write such a program: |
| 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:20:17 +0200 | <hellwolf> | you then do something again, with the assumption that the balance of beforeBalanceA is still valid |
| 2025-05-08 10:20:26 +0200 | <tomsmeding> | that sounds like the versioning, not the linear types |
| 2025-05-08 10:20:29 +0200 | <hellwolf> | in a open financial API system, that creates a vulnerability |
| 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:53 +0200 | <hellwolf> | it's a type error if you use dated data |
| 2025-05-08 10:21:12 +0200 | <hellwolf> | there were millions lost due to this kind of bugs. |
| 2025-05-08 10:21:42 +0200 | <hellwolf> | can you enforce it in type safety in other means? |
| 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:59 +0200 | <hellwolf> | I am all ears. I am an engineer, so I am here just to assemble solutions. |
| 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:22:19 +0200 | <hellwolf> | bad habit. |
| 2025-05-08 10:22:22 +0200 | <tomsmeding> | :D |
| 2025-05-08 10:22:40 +0200 | Boarders_____ | (sid425905@id-425905.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-08 10:23:39 +0200 | <hellwolf> | but does that program example make sense? |
| 2025-05-08 10:23:50 +0200 | <tomsmeding> | yes it does |
| 2025-05-08 10:23:58 +0200 | tomsmeding | is looking at the LVM definition |
| 2025-05-08 10:24:14 +0200 | <hellwolf> | excuse moi, that's my own sh*t |
| 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:19 +0200 | <hellwolf> | here |
| 2025-05-08 10:24:24 +0200 | <tomsmeding> | yes I found it :) |
| 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:27:01 +0200 | <tomsmeding> | the input ctx, that is |
| 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:49 +0200 | <hellwolf> | not sure I would say ctx having a version, per se. |
| 2025-05-08 10:27:56 +0200 | <tomsmeding> | is there anything at version 'va'? |
| 2025-05-08 10:28:00 +0200 | <hellwolf> | it's more about what you can be bound with |
| 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:46 +0200 | <hellwolf> | (_ :: m ctx va vb a) >>= (_ :: a -> m ctx vb vc b) ? |
| 2025-05-08 10:29:07 +0200 | <hellwolf> | I would not see version independently, it's all about the >>= |
| 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:29 +0200 | <hellwolf> | corect |
| 2025-05-08 10:30:27 +0200 | <tomsmeding> | (it's spelled "referentiable", not "referenciable") |
| 2025-05-08 10:30:39 +0200 | <tomsmeding> | or perhaps "referrable" |
| 2025-05-08 10:31:05 +0200 | <hellwolf> | where did you see that? |
| 2025-05-08 10:31:10 +0200 | <tomsmeding> | LVMVar.hs |
| 2025-05-08 10:31:24 +0200 | <hellwolf> | okay, thanks, I will fix |
| 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: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:32:30 +0200 | <hellwolf> | let me show you, it's not obvious, if you only look at LVM definitinop |
| 2025-05-08 10:32:38 +0200 | <hellwolf> | since @a@ has no injectivty to @va@ |
| 2025-05-08 10:32:44 +0200 | <tomsmeding> | sure |
| 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: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:33:10 +0200 | <hellwolf> | data uses the "port api" from linear-smc library |
| 2025-05-08 10:33:13 +0200 | <hellwolf> | so all data are versioned |
| 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:39 +0200 | <tomsmeding> | hence me not yet understanding what va is used for |
| 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:34:04 +0200 | <hellwolf> | not all @a@ has to be |
| 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:24 +0200 | <tomsmeding> | sure |
| 2025-05-08 10:34:37 +0200 | <tomsmeding> | reads like klingon |
| 2025-05-08 10:35:16 +0200 | <hellwolf> | :) what I just said, or the code related to P? |
| 2025-05-08 10:35:22 +0200 | <tomsmeding> | "P'v v r a" |
| 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:36:03 +0200 | <hellwolf> | "P k r a" was the original API |
| 2025-05-08 10:36:24 +0200 | <hellwolf> | -- | Yul port with linearly versioned data, aka. versioned yul ports. |
| 2025-05-08 10:36:25 +0200 | <hellwolf> | type P'V v = P'x (VersionedPort v) |
| 2025-05-08 10:36:29 +0200 | <hellwolf> | -- | Yul port with the port effect kind, aka. yul ports. |
| 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:38:15 +0200 | <hellwolf> | the example actually shows such a data version type safety in action, is here: |
| 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:38 +0200 | <hellwolf> | if you swap the onTokenMinted and sputs |
| 2025-05-08 10:38:50 +0200 | <hellwolf> | you get a type error, because onTokenMinted might render data stale |
| 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:39:33 +0200 | <hellwolf> | *use |
| 2025-05-08 10:40:08 +0200 | <tomsmeding> | right, I see that an Rv indeed has a single 'v' version |
| 2025-05-08 10:40:23 +0200 | <tomsmeding> | and `sget` produces a computation with va=v and vb=v |
| 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:41:42 +0200 | <tomsmeding> | I may be wrong |
| 2025-05-08 10:41:59 +0200 | <hellwolf> | yep, happy to continue the discussion |
| 2025-05-08 10:42:06 +0200 | <hellwolf> | my hunch is you cannot do without linear types |
| 2025-05-08 10:42:15 +0200 | <hellwolf> | I dont' have a full theoretical survey about this problem |
| 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:30 +0200 | <hellwolf> | and I consider this a special case of LTL |
| 2025-05-08 10:42:32 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-08 10:42:49 +0200 | <hellwolf> | but I am not a theoretician by trade |
| 2025-05-08 10:42:53 +0200 | <tomsmeding> | me neither |
| 2025-05-08 10:43:29 +0200 | <hellwolf> | the thing without linearity on arrow is that |
| 2025-05-08 10:43:45 +0200 | <hellwolf> | you can copy a versioned data too freely without type system knowing |
| 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:44:03 +0200 | <tomsmeding> | but it will retain the same version, surely? |
| 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:19 +0200 | <hellwolf> | it is the same version |
| 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:29 +0200 | <hellwolf> | but then you can diverge from the same version to other course of actions |
| 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: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:45:18 +0200 | <tomsmeding> | can you "upgrade" the version of a variable? |
| 2025-05-08 10:45:25 +0200 | <hellwolf> | not safely |
| 2025-05-08 10:45:35 +0200 | <hellwolf> | there is unsafe api for building other safe API |
| 2025-05-08 10:45:38 +0200 | <tomsmeding> | then I still don't see the problem |
| 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:46:06 +0200 | <hellwolf> | think of diamond-shaped path |
| 2025-05-08 10:46:24 +0200 | <hellwolf> | va >>= vb in one monad, and va >>= vb in another monad |
| 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:42 +0200 | <tomsmeding> | oh I see |
| 2025-05-08 10:46:53 +0200 | <hellwolf> | only linearity on arrow can enforce that |
| 2025-05-08 10:47:08 +0200 | <tomsmeding> | because versions are actually natural numbers, and those have too much structure |
| 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:29 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds) |
| 2025-05-08 10:47:35 +0200 | <hellwolf> | are you familiar with LTL? |
| 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: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: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:36 +0200 | <tomsmeding> | but they aren't necessarily equal |
| 2025-05-08 10:48:52 +0200 | <hellwolf> | that's right |
| 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:49:14 +0200 | <hellwolf> | hmm, interesting |
| 2025-05-08 10:49:17 +0200 | <tomsmeding> | this is probably extremely awkward to encode in haskell |
| 2025-05-08 10:49:32 +0200 | <hellwolf> | which is awkward to encode? |
| 2025-05-08 10:49:38 +0200 | <hellwolf> | partial order in type? |
| 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:53 +0200 | <tomsmeding> | so you have RankNTypes EVERYWHERE |
| 2025-05-08 10:50:02 +0200 | <tomsmeding> | probably too much for ghc to cope with |
| 2025-05-08 10:50:08 +0200 | <hellwolf> | that's for library write to hid? |
| 2025-05-08 10:50:11 +0200 | <hellwolf> | oh :) |
| 2025-05-08 10:50:16 +0200 | <hellwolf> | I assume GHC is glorious |
| 2025-05-08 10:50:23 +0200 | <tomsmeding> | it is |
| 2025-05-08 10:50:35 +0200 | <tomsmeding> | % System.Process.system "ghc --version" |
| 2025-05-08 10:50:35 +0200 | <yahb2> | The Glorious Glasgow Haskell Compilation System, version 9.12.2 ; ExitSuccess |
| 2025-05-08 10:50:51 +0200 | <hellwolf> | % System.Procerss.systme "rm -rf /hahaha" |
| 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:51:13 +0200 | <tomsmeding> | you have write access only to a small tmpfs |
| 2025-05-08 10:51:31 +0200 | <hellwolf> | you thinki so, did it enforce it in the type system? |
| 2025-05-08 10:51:38 +0200 | <tomsmeding> | :) |
| 2025-05-08 10:51:55 +0200 | <tomsmeding> | https://git.tomsmeding.com/yahb2/tree/bwrap-files/start.sh |
| 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:52:19 +0200 | <hellwolf> | I have no time to write down everything yet. |
| 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:57:21 +0200 | <tomsmeding> | perhaps GHC is fine, I dunno |
| 2025-05-08 10:59:02 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 11:00:49 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-05-08 11:00:56 +0200 | yoneda | (~mike@193.206.102.122) |
| 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:02:51 +0200 | <tomsmeding> | you end up having to CPS all code to express what I described |
| 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:03:48 +0200 | <hellwolf> | your idea of the variable labeling? |
| 2025-05-08 11:03:56 +0200 | <hellwolf> | using unsafe io? |
| 2025-05-08 11:04:04 +0200 | <tomsmeding> | no, the "use (v, exists w. w) instead of (v, v+1)" |
| 2025-05-08 11:04:20 +0200 | <tomsmeding> | variable labeling is implemented successfully by accelerate |
| 2025-05-08 11:04:20 +0200 | <hellwolf> | ah, okay, I didn't fully understand 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: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:05:06 +0200 | <tomsmeding> | I'd like someone to use https://git.tomsmeding.com/sharing-recovery/about/ in anger :p |
| 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:06:52 +0200 | <tomsmeding> | (the core function there is sharingRecovery at the bottom of this file https://git.tomsmeding.com/sharing-recovery/tree/src/Data/Expr/SharingRecovery/Internal.hs#n454 ) |
| 2025-05-08 11:07:32 +0200 | <tomsmeding> | but in your case it may not solve anything because you require the linear types for versioning too |
| 2025-05-08 11:07:42 +0200 | <tomsmeding> | because my partial-order thing doesn't (easily?) work |
| 2025-05-08 11:08:26 +0200 | <hellwolf> | let me read your project: one-liner README :) |
| 2025-05-08 11:08:55 +0200 | <hellwolf> | | This is an attempt at implementing "Optimising Purely Functional GPU Programs" by McDonell et al. (ICFP 2013) in a generic fashion. |
| 2025-05-08 11:11:32 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 11:11:49 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 248 seconds) |
| 2025-05-08 11:13:13 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-05-08 11:13:21 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2025-05-08 11:13:25 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 2025-05-08 11:19:49 +0200 | rvalue- | rvalue |
| 2025-05-08 11:25:13 +0200 | <tomsmeding> | hellwolf: yeah only the sharing recovery part of it |
| 2025-05-08 11:25:38 +0200 | <tomsmeding> | the pitch is: https://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf does sharing recovery just fine, and it's implemented in https://hackage.haskell.org/package/data-reify |
| 2025-05-08 11:25:46 +0200 | <tomsmeding> | but the expression it creates is untyped |
| 2025-05-08 11:26:15 +0200 | <tomsmeding> | The McDonell et al paper presents an algorithm that does sharing recovery on an AST indexed by the type of the expression that it represents |
| 2025-05-08 11:28:34 +0200 | <hellwolf> | thanks, printed. will read to enrich my knowledge here. it seems relevant to what I do. |
| 2025-05-08 11:29:14 +0200 | <tomsmeding> | I find the presentation in the McDonell paper to be hard to understand personally |
| 2025-05-08 11:29:37 +0200 | <tomsmeding> | that's part of the reason I wanted to make an implementation: to then proceed to document that well so that it can serve as a better explanation for haskellers |
| 2025-05-08 11:29:43 +0200 | <tomsmeding> | but the documentation part never happened, lol |
| 2025-05-08 11:29:59 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 2025-05-08 11:32:46 +0200 | euleritian | (~euleritia@dynamic-176-006-143-223.176.6.pool.telefonica.de) |
| 2025-05-08 11:36:44 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) typedfern |
| 2025-05-08 11:37:28 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2025-05-08 11:38:17 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) typedfern |
| 2025-05-08 11:44:19 +0200 | <hellwolf> | :D code is better than paper? |
| 2025-05-08 11:45:31 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2025-05-08 11:46:11 +0200 | <Lears> | hellwolf: Not sure if this is helpful, but your `LVM` appears to be linear state transformed by the Atkey indexed writer monad: https://paste.tomsmeding.com/EOqwUoJZ |
| 2025-05-08 11:51:47 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-08 12:01:09 +0200 | <hellwolf> | Oh, I have never heard of the Atkey thing. |
| 2025-05-08 12:01:41 +0200 | <hellwolf> | It looks similar indeed. LVM itself is kinda trivial. It's good to know that there is a name for the general version of it. |
| 2025-05-08 12:02:01 +0200 | <hellwolf> | I was suspecting some sort of indexed monad, but I just didn't know what it's called. |
| 2025-05-08 12:05:52 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 12:06:59 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 12:07:45 +0200 | <hellwolf> | tom, do you think there is something in linear arrows to address the sharing issue? Although it might sound like "solving issue by not solving it", since the trade-off is the loosing the ergonomics of being able to copy variables however many times you wanted. |
| 2025-05-08 12:07:55 +0200 | <hellwolf> | "losign" |
| 2025-05-08 12:08:01 +0200 | <hellwolf> | *losing of |
| 2025-05-08 12:08:08 +0200 | <hellwolf> | darn it. typing in IRC is hard. |
| 2025-05-08 12:08:12 +0200 | <tomsmeding> | it is |
| 2025-05-08 12:08:14 +0200 | euleritian | (~euleritia@dynamic-176-006-143-223.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-08 12:08:33 +0200 | <hellwolf> | what it is? |
| 2025-05-08 12:08:42 +0200 | <tomsmeding> | typing is hard |
| 2025-05-08 12:08:48 +0200 | <hellwolf> | :) |
| 2025-05-08 12:09:03 +0200 | <tomsmeding> | well I think your solution works |
| 2025-05-08 12:09:34 +0200 | <tomsmeding> | separately I think that my suggestion doesn't work in normal haskell, because it requires the user to write CPS'ed code, which is in some ways even worse than the linear typing |
| 2025-05-08 12:10:03 +0200 | <tomsmeding> | I still feel there might be more ways to solve it besides yours |
| 2025-05-08 12:10:30 +0200 | <hellwolf> | oh, there must be. I'd be interested in dicussing these ideas, and convert them into engineering solutions. |
| 2025-05-08 12:10:45 +0200 | <hellwolf> | I am a packager of solutions :P |
| 2025-05-08 12:11:20 +0200 | <hellwolf> | good to hear that my general direction seems okay in expert's eyes. I need to really write them up. |
| 2025-05-08 12:11:35 +0200 | <tomsmeding> | "expert" |
| 2025-05-08 12:11:48 +0200 | <hellwolf> | relative monad wise |
| 2025-05-08 12:11:56 +0200 | <hellwolf> | I am a monad with no grade |
| 2025-05-08 12:12:31 +0200 | euleritian | (~euleritia@77.23.248.100) |
| 2025-05-08 12:13:40 +0200 | yin | (~z@user/zero) (Ping timeout: 244 seconds) |
| 2025-05-08 12:15:30 +0200 | yin | (~z@user/zero) zero |
| 2025-05-08 12:19:04 +0200 | <hellwolf> | Lears: I didn't see linear arrows used though? |
| 2025-05-08 12:19:19 +0200 | <hellwolf> | (>>=) seems having %Many |
| 2025-05-08 12:23:17 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 2025-05-08 12:23:28 +0200 | <Lears> | hellwolf: I didn't put any on the `Atkey` class, no, but you can slip them in if you need to. |
| 2025-05-08 12:23:50 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) (Quit: fp) |
| 2025-05-08 12:23:56 +0200 | Lears | Leary |
| 2025-05-08 12:25:31 +0200 | yin | (~z@user/zero) (Ping timeout: 252 seconds) |
| 2025-05-08 12:27:01 +0200 | yin | (~z@user/zero) zero |
| 2025-05-08 12:33:39 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-05-08 12:37:22 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-05-08 12:38:07 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds) |
| 2025-05-08 12:39:16 +0200 | <hellwolf> | > essentially you'd be building up a partial order of versions, instead of using the "too structured" natural numbers |
| 2025-05-08 12:39:16 +0200 | <hellwolf> | I thought about this again. I remembered in the literature it's called linear transition system (LTS), it's a graph, but you can unravel it and it becomes a tree. So it's more than the partial order here. |
| 2025-05-08 12:39:18 +0200 | <lambdabot> | <hint>:1:50: error: parse error on input ‘of’ |
| 2025-05-08 12:39:40 +0200 | <hellwolf> | that's what I want to encode in Haskell, perhaps in 2026 |
| 2025-05-08 12:40:07 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-08 12:40:29 +0200 | <hellwolf> | to me, if I were right about this, it's criminally underselling linear arrows of GHC. |
| 2025-05-08 12:40:59 +0200 | <hellwolf> | everyone talks about uniqueness typing, but I find that less interesting since most of the time people can argue that ST monad does it just fine. |
| 2025-05-08 12:41:24 +0200 | <hellwolf> | the linear-safety ergonomics loss is a turnoff to a lot of people |
| 2025-05-08 12:42:06 +0200 | <hellwolf> | you gotta provide something that you cannnot do otherwise. and I hope I am right here that LTL is an orthogonal use case of linear arrows in GHC. |
| 2025-05-08 12:42:34 +0200 | <hellwolf> | I will admit that I haven't even convinced or conveyed what I am doing to Arnauld :D |
| 2025-05-08 12:44:36 +0200 | yin | (~z@user/zero) (Ping timeout: 252 seconds) |
| 2025-05-08 12:44:47 +0200 | <JuanDaugherty> | i was speculating when i first heard of ML, if it coulda been in the '70s |
| 2025-05-08 12:45:11 +0200 | <JuanDaugherty> | it was 2 years b4 i wrote my first program |
| 2025-05-08 12:45:17 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-05-08 12:45:31 +0200 | yin | (~z@user/zero) zero |
| 2025-05-08 12:45:45 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-05-08 12:45:48 +0200 | <JuanDaugherty> | i didn realize how straight and well penciled the line was from ML to haskell and GHC |
| 2025-05-08 12:46:17 +0200 | <JuanDaugherty> | edinburgh and the milner and what not |
| 2025-05-08 12:46:25 +0200 | <JuanDaugherty> | s/the// |
| 2025-05-08 12:47:09 +0200 | <JuanDaugherty> | i.e. ML was 2 years, unclear when I first heard of it but b6 1980 |
| 2025-05-08 12:48:25 +0200 | <JuanDaugherty> | i thought the uni just glommed onto haskell and it originated in some amorphose global academic ML cloud |
| 2025-05-08 12:48:54 +0200 | <hellwolf> | with conclave and inaccessible cardinals? |
| 2025-05-08 12:49:07 +0200 | <hellwolf> | (stealing this joke from functional cafe.) |
| 2025-05-08 12:49:09 +0200 | <JuanDaugherty> | dont forget the smoke |
| 2025-05-08 12:50:10 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-05-08 12:50:40 +0200 | <JuanDaugherty> | *b4 1980 |
| 2025-05-08 12:51:26 +0200 | <JuanDaugherty> | i didn think it (ML) actually did useful, non theoretical programming |
| 2025-05-08 12:51:54 +0200 | zzz | (~z@user/zero) zero |
| 2025-05-08 12:52:11 +0200 | <hellwolf> | does it now? |
| 2025-05-08 12:52:27 +0200 | <JuanDaugherty> | which misimpression wasn dispelled until hs started getting real |
| 2025-05-08 12:52:33 +0200 | yin | (~z@user/zero) (Read error: Connection reset by peer) |
| 2025-05-08 12:52:33 +0200 | zzz | yin |
| 2025-05-08 12:53:07 +0200 | <JuanDaugherty> | c. '06 for me; yes i now realize ML always did have that property i thought it didn |
| 2025-05-08 12:53:16 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 276 seconds) |
| 2025-05-08 12:54:15 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2025-05-08 12:54:48 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-08 12:55:02 +0200 | <JuanDaugherty> | or rather i've been aware of it for some time |
| 2025-05-08 12:55:06 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-05-08 12:57:30 +0200 | <JuanDaugherty> | something like that must be how the typical programming IT worker of today views hs except that now know u can do stuff |
| 2025-05-08 12:57:53 +0200 | <JuanDaugherty> | *now they/u know |
| 2025-05-08 12:58:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-05-08 12:58:08 +0200 | <JuanDaugherty> | but it's still "what is this shit?" |
| 2025-05-08 12:59:19 +0200 | <hellwolf> | turing-complete machine is such an amazing beast. |
| 2025-05-08 12:59:28 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-05-08 12:59:42 +0200 | <hellwolf> | you can ask it to do whatever it can, so long it has the access to the external world, including launching a missle |
| 2025-05-08 13:00:00 +0200 | <hellwolf> | *missile |
| 2025-05-08 13:00:04 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-08 13:00:06 +0200 | <JuanDaugherty> | can u? |
| 2025-05-08 13:00:32 +0200 | <JuanDaugherty> | is there some stunning copilot or llm stuffs with hs i dont know about? |
| 2025-05-08 13:00:44 +0200 | <hellwolf> | that makes people who work on it, self-labeled programmers, think they are powerful. |
| 2025-05-08 13:01:06 +0200 | <darkling> | hellwolf: Missal? Are we back to the inaccessible cardinals again? |
| 2025-05-08 13:01:11 +0200 | <JuanDaugherty> | well no, that's not required |
| 2025-05-08 13:01:19 +0200 | <hellwolf> | But, we FP people is looking for a different relation with the machine: how can we be told by math to do the right thing using the machien? |
| 2025-05-08 13:01:27 +0200 | <JuanDaugherty> | they dont have to understand the code to use it |
| 2025-05-08 13:01:44 +0200 | <hellwolf> | I think that's the crust why many don't understand FP's appeal |
| 2025-05-08 13:01:45 +0200 | <JuanDaugherty> | u FP ppl |
| 2025-05-08 13:01:46 +0200 | jespada | (~jespada@179.26.249.228) jespada |
| 2025-05-08 13:02:01 +0200 | <hellwolf> | if all your end goal is to tell machine to do whatever you want it to do, then yes, it's pointless. |
| 2025-05-08 13:02:08 +0200 | <hellwolf> | But we pursue a different goal. |
| 2025-05-08 13:02:18 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-08 13:02:27 +0200 | <JuanDaugherty> | somebody said something was point free |
| 2025-05-08 13:03:11 +0200 | <JuanDaugherty> | and yes, with computers, that's all my end goal is |
| 2025-05-08 13:03:17 +0200 | yin | (~z@user/zero) (Ping timeout: 248 seconds) |
| 2025-05-08 13:03:18 +0200 | <hellwolf> | we serve a different god here, end of conversation; that's my solution to people who is obsessed with satanic ritual of beating machines into submission. |
| 2025-05-08 13:03:27 +0200 | <JuanDaugherty> | god fart |
| 2025-05-08 13:03:32 +0200 | <JuanDaugherty> | u lose |
| 2025-05-08 13:04:06 +0200 | <hellwolf> | :) |
| 2025-05-08 13:04:11 +0200 | hellwolf | duck and continue coding |
| 2025-05-08 13:04:19 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 2025-05-08 13:05:24 +0200 | <JuanDaugherty> | unless i'm mistaken something should be forthcoming to fill that role (nlp - hs relation) |
| 2025-05-08 13:07:16 +0200 | <JuanDaugherty> | which if it does will be monstrous irony if ppl that cant understand hs code can crank out programs in it, prodigyously with the circle jerk |
| 2025-05-08 13:07:43 +0200 | <JuanDaugherty> | *prodigously |
| 2025-05-08 13:08:54 +0200 | <hellwolf> | I was monologueing, sorry, I didn't target anyone personally. I am speaking to strawmen I saw on X social. |
| 2025-05-08 13:09:05 +0200 | <hellwolf> | didn't want to engage there, so I rant in IRC. |
| 2025-05-08 13:09:11 +0200 | <JuanDaugherty> | well carry on |
| 2025-05-08 13:10:00 +0200 | <hellwolf> | it's alright, I am going too far already bringing out the metaphysical aspects of people. |
| 2025-05-08 13:10:18 +0200 | <hellwolf> | but sometimes, to me, that's the only relevant part to end a conversation. |
| 2025-05-08 13:10:36 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 13:10:40 +0200 | <JuanDaugherty> | *without the circle jerk |
| 2025-05-08 13:10:47 +0200 | <hellwolf> | even as a rationalist, I find it simply a impossible conversation to continue with people refuse rational thinking. |
| 2025-05-08 13:11:14 +0200 | hellwolf | duck for real. have a good day gents. |
| 2025-05-08 13:11:17 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 248 seconds) |
| 2025-05-08 13:11:49 +0200 | <JuanDaugherty> | u'd be surprised how far the refusal reaches |
| 2025-05-08 13:12:53 +0200 | yin | (~z@user/zero) zero |
| 2025-05-08 13:15:22 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-05-08 13:24:51 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-05-08 13:26:41 +0200 | kh0d | (~kh0d@89.216.103.150) |
| 2025-05-08 13:30:38 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-05-08 13:30:54 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-05-08 13:31:05 +0200 | xff0x | (~xff0x@2405:6580:b080:900:df43:4d2b:b873:7ac7) |
| 2025-05-08 13:33:46 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 13:33:57 +0200 | j1n37- | (~j1n37@user/j1n37) (Quit: Ich bin der Welt abhanden gekommen) |
| 2025-05-08 13:34:13 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 13:38:32 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-08 13:42:12 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 13:44:31 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-08 13:47:15 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-08 13:49:08 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 265 seconds) |
| 2025-05-08 13:52:30 +0200 | JuanDaugherty | ColinRobinson |
| 2025-05-08 14:09:12 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
| 2025-05-08 14:09:54 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-05-08 14:19:38 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-05-08 14:23:43 +0200 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-08 14:38:44 +0200 | <haskellbridge> | <hellwolf> lunch break thought, to tom: my hunch is that to build more general LTL, my hunch is to a type-level CPS style ish thing to enforce state transition in types. I might hit unsaturated type family limitation, which I could work around with newtype wrapper. Or, hopefully in 2026 int-e had it finished :p |
| 2025-05-08 14:40:37 +0200 | kuribas | (~user@ptr-17d51em669ysrfo60ou.18120a2.ip6.access.telenet.be) kuribas |
| 2025-05-08 14:43:51 +0200 | Digitteknohippie | (~user@69.47.7.51.dyn.plus.net) |
| 2025-05-08 14:44:07 +0200 | Digit | (~user@69.47.7.51.dyn.plus.net) (Ping timeout: 252 seconds) |
| 2025-05-08 14:49:33 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-05-08 14:49:41 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-05-08 14:49:47 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-08 15:06:51 +0200 | kh0d | (~kh0d@89.216.103.150) (Quit: Leaving...) |
| 2025-05-08 15:08:29 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-05-08 15:08:33 +0200 | euleritian | (~euleritia@77.23.248.100) (Remote host closed the connection) |
| 2025-05-08 15:08:49 +0200 | <int-e> | hellwolf: dym int-index maybe (it's certainly not me) |
| 2025-05-08 15:08:51 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 2025-05-08 15:09:26 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-05-08 15:10:08 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 2025-05-08 15:12:47 +0200 | segfaultfizzbuzz | (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Remote host closed the connection) |
| 2025-05-08 15:13:21 +0200 | atwm | (~andrew@19-193-28-81.ftth.cust.kwaoo.net) (Quit: WeeChat 4.6.1) |
| 2025-05-08 15:13:29 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-05-08 15:25:56 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 15:35:24 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 2025-05-08 15:37:06 +0200 | euleritian | (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) |
| 2025-05-08 15:38:03 +0200 | euleritian | (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-08 15:38:21 +0200 | euleritian | (~euleritia@77.23.248.100) |
| 2025-05-08 15:39:03 +0200 | ystael | (~ystael@user/ystael) ystael |
| 2025-05-08 15:39:17 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 15:53:17 +0200 | stef204 | (~stef204@user/stef204) stef204 |
| 2025-05-08 15:57:44 +0200 | prasad | (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) (Remote host closed the connection) |
| 2025-05-08 16:06:00 +0200 | euleritian | (~euleritia@77.23.248.100) (Remote host closed the connection) |
| 2025-05-08 16:06:18 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 2025-05-08 16:06:25 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Quit: leaving) |
| 2025-05-08 16:09:22 +0200 | <hellwolf> | oh, iIsomehow thought it was you :) |
| 2025-05-08 16:20:00 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2025-05-08 16:20:46 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) |
| 2025-05-08 16:21:00 +0200 | euleritian | (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) |
| 2025-05-08 16:33:44 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-05-08 16:35:05 +0200 | euleritian | (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) (Ping timeout: 272 seconds) |
| 2025-05-08 16:36:15 +0200 | euleritian | (~euleritia@dynamic-176-006-145-187.176.6.pool.telefonica.de) |
| 2025-05-08 16:37:30 +0200 | Sgeo_ | (~Sgeo@user/sgeo) Sgeo |
| 2025-05-08 16:41:18 +0200 | Sgeo | (~Sgeo@user/sgeo) (Ping timeout: 244 seconds) |
| 2025-05-08 16:41:24 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 2025-05-08 16:42:15 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 16:45:41 +0200 | OftenFaded | (~OftenFade@user/tisktisk) (Quit: OftenFaded) |
| 2025-05-08 16:46:32 +0200 | wbrawner | (~wbrawner@static.205.41.78.5.clients.your-server.de) (Remote host closed the connection) |
| 2025-05-08 17:00:53 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) sprout |
| 2025-05-08 17:05:28 +0200 | troydm | (~troydm@user/troydm) (Ping timeout: 276 seconds) |
| 2025-05-08 17:08:07 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 17:09:07 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Client Quit) |
| 2025-05-08 17:11:56 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 17:15:16 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-08 17:15:48 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-08 17:20:09 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-05-08 17:21:03 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2025-05-08 17:46:49 +0200 | volsand | (~volsand@2804:1b1:1080:da6:dcbd:80c:8e7b:1cf7) |
| 2025-05-08 17:49:09 +0200 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 248 seconds) |
| 2025-05-08 17:49:21 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-05-08 17:50:12 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: "Inté pros bão que junto a gente fica mió") |
| 2025-05-08 17:50:12 +0200 | prasad | (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 2025-05-08 17:50:36 +0200 | kuribas | (~user@ptr-17d51em669ysrfo60ou.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2025-05-08 17:50:50 +0200 | kuribas | (~user@ptr-17d51eo8yjf3h7nzszs.18120a2.ip6.access.telenet.be) kuribas |
| 2025-05-08 17:50:59 +0200 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) tessier |
| 2025-05-08 17:52:54 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-08 17:57:20 +0200 | Guest65 | (~Guest54@117.107.131.196) |
| 2025-05-08 17:59:32 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 18:00:59 +0200 | Guest65 | (~Guest54@117.107.131.196) (Client Quit) |
| 2025-05-08 18:04:39 +0200 | arahael | (~arahael@user/arahael) (Read error: Connection reset by peer) |
| 2025-05-08 18:05:22 +0200 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-05-08 18:06:00 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-05-08 18:09:04 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Error from remote client) |
| 2025-05-08 18:12:33 +0200 | jespada_ | (~jespada@r167-61-122-127.dialup.adsl.anteldata.net.uy) jespada |
| 2025-05-08 18:15:23 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) ft |
| 2025-05-08 18:15:45 +0200 | jespada | (~jespada@179.26.249.228) (Ping timeout: 276 seconds) |
| 2025-05-08 18:18:25 +0200 | mari-estel | (~mari-este@user/mari-estel) (Ping timeout: 248 seconds) |
| 2025-05-08 18:19:52 +0200 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-05-08 18:20:01 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 2025-05-08 18:21:20 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-05-08 18:21:53 +0200 | mari-estel | (~mari-este@user/mari-estel) (Remote host closed the connection) |
| 2025-05-08 18:28:37 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f49a8c9e3402b4ffa7d.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-05-08 18:38:26 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-08 18:39:42 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-05-08 18:40:11 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 18:42:48 +0200 | <tomsmeding> | hellwolf: mention my full nick, I don't have highlight on just 'tom' (too many toms) |
| 2025-05-08 18:43:08 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 18:43:18 +0200 | <tomsmeding> | and there's too much blather here to diligently read scrollback for me :) |
| 2025-05-08 18:44:18 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-05-08 18:45:02 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-05-08 18:49:42 +0200 | milan | (~milan@88.212.61.169) |
| 2025-05-08 18:54:07 +0200 | <hellwolf> | I didn't want to tag you |
| 2025-05-08 18:54:19 +0200 | <hellwolf> | but I will, if you don't mind |
| 2025-05-08 18:55:02 +0200 | <tomsmeding> | if you want me to read something, tag me; if you want me to miss it, don't tag me :p |
| 2025-05-08 18:55:25 +0200 | <tomsmeding> | there's no guarantee I'll read something if you tag me, because my bouncer retains only a history of 500 (I think?) messages per channel when I'm offline |
| 2025-05-08 18:55:37 +0200 | <Rembane> | Schrödinger's tomsmeding! |
| 2025-05-08 18:55:38 +0200 | <tomsmeding> | and sometimes I don't open irc over a weekend or so |
| 2025-05-08 18:55:40 +0200 | <tomsmeding> | yes |
| 2025-05-08 19:02:33 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 19:06:33 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-05-08 19:06:57 +0200 | <tomsmeding> | recently monochrom replied to a message from me where I didn't even mention anyone, that was more than two screens up at that point -- in -offtopic |
| 2025-05-08 19:07:06 +0200 | <tomsmeding> | I don't do that level of scrollback reading, apologies |
| 2025-05-08 19:07:31 +0200 | yoneda | (~mike@193.206.102.122) (Quit: leaving) |
| 2025-05-08 19:09:45 +0200 | <hellwolf> | :) |
| 2025-05-08 19:09:59 +0200 | <hellwolf> | we can move some detailed discuss DM too, when there is more sustance |
| 2025-05-08 19:12:03 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-05-08 19:19:39 +0200 | sprotte24 | (~sprotte24@p200300d16f4546009040e212dd81e9a6.dip0.t-ipconnect.de) |
| 2025-05-08 19:20:40 +0200 | euleritian | (~euleritia@dynamic-176-006-145-187.176.6.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 2025-05-08 19:22:59 +0200 | <tomsmeding> | hellwolf: a sketch of how you can do versioning with CPS-style code https://paste.tomsmeding.com/Fu4HP0Sh |
| 2025-05-08 19:23:15 +0200 | <tomsmeding> | I _think_ this is a safe API, but I'm not 100% sure |
| 2025-05-08 19:23:28 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 2025-05-08 19:23:49 +0200 | <tomsmeding> | "safe" as in: cannot have "diverging histories", as you've described, nor can you arrange to use a Ref after a Port operation |
| 2025-05-08 19:24:38 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 19:24:47 +0200 | sajenim | (~sajenim@user/sajenim) (Ping timeout: 244 seconds) |
| 2025-05-08 19:25:26 +0200 | <EvanR> | yeah there's just way too much traffic in this channel |
| 2025-05-08 19:25:39 +0200 | <EvanR> | 🦗 |
| 2025-05-08 19:26:32 +0200 | <hellwolf> | tomsmeding: what does Fr mean here? |
| 2025-05-08 19:26:40 +0200 | <tomsmeding> | "fresh" |
| 2025-05-08 19:26:46 +0200 | <hellwolf> | :) |
| 2025-05-08 19:27:02 +0200 | <tomsmeding> | I was going to call it "FM" for "fresh monad", but it's not a monad -- in fact, the whole _point_ is that it's not a monad |
| 2025-05-08 19:27:13 +0200 | <hellwolf> | Ur, Uv, Rv, Fr, the two-lettered family of spells |
| 2025-05-08 19:28:08 +0200 | <hellwolf> | fwiw, I have the VersionThread API, without monad; but that also requires linear arrows |
| 2025-05-08 19:28:18 +0200 | <hellwolf> | (let me read into your Fr more...) |
| 2025-05-08 19:28:48 +0200 | <tomsmeding> | the idea of Fr is that every operation requires you to proceed in a callback |
| 2025-05-08 19:29:15 +0200 | <tomsmeding> | the Ref operations are written in more usual monadic style but I realise now that that's pointless, because Fr is not a monad |
| 2025-05-08 19:29:36 +0200 | <tomsmeding> | so you should consider the compositions with 'cps' to be the actual Ref operations, as used in MainCPS |
| 2025-05-08 19:29:49 +0200 | <tomsmeding> | hence you automatically get a linear sequence of operations |
| 2025-05-08 19:30:15 +0200 | <tomsmeding> | side-effectfulness of an operation is indicated by freshening the v variable in the continuation; the freshened version is called 'w' in the Port operations |
| 2025-05-08 19:30:48 +0200 | <hellwolf> | but I surely can use the same monad a few times, without linear arrows? |
| 2025-05-08 19:30:54 +0200 | <hellwolf> | would that introduce unsoundness |
| 2025-05-08 19:31:09 +0200 | <tomsmeding> | I think you have to use the 'cps' function to do that, right? |
| 2025-05-08 19:31:18 +0200 | <tomsmeding> | so 'cps' should indeed not be exported |
| 2025-05-08 19:32:05 +0200 | <tomsmeding> | hellwolf: can you do it without 'cps'? |
| 2025-05-08 19:32:23 +0200 | <tomsmeding> | assuming that the Ref functions are rewritten to have 'cps' baked-in; currently doing that |
| 2025-05-08 19:33:16 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 2025-05-08 19:33:27 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) manwithluck |
| 2025-05-08 19:33:41 +0200 | <tomsmeding> | hellwolf: fixed version https://paste.tomsmeding.com/CFVMMNbL |
| 2025-05-08 19:33:44 +0200 | <hellwolf> | I am not follow fully yet, since cps returns Fr with the same "v" |
| 2025-05-08 19:33:53 +0200 | <tomsmeding> | yes ignore cps, it's gone in the fixed version |
| 2025-05-08 19:34:03 +0200 | <tomsmeding> | oh the comment is still there, ignore the comment too :p |
| 2025-05-08 19:34:17 +0200 | <tomsmeding> | (the comment on line 27 in the fixed version) |
| 2025-05-08 19:35:37 +0200 | <tomsmeding> | I wonder whether a Port also needs a version index |
| 2025-05-08 19:36:37 +0200 | <hellwolf> | my hunch is that you might need, but I haven't tried to break your code yet. |
| 2025-05-08 19:36:48 +0200 | <hellwolf> | I mean break the intended "correctness protection" |
| 2025-05-08 19:36:51 +0200 | <tomsmeding> | yes |
| 2025-05-08 19:37:03 +0200 | <tomsmeding> | I assumed here that you can continue using Ports even after the version changed |
| 2025-05-08 19:37:25 +0200 | <tomsmeding> | if you can't then they just get a version index just like Ref, but this case is more interesting |
| 2025-05-08 19:38:27 +0200 | <hellwolf> | (forall w. Port a %? -> Fr w r) |
| 2025-05-08 19:38:39 +0200 | <tomsmeding> | no linear arrows here |
| 2025-05-08 19:38:47 +0200 | <hellwolf> | without the multiplicity, you can use it anytime, just need to check if that introduces problem |
| 2025-05-08 19:38:49 +0200 | <tomsmeding> | this does not at all address sharing |
| 2025-05-08 19:38:55 +0200 | <tomsmeding> | sharing is orthogonal to the versioning issue |
| 2025-05-08 19:39:08 +0200 | <hellwolf> | okay, that's an observation I need to digest a little. |
| 2025-05-08 19:39:26 +0200 | <tomsmeding> | as in, sharing recovery to prevent duplicate computation or duplicate side-effects |
| 2025-05-08 19:39:45 +0200 | <tomsmeding> | this particular encoding is only suitable for interpreting directly, not for compilation |
| 2025-05-08 19:40:01 +0200 | <tomsmeding> | the point of the design is that as long as you descend deeper and deeper in the chain of callbacks, you can never run Fr code in an "older" version, because you have to return something in a fresh 'Fr w' |
| 2025-05-08 19:40:15 +0200 | <hellwolf> | I get that. |
| 2025-05-08 19:40:25 +0200 | <tomsmeding> | the only way to do something in an "older version" would be to do something _after_ a callback returned, because you are "back" in the older version then |
| 2025-05-08 19:40:39 +0200 | <tomsmeding> | but the API doesn't ever let you do something "after" a Fr operation |
| 2025-05-08 19:40:44 +0200 | <tomsmeding> | there's no (>>=) |
| 2025-05-08 19:40:45 +0200 | <hellwolf> | and you do not expose the "cps" starter which you can use to cheat |
| 2025-05-08 19:40:53 +0200 | <tomsmeding> | yes |
| 2025-05-08 19:41:03 +0200 | <tomsmeding> | I'm actually not completely sure the 'cps' function was broken |
| 2025-05-08 19:41:27 +0200 | <tomsmeding> | with the current setup it would be because you can create a Port later, return it back, and then do stuff with it in an earlier version |
| 2025-05-08 19:41:33 +0200 | <tomsmeding> | which, if not unsound, is certainly strange |
| 2025-05-08 19:42:10 +0200 | <tomsmeding> | but even that could potentially be fixed by indexing Port with a "minimum version" it needs to run in, and then in addition to generating fresh w's each time, generate some magic type class evidence that the new w is "greater" than the old v |
| 2025-05-08 19:42:28 +0200 | <tomsmeding> | but without the 'cps' function, that worry should, hopefully, not exist |
| 2025-05-08 19:43:32 +0200 | <tomsmeding> | as you can see in 'main', the code is awkward CPS-style |
| 2025-05-08 19:43:42 +0200 | <hellwolf> | cps and Cont monad is the same thing, if you try, right? |
| 2025-05-08 19:43:45 +0200 | <tomsmeding> | but the point of this experiment is that it's very low-tech |
| 2025-05-08 19:43:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-05-08 19:43:52 +0200 | <tomsmeding> | eh |
| 2025-05-08 19:44:01 +0200 | <tomsmeding> | the 'cps' function was awfully named |
| 2025-05-08 19:44:14 +0200 | <tomsmeding> | continuation-passing style is the kind of code that you see in MainCPS |
| 2025-05-08 19:44:35 +0200 | <tomsmeding> | Cont is a monad that runs everything in CPS |
| 2025-05-08 19:44:37 +0200 | <tomsmeding> | @src ContT |
| 2025-05-08 19:44:37 +0200 | <lambdabot> | newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r } |
| 2025-05-08 19:45:02 +0200 | <tomsmeding> | a computation that produces an 'a' is a function that, given a _continuation_ taking an 'a', runs that continuation |
| 2025-05-08 19:45:07 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 19:45:19 +0200 | <hellwolf> | 05-08 20:43 <tomsmeding> but the point of this experiment is that it's very low-tech |
| 2025-05-08 19:45:19 +0200 | <hellwolf> | I understand. I think your observation of its orthogonality to the solving sharing with linear arrows is interesting. Since if all we need is data versioning, cps style can work, without all the machinery I have built. |
| 2025-05-08 19:45:20 +0200 | <tomsmeding> | but Cont(T) assumes that that 'm' doesn't change, and we want it to change |
| 2025-05-08 19:45:24 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 2025-05-08 19:45:31 +0200 | <tomsmeding> | right |
| 2025-05-08 19:45:38 +0200 | <hellwolf> | tomsmeding:sure, but I had to change standard monad too |
| 2025-05-08 19:45:44 +0200 | <hellwolf> | "graded Cont" |
| 2025-05-08 19:45:49 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) manwithluck |
| 2025-05-08 19:45:55 +0200 | <hellwolf> | just don't pronounce that in front of a brit. |
| 2025-05-08 19:46:07 +0200 | <tomsmeding> | I tried to do this kind of versioning in a monad style but I couldn't, not without linear types |
| 2025-05-08 19:46:12 +0200 | <tomsmeding> | doesn't mean that it can't be done |
| 2025-05-08 19:46:26 +0200 | <tomsmeding> | but I think this Fr thing, outside of a monad, does work |
| 2025-05-08 19:46:41 +0200 | <hellwolf> | I havent' found a hole yet |
| 2025-05-08 19:46:44 +0200 | <tomsmeding> | yay |
| 2025-05-08 19:46:47 +0200 | <hellwolf> | I might get back to you after I finish the code gen. |
| 2025-05-08 19:46:51 +0200 | <hellwolf> | and look this again |
| 2025-05-08 19:47:05 +0200 | <hellwolf> | If I were to write an article, I need to be a little bit complete and surveying around. |
| 2025-05-08 19:47:07 +0200 | <hellwolf> | this is a good one. |
| 2025-05-08 19:47:37 +0200 | <tomsmeding> | this stuff is dangerous for my phd thesis, by the way, because messing around with fun FP stuff is more fun than writing |
| 2025-05-08 19:48:00 +0200 | <hellwolf> | :D .... 5 years then panic |
| 2025-05-08 19:48:05 +0200 | <hellwolf> | before that all dandy |
| 2025-05-08 19:48:48 +0200 | <hellwolf> | but what's your phd is about, not FP?! |
| 2025-05-08 19:49:36 +0200 | <tomsmeding> | also FP but writing a literature overview is unfun |
| 2025-05-08 19:50:03 +0200 | <tomsmeding> | https://arxiv.org/pdf/2207.03418 https://dl.acm.org/doi/pdf/10.1145/3632878 |
| 2025-05-08 19:50:28 +0200 | <tomsmeding> | "applied FP"? |
| 2025-05-08 19:50:31 +0200 | <tomsmeding> | if that's a thing |
| 2025-05-08 19:50:51 +0200 | <tomsmeding> | still fairly theoretical, and there's a bit of FP fun in there too, but not as fundamental as this |
| 2025-05-08 19:50:55 +0200 | <int-e> | . o O ( https://arxiv.org/abs/2207.03418 ) |
| 2025-05-08 19:51:20 +0200 | <tomsmeding> | int-e: what do you get from the /abs/ page? |
| 2025-05-08 19:51:33 +0200 | <int-e> | tomsmeding: the title, abstract and meta information |
| 2025-05-08 19:51:46 +0200 | <tomsmeding> | I guess the metadata is useful, yes |
| 2025-05-08 19:51:59 +0200 | <hellwolf> | efficient chad... I can run a crypto scam meme coin with this title. |
| 2025-05-08 19:52:06 +0200 | <tomsmeding> | :D |
| 2025-05-08 19:52:06 +0200 | <EvanR> | differentiates most of haskell 98. So haskell 98 is differentiable, i.e. pretty smooth |
| 2025-05-08 19:52:17 +0200 | <tomsmeding> | EvanR: the one does not imply the other |
| 2025-05-08 19:52:36 +0200 | <EvanR> | pretty smooth as in "I'm pretty sure..." |
| 2025-05-08 19:52:51 +0200 | <tomsmeding> | in the sense of AD, I can differentiate a function Int -> Int just fine: its derivative is trivial, () -> () |
| 2025-05-08 19:52:58 +0200 | <tomsmeding> | because Int is discrete :) |
| 2025-05-08 19:53:15 +0200 | <EvanR> | ok makes sense |
| 2025-05-08 19:56:29 +0200 | <tomsmeding> | EvanR: damn, I should have replied "but not as smooth as CHAD" |
| 2025-05-08 19:56:59 +0200 | <EvanR> | CHAD |
| 2025-05-08 19:57:05 +0200 | <EvanR> | EXPLAIN |
| 2025-05-08 19:57:14 +0200 | <tomsmeding> | combinatory homomorphic automatic differentiation |
| 2025-05-08 19:57:21 +0200 | <tomsmeding> | except that there aren't even any combinators any more |
| 2025-05-08 19:58:00 +0200 | <EvanR> | so you're saying it's not even combinatory, or differentiation |
| 2025-05-08 19:58:18 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-05-08 19:58:19 +0200 | <EvanR> | HA |
| 2025-05-08 19:58:19 +0200 | <tomsmeding> | there's definitely a big homomorphism, and it's definitely automatic differentiation |
| 2025-05-08 19:58:19 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 2025-05-08 19:58:23 +0200 | <tomsmeding> | but we did away with the combinators |
| 2025-05-08 19:58:27 +0200 | <tomsmeding> | it HAD combinators |
| 2025-05-08 19:58:35 +0200 | <EvanR> | HAD |
| 2025-05-08 19:58:41 +0200 | <EvanR> | good one |
| 2025-05-08 19:58:47 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 2025-05-08 19:59:07 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) manwithluck |
| 2025-05-08 19:59:34 +0200 | <EvanR> | you could called it HAD combinators |
| 2025-05-08 19:59:43 +0200 | <tomsmeding> | wouldn't sell as well, though |
| 2025-05-08 19:59:46 +0200 | <EvanR> | lol |
| 2025-05-08 20:00:06 +0200 | <tomsmeding> | the combinators were unreadable |
| 2025-05-08 20:00:20 +0200 | <EvanR> | that's why it's past tense |
| 2025-05-08 20:00:27 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 20:00:59 +0200 | <tomsmeding> | https://arxiv.org/pdf/2103.15776v2 section 9.2, the typesetting/layout doesn't help |
| 2025-05-08 20:01:30 +0200 | <tomsmeding> | it's on the lambda calculus now if you look at later versions |
| 2025-05-08 20:01:54 +0200 | <tomsmeding> | the neatest presentation of the code transformation, IMO, is in https://dl.acm.org/doi/pdf/10.1145/3632878 figure 2 |
| 2025-05-08 20:02:35 +0200 | <tomsmeding> | if you have layout suggestions for that D[case] equation, I'm all ears |
| 2025-05-08 20:02:43 +0200 | <tomsmeding> | this multi-line left-hand side is just awful |