| 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 |
| 2025-05-08 20:09:08 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 20:09:50 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-08 20:10:34 +0200 | Digitteknohippie | Digit |
| 2025-05-08 20:10:39 +0200 | kuribas | (~user@ptr-17d51eo8yjf3h7nzszs.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2025-05-08 20:12:08 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 2025-05-08 20:12:56 +0200 | <hellwolf> | if I may get back to the Fr topic, I think there is still a hole, since you can have a port-based API using the same Port multiple times within the same cps callback, and that port API also returns a Fr, which Fr is correct to return? |
| 2025-05-08 20:13:05 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) |
| 2025-05-08 20:13:15 +0200 | <hellwolf> | there is not an extensive set of API, hard for me to think of all cases. |
| 2025-05-08 20:13:23 +0200 | <hellwolf> | but I am following some hunch |
| 2025-05-08 20:13:47 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 20:15:53 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 20:18:51 +0200 | <hellwolf> | simplest API: write to a "storage" location multiple times with (+ 1) |
| 2025-05-08 20:19:14 +0200 | <hellwolf> | which also returns the value, which one do you return? |
| 2025-05-08 20:19:59 +0200 | <hellwolf> | pardon me, if I brain farted. I am multitasking :/ |
| 2025-05-08 20:21:15 +0200 | Guest48 | (~Guest48@104.156.111.174) |
| 2025-05-08 20:21:54 +0200 | <tomsmeding> | hellwolf: if you write to a Port multiple times, you do that in successive callbacks, and the returned r is still from the innermost level where there is necessarily a 'finish' |
| 2025-05-08 20:22:11 +0200 | <tomsmeding> | because that's the only function that produces a Fr without taking yet another callback |
| 2025-05-08 20:23:52 +0200 | <tomsmeding> | notice that all functions (except 'finish') return precisely what their callback returns |
| 2025-05-08 20:23:56 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 2025-05-08 20:24:04 +0200 | <hellwolf> | yea. hence the ergonomics of $ \x -> |
| 2025-05-08 20:24:23 +0200 | <hellwolf> | vs. the infamous linear-types "& \x ->" chains |
| 2025-05-08 20:24:33 +0200 | <hellwolf> | with a symbol difference. |
| 2025-05-08 20:24:49 +0200 | <tomsmeding> | right |
| 2025-05-08 20:24:51 +0200 | <hellwolf> | maybe there is some interesting duo/correspondance there. |
| 2025-05-08 20:25:01 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-05-08 20:26:12 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) |
| 2025-05-08 20:26:35 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 2025-05-08 20:29:55 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 20:34:10 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-05-08 20:34:23 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f49f4d0e34d1c0f8686.dip0.t-ipconnect.de) acidjnk |
| 2025-05-08 20:37:24 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-05-08 20:40:32 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 2025-05-08 20:40:57 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) manwithluck |
| 2025-05-08 20:44:02 +0200 | Guest48 | (~Guest48@104.156.111.174) (Quit: Client closed) |
| 2025-05-08 20:47:46 +0200 | myme | (~myme@2a01:799:d5e:5f00:5054:783f:d768:b894) (Ping timeout: 276 seconds) |
| 2025-05-08 20:48:05 +0200 | myme | (~myme@2a01:799:d5e:5f00:1c16:e41e:c241:8a37) myme |
| 2025-05-08 20:50:34 +0200 | <[exa]> | evening everyone |
| 2025-05-08 20:51:27 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-08 20:51:33 +0200 | manwithluck | (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Ping timeout: 248 seconds) |
| 2025-05-08 20:52:08 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 20:52:24 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-05-08 20:56:25 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 2025-05-08 20:58:20 +0200 | <tomsmeding> | what language have you been programming in today |
| 2025-05-08 20:59:26 +0200 | <EvanR> | LLM infused C, for the proofs |
| 2025-05-08 20:59:59 +0200 | <darkling> | I've written about a dozen lines of bash, and installed Debian on a spare machine. |
| 2025-05-08 21:00:02 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-08 21:00:12 +0200 | <darkling> | Light duty. :) |
| 2025-05-08 21:00:22 +0200 | <mauke> | perl, sql |
| 2025-05-08 21:00:32 +0200 | <Athas> | I've done a bit of Julia and of course always Haskell. |
| 2025-05-08 21:00:39 +0200 | <tomsmeding> | EvanR: what part was about the proofs, the LLM-infused part or the other part |
| 2025-05-08 21:00:41 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-08 21:01:00 +0200 | <mauke> | but I read a bit about algebraic data types in C |
| 2025-05-08 21:01:00 +0200 | <Athas> | Whenever I use non-Haskell languages I end up annoyed with how complicated their semantics are (although Julia is really not so bad). |
| 2025-05-08 21:01:25 +0200 | <tomsmeding> | I think Haskell has tricky enough semantics too, sometimes |
| 2025-05-08 21:01:39 +0200 | <tomsmeding> | but if you're used to them, they make sense :) |
| 2025-05-08 21:01:51 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 21:01:59 +0200 | <EvanR> | it's true |
| 2025-05-08 21:02:04 +0200 | <EvanR> | haskell can get non trivial |
| 2025-05-08 21:02:16 +0200 | [exa] | did haskell+julia+bash |
| 2025-05-08 21:02:19 +0200 | <tomsmeding> | the static semantics can get _highly_ non-trivial |
| 2025-05-08 21:02:19 +0200 | <EvanR> | luckily there's a lot you can do which is trivially rightr |
| 2025-05-08 21:02:21 +0200 | <EvanR> | right |
| 2025-05-08 21:02:32 +0200 | <EvanR> | "obviously right" |
| 2025-05-08 21:02:44 +0200 | <tomsmeding> | two people who did Julia today! |
| 2025-05-08 21:02:45 +0200 | <Athas> | I mean the dynamic semantics. I can deal with complicated type systems much better. |
| 2025-05-08 21:03:01 +0200 | <tomsmeding> | haskell has very tame dynamic semantics |
| 2025-05-08 21:03:05 +0200 | <Athas> | "This program will not compile" is a much easier problem to deal with than "this program produces a bogus result". |
| 2025-05-08 21:03:09 +0200 | <Athas> | Yes, exactly. I like that. |
| 2025-05-08 21:03:11 +0200 | <tomsmeding> | :) |
| 2025-05-08 21:03:35 +0200 | <[exa]> | julia is such a love/hate trigger |
| 2025-05-08 21:03:45 +0200 | <tomsmeding> | mauke: how does one do algebraic data types in C? |
| 2025-05-08 21:03:50 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 2025-05-08 21:04:12 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 21:04:17 +0200 | <Athas> | I was put off by Julia for some time because of their abuse of terminology, but my recent dabbling reveals it's actually a fairly nice and simple language. Fortran-ish, in a good way. |
| 2025-05-08 21:04:21 +0200 | <tomsmeding> | even std::variant in C++ is a mere shade of proper sum types |
| 2025-05-08 21:04:44 +0200 | <Athas> | Julia people do absolutely awful things with metaprogramming, though. Makes template haskell look well-behaved. |
| 2025-05-08 21:05:26 +0200 | <tomsmeding> | Athas: what kind of metaprogramming do they do? Manipulate syntax trees or token lists? Or is the thing you're most horrified by the prevalence of it? |
| 2025-05-08 21:05:47 +0200 | <[exa]> | Athas: did you notice that there's this half of the ecosystem which is matlab-level toxic because people just try to emulate matlab, and the other half which is just absolutely marvelous |
| 2025-05-08 21:06:15 +0200 | <mauke> | tomsmeding: peep and weep: https://github.com/Hirrolot/datatype99 |
| 2025-05-08 21:06:45 +0200 | <mauke> | (yes, it's cpp abuse) |
| 2025-05-08 21:07:04 +0200 | <tomsmeding> | I assumed it was cpp abuse before clicking the link |
| 2025-05-08 21:07:47 +0200 | <Athas> | [exa]: no, I didn't poke that deep yet. |
| 2025-05-08 21:08:05 +0200 | <Athas> | tomsmeding: yes, macros, which they use to implement things like, say, an AD library. |
| 2025-05-08 21:08:13 +0200 | <tomsmeding> | "Specify -ftrack-macro-expansion=0 (GCC) or -fmacro-backtrace-limit=1 (Clang) to avoid useless macro expansion errors." -- useless as in, they're too cool for the default limits? |
| 2025-05-08 21:08:17 +0200 | <Athas> | Considering the size of the hammer, it works remarkably well. |
| 2025-05-08 21:08:42 +0200 | <tomsmeding> | Athas: I'm not actually sure I dislike that use of metaprogramming |
| 2025-05-08 21:08:47 +0200 | <tomsmeding> | how else would you do AD? |
| 2025-05-08 21:09:10 +0200 | <mauke> | tomsmeding: useless as in they expose library internals, I assume |
| 2025-05-08 21:09:20 +0200 | <Athas> | Operator overloading or a proper compiler plugin, maybe. Or actually built into the language. |
| 2025-05-08 21:09:24 +0200 | <[exa]> | tomsmeding: would you do AD in template haskell evaluated at runtime? |
| 2025-05-08 21:09:42 +0200 | <tomsmeding> | right, the other two options are a compiler plugin or operator overloading |
| 2025-05-08 21:10:00 +0200 | <tomsmeding> | writing a compiler plugin is always fraught because now you're at the whims of compiler developers that change APIs |
| 2025-05-08 21:10:08 +0200 | <mauke> | the options don't affect macro expansion, only error reporting |
| 2025-05-08 21:10:21 +0200 | <Athas> | But considering how much metaprogramming power Julia exposes, it is quite remarkable how intact Julia programmers' feet are. Future languages should probably study how that happened. |
| 2025-05-08 21:10:29 +0200 | <tomsmeding> | and operator overloading either gets you in the weeds of embedded language design, sharing recovery, etc., or is slower than static AD |
| 2025-05-08 21:10:46 +0200 | <tomsmeding> | mauke: right |
| 2025-05-08 21:11:02 +0200 | <tomsmeding> | oh I see, it's for backtrace tracking for diagnostics |
| 2025-05-08 21:11:03 +0200 | <Athas> | In contrast, Template Haskell is probably the source of 90% of my Haskell hassle, and I barely use it at all. |
| 2025-05-08 21:11:47 +0200 | <[exa]> | Athas: julia is not used for "critical code", there's always a sciencey guy next to the REPL who can fix stuffs. that approach is an advantage. |
| 2025-05-08 21:12:07 +0200 | <[exa]> | (yeah the REPL is so cool for people who never saw a good terminal app) |
| 2025-05-08 21:12:25 +0200 | <tomsmeding> | [exa]: is the person writing the code normally not a sciencey guy? |
| 2025-05-08 21:13:08 +0200 | <Athas> | That's an interesting point. It may be that Julia does break often, but not in ways that matter for the users. |
| 2025-05-08 21:13:10 +0200 | <[exa]> | tomsmeding: writing the code yeah, but the users here are also kinda scientists |
| 2025-05-08 21:13:44 +0200 | <tomsmeding> | I would expect a sciencey person to write the code, and there to be a programmer person beside ready to fix stuff. :P |
| 2025-05-08 21:13:59 +0200 | <tomsmeding> | but you put the sciencey person on the side, so now I wonder who the programmer is :) |
| 2025-05-08 21:14:00 +0200 | <Athas> | Julia has 14 libraries for autodiff (so many that they have a 15th library for providing a common interface), which I suggested to a Julia programmer might be a symptom of a problem, but I don't think he understood my point. |
| 2025-05-08 21:14:18 +0200 | <tomsmeding> | what's the problem with 14 autodiff libraries? |
| 2025-05-08 21:14:23 +0200 | <[exa]> | tomsmeding: yeah that's my last 4 publications or so :D |
| 2025-05-08 21:14:45 +0200 | <[exa]> | (the fixy computer guy, not the autodiff libs :D ) |
| 2025-05-08 21:14:51 +0200 | <tomsmeding> | :) |
| 2025-05-08 21:14:55 +0200 | <Athas> | tomsmeding: are there really 14 fundamentally different ways to do it? It is more likely that there is something that prevents a single design from properly handling more than a single use case. |
| 2025-05-08 21:15:14 +0200 | <tomsmeding> | Athas: that explanation assumes there is good reason for there to be 14 libraries |
| 2025-05-08 21:15:32 +0200 | <tomsmeding> | not knowing what those 14 are, I would rather expect there could have been 3, but people just felt like writing their own |
| 2025-05-08 21:15:57 +0200 | <Athas> | tomsmeding: well, depends on what you mean by "good", but looking at the list it doesn't look like merely itch-scratching. |
| 2025-05-08 21:16:19 +0200 | <Athas> | It's also a smell that creating a new library is easier than extending an existing one. That suggests that perhaps these kinds of libraries are not easy to maintain. |
| 2025-05-08 21:16:21 +0200 | <tomsmeding> | okay, then it is somewhat converning, yes |
| 2025-05-08 21:16:23 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 244 seconds) |
| 2025-05-08 21:16:28 +0200 | <tomsmeding> | *concerning |
| 2025-05-08 21:16:37 +0200 | <Athas> | It may also suggest that in Julia it is just incredibly easy and fun to write AD libraries, who knows. |
| 2025-05-08 21:16:49 +0200 | tomsmeding | would suspect that is a decent part of the cause |
| 2025-05-08 21:16:51 +0200 | <[exa]> | Athas: there's no single best way to do the API there, most of the ecosystem is only learning to properly invert dependencies for example. In turn the software doesn't really compose well, yet it's fun to create new one. |
| 2025-05-08 21:16:54 +0200 | <Athas> | They have so many of them that there is a meta-project for collating them: https://juliadiff.org/ It's amazing! |
| 2025-05-08 21:17:20 +0200 | <Athas> | Julia is probably the most vigorous and interesting community for people who care about AD, but it is also surprisingly messy. |
| 2025-05-08 21:17:50 +0200 | <[exa]> | ah there's the megacommunity for ODE solving :D :D |
| 2025-05-08 21:18:04 +0200 | <[exa]> | that's got like 6 gazillion packages for everything |
| 2025-05-08 21:18:07 +0200 | <Athas> | My impression is that there's two Julia libraries that Will Do It All: Enzyme.lj (which doesn't use Julia's metaprogramming support, it's an LLVM plugin), and Mooncake.jl (which I don't yet understand, and is WIP). |
| 2025-05-08 21:18:19 +0200 | <Athas> | In Haskell we have 'ad' which is good but slow, and hopefully horde-ad in the future! |
| 2025-05-08 21:19:08 +0200 | <tomsmeding> | I still find it amazing that Julia has an AD library that _differentiates LLVM IR_ |
| 2025-05-08 21:19:20 +0200 | <tomsmeding> | and apparently it's usefully performant! |
| 2025-05-08 21:19:23 +0200 | <Athas> | That's just Enzyme. C++ has that too. |
| 2025-05-08 21:19:43 +0200 | <tomsmeding> | I would expect that you've lost too much structure at that point |
| 2025-05-08 21:20:17 +0200 | <[exa]> | ah yes you know what's coolest about julia? you can @eval a definition of a function and it compiles and optimizes like crazy |
| 2025-05-08 21:20:25 +0200 | <Athas> | Welllll, Julia does JIT-compilation based on types, so the LLVM IR doesn't look so weird. |
| 2025-05-08 21:20:29 +0200 | <tomsmeding> | I wonder if it's fast (assuming it is) only by way of pattern-matching all the interesting higher-level constructures from the LLVM IR |
| 2025-05-08 21:20:40 +0200 | <Athas> | I think one could also use Enzyme to differentiate Haskell actually, but the laziness might make it difficult. |
| 2025-05-08 21:21:05 +0200 | <Athas> | tomsmeding: (i) it is not fast for that reason. (ii) it is not _really_ fast depending on what you expect. |
| 2025-05-08 21:22:16 +0200 | <tomsmeding> | at the risk of getting too much into details that I'm not sure I have energy for now: if you write a naive matrix multiplication manually, does Enzyme reverse-differentiate that to something that optimises down to a similarly-efficient matrix multiplication? |
| 2025-05-08 21:22:42 +0200 | <Athas> | A naive matrix multiplication? Yes. |
| 2025-05-08 21:22:54 +0200 | <tomsmeding> | cool |
| 2025-05-08 21:23:03 +0200 | <Athas> | But it will not do as well with a heavily optimised one. |
| 2025-05-08 21:23:06 +0200 | <tomsmeding> | sure |
| 2025-05-08 21:24:20 +0200 | <Athas> | While Enzyme is basically very good, I'm having some students working with Enzyme, and the fine print is really long and... well, undocumented. |
| 2025-05-08 21:25:39 +0200 | <[exa]> | research software quality™ |
| 2025-05-08 21:25:55 +0200 | <Athas> | Now now, research software doesn't have to be that way. GHC is research software. |
| 2025-05-08 21:26:25 +0200 | <[exa]> | ghc is done by researchers who literally do the research to eliminate corner cases and have good code |
| 2025-05-08 21:27:05 +0200 | <[exa]> | which kinda biases the choices :D |
| 2025-05-08 21:27:31 +0200 | <tomsmeding> | I think "AD on LLVM IR" is naturally a fairly plentiful source of corner cases |
| 2025-05-08 21:27:48 +0200 | <[exa]> | for many others it's "yeah so my problem X is finally computed, I can delete my github account now" |
| 2025-05-08 21:29:25 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-08 21:29:34 +0200 | <tomsmeding> | also, if there are people paid to make the thing more stable (GHC), can you really consider it "research software" any more? |
| 2025-05-08 21:29:50 +0200 | <tomsmeding> | people also do research on LLVM, but LLVM is not considered research software |
| 2025-05-08 21:30:41 +0200 | <[exa]> | yeah well, I meant that kind of "research software" where there's a postdoc, a problem, and 3 years of funding |
| 2025-05-08 21:31:01 +0200 | <Athas> | GHC was well documented and such before it had industrial financing. |
| 2025-05-08 21:31:22 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-05-08 21:31:22 +0200 | ljdarj1 | ljdarj |
| 2025-05-08 21:35:26 +0200 | <[exa]> | Athas: well the question then is what happened that differentiated these |
| 2025-05-08 21:35:57 +0200 | <[exa]> | ("differentiated" not as in AD now! :D ) |
| 2025-05-08 21:36:53 +0200 | <tomsmeding> | I have to prevent myself so often from writing "we can derive xyz equations" when talking about AD |
| 2025-05-08 21:36:59 +0200 | <Athas> | Not sure. It may be something as trivial as most programmers don't like writing documentation, so they don't. |
| 2025-05-08 21:37:20 +0200 | <Athas> | tomsmeding: the most difficult part of implementing AD in Haskell is that the usual x' convention becomes confusing. |
| 2025-05-08 21:37:44 +0200 | tomsmeding | doesn't get |
| 2025-05-08 21:38:17 +0200 | <tomsmeding> | how do variable naming conventions make implementing AD harder? |
| 2025-05-08 21:39:14 +0200 | <sprout> | derivative naming? |
| 2025-05-08 21:40:03 +0200 | <tomsmeding> | just make it dx instead |
| 2025-05-08 21:40:33 +0200 | <Athas> | In Haskell it is common to use the name x' for some variable derived from x, but that doesn't mean x' is the mathematical derivative of x, but when implementing AD you _do_ need a naming convention for that. |
| 2025-05-08 21:41:03 +0200 | <tomsmeding> | I see -- yes, "dx" is what I use |
| 2025-05-08 21:41:10 +0200 | <Athas> | https://github.com/diku-dk/futhark/blob/master/src/Futhark/AD/Rev.hs#L5-L8 |
| 2025-05-08 21:41:42 +0200 | <tomsmeding> | funny, I've never even thought about this being a problem |
| 2025-05-08 21:42:15 +0200 | <tomsmeding> | the ' notation for derivatives is not helpful in the context of AD anyway, because it carries much too little information about with respect to what you're actually differentiating |
| 2025-05-08 21:42:31 +0200 | <tomsmeding> | and furthermore, is an adjoint really a derivative of a thing? |
| 2025-05-08 21:42:48 +0200 | <tomsmeding> | with conventional meaning of "'", naming an adjoint of x as x' doesn't even make much sense |
| 2025-05-08 21:42:56 +0200 | <Athas> | No, it's a bigger problem for forward mode (where we use a _tan suffix). |
| 2025-05-08 21:43:21 +0200 | <tomsmeding> | ah, I think I see why I don't have problems with this |
| 2025-05-08 21:43:43 +0200 | <tomsmeding> | I write two kinds of AD code: dual-numbers forward mode where I just use "x" and "dx", and the code is simple enough anyway that it's all clear |
| 2025-05-08 21:44:03 +0200 | <tomsmeding> | and reverse-mode in a highly typed way where adjoints (cotangents) and primal values have _distinct types_ |
| 2025-05-08 21:44:10 +0200 | <EvanR> | the blog post related to datatype99 "What's the point of the C preprocessor, actually?" is kind of inspiring. And makes me think, what if you had a different preprocessor entirely |
| 2025-05-08 21:44:10 +0200 | <tomsmeding> | so if I confuse them, GHC yells at me |
| 2025-05-08 21:44:23 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-05-08 21:44:46 +0200 | manwithluck | (~manwithlu@2a09:bac1:5b80:20::49:f6) manwithluck |
| 2025-05-08 21:44:49 +0200 | <EvanR> | can gcc be told to use a different preprocessor |
| 2025-05-08 21:46:14 +0200 | <tomsmeding> | ghc can be |
| 2025-05-08 21:46:30 +0200 | <EvanR> | cool |
| 2025-05-08 21:46:42 +0200 | <tomsmeding> | https://hackage.haskell.org/package/record-dot-preprocessor ctrl-F for "use this magic" |
| 2025-05-08 21:51:04 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f4911c235e3ddcab2f1.dip0.t-ipconnect.de) acidjnk |
| 2025-05-08 21:51:17 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f49f4d0e34d1c0f8686.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-05-08 21:52:24 +0200 | <[exa]> | EvanR: for gcc, see the note below here https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html |
| 2025-05-08 21:53:51 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-05-08 21:53:53 +0200 | <[exa]> | I knew a guy who did type inference in the C code as the preprocessing step, can't find the thesis now tho |
| 2025-05-08 21:54:55 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 2025-05-08 21:55:00 +0200 | <EvanR> | wow |
| 2025-05-08 21:58:38 +0200 | <EvanR> | hell yeah |
| 2025-05-08 22:00:47 +0200 | rvalue- | rvalue |
| 2025-05-08 22:06:45 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-05-08 22:09:15 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 22:13:05 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-05-08 22:13:49 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-05-08 22:22:30 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) |
| 2025-05-08 22:27:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-08 22:27:57 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 2025-05-08 22:27:59 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) (Ping timeout: 244 seconds) |
| 2025-05-08 22:28:22 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 22:28:57 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) |
| 2025-05-08 22:35:49 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 2025-05-08 22:44:02 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 2025-05-08 22:52:00 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 22:59:25 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 23:01:06 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-05-08 23:11:49 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-08 23:12:49 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-08 23:21:03 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-05-08 23:22:54 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) (Ping timeout: 245 seconds) |
| 2025-05-08 23:25:31 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-05-08 23:28:48 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-08 23:39:54 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-08 23:43:15 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-05-08 23:43:45 +0200 | euleritian | (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-05-08 23:44:14 +0200 | euleritian | (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) |
| 2025-05-08 23:47:28 +0200 | madalin` | (~mad@89.90.150.62) |
| 2025-05-08 23:47:59 +0200 | madalin` | (~mad@89.90.150.62) (Client Quit) |
| 2025-05-08 23:50:31 +0200 | dofsyl^ | (~dofsyl@50.168.231.214) |
| 2025-05-08 23:51:58 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: Lost terminal) |
| 2025-05-08 23:52:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 2025-05-08 23:55:44 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) ft |
| 2025-05-08 23:58:09 +0200 | sprotte24 | (~sprotte24@p200300d16f4546009040e212dd81e9a6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |