2025/05/08

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 +0200merijn(~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 +0200machinedgod(~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 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 00:20:13 +0200hellwolfduck. good night.
2025-05-08 00:22:27 +0200xff0x(~xff0x@2405:6580:b080:900:c380:f27a:d8a3:29c7) (Ping timeout: 252 seconds)
2025-05-08 00:23:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 00:24:02 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2025-05-08 00:30:24 +0200tromp(~textual@2001:1c00:3487:1b00:d43:3b62:1503:cb84) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-05-08 00:34:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 00:38:14 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer)
2025-05-08 00:38:45 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-05-08 00:40:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-05-08 00:41:59 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-05-08 00:49:20 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net)
2025-05-08 00:50:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 00:53:09 +0200acidjnk(~acidjnk@p200300d6e71c4f51b11b7fbde7c758e1.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-05-08 00:55:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 00:56:32 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-05-08 01:04:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 01:08:36 +0200chexum(~quassel@gateway/tor-sasl/chexum) (Ping timeout: 264 seconds)
2025-05-08 01:08:45 +0200chexum(~quassel@gateway/tor-sasl/chexum) chexum
2025-05-08 01:11:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 01:11:16 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-05-08 01:12:32 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-08 01:13:01 +0200sprotte24(~sprotte24@p200300d16f3ca800283c8f0415b7b94b.dip0.t-ipconnect.de) (Quit: Leaving)
2025-05-08 01:13:52 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-05-08 01:14:25 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-05-08 01:21:43 +0200Kaladin(~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) (Quit: Leaving)
2025-05-08 01:22:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 01:26:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 01:28:19 +0200shapr(~user@2600:4040:5c49:5600:cacf:8e54:c9ac:25) (Remote host closed the connection)
2025-05-08 01:30:40 +0200Kaladin(~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) Kaladin
2025-05-08 01:33:49 +0200Guest84(~Guest84@host-95-237-69-25.retail.telecomitalia.it)
2025-05-08 01:37:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 01:42:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 01:45:20 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
2025-05-08 01:56:01 +0200ystael(~ystael@user/ystael) (Ping timeout: 248 seconds)
2025-05-08 02:00:57 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-05-08 02:04:31 +0200jespada(~jespada@179.26.249.126) (Ping timeout: 244 seconds)
2025-05-08 02:04:33 +0200hiredman(~hiredman@frontier1.downey.family) (Ping timeout: 248 seconds)
2025-05-08 02:07:18 +0200hiredman(~hiredman@frontier1.downey.family) hiredman
2025-05-08 02:09:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 02:12:05 +0200Guest84(~Guest84@host-95-237-69-25.retail.telecomitalia.it) (Quit: Client closed)
2025-05-08 02:12:07 +0200Kaladin(~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) (Quit: Leaving)
2025-05-08 02:14:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 02:20:51 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net)
2025-05-08 02:25:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 02:26:25 +0200ttybitnik(~ttybitnik@user/wolper) (Remote host closed the connection)
2025-05-08 02:27:14 +0200Axma13761(~Axman6@user/axman6) Axman6
2025-05-08 02:28:47 +0200JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-05-08 02:29:33 +0200Axman6(~Axman6@user/axman6) (Ping timeout: 250 seconds)
2025-05-08 02:30:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 02:30:28 +0200tolgo(~Thunderbi@199.115.144.130)
2025-05-08 02:30:31 +0200tolgo(~Thunderbi@199.115.144.130) (Client Quit)
2025-05-08 02:32:39 +0200Natch(~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 260 seconds)
2025-05-08 02:35:59 +0200Natch(~natch@c-92-34-7-158.bbcust.telenor.se) Natch
2025-05-08 02:40:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 02:46:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-05-08 02:56:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 02:58:19 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds)
2025-05-08 02:58:25 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 248 seconds)
2025-05-08 03:01:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-05-08 03:02:39 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-05-08 03:09:04 +0200haritz(~hrtz@2a01:4b00:bc2e:7000::2)
2025-05-08 03:10:29 +0200sajenim(~sajenim@user/sajenim) sajenim
2025-05-08 03:10:49 +0200haritz(~hrtz@2a01:4b00:bc2e:7000::2) (Changing host)
2025-05-08 03:10:49 +0200haritz(~hrtz@user/haritz) haritz
2025-05-08 03:12:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 03:17:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-05-08 03:28:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 03:33:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 03:38:15 +0200pointlessslippe1(~pointless@62.106.85.17) (Read error: Connection reset by peer)
2025-05-08 03:41:41 +0200pointlessslippe1(~pointless@62.106.85.17) pointlessslippe1
2025-05-08 03:44:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 03:46:01 +0200img(~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
2025-05-08 03:48:55 +0200img(~img@user/img) img
2025-05-08 03:51:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-05-08 04:02:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 04:04:37 +0200joeyadams(~textual@syn-162-154-010-038.res.spectrum.com)
2025-05-08 04:06:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 04:15:41 +0200tavare(~tavare@user/tavare) tavare
2025-05-08 04:17:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 04:19:57 +0200chewybread(~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70)
2025-05-08 04:19:57 +0200chewybread(~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70) (Changing host)
2025-05-08 04:19:57 +0200chewybread(~chewybrea@user/chewybread) chewybread
2025-05-08 04:22:01 +0200td_(~td@i5387091E.versanet.de) (Ping timeout: 252 seconds)
2025-05-08 04:22:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 04:22:48 +0200Square(~Square@user/square) Square
2025-05-08 04:23:00 +0200tabaqui(~tabaqui@167.71.80.236) (Ping timeout: 252 seconds)
2025-05-08 04:23:48 +0200td_(~td@i53870937.versanet.de)
2025-05-08 04:29:22 +0200tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-05-08 04:33:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 04:39:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 04:45:36 +0200chewybread(~chewybrea@user/chewybread) (Remote host closed the connection)
2025-05-08 04:49:26 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 04:54:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 04:58:10 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 05:03:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 05:10:29 +0200tabaqui(~tabaqui@167.71.80.236) tabaqui
2025-05-08 05:12:00 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-05-08 05:13:58 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-05-08 05:21:40 +0200tabaqui(~tabaqui@167.71.80.236) (Ping timeout: 252 seconds)
2025-05-08 05:23:46 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net)
2025-05-08 05:29:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 05:34:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-05-08 05:44:02 +0200aforemny_(~aforemny@i59F4C598.versanet.de) aforemny
2025-05-08 05:45:19 +0200aforemny(~aforemny@2001:9e8:6ce9:2000:c495:2bb2:ad61:d989) (Ping timeout: 265 seconds)
2025-05-08 05:45:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 05:50:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 06:01:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 06:06:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-05-08 06:10:25 +0200Square(~Square@user/square) (Ping timeout: 248 seconds)
2025-05-08 06:17:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 06:21:49 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-05-08 06:35:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 06:37:14 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-05-08 06:38:28 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 272 seconds)
2025-05-08 06:41:57 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 06:49:27 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-05-08 06:52:48 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-05-08 06:53:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 06:54:09 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds)
2025-05-08 07:04:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 07:06:45 +0200takuan(~takuan@d8D86B601.access.telenet.be)
2025-05-08 07:09:39 +0200takuan(~takuan@d8D86B601.access.telenet.be) (Read error: Connection reset by peer)
2025-05-08 07:10:08 +0200takuan(~takuan@d8D86B601.access.telenet.be)
2025-05-08 07:14:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 07:19:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-05-08 07:27:13 +0200califax(~califax@user/califx) (Remote host closed the connection)
2025-05-08 07:27:32 +0200califax(~califax@user/califx) califx
2025-05-08 07:28:13 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net)
2025-05-08 07:30:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 07:32:41 +0200haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2025-05-08 07:35:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-05-08 07:46:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 07:51:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-05-08 07:51:33 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds)
2025-05-08 08:00:10 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 08:05:11 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 08:08:48 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-08 08:10:19 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 265 seconds)
2025-05-08 08:15:49 +0200internatetional(~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) internatetional
2025-05-08 08:15:57 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-05-08 08:20:55 +0200internatetional(~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) (Ping timeout: 276 seconds)
2025-05-08 08:21:34 +0200merijn(~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 +0200merijn(~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 +0200Frostillicus_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 +0200joeyadams(~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com)
2025-05-08 08:36:12 +0200peterbecich(~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 +0200merijn(~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 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2025-05-08 08:41:53 +0200peterbecich(~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 +0200acidjnk(~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 +0200merijn(~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 +0200lortabac(~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 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 272 seconds)
2025-05-08 08:52:30 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-05-08 08:53:24 +0200ft(~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving)
2025-05-08 08:54:45 +0200jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 248 seconds)
2025-05-08 08:56:57 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-08 09:00:03 +0200caconym7(~caconym@user/caconym) (Quit: bye)
2025-05-08 09:00:45 +0200caconym7(~caconym@user/caconym) caconym
2025-05-08 09:06:41 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-05-08 09:14:41 +0200tromp(~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6)
2025-05-08 09:19:10 +0200sord937(~sord937@gateway/tor-sasl/sord937) sord937
2025-05-08 09:20:36 +0200Guest44(~Guest44@91-154-214-151.elisa-laajakaista.fi)
2025-05-08 09:29:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-05-08 09:29:28 +0200YoungFrog(~youngfrog@2a02:a03f:c9db:fc00:93c8:3aef:156:8fed) (Ping timeout: 272 seconds)
2025-05-08 09:33:14 +0200YoungFrog(~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog
2025-05-08 09:34:42 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-05-08 09:36:00 +0200Frostillicus_1(~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection)
2025-05-08 09:43:45 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-05-08 09:44:43 +0200merijn(~merijn@77.242.116.146) merijn
2025-05-08 09:56:37 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-05-08 09:56:43 +0200fp(~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 +0200tzh(~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 +0200Guest44(~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 +0200tomsmedinghas 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 +0200Boarders_____(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 +0200tomsmedingis 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 +0200econo_(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 +0200fp(~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 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-05-08 11:00:49 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-05-08 11:00:56 +0200yoneda(~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 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-05-08 11:11:49 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 248 seconds)
2025-05-08 11:13:13 +0200rvalue-(~rvalue@user/rvalue) rvalue
2025-05-08 11:13:21 +0200fp(~Thunderbi@2001:708:20:1406::10c5) fp
2025-05-08 11:13:25 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 248 seconds)
2025-05-08 11:19:49 +0200rvalue-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 +0200euleritian(~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds)
2025-05-08 11:32:46 +0200euleritian(~euleritia@dynamic-176-006-143-223.176.6.pool.telefonica.de)
2025-05-08 11:36:44 +0200Typedfern(~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) typedfern
2025-05-08 11:37:28 +0200Typedfern(~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Remote host closed the connection)
2025-05-08 11:38:17 +0200Typedfern(~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 +0200Typedfern(~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 +0200Typedfern(~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 +0200tromp(~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-05-08 12:06:59 +0200tromp(~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 +0200euleritian(~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 +0200euleritian(~euleritia@77.23.248.100)
2025-05-08 12:13:40 +0200yin(~z@user/zero) (Ping timeout: 244 seconds)
2025-05-08 12:15:30 +0200yin(~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 +0200xff0x(~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 +0200fp(~Thunderbi@2001:708:20:1406::10c5) (Quit: fp)
2025-05-08 12:23:56 +0200LearsLeary
2025-05-08 12:25:31 +0200yin(~z@user/zero) (Ping timeout: 252 seconds)
2025-05-08 12:27:01 +0200yin(~z@user/zero) zero
2025-05-08 12:33:39 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-05-08 12:37:22 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-05-08 12:38:07 +0200lortabac(~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 +0200JuanDaugherty(~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 +0200yin(~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 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-05-08 12:45:31 +0200yin(~z@user/zero) zero
2025-05-08 12:45:45 +0200L29Ah(~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