Logs on 2025-05-08 (liberachat/#haskell)
| 00:00:57 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:04:31 | × | jespada quits (~jespada@179.26.249.126) (Ping timeout: 244 seconds) |
| 00:04:33 | × | hiredman quits (~hiredman@frontier1.downey.family) (Ping timeout: 248 seconds) |
| 00:07:18 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 00:09:17 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:12:05 | × | Guest84 quits (~Guest84@host-95-237-69-25.retail.telecomitalia.it) (Quit: Client closed) |
| 00:12:07 | × | Kaladin quits (~Kaladin@157-131-203-96.fiber.dynamic.sonic.net) (Quit: Leaving) |
| 00:14:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 00:20:51 | → | Frostillicus_1 joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:25:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:26:25 | × | ttybitnik quits (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 00:27:14 | → | Axma13761 joins (~Axman6@user/axman6) |
| 00:28:47 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 00:29:33 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 250 seconds) |
| 00:30:03 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 00:30:28 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 00:30:31 | × | tolgo quits (~Thunderbi@199.115.144.130) (Client Quit) |
| 00:32:39 | × | Natch quits (~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 260 seconds) |
| 00:35:59 | → | Natch joins (~natch@c-92-34-7-158.bbcust.telenor.se) |
| 00:40:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:46:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 00:56:39 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:58:19 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 00:58:25 | × | Frostillicus_1 quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 01:01:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 01:02:39 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:09:04 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000::2) |
| 01:10:29 | → | sajenim joins (~sajenim@user/sajenim) |
| 01:10:49 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000::2) (Changing host) |
| 01:10:49 | → | haritz joins (~hrtz@user/haritz) |
| 01:12:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:17:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 01:28:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:33:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:38:15 | × | pointlessslippe1 quits (~pointless@62.106.85.17) (Read error: Connection reset by peer) |
| 01:41:41 | → | pointlessslippe1 joins (~pointless@62.106.85.17) |
| 01:44:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:46:01 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:48:55 | → | img joins (~img@user/img) |
| 01:51:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 02:02:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:04:37 | → | joeyadams joins (~textual@syn-162-154-010-038.res.spectrum.com) |
| 02:06:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 02:15:41 | → | tavare joins (~tavare@user/tavare) |
| 02:17:51 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:19:57 | → | chewybread joins (~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70) |
| 02:19:57 | × | chewybread quits (~chewybrea@2601:984:201:3890:b96e:b2c9:c50:1e70) (Changing host) |
| 02:19:57 | → | chewybread joins (~chewybrea@user/chewybread) |
| 02:22:01 | × | td_ quits (~td@i5387091E.versanet.de) (Ping timeout: 252 seconds) |
| 02:22:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:22:48 | → | Square joins (~Square@user/square) |
| 02:23:00 | × | tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 02:23:48 | → | td_ joins (~td@i53870937.versanet.de) |
| 02:29:22 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 02:33:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:39:21 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 02:45:36 | × | chewybread quits (~chewybrea@user/chewybread) (Remote host closed the connection) |
| 02:49:26 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:54:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 02:58:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:03:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 03:10:29 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 03:12:00 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:13:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:16:24 | <monochrom> | No one can steal lambda from Haskell without also stealing purity, laziness, preferring currying, ... |
| 03:19:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 03:21:40 | × | tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 03:23:46 | → | Frostillicus_1 joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 03:29:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:34:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 03:44:02 | → | aforemny_ joins (~aforemny@i59F4C598.versanet.de) |
| 03:45:19 | × | aforemny quits (~aforemny@2001:9e8:6ce9:2000:c495:2bb2:ad61:d989) (Ping timeout: 265 seconds) |
| 03:45:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:50:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 04:01:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:06:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 04:10:25 | × | Square quits (~Square@user/square) (Ping timeout: 248 seconds) |
| 04:17:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:21:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 04:35:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:37:14 | → | j1n37- joins (~j1n37@user/j1n37) |
| 04:38:28 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 04:41:57 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 04:49:27 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 04:52:48 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 04:53:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:54:09 | × | Frostillicus_1 quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 05:04:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 05:06:45 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 05:09:39 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Read error: Connection reset by peer) |
| 05:10:08 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 05:14:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:19:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 05:27:13 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 05:27:32 | → | califax joins (~califax@user/califx) |
| 05:28:13 | → | Frostillicus_1 joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 05:30:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:32:41 | × | haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 05:35:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 05:46:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:51:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:51:33 | × | Frostillicus_1 quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds) |
| 06:00:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:05:11 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:08:48 | → | j1n37 joins (~j1n37@user/j1n37) |
| 06:10:19 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 06:15:49 | → | internatetional joins (~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) |
| 06:15:57 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:20:55 | × | internatetional quits (~nate@2001:448a:20a3:c2e5:f5f8:a31:7307:70a6) (Ping timeout: 276 seconds) |
| 06:21:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 06:31:20 | <haskellbridge> | <hellwolf> morning thought to continue... |
| 06:31:20 | <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. |
| 06:31:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:32:25 | <haskellbridge> | <hellwolf> It intends to solve the "exponentially growing diagrams" issue, similar to what let var sharing solves. |
| 06:32:42 | <haskellbridge> | <hellwolf> The word "exponential" appears twice seems an interesting coincidence. |
| 06:33:37 | → | Frostillicus_1 joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 06:34:17 | <haskellbridge> | <hellwolf> Furthermore, LinearTypes offers another alternative: force you to express sharing using combinators such as "dup" |
| 06:34:47 | × | joeyadams quits (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 06:36:12 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:37:07 | <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. |
| 06:37:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 06:37:31 | <haskellbridge> | <hellwolf> It's a trade-off again: now, you need to program in a monad |
| 06:41:20 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 06:41:53 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:42:31 | <haskellbridge> | <hellwolf> further further furthermore, while using monad and LinrarTypes seems to defeat the benefits of using LinrarTypes to express "parallelizable branches", |
| 06:44:02 | <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". |
| 06:45:31 | → | acidjnk joins (~acidjnk@p200300d6e71c4f49a8c9e3402b4ffa7d.dip0.t-ipconnect.de) |
| 06:46:55 | <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. |
| 06:47:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:48:28 | <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. |
| 06:49:20 | <haskellbridge> | <hellwolf> linear-versioned monad that I build for yolc is a rather special case of LTL |
| 06:49:53 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:50:58 | <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. |
| 06:51:05 | <haskellbridge> | <hellwolf> alright. fin. |
| 06:51:28 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 06:52:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:53:24 | × | ft quits (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:54:45 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 06:56:57 | → | j1n37 joins (~j1n37@user/j1n37) |
| 07:00:03 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:45 | → | caconym7 joins (~caconym@user/caconym) |
| 07:06:41 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 07:14:41 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 07:19:10 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:20:36 | → | Guest44 joins (~Guest44@91-154-214-151.elisa-laajakaista.fi) |
| 07:29:25 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 07:29:28 | × | YoungFrog quits (~youngfrog@2a02:a03f:c9db:fc00:93c8:3aef:156:8fed) (Ping timeout: 272 seconds) |
| 07:33:14 | → | YoungFrog joins (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
| 07:34:42 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 07:36:00 | × | Frostillicus_1 quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 07:43:45 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:44:43 | → | merijn joins (~merijn@77.242.116.146) |
| 07:56:37 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 07:56:43 | → | fp joins (~Thunderbi@2001:708:20:1406::10c5) |
| 08:07:33 | <tomsmeding> | hellwolf: haven't read further in your monologue here, but generating IDs for sharing recovery using template haskell is unsound |
| 08:07:51 | <tomsmeding> | the same haskell term at the very same place in the diagram might produce distinct, non-unifiable nodes in the diagram |
| 08:08:35 | <tomsmeding> | `let f = \x -> x + x in f a + f b` in haskell |
| 08:09:05 | <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 |
| 08:09:49 | <tomsmeding> | the sharing that you can recover is not _lexical_ identity of the variables in question, but _runtime_ heap pointer identity |
| 08:09:54 | <tomsmeding> | or something that approximates the latter |
| 08:11:18 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:12:12 | <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? |
| 08:14:15 | → | __monty__ joins (~toonn@user/toonn) |
| 08:14:17 | × | Guest44 quits (~Guest44@91-154-214-151.elisa-laajakaista.fi) (Quit: Client closed) |
| 08:14:56 | <hellwolf> | yea, template haskell is unsound. I should read into your approach |
| 08:15:27 | <hellwolf> | > but how do you ensure the variable is dropped |
| 08:15:27 | <hellwolf> | the monad runner as a "cleanup block" that cleanup the variable references in the end. |
| 08:15:29 | <lambdabot> | error: |
| 08:15:29 | <lambdabot> | Unexpected do block in function application: |
| 08:15:29 | <lambdabot> | do you ensure the variable is dropped |
| 08:16:09 | <tomsmeding> | right, so apparently it doesn't matter in your application domain that variables are duplicated more often than strictly necessary? |
| 08:16:16 | <tomsmeding> | there's no performance cost associated with duplication? |
| 08:16:38 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/2b39ca47cb55324cab4eda36c0546ea1fb3d7aca/hs-pkgs/yul-dsl-linear-smc/src/YulDSL/Haskell/Effects/LinearSMC/YLVM.hs#L67C1-L67C29 see runYLVM |
| 08:16:56 | <hellwolf> | tomsmeding: yep, variable duplication is not a runtime thing! |
| 08:17:04 | <tomsmeding> | then this works |
| 08:17:13 | <hellwolf> | it's jsut for evaluator (the codegen most importantlh) |
| 08:17:29 | <tomsmeding> | then I actually question whether you _need_ linear types for this |
| 08:17:40 | <tomsmeding> | it's a technique to make the sharing explicit _in an embedding in haskell_ |
| 08:18:15 | <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 |
| 08:18:24 | <tomsmeding> | no need for linear types to make sharing visible |
| 08:18:41 | <hellwolf> | yea, linear-type is for "data freshness" |
| 08:18:50 | tomsmeding | has no clue what that means |
| 08:19:05 | <hellwolf> | yea, it's domain specific. let me see if I can explain |
| 08:19:21 | <hellwolf> | so, say, you write such a program: |
| 08:19:58 | <hellwolf> | you read the balance of account A -> beforeBalanceA; you invoke some side effects |
| 08:20:17 | <hellwolf> | you then do something again, with the assumption that the balance of beforeBalanceA is still valid |
| 08:20:26 | <tomsmeding> | that sounds like the versioning, not the linear types |
| 08:20:29 | <hellwolf> | in a open financial API system, that creates a vulnerability |
| 08:20:45 | <hellwolf> | yea, I use linear types ot create a type safe way to encode that |
| 08:20:53 | <hellwolf> | it's a type error if you use dated data |
| 08:21:12 | <hellwolf> | there were millions lost due to this kind of bugs. |
| 08:21:42 | <hellwolf> | can you enforce it in type safety in other means? |
| 08:21:54 | <tomsmeding> | you don't need to shout large numbers to convince me that it's interesting to care about software correctness ;) |
| 08:21:59 | <hellwolf> | I am all ears. I am an engineer, so I am here just to assemble solutions. |
| 08:22:16 | <hellwolf> | tomsmeding: haha, sorry, it's just sometimes I need to say things to peopel giving money |
| 08:22:19 | <hellwolf> | bad habit. |
| 08:22:22 | <tomsmeding> | :D |
| 08:22:40 | × | Boarders_____ quits (sid425905@id-425905.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:23:39 | <hellwolf> | but does that program example make sense? |
| 08:23:50 | <tomsmeding> | yes it does |
| 08:23:58 | tomsmeding | is looking at the LVM definition |
| 08:24:14 | <hellwolf> | excuse moi, that's my own sh*t |
| 08:24:19 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl-linear-smc/internal/lvm/Control/LinearlyVersionedMonad/LVM.hs |
| 08:24:19 | <hellwolf> | here |
| 08:24:24 | <tomsmeding> | yes I found it :) |
| 08:26:49 | <tomsmeding> | is it the idea that ctx is at version va, and that a is at version vb? |
| 08:27:01 | <tomsmeding> | the input ctx, that is |
| 08:27:30 | <hellwolf> | hmm in a way, I guess. a is the output type at version @vb@. |
| 08:27:49 | <hellwolf> | not sure I would say ctx having a version, per se. |
| 08:27:56 | <tomsmeding> | is there anything at version 'va'? |
| 08:28:00 | <hellwolf> | it's more about what you can be bound with |
| 08:28:41 | <tomsmeding> | presumably the idea is that pure primitive LVM operations have va=vb, and side-effectful primitive LVM operations have va < vb? |
| 08:28:46 | <hellwolf> | (_ :: m ctx va vb a) >>= (_ :: a -> m ctx vb vc b) ? |
| 08:29:07 | <hellwolf> | I would not see version independently, it's all about the >>= |
| 08:29:29 | <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? |
| 08:29:29 | <hellwolf> | corect |
| 08:30:27 | <tomsmeding> | (it's spelled "referentiable", not "referenciable") |
| 08:30:39 | <tomsmeding> | or perhaps "referrable" |
| 08:31:05 | <hellwolf> | where did you see that? |
| 08:31:10 | <tomsmeding> | LVMVar.hs |
| 08:31:24 | <hellwolf> | okay, thanks, I will fix |
| 08:31:52 | <tomsmeding> | I'm looking for something that shows me how using a non-fresh reference will result in a type error |
| 08:32:05 | <tomsmeding> | so I thought I'd look at variables, but I haven't found what I'm looking for yet |
| 08:32:30 | <hellwolf> | let me show you, it's not obvious, if you only look at LVM definitinop |
| 08:32:38 | <hellwolf> | since @a@ has no injectivty to @va@ |
| 08:32:44 | <tomsmeding> | sure |
| 08:32:53 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl-linear-smc/src/YulDSL/Haskell/Effects/LinearSMC/Storage.hs |
| 08:32:59 | <hellwolf> | sput'l :: forall. VersionThread r ⊸ P'V v r a ⊸ P'V v r b ⊸ (VersionThread r, P'V (v + 1) r ()) |
| 08:33:10 | <hellwolf> | data uses the "port api" from linear-smc library |
| 08:33:13 | <hellwolf> | so all data are versioned |
| 08:33:20 | <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 |
| 08:33:39 | <tomsmeding> | hence me not yet understanding what va is used for |
| 08:34:01 | <hellwolf> | right, to be precise, @a@ has a chance to be versioned at @va@ |
| 08:34:04 | <hellwolf> | not all @a@ has to be |
| 08:34:14 | <hellwolf> | e.g. Ur or (), or this type of thing doesn't carry such a version information |
| 08:34:24 | <tomsmeding> | sure |
| 08:34:24 | <hellwolf> | but for things that matter, they do, see "P'V v r a" api |
| 08:34:37 | <tomsmeding> | reads like klingon |
| 08:35:16 | <hellwolf> | :) what I just said, or the code related to P? |
| 08:35:22 | <tomsmeding> | "P'v v r a" |
| 08:35:41 | <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 |
| 08:36:03 | <hellwolf> | "P k r a" was the original API |
| 08:36:24 | <hellwolf> | -- | Yul port with linearly versioned data, aka. versioned yul ports. |
| 08:36:25 | <hellwolf> | type P'V v = P'x (VersionedPort v) |
| 08:36:29 | <hellwolf> | -- | Yul port with the port effect kind, aka. yul ports. |
| 08:36:29 | <hellwolf> | newtype P'x (eff :: PortEffect) r a = MkP'x (P (YulCat LinearEffectX) r a) |
| 08:38:15 | <hellwolf> | the example actually shows such a data version type safety in action, is here: |
| 08:38:28 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/examples/demo/src/ERC20.hs mint function |
| 08:38:38 | <hellwolf> | if you swap the onTokenMinted and sputs |
| 08:38:50 | <hellwolf> | you get a type error, because onTokenMinted might render data stale |
| 08:39:08 | <hellwolf> | the type is built to be conservative, and assume it will and forbid you to sue the data again |
| 08:39:33 | <hellwolf> | *use |
| 08:40:08 | <tomsmeding> | right, I see that an Rv indeed has a single 'v' version |
| 08:40:23 | <tomsmeding> | and `sget` produces a computation with va=v and vb=v |
| 08:41:38 | <tomsmeding> | I'm probably not seeing everything, but I have the feeling the goal of requiring freshness of variables can be achieved more simply |
| 08:41:42 | <tomsmeding> | I may be wrong |
| 08:41:59 | <hellwolf> | yep, happy to continue the discussion |
| 08:42:06 | <hellwolf> | my hunch is you cannot do without linear types |
| 08:42:15 | <hellwolf> | I dont' have a full theoretical survey about this problem |
| 08:42:26 | <hellwolf> | but the hunch is that without linearity on arrows, you can't build LTL |
| 08:42:30 | <hellwolf> | and I consider this a special case of LTL |
| 08:42:32 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:42:49 | <hellwolf> | but I am not a theoretician by trade |
| 08:42:53 | <tomsmeding> | me neither |
| 08:43:29 | <hellwolf> | the thing without linearity on arrow is that |
| 08:43:45 | <hellwolf> | you can copy a versioned data too freely without type system knowing |
| 08:44:01 | <hellwolf> | it will be "unsound"; I dont' use this word too rigoursly, so don't quote me |
| 08:44:03 | <tomsmeding> | but it will retain the same version, surely? |
| 08:44:13 | <tomsmeding> | even if you copy data at version v, the copy will still be at version v |
| 08:44:19 | <hellwolf> | it is the same version |
| 08:44:27 | <tomsmeding> | and you still can't use it at version v+1, which is the freshness restriction |
| 08:44:29 | <hellwolf> | but then you can diverge from the same version to other course of actions |
| 08:44:49 | <hellwolf> | you produce future version of the data of the same version but not from the same "course" |
| 08:45:16 | <hellwolf> | I have drew on paper, but I just don't have a actual "paper" to check if I was right about my hunch |
| 08:45:18 | <tomsmeding> | can you "upgrade" the version of a variable? |
| 08:45:25 | <hellwolf> | not safely |
| 08:45:35 | <hellwolf> | there is unsafe api for building other safe API |
| 08:45:38 | <tomsmeding> | then I still don't see the problem |
| 08:45:58 | <tomsmeding> | sure, unsafe APIs are for living dangerously, we're talking about the safe APIs |
| 08:46:06 | <hellwolf> | think of diamond-shaped path |
| 08:46:24 | <hellwolf> | va >>= vb in one monad, and va >>= vb in another monad |
| 08:46:38 | <hellwolf> | you have two data that has @vb, but they don't aggree with the timeline! |
| 08:46:42 | <tomsmeding> | oh I see |
| 08:46:53 | <hellwolf> | only linearity on arrow can enforce that |
| 08:47:08 | <tomsmeding> | because versions are actually natural numbers, and those have too much structure |
| 08:47:20 | <hellwolf> | that's a mathy way to say, I can see where you are going |
| 08:47:29 | × | fp quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds) |
| 08:47:35 | <hellwolf> | are you familiar with LTL? |
| 08:48:00 | <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. |
| 08:48:05 | <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 |
| 08:48:28 | <tomsmeding> | then doing two separate side-effectful things to a 'va'-versioned variable would produce w1 and w2 that are both greater than 'va' |
| 08:48:36 | <tomsmeding> | but they aren't necessarily equal |
| 08:48:52 | <hellwolf> | that's right |
| 08:49:05 | <tomsmeding> | essentially you'd be building up a partial order of versions, instead of using the "too structured" natural numbers |
| 08:49:14 | <hellwolf> | hmm, interesting |
| 08:49:17 | <tomsmeding> | this is probably extremely awkward to encode in haskell |
| 08:49:32 | <hellwolf> | which is awkward to encode? |
| 08:49:38 | <hellwolf> | partial order in type? |
| 08:49:40 | <tomsmeding> | because the encoding I just described requires that the continuation of a side-effectful primop has a polymorphic type, to accept any w |
| 08:49:53 | <tomsmeding> | so you have RankNTypes EVERYWHERE |
| 08:50:02 | <tomsmeding> | probably too much for ghc to cope with |
| 08:50:08 | <hellwolf> | that's for library write to hid? |
| 08:50:11 | <hellwolf> | oh :) |
| 08:50:16 | <hellwolf> | I assume GHC is glorious |
| 08:50:23 | <tomsmeding> | it is |
| 08:50:35 | <tomsmeding> | % System.Process.system "ghc --version" |
| 08:50:35 | <yahb2> | The Glorious Glasgow Haskell Compilation System, version 9.12.2 ; ExitSuccess |
| 08:50:51 | <hellwolf> | % System.Procerss.systme "rm -rf /hahaha" |
| 08:50:51 | <yahb2> | <interactive>:99:1: error: [GHC-76037] ; Not in scope: ‘System.Procerss.systme’ ; Note: No module named ‘System.Procerss’ is imported. |
| 08:51:13 | <tomsmeding> | you have write access only to a small tmpfs |
| 08:51:31 | <hellwolf> | you thinki so, did it enforce it in the type system? |
| 08:51:38 | <tomsmeding> | :) |
| 08:51:55 | <tomsmeding> | https://git.tomsmeding.com/yahb2/tree/bwrap-files/start.sh |
| 08:52:12 | <hellwolf> | thanks for being the rubber duck with me. you are the first one actually I conversed in details with what I built :D |
| 08:52:19 | <hellwolf> | I have no time to write down everything yet. |
| 08:57:02 | <Lears> | How would GHC fail to cope with too much RankNTypes? Bluefin also requires polymorphic continuations everywhere, and it does just fine. |
| 08:57:21 | <tomsmeding> | perhaps GHC is fine, I dunno |
| 08:59:02 | → | j1n37- joins (~j1n37@user/j1n37) |
| 09:00:49 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 09:00:56 | → | yoneda joins (~mike@193.206.102.122) |
| 09:02:15 | <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 |
| 09:02:51 | <tomsmeding> | you end up having to CPS all code to express what I described |
| 09:03:42 | <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 |
| 09:03:48 | <hellwolf> | your idea of the variable labeling? |
| 09:03:56 | <hellwolf> | using unsafe io? |
| 09:04:04 | <tomsmeding> | no, the "use (v, exists w. w) instead of (v, v+1)" |
| 09:04:20 | <tomsmeding> | variable labeling is implemented successfully by accelerate |
| 09:04:20 | <hellwolf> | ah, okay, I didn't fully understand that |
| 09:04:42 | <tomsmeding> | the unsafePerformIO ID generation trick is sucessfully implemented by horde-ad (a library a collaborator of mine is working on) |
| 09:04:43 | <hellwolf> | (we talk about variable labeling another time, when I get to that; I am okay with what I have now for that.) |
| 09:05:06 | <tomsmeding> | I'd like someone to use https://git.tomsmeding.com/sharing-recovery/about/ in anger :p |
| 09:05:17 | <hellwolf> | I am all ears to hear feedback and criticism on my whole LVM approach |
| 09:06:52 | <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 ) |
| 09:07:32 | <tomsmeding> | but in your case it may not solve anything because you require the linear types for versioning too |
| 09:07:42 | <tomsmeding> | because my partial-order thing doesn't (easily?) work |
| 09:08:26 | <hellwolf> | let me read your project: one-liner README :) |
| 09:08:55 | <hellwolf> | | This is an attempt at implementing "Optimising Purely Functional GPU Programs" by McDonell et al. (ICFP 2013) in a generic fashion. |
| 09:11:32 | → | j1n37 joins (~j1n37@user/j1n37) |
| 09:11:49 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 248 seconds) |
| 09:13:13 | → | rvalue- joins (~rvalue@user/rvalue) |
| 09:13:21 | → | fp joins (~Thunderbi@2001:708:20:1406::10c5) |
| 09:13:25 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 09:19:49 | rvalue- | is now known as rvalue |
| 09:25:13 | <tomsmeding> | hellwolf: yeah only the sharing recovery part of it |
| 09:25:38 | <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 |
| 09:25:46 | <tomsmeding> | but the expression it creates is untyped |
| 09:26:15 | <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 |
| 09:28:34 | <hellwolf> | thanks, printed. will read to enrich my knowledge here. it seems relevant to what I do. |
| 09:29:14 | <tomsmeding> | I find the presentation in the McDonell paper to be hard to understand personally |
| 09:29:37 | <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 |
| 09:29:43 | <tomsmeding> | but the documentation part never happened, lol |
| 09:29:59 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 09:32:46 | → | euleritian joins (~euleritia@dynamic-176-006-143-223.176.6.pool.telefonica.de) |
| 09:36:44 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 09:37:28 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 09:38:17 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 09:44:19 | <hellwolf> | :D code is better than paper? |
| 09:45:31 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 09:46:11 | <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 |
| 09:51:47 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 10:01:09 | <hellwolf> | Oh, I have never heard of the Atkey thing. |
| 10:01:41 | <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. |
| 10:02:01 | <hellwolf> | I was suspecting some sort of indexed monad, but I just didn't know what it's called. |
| 10:05:52 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:06:59 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 10:07:45 | <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. |
| 10:07:55 | <hellwolf> | "losign" |
| 10:08:01 | <hellwolf> | *losing of |
| 10:08:08 | <hellwolf> | darn it. typing in IRC is hard. |
| 10:08:12 | <tomsmeding> | it is |
| 10:08:14 | × | euleritian quits (~euleritia@dynamic-176-006-143-223.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:08:33 | <hellwolf> | what it is? |
| 10:08:42 | <tomsmeding> | typing is hard |
| 10:08:48 | <hellwolf> | :) |
| 10:09:03 | <tomsmeding> | well I think your solution works |
| 10:09:34 | <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 |
| 10:10:03 | <tomsmeding> | I still feel there might be more ways to solve it besides yours |
| 10:10:30 | <hellwolf> | oh, there must be. I'd be interested in dicussing these ideas, and convert them into engineering solutions. |
| 10:10:45 | <hellwolf> | I am a packager of solutions :P |
| 10:11:20 | <hellwolf> | good to hear that my general direction seems okay in expert's eyes. I need to really write them up. |
| 10:11:35 | <tomsmeding> | "expert" |
| 10:11:48 | <hellwolf> | relative monad wise |
| 10:11:56 | <hellwolf> | I am a monad with no grade |
| 10:12:31 | → | euleritian joins (~euleritia@77.23.248.100) |
| 10:13:40 | × | yin quits (~z@user/zero) (Ping timeout: 244 seconds) |
| 10:15:30 | → | yin joins (~z@user/zero) |
| 10:19:04 | <hellwolf> | Lears: I didn't see linear arrows used though? |
| 10:19:19 | <hellwolf> | (>>=) seems having %Many |
| 10:23:17 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 10:23:28 | <Lears> | hellwolf: I didn't put any on the `Atkey` class, no, but you can slip them in if you need to. |
| 10:23:50 | × | fp quits (~Thunderbi@2001:708:20:1406::10c5) (Quit: fp) |
| 10:23:56 | Lears | is now known as Leary |
| 10:25:31 | × | yin quits (~z@user/zero) (Ping timeout: 252 seconds) |
| 10:27:01 | → | yin joins (~z@user/zero) |
| 10:33:39 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 10:37:22 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 10:38:07 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds) |
| 10:39:16 | <hellwolf> | > essentially you'd be building up a partial order of versions, instead of using the "too structured" natural numbers |
| 10:39:16 | <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. |
| 10:39:18 | <lambdabot> | <hint>:1:50: error: parse error on input ‘of’ |
| 10:39:40 | <hellwolf> | that's what I want to encode in Haskell, perhaps in 2026 |
| 10:40:07 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 10:40:29 | <hellwolf> | to me, if I were right about this, it's criminally underselling linear arrows of GHC. |
| 10:40:59 | <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. |
| 10:41:24 | <hellwolf> | the linear-safety ergonomics loss is a turnoff to a lot of people |
| 10:42:06 | <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. |
| 10:42:34 | <hellwolf> | I will admit that I haven't even convinced or conveyed what I am doing to Arnauld :D |
| 10:44:36 | × | yin quits (~z@user/zero) (Ping timeout: 252 seconds) |
| 10:44:47 | <JuanDaugherty> | i was speculating when i first heard of ML, if it coulda been in the '70s |
| 10:45:11 | <JuanDaugherty> | it was 2 years b4 i wrote my first program |
| 10:45:17 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 10:45:31 | → | yin joins (~z@user/zero) |
| 10:45:45 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 10:45:48 | <JuanDaugherty> | i didn realize how straight and well penciled the line was from ML to haskell and GHC |
| 10:46:17 | <JuanDaugherty> | edinburgh and the milner and what not |
| 10:46:25 | <JuanDaugherty> | s/the// |
| 10:47:09 | <JuanDaugherty> | i.e. ML was 2 years, unclear when I first heard of it but b6 1980 |
| 10:48:25 | <JuanDaugherty> | i thought the uni just glommed onto haskell and it originated in some amorphose global academic ML cloud |
| 10:48:54 | <hellwolf> | with conclave and inaccessible cardinals? |
| 10:49:07 | <hellwolf> | (stealing this joke from functional cafe.) |
| 10:49:09 | <JuanDaugherty> | dont forget the smoke |
| 10:50:10 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 10:50:40 | <JuanDaugherty> | *b4 1980 |
| 10:51:26 | <JuanDaugherty> | i didn think it (ML) actually did useful, non theoretical programming |
| 10:51:54 | → | zzz joins (~z@user/zero) |
| 10:52:11 | <hellwolf> | does it now? |
| 10:52:27 | <JuanDaugherty> | which misimpression wasn dispelled until hs started getting real |
| 10:52:33 | × | yin quits (~z@user/zero) (Read error: Connection reset by peer) |
| 10:52:33 | zzz | is now known as yin |
| 10:53:07 | <JuanDaugherty> | c. '06 for me; yes i now realize ML always did have that property i thought it didn |
| 10:53:16 | × | m1dnight quits (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 276 seconds) |
| 10:54:15 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 10:54:48 | → | m1dnight joins (~m1dnight@d8D861908.access.telenet.be) |
| 10:55:02 | <JuanDaugherty> | or rather i've been aware of it for some time |
| 10:55:06 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 10:57:30 | <JuanDaugherty> | something like that must be how the typical programming IT worker of today views hs except that now know u can do stuff |
| 10:57:53 | <JuanDaugherty> | *now they/u know |
| 10:58:08 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:58:08 | <JuanDaugherty> | but it's still "what is this shit?" |
| 10:59:19 | <hellwolf> | turing-complete machine is such an amazing beast. |
| 10:59:28 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 10:59:42 | <hellwolf> | you can ask it to do whatever it can, so long it has the access to the external world, including launching a missle |
| 11:00:00 | <hellwolf> | *missile |
| 11:00:04 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 11:00:06 | <JuanDaugherty> | can u? |
| 11:00:32 | <JuanDaugherty> | is there some stunning copilot or llm stuffs with hs i dont know about? |
| 11:00:44 | <hellwolf> | that makes people who work on it, self-labeled programmers, think they are powerful. |
| 11:01:06 | <darkling> | hellwolf: Missal? Are we back to the inaccessible cardinals again? |
| 11:01:11 | <JuanDaugherty> | well no, that's not required |
| 11:01:19 | <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? |
| 11:01:27 | <JuanDaugherty> | they dont have to understand the code to use it |
| 11:01:44 | <hellwolf> | I think that's the crust why many don't understand FP's appeal |
| 11:01:45 | <JuanDaugherty> | u FP ppl |
| 11:01:46 | → | jespada joins (~jespada@179.26.249.228) |
| 11:02:01 | <hellwolf> | if all your end goal is to tell machine to do whatever you want it to do, then yes, it's pointless. |
| 11:02:08 | <hellwolf> | But we pursue a different goal. |
| 11:02:18 | → | caconym7 joins (~caconym@user/caconym) |
| 11:02:27 | <JuanDaugherty> | somebody said something was point free |
| 11:03:11 | <JuanDaugherty> | and yes, with computers, that's all my end goal is |
| 11:03:17 | × | yin quits (~z@user/zero) (Ping timeout: 248 seconds) |
| 11:03:18 | <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. |
| 11:03:27 | <JuanDaugherty> | god fart |
| 11:03:32 | <JuanDaugherty> | u lose |
| 11:04:06 | <hellwolf> | :) |
| 11:04:11 | hellwolf | duck and continue coding |
| 11:04:19 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 11:05:24 | <JuanDaugherty> | unless i'm mistaken something should be forthcoming to fill that role (nlp - hs relation) |
| 11:07:16 | <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 |
| 11:07:43 | <JuanDaugherty> | *prodigously |
| 11:08:54 | <hellwolf> | I was monologueing, sorry, I didn't target anyone personally. I am speaking to strawmen I saw on X social. |
| 11:09:05 | <hellwolf> | didn't want to engage there, so I rant in IRC. |
| 11:09:11 | <JuanDaugherty> | well carry on |
| 11:10:00 | <hellwolf> | it's alright, I am going too far already bringing out the metaphysical aspects of people. |
| 11:10:18 | <hellwolf> | but sometimes, to me, that's the only relevant part to end a conversation. |
| 11:10:36 | → | j1n37- joins (~j1n37@user/j1n37) |
| 11:10:40 | <JuanDaugherty> | *without the circle jerk |
| 11:10:47 | <hellwolf> | even as a rationalist, I find it simply a impossible conversation to continue with people refuse rational thinking. |
| 11:11:14 | hellwolf | duck for real. have a good day gents. |
| 11:11:17 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 248 seconds) |
| 11:11:49 | <JuanDaugherty> | u'd be surprised how far the refusal reaches |
| 11:12:53 | → | yin joins (~z@user/zero) |
| 11:15:22 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 11:24:51 | → | infinity0 joins (~infinity0@pwned.gg) |
| 11:26:41 | → | kh0d joins (~kh0d@89.216.103.150) |
| 11:30:38 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 11:30:54 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:31:05 | → | xff0x joins (~xff0x@2405:6580:b080:900:df43:4d2b:b873:7ac7) |
| 11:33:46 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:33:57 | × | j1n37- quits (~j1n37@user/j1n37) (Quit: Ich bin der Welt abhanden gekommen) |
| 11:34:13 | → | j1n37 joins (~j1n37@user/j1n37) |
| 11:38:32 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 11:42:12 | → | j1n37 joins (~j1n37@user/j1n37) |
| 11:44:31 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 11:47:15 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:49:08 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 265 seconds) |
| 11:52:30 | JuanDaugherty | is now known as ColinRobinson |
| 12:09:12 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
| 12:09:54 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 12:19:38 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 12:23:43 | × | ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 12:38:44 | <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 |
| 12:40:37 | → | kuribas joins (~user@ptr-17d51em669ysrfo60ou.18120a2.ip6.access.telenet.be) |
| 12:43:51 | → | Digitteknohippie joins (~user@69.47.7.51.dyn.plus.net) |
| 12:44:07 | × | Digit quits (~user@69.47.7.51.dyn.plus.net) (Ping timeout: 252 seconds) |
| 12:49:33 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 12:49:41 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:49:47 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 13:06:51 | × | kh0d quits (~kh0d@89.216.103.150) (Quit: Leaving...) |
| 13:08:29 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 13:08:33 | × | euleritian quits (~euleritia@77.23.248.100) (Remote host closed the connection) |
| 13:08:49 | <int-e> | hellwolf: dym int-index maybe (it's certainly not me) |
| 13:08:51 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 13:09:26 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 13:10:08 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 13:12:47 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Remote host closed the connection) |
| 13:13:21 | × | atwm quits (~andrew@19-193-28-81.ftth.cust.kwaoo.net) (Quit: WeeChat 4.6.1) |
| 13:13:29 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 13:25:56 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 13:35:24 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 13:37:06 | → | euleritian joins (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) |
| 13:38:03 | × | euleritian quits (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:38:21 | → | euleritian joins (~euleritia@77.23.248.100) |
| 13:39:03 | → | ystael joins (~ystael@user/ystael) |
| 13:39:17 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 13:53:17 | → | stef204 joins (~stef204@user/stef204) |
| 13:57:44 | × | prasad quits (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) (Remote host closed the connection) |
| 14:06:00 | × | euleritian quits (~euleritia@77.23.248.100) (Remote host closed the connection) |
| 14:06:18 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 14:06:25 | × | sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (Quit: leaving) |
| 14:09:22 | <hellwolf> | oh, iIsomehow thought it was you :) |
| 14:20:00 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 14:20:46 | → | sprout joins (~sprout@84-80-106-227.fixed.kpn.net) |
| 14:21:00 | → | euleritian joins (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) |
| 14:33:44 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:35:05 | × | euleritian quits (~euleritia@dynamic-176-006-143-056.176.6.pool.telefonica.de) (Ping timeout: 272 seconds) |
| 14:36:15 | → | euleritian joins (~euleritia@dynamic-176-006-145-187.176.6.pool.telefonica.de) |
| 14:37:30 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 14:41:18 | × | Sgeo quits (~Sgeo@user/sgeo) (Ping timeout: 244 seconds) |
| 14:41:24 | × | sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (Ping timeout: 272 seconds) |
| 14:42:15 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:45:41 | × | OftenFaded quits (~OftenFade@user/tisktisk) (Quit: OftenFaded) |
| 14:46:32 | × | wbrawner quits (~wbrawner@static.205.41.78.5.clients.your-server.de) (Remote host closed the connection) |
| 15:00:53 | → | sprout joins (~sprout@84-80-106-227.fixed.kpn.net) |
| 15:05:28 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 276 seconds) |
| 15:08:07 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 15:09:07 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Client Quit) |
| 15:11:56 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 15:15:16 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 15:15:48 | → | califax joins (~califax@user/califx) |
| 15:20:09 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 15:21:03 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 15:46:49 | → | volsand joins (~volsand@2804:1b1:1080:da6:dcbd:80c:8e7b:1cf7) |
| 15:49:09 | × | tessier quits (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 248 seconds) |
| 15:49:21 | → | weary-traveler joins (~user@user/user363627) |
| 15:50:12 | × | ttybitnik quits (~ttybitnik@user/wolper) (Quit: "Inté pros bão que junto a gente fica mió") |
| 15:50:12 | → | prasad joins (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 15:50:36 | × | kuribas quits (~user@ptr-17d51em669ysrfo60ou.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 15:50:50 | → | kuribas joins (~user@ptr-17d51eo8yjf3h7nzszs.18120a2.ip6.access.telenet.be) |
| 15:50:59 | → | tessier joins (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 15:52:54 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 15:57:20 | → | Guest65 joins (~Guest54@117.107.131.196) |
| 15:59:32 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 16:00:59 | × | Guest65 quits (~Guest54@117.107.131.196) (Client Quit) |
| 16:04:39 | × | arahael quits (~arahael@user/arahael) (Read error: Connection reset by peer) |
| 16:05:22 | → | mari-estel joins (~mari-este@user/mari-estel) |
| 16:06:00 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 16:09:04 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) (Error from remote client) |
| 16:12:33 | → | jespada_ joins (~jespada@r167-61-122-127.dialup.adsl.anteldata.net.uy) |
| 16:15:23 | → | ft joins (~ft@p4fc2a6e6.dip0.t-ipconnect.de) |
| 16:15:45 | × | jespada quits (~jespada@179.26.249.228) (Ping timeout: 276 seconds) |
| 16:18:25 | × | mari-estel quits (~mari-este@user/mari-estel) (Ping timeout: 248 seconds) |
| 16:19:52 | → | mari-estel joins (~mari-este@user/mari-estel) |
| 16:20:01 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 16:21:20 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 16:21:53 | × | mari-estel quits (~mari-este@user/mari-estel) (Remote host closed the connection) |
| 16:28:37 | × | acidjnk quits (~acidjnk@p200300d6e71c4f49a8c9e3402b4ffa7d.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 16:38:26 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 16:39:42 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 16:40:11 | → | j1n37 joins (~j1n37@user/j1n37) |
| 16:42:48 | <tomsmeding> | hellwolf: mention my full nick, I don't have highlight on just 'tom' (too many toms) |
| 16:43:08 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:43:18 | <tomsmeding> | and there's too much blather here to diligently read scrollback for me :) |
| 16:44:18 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:45:02 | → | gmg joins (~user@user/gehmehgeh) |
| 16:49:42 | → | milan joins (~milan@88.212.61.169) |
| 16:54:07 | <hellwolf> | I didn't want to tag you |
| 16:54:19 | <hellwolf> | but I will, if you don't mind |
| 16:55:02 | <tomsmeding> | if you want me to read something, tag me; if you want me to miss it, don't tag me :p |
| 16:55:25 | <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 |
| 16:55:37 | <Rembane> | Schrödinger's tomsmeding! |
| 16:55:38 | <tomsmeding> | and sometimes I don't open irc over a weekend or so |
| 16:55:40 | <tomsmeding> | yes |
| 17:02:33 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 17:06:33 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:06:57 | <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 |
| 17:07:06 | <tomsmeding> | I don't do that level of scrollback reading, apologies |
| 17:07:31 | × | yoneda quits (~mike@193.206.102.122) (Quit: leaving) |
| 17:09:45 | <hellwolf> | :) |
| 17:09:59 | <hellwolf> | we can move some detailed discuss DM too, when there is more sustance |
| 17:12:03 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 17:19:39 | → | sprotte24 joins (~sprotte24@p200300d16f4546009040e212dd81e9a6.dip0.t-ipconnect.de) |
| 17:20:40 | × | euleritian quits (~euleritia@dynamic-176-006-145-187.176.6.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 17:22:59 | <tomsmeding> | hellwolf: a sketch of how you can do versioning with CPS-style code https://paste.tomsmeding.com/Fu4HP0Sh |
| 17:23:15 | <tomsmeding> | I _think_ this is a safe API, but I'm not 100% sure |
| 17:23:28 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 17:23:49 | <tomsmeding> | "safe" as in: cannot have "diverging histories", as you've described, nor can you arrange to use a Ref after a Port operation |
| 17:24:38 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:24:47 | × | sajenim quits (~sajenim@user/sajenim) (Ping timeout: 244 seconds) |
| 17:25:26 | <EvanR> | yeah there's just way too much traffic in this channel |
| 17:25:39 | <EvanR> | 🦗 |
| 17:26:32 | <hellwolf> | tomsmeding: what does Fr mean here? |
| 17:26:40 | <tomsmeding> | "fresh" |
| 17:26:46 | <hellwolf> | :) |
| 17:27:02 | <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 |
| 17:27:13 | <hellwolf> | Ur, Uv, Rv, Fr, the two-lettered family of spells |
| 17:28:08 | <hellwolf> | fwiw, I have the VersionThread API, without monad; but that also requires linear arrows |
| 17:28:18 | <hellwolf> | (let me read into your Fr more...) |
| 17:28:48 | <tomsmeding> | the idea of Fr is that every operation requires you to proceed in a callback |
| 17:29:15 | <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 |
| 17:29:36 | <tomsmeding> | so you should consider the compositions with 'cps' to be the actual Ref operations, as used in MainCPS |
| 17:29:49 | <tomsmeding> | hence you automatically get a linear sequence of operations |
| 17:30:15 | <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 |
| 17:30:48 | <hellwolf> | but I surely can use the same monad a few times, without linear arrows? |
| 17:30:54 | <hellwolf> | would that introduce unsoundness |
| 17:31:09 | <tomsmeding> | I think you have to use the 'cps' function to do that, right? |
| 17:31:18 | <tomsmeding> | so 'cps' should indeed not be exported |
| 17:32:05 | <tomsmeding> | hellwolf: can you do it without 'cps'? |
| 17:32:23 | <tomsmeding> | assuming that the Ref functions are rewritten to have 'cps' baked-in; currently doing that |
| 17:33:16 | × | manwithluck quits (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 17:33:27 | → | manwithluck joins (~manwithlu@2a09:bac5:5081:2dc::49:f6) |
| 17:33:41 | <tomsmeding> | hellwolf: fixed version https://paste.tomsmeding.com/CFVMMNbL |
| 17:33:44 | <hellwolf> | I am not follow fully yet, since cps returns Fr with the same "v" |
| 17:33:53 | <tomsmeding> | yes ignore cps, it's gone in the fixed version |
| 17:34:03 | <tomsmeding> | oh the comment is still there, ignore the comment too :p |
| 17:34:17 | <tomsmeding> | (the comment on line 27 in the fixed version) |
| 17:35:37 | <tomsmeding> | I wonder whether a Port also needs a version index |
| 17:36:37 | <hellwolf> | my hunch is that you might need, but I haven't tried to break your code yet. |
| 17:36:48 | <hellwolf> | I mean break the intended "correctness protection" |
| 17:36:51 | <tomsmeding> | yes |
| 17:37:03 | <tomsmeding> | I assumed here that you can continue using Ports even after the version changed |
| 17:37:25 | <tomsmeding> | if you can't then they just get a version index just like Ref, but this case is more interesting |
| 17:38:27 | <hellwolf> | (forall w. Port a %? -> Fr w r) |
| 17:38:39 | <tomsmeding> | no linear arrows here |
| 17:38:47 | <hellwolf> | without the multiplicity, you can use it anytime, just need to check if that introduces problem |
| 17:38:49 | <tomsmeding> | this does not at all address sharing |
| 17:38:55 | <tomsmeding> | sharing is orthogonal to the versioning issue |
| 17:39:08 | <hellwolf> | okay, that's an observation I need to digest a little. |
| 17:39:26 | <tomsmeding> | as in, sharing recovery to prevent duplicate computation or duplicate side-effects |
| 17:39:45 | <tomsmeding> | this particular encoding is only suitable for interpreting directly, not for compilation |
| 17:40:01 | <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' |
| 17:40:15 | <hellwolf> | I get that. |
| 17:40:25 | <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 |
| 17:40:39 | <tomsmeding> | but the API doesn't ever let you do something "after" a Fr operation |
| 17:40:44 | <tomsmeding> | there's no (>>=) |
| 17:40:45 | <hellwolf> | and you do not expose the "cps" starter which you can use to cheat |
| 17:40:53 | <tomsmeding> | yes |
| 17:41:03 | <tomsmeding> | I'm actually not completely sure the 'cps' function was broken |
| 17:41:27 | <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 |
| 17:41:33 | <tomsmeding> | which, if not unsound, is certainly strange |
| 17:42:10 | <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 |
| 17:42:28 | <tomsmeding> | but without the 'cps' function, that worry should, hopefully, not exist |
| 17:43:32 | <tomsmeding> | as you can see in 'main', the code is awkward CPS-style |
| 17:43:42 | <hellwolf> | cps and Cont monad is the same thing, if you try, right? |
| 17:43:45 | <tomsmeding> | but the point of this experiment is that it's very low-tech |
| 17:43:45 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 17:43:52 | <tomsmeding> | eh |
| 17:44:01 | <tomsmeding> | the 'cps' function was awfully named |
| 17:44:14 | <tomsmeding> | continuation-passing style is the kind of code that you see in MainCPS |
| 17:44:35 | <tomsmeding> | Cont is a monad that runs everything in CPS |
| 17:44:37 | <tomsmeding> | @src ContT |
| 17:44:37 | <lambdabot> | newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r } |
| 17:45:02 | <tomsmeding> | a computation that produces an 'a' is a function that, given a _continuation_ taking an 'a', runs that continuation |
| 17:45:07 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 17:45:19 | <hellwolf> | 05-08 20:43 <tomsmeding> but the point of this experiment is that it's very low-tech |
| 17:45:19 | <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. |
| 17:45:20 | <tomsmeding> | but Cont(T) assumes that that 'm' doesn't change, and we want it to change |
| 17:45:24 | × | manwithluck quits (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 17:45:31 | <tomsmeding> | right |
| 17:45:38 | <hellwolf> | tomsmeding:sure, but I had to change standard monad too |
| 17:45:44 | <hellwolf> | "graded Cont" |
| 17:45:49 | → | manwithluck joins (~manwithlu@2a09:bac5:5081:2dc::49:f6) |
| 17:45:55 | <hellwolf> | just don't pronounce that in front of a brit. |
| 17:46:07 | <tomsmeding> | I tried to do this kind of versioning in a monad style but I couldn't, not without linear types |
| 17:46:12 | <tomsmeding> | doesn't mean that it can't be done |
| 17:46:26 | <tomsmeding> | but I think this Fr thing, outside of a monad, does work |
| 17:46:41 | <hellwolf> | I havent' found a hole yet |
| 17:46:44 | <tomsmeding> | yay |
| 17:46:47 | <hellwolf> | I might get back to you after I finish the code gen. |
| 17:46:51 | <hellwolf> | and look this again |
| 17:47:05 | <hellwolf> | If I were to write an article, I need to be a little bit complete and surveying around. |
| 17:47:07 | <hellwolf> | this is a good one. |
| 17:47:37 | <tomsmeding> | this stuff is dangerous for my phd thesis, by the way, because messing around with fun FP stuff is more fun than writing |
| 17:48:00 | <hellwolf> | :D .... 5 years then panic |
| 17:48:05 | <hellwolf> | before that all dandy |
| 17:48:48 | <hellwolf> | but what's your phd is about, not FP?! |
| 17:49:36 | <tomsmeding> | also FP but writing a literature overview is unfun |
| 17:50:03 | <tomsmeding> | https://arxiv.org/pdf/2207.03418 https://dl.acm.org/doi/pdf/10.1145/3632878 |
| 17:50:28 | <tomsmeding> | "applied FP"? |
| 17:50:31 | <tomsmeding> | if that's a thing |
| 17:50:51 | <tomsmeding> | still fairly theoretical, and there's a bit of FP fun in there too, but not as fundamental as this |
| 17:50:55 | <int-e> | . o O ( https://arxiv.org/abs/2207.03418 ) |
| 17:51:20 | <tomsmeding> | int-e: what do you get from the /abs/ page? |
| 17:51:33 | <int-e> | tomsmeding: the title, abstract and meta information |
| 17:51:46 | <tomsmeding> | I guess the metadata is useful, yes |
| 17:51:59 | <hellwolf> | efficient chad... I can run a crypto scam meme coin with this title. |
| 17:52:06 | <tomsmeding> | :D |
| 17:52:06 | <EvanR> | differentiates most of haskell 98. So haskell 98 is differentiable, i.e. pretty smooth |
| 17:52:17 | <tomsmeding> | EvanR: the one does not imply the other |
| 17:52:36 | <EvanR> | pretty smooth as in "I'm pretty sure..." |
| 17:52:51 | <tomsmeding> | in the sense of AD, I can differentiate a function Int -> Int just fine: its derivative is trivial, () -> () |
| 17:52:58 | <tomsmeding> | because Int is discrete :) |
| 17:53:15 | <EvanR> | ok makes sense |
| 17:56:29 | <tomsmeding> | EvanR: damn, I should have replied "but not as smooth as CHAD" |
| 17:56:59 | <EvanR> | CHAD |
| 17:57:05 | <EvanR> | EXPLAIN |
| 17:57:14 | <tomsmeding> | combinatory homomorphic automatic differentiation |
| 17:57:21 | <tomsmeding> | except that there aren't even any combinators any more |
| 17:58:00 | <EvanR> | so you're saying it's not even combinatory, or differentiation |
| 17:58:18 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:58:19 | <EvanR> | HA |
| 17:58:19 | <tomsmeding> | there's definitely a big homomorphism, and it's definitely automatic differentiation |
| 17:58:19 | × | manwithluck quits (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 17:58:23 | <tomsmeding> | but we did away with the combinators |
| 17:58:27 | <tomsmeding> | it HAD combinators |
| 17:58:35 | <EvanR> | HAD |
| 17:58:41 | <EvanR> | good one |
| 17:58:47 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 17:59:07 | → | manwithluck joins (~manwithlu@2a09:bac5:5081:2dc::49:f6) |
| 17:59:34 | <EvanR> | you could called it HAD combinators |
| 17:59:43 | <tomsmeding> | wouldn't sell as well, though |
| 17:59:46 | <EvanR> | lol |
| 18:00:06 | <tomsmeding> | the combinators were unreadable |
| 18:00:20 | <EvanR> | that's why it's past tense |
| 18:00:27 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 18:00:59 | <tomsmeding> | https://arxiv.org/pdf/2103.15776v2 section 9.2, the typesetting/layout doesn't help |
| 18:01:30 | <tomsmeding> | it's on the lambda calculus now if you look at later versions |
| 18:01:54 | <tomsmeding> | the neatest presentation of the code transformation, IMO, is in https://dl.acm.org/doi/pdf/10.1145/3632878 figure 2 |
| 18:02:35 | <tomsmeding> | if you have layout suggestions for that D[case] equation, I'm all ears |
| 18:02:43 | <tomsmeding> | this multi-line left-hand side is just awful |
| 18:09:08 | → | j1n37- joins (~j1n37@user/j1n37) |
| 18:09:50 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 18:10:34 | Digitteknohippie | is now known as Digit |
| 18:10:39 | × | kuribas quits (~user@ptr-17d51eo8yjf3h7nzszs.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 18:12:08 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 18:12:56 | <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? |
| 18:13:05 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 18:13:15 | <hellwolf> | there is not an extensive set of API, hard for me to think of all cases. |
| 18:13:23 | <hellwolf> | but I am following some hunch |
| 18:13:47 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 18:15:53 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 18:18:51 | <hellwolf> | simplest API: write to a "storage" location multiple times with (+ 1) |
| 18:19:14 | <hellwolf> | which also returns the value, which one do you return? |
| 18:19:59 | <hellwolf> | pardon me, if I brain farted. I am multitasking :/ |
| 18:21:15 | → | Guest48 joins (~Guest48@104.156.111.174) |
| 18:21:54 | <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' |
| 18:22:11 | <tomsmeding> | because that's the only function that produces a Fr without taking yet another callback |
| 18:23:52 | <tomsmeding> | notice that all functions (except 'finish') return precisely what their callback returns |
| 18:23:56 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 18:24:04 | <hellwolf> | yea. hence the ergonomics of $ \x -> |
| 18:24:23 | <hellwolf> | vs. the infamous linear-types "& \x ->" chains |
| 18:24:33 | <hellwolf> | with a symbol difference. |
| 18:24:49 | <tomsmeding> | right |
| 18:24:51 | <hellwolf> | maybe there is some interesting duo/correspondance there. |
| 18:25:01 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 18:26:12 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 18:26:35 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 18:29:55 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:34:10 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 18:34:23 | → | acidjnk joins (~acidjnk@p200300d6e71c4f49f4d0e34d1c0f8686.dip0.t-ipconnect.de) |
| 18:37:24 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 18:40:32 | × | manwithluck quits (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Remote host closed the connection) |
| 18:40:57 | → | manwithluck joins (~manwithlu@2a09:bac5:5081:2dc::49:f6) |
| 18:44:02 | × | Guest48 quits (~Guest48@104.156.111.174) (Quit: Client closed) |
| 18:47:46 | × | myme quits (~myme@2a01:799:d5e:5f00:5054:783f:d768:b894) (Ping timeout: 276 seconds) |
| 18:48:05 | → | myme joins (~myme@2a01:799:d5e:5f00:1c16:e41e:c241:8a37) |
| 18:50:34 | <[exa]> | evening everyone |
| 18:51:27 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 18:51:33 | × | manwithluck quits (~manwithlu@2a09:bac5:5081:2dc::49:f6) (Ping timeout: 248 seconds) |
| 18:52:08 | → | j1n37 joins (~j1n37@user/j1n37) |
| 18:52:24 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 18:56:25 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 18:58:20 | <tomsmeding> | what language have you been programming in today |
| 18:59:26 | <EvanR> | LLM infused C, for the proofs |
| 18:59:59 | <darkling> | I've written about a dozen lines of bash, and installed Debian on a spare machine. |
| 19:00:02 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:12 | <darkling> | Light duty. :) |
| 19:00:22 | <mauke> | perl, sql |
| 19:00:32 | <Athas> | I've done a bit of Julia and of course always Haskell. |
| 19:00:39 | <tomsmeding> | EvanR: what part was about the proofs, the LLM-infused part or the other part |
| 19:00:41 | → | caconym7 joins (~caconym@user/caconym) |
| 19:01:00 | <mauke> | but I read a bit about algebraic data types in C |
| 19:01:00 | <Athas> | Whenever I use non-Haskell languages I end up annoyed with how complicated their semantics are (although Julia is really not so bad). |
| 19:01:25 | <tomsmeding> | I think Haskell has tricky enough semantics too, sometimes |
| 19:01:39 | <tomsmeding> | but if you're used to them, they make sense :) |
| 19:01:51 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:01:59 | <EvanR> | it's true |
| 19:02:04 | <EvanR> | haskell can get non trivial |
| 19:02:16 | [exa] | did haskell+julia+bash |
| 19:02:19 | <tomsmeding> | the static semantics can get _highly_ non-trivial |
| 19:02:19 | <EvanR> | luckily there's a lot you can do which is trivially rightr |
| 19:02:21 | <EvanR> | right |
| 19:02:32 | <EvanR> | "obviously right" |
| 19:02:44 | <tomsmeding> | two people who did Julia today! |
| 19:02:45 | <Athas> | I mean the dynamic semantics. I can deal with complicated type systems much better. |
| 19:03:01 | <tomsmeding> | haskell has very tame dynamic semantics |
| 19:03:05 | <Athas> | "This program will not compile" is a much easier problem to deal with than "this program produces a bogus result". |
| 19:03:09 | <Athas> | Yes, exactly. I like that. |
| 19:03:11 | <tomsmeding> | :) |
| 19:03:35 | <[exa]> | julia is such a love/hate trigger |
| 19:03:45 | <tomsmeding> | mauke: how does one do algebraic data types in C? |
| 19:03:50 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 19:04:12 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 19:04:17 | <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. |
| 19:04:21 | <tomsmeding> | even std::variant in C++ is a mere shade of proper sum types |
| 19:04:44 | <Athas> | Julia people do absolutely awful things with metaprogramming, though. Makes template haskell look well-behaved. |
| 19:05:26 | <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? |
| 19:05:47 | <[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 |
| 19:06:15 | <mauke> | tomsmeding: peep and weep: https://github.com/Hirrolot/datatype99 |
| 19:06:45 | <mauke> | (yes, it's cpp abuse) |
| 19:07:04 | <tomsmeding> | I assumed it was cpp abuse before clicking the link |
| 19:07:47 | <Athas> | [exa]: no, I didn't poke that deep yet. |
| 19:08:05 | <Athas> | tomsmeding: yes, macros, which they use to implement things like, say, an AD library. |
| 19:08:13 | <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? |
| 19:08:17 | <Athas> | Considering the size of the hammer, it works remarkably well. |
| 19:08:42 | <tomsmeding> | Athas: I'm not actually sure I dislike that use of metaprogramming |
| 19:08:47 | <tomsmeding> | how else would you do AD? |
| 19:09:10 | <mauke> | tomsmeding: useless as in they expose library internals, I assume |
| 19:09:20 | <Athas> | Operator overloading or a proper compiler plugin, maybe. Or actually built into the language. |
| 19:09:24 | <[exa]> | tomsmeding: would you do AD in template haskell evaluated at runtime? |
| 19:09:42 | <tomsmeding> | right, the other two options are a compiler plugin or operator overloading |
| 19:10:00 | <tomsmeding> | writing a compiler plugin is always fraught because now you're at the whims of compiler developers that change APIs |
| 19:10:08 | <mauke> | the options don't affect macro expansion, only error reporting |
| 19:10:21 | <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. |
| 19:10:29 | <tomsmeding> | and operator overloading either gets you in the weeds of embedded language design, sharing recovery, etc., or is slower than static AD |
| 19:10:46 | <tomsmeding> | mauke: right |
| 19:11:02 | <tomsmeding> | oh I see, it's for backtrace tracking for diagnostics |
| 19:11:03 | <Athas> | In contrast, Template Haskell is probably the source of 90% of my Haskell hassle, and I barely use it at all. |
| 19:11:47 | <[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. |
| 19:12:07 | <[exa]> | (yeah the REPL is so cool for people who never saw a good terminal app) |
| 19:12:25 | <tomsmeding> | [exa]: is the person writing the code normally not a sciencey guy? |
| 19:13:08 | <Athas> | That's an interesting point. It may be that Julia does break often, but not in ways that matter for the users. |
| 19:13:10 | <[exa]> | tomsmeding: writing the code yeah, but the users here are also kinda scientists |
| 19:13:44 | <tomsmeding> | I would expect a sciencey person to write the code, and there to be a programmer person beside ready to fix stuff. :P |
| 19:13:59 | <tomsmeding> | but you put the sciencey person on the side, so now I wonder who the programmer is :) |
| 19:14:00 | <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. |
| 19:14:18 | <tomsmeding> | what's the problem with 14 autodiff libraries? |
| 19:14:23 | <[exa]> | tomsmeding: yeah that's my last 4 publications or so :D |
| 19:14:45 | <[exa]> | (the fixy computer guy, not the autodiff libs :D ) |
| 19:14:51 | <tomsmeding> | :) |
| 19:14:55 | <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. |
| 19:15:14 | <tomsmeding> | Athas: that explanation assumes there is good reason for there to be 14 libraries |
| 19:15:32 | <tomsmeding> | not knowing what those 14 are, I would rather expect there could have been 3, but people just felt like writing their own |
| 19:15:57 | <Athas> | tomsmeding: well, depends on what you mean by "good", but looking at the list it doesn't look like merely itch-scratching. |
| 19:16:19 | <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. |
| 19:16:21 | <tomsmeding> | okay, then it is somewhat converning, yes |
| 19:16:23 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 244 seconds) |
| 19:16:28 | <tomsmeding> | *concerning |
| 19:16:37 | <Athas> | It may also suggest that in Julia it is just incredibly easy and fun to write AD libraries, who knows. |
| 19:16:49 | tomsmeding | would suspect that is a decent part of the cause |
| 19:16:51 | <[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. |
| 19:16:54 | <Athas> | They have so many of them that there is a meta-project for collating them: https://juliadiff.org/ It's amazing! |
| 19:17:20 | <Athas> | Julia is probably the most vigorous and interesting community for people who care about AD, but it is also surprisingly messy. |
| 19:17:50 | <[exa]> | ah there's the megacommunity for ODE solving :D :D |
| 19:18:04 | <[exa]> | that's got like 6 gazillion packages for everything |
| 19:18:07 | <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). |
| 19:18:19 | <Athas> | In Haskell we have 'ad' which is good but slow, and hopefully horde-ad in the future! |
| 19:19:08 | <tomsmeding> | I still find it amazing that Julia has an AD library that _differentiates LLVM IR_ |
| 19:19:20 | <tomsmeding> | and apparently it's usefully performant! |
| 19:19:23 | <Athas> | That's just Enzyme. C++ has that too. |
| 19:19:43 | <tomsmeding> | I would expect that you've lost too much structure at that point |
| 19:20:17 | <[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 |
| 19:20:25 | <Athas> | Welllll, Julia does JIT-compilation based on types, so the LLVM IR doesn't look so weird. |
| 19:20:29 | <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 |
| 19:20:40 | <Athas> | I think one could also use Enzyme to differentiate Haskell actually, but the laziness might make it difficult. |
| 19:21:05 | <Athas> | tomsmeding: (i) it is not fast for that reason. (ii) it is not _really_ fast depending on what you expect. |
| 19:22:16 | <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? |
| 19:22:42 | <Athas> | A naive matrix multiplication? Yes. |
| 19:22:54 | <tomsmeding> | cool |
| 19:23:03 | <Athas> | But it will not do as well with a heavily optimised one. |
| 19:23:06 | <tomsmeding> | sure |
| 19:24:20 | <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. |
| 19:25:39 | <[exa]> | research software quality™ |
| 19:25:55 | <Athas> | Now now, research software doesn't have to be that way. GHC is research software. |
| 19:26:25 | <[exa]> | ghc is done by researchers who literally do the research to eliminate corner cases and have good code |
| 19:27:05 | <[exa]> | which kinda biases the choices :D |
| 19:27:31 | <tomsmeding> | I think "AD on LLVM IR" is naturally a fairly plentiful source of corner cases |
| 19:27:48 | <[exa]> | for many others it's "yeah so my problem X is finally computed, I can delete my github account now" |
| 19:29:25 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 19:29:34 | <tomsmeding> | also, if there are people paid to make the thing more stable (GHC), can you really consider it "research software" any more? |
| 19:29:50 | <tomsmeding> | people also do research on LLVM, but LLVM is not considered research software |
| 19:30:41 | <[exa]> | yeah well, I meant that kind of "research software" where there's a postdoc, a problem, and 3 years of funding |
| 19:31:01 | <Athas> | GHC was well documented and such before it had industrial financing. |
| 19:31:22 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 19:31:22 | ljdarj1 | is now known as ljdarj |
| 19:35:26 | <[exa]> | Athas: well the question then is what happened that differentiated these |
| 19:35:57 | <[exa]> | ("differentiated" not as in AD now! :D ) |
| 19:36:53 | <tomsmeding> | I have to prevent myself so often from writing "we can derive xyz equations" when talking about AD |
| 19:36:59 | <Athas> | Not sure. It may be something as trivial as most programmers don't like writing documentation, so they don't. |
| 19:37:20 | <Athas> | tomsmeding: the most difficult part of implementing AD in Haskell is that the usual x' convention becomes confusing. |
| 19:37:44 | tomsmeding | doesn't get |
| 19:38:17 | <tomsmeding> | how do variable naming conventions make implementing AD harder? |
| 19:39:14 | <sprout> | derivative naming? |
| 19:40:03 | <tomsmeding> | just make it dx instead |
| 19:40:33 | <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. |
| 19:41:03 | <tomsmeding> | I see -- yes, "dx" is what I use |
| 19:41:10 | <Athas> | https://github.com/diku-dk/futhark/blob/master/src/Futhark/AD/Rev.hs#L5-L8 |
| 19:41:42 | <tomsmeding> | funny, I've never even thought about this being a problem |
| 19:42:15 | <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 |
| 19:42:31 | <tomsmeding> | and furthermore, is an adjoint really a derivative of a thing? |
| 19:42:48 | <tomsmeding> | with conventional meaning of "'", naming an adjoint of x as x' doesn't even make much sense |
| 19:42:56 | <Athas> | No, it's a bigger problem for forward mode (where we use a _tan suffix). |
| 19:43:21 | <tomsmeding> | ah, I think I see why I don't have problems with this |
| 19:43:43 | <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 |
| 19:44:03 | <tomsmeding> | and reverse-mode in a highly typed way where adjoints (cotangents) and primal values have _distinct types_ |
| 19:44:10 | <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 |
| 19:44:10 | <tomsmeding> | so if I confuse them, GHC yells at me |
| 19:44:23 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 19:44:46 | → | manwithluck joins (~manwithlu@2a09:bac1:5b80:20::49:f6) |
| 19:44:49 | <EvanR> | can gcc be told to use a different preprocessor |
| 19:46:14 | <tomsmeding> | ghc can be |
| 19:46:30 | <EvanR> | cool |
| 19:46:42 | <tomsmeding> | https://hackage.haskell.org/package/record-dot-preprocessor ctrl-F for "use this magic" |
| 19:51:04 | → | acidjnk_new joins (~acidjnk@p200300d6e71c4f4911c235e3ddcab2f1.dip0.t-ipconnect.de) |
| 19:51:17 | × | acidjnk quits (~acidjnk@p200300d6e71c4f49f4d0e34d1c0f8686.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 19:52:24 | <[exa]> | EvanR: for gcc, see the note below here https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html |
| 19:53:51 | → | rvalue- joins (~rvalue@user/rvalue) |
| 19:53:53 | <[exa]> | I knew a guy who did type inference in the C code as the preprocessing step, can't find the thesis now tho |
| 19:54:55 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 19:55:00 | <EvanR> | wow |
| 19:58:38 | <EvanR> | hell yeah |
| 20:00:47 | rvalue- | is now known as rvalue |
| 20:06:45 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 20:09:15 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 20:13:05 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 20:13:49 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 20:22:30 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 20:27:54 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 20:27:57 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 20:27:59 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Ping timeout: 244 seconds) |
| 20:28:22 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 20:28:57 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 20:35:49 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 20:44:02 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 20:52:00 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 20:59:25 | → | j1n37- joins (~j1n37@user/j1n37) |
| 21:01:06 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 21:11:49 | → | j1n37 joins (~j1n37@user/j1n37) |
| 21:12:49 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 21:21:03 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 21:22:54 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Ping timeout: 245 seconds) |
| 21:25:31 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 21:28:48 | → | euphores joins (~SASL_euph@user/euphores) |
| 21:39:54 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:43:15 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:43:45 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 21:44:14 | → | euleritian joins (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) |
| 21:47:28 | → | madalin` joins (~mad@89.90.150.62) |
| 21:47:59 | × | madalin` quits (~mad@89.90.150.62) (Client Quit) |
| 21:50:31 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 21:51:58 | × | ft quits (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: Lost terminal) |
| 21:52:05 | → | tromp joins (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) |
| 21:55:44 | → | ft joins (~ft@p4fc2a6e6.dip0.t-ipconnect.de) |
| 21:58:09 | × | sprotte24 quits (~sprotte24@p200300d16f4546009040e212dd81e9a6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 22:00:15 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 276 seconds) |
| 22:00:44 | × | volsand quits (~volsand@2804:1b1:1080:da6:dcbd:80c:8e7b:1cf7) (Remote host closed the connection) |
| 22:05:41 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 22:14:29 | → | mxs9 joins (~mxs@user/mxs) |
| 22:27:04 | → | chas joins (~chas@69.243.201.37) |
| 22:30:18 | → | Guest58 joins (~Guest58@2601:483:b00:d550:552d:ffa9:4fce:b2c6) |
| 22:31:43 | × | Guest58 quits (~Guest58@2601:483:b00:d550:552d:ffa9:4fce:b2c6) (Client Quit) |
| 22:33:45 | × | chas quits (~chas@69.243.201.37) (Quit: leaving) |
| 22:34:15 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 22:35:27 | × | tromp quits (~textual@2001:1c00:3487:1b00:f14f:b20f:416b:87c6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:38:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:39:24 | → | j1n37 joins (~j1n37@user/j1n37) |
| 22:39:41 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 22:40:41 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 22:41:01 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 22:41:16 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 22:42:33 | Lord_of_Life_ | is now known as Lord_of_Life |
| 22:43:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 22:48:09 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 22:53:37 | × | xff0x quits (~xff0x@2405:6580:b080:900:df43:4d2b:b873:7ac7) (Ping timeout: 248 seconds) |
| 22:54:04 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 22:54:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:54:18 | → | xff0x joins (~xff0x@2405:6580:b080:900:a861:5434:8d1e:f1de) |
| 22:59:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 22:59:58 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 23:00:24 | → | j1n37 joins (~j1n37@user/j1n37) |
| 23:04:34 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 23:07:15 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 23:07:15 | ljdarj1 | is now known as ljdarj |
| 23:09:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:13:12 | → | wbrawner joins (~wbrawner@static.205.41.78.5.clients.your-server.de) |
| 23:13:20 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 23:15:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:19:45 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 23:24:12 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 23:24:24 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:25:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:29:11 | × | xff0x quits (~xff0x@2405:6580:b080:900:a861:5434:8d1e:f1de) (Quit: xff0x) |
| 23:32:47 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 23:38:20 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 23:39:01 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 23:39:13 | → | dofsyl^ joins (~dofsyl@50.168.231.214) |
| 23:43:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:48:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:49:00 | × | acidjnk_new quits (~acidjnk@p200300d6e71c4f4911c235e3ddcab2f1.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 23:49:36 | → | xff0x joins (~xff0x@2405:6580:b080:900:200d:e23d:ad3b:4ed4) |
| 23:50:48 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:51:39 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 23:55:33 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
All times are in UTC on 2025-05-08.