Newest at the top
| 2025-02-10 00:35:15 +0100 | robertm | (robertm@lattice.rojoma.com) robertm |
| 2025-02-10 00:32:48 +0100 | robertm | (robertm@lattice.rojoma.com) (Quit: WeeChat 3.8) |
| 2025-02-10 00:28:37 +0100 | xff0x | (~xff0x@2405:6580:b080:900:f597:997a:28cf:fd48) |
| 2025-02-10 00:18:55 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Remote host closed the connection) |
| 2025-02-10 00:16:00 +0100 | xff0x | (~xff0x@2405:6580:b080:900:f1ee:cf4b:ec98:147a) (Client Quit) |
| 2025-02-10 00:13:48 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-10 00:13:10 +0100 | xff0x | (~xff0x@2405:6580:b080:900:f1ee:cf4b:ec98:147a) |
| 2025-02-10 00:12:00 +0100 | xff0x | (~xff0x@2405:6580:b080:900:a75:2366:4e5c:4ce9) (Ping timeout: 246 seconds) |
| 2025-02-10 00:09:29 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-10 00:07:36 +0100 | ljdarj1 | ljdarj |
| 2025-02-10 00:07:36 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-02-10 00:04:25 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-10 00:01:07 +0100 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) myxokephale |
| 2025-02-09 23:59:39 +0100 | lunitur | (~halloy485@2a00:1bb8:11c:a9a5:5d31:a95b:66b2:d7f4) (Ping timeout: 265 seconds) |
| 2025-02-09 23:53:43 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-02-09 23:48:09 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Client Quit) |
| 2025-02-09 23:48:04 +0100 | mange | (~user@user/mange) mange |
| 2025-02-09 23:48:02 +0100 | <haskellbridge> | <Bowuigi> Sorry, "(x : k) -> t" is visible quantification, "{x : k} t" is invisible |
| 2025-02-09 23:48:01 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
| 2025-02-09 23:46:56 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
| 2025-02-09 23:46:19 +0100 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-02-09 23:46:00 +0100 | <haskellbridge> | <Bowuigi> Currently I have "func : {a b : *} (f : * -> *) a -> f b = ...", where a and b are invisibly quantified (AKA their applications are inferred) and f is visibly quantified (AKA you must apply it as if it was a term), with "func @A @B F" as the application syntax |
| 2025-02-09 23:42:26 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 248 seconds) |
| 2025-02-09 23:39:58 +0100 | <haskellbridge> | <Bowuigi> In general I mean, not just in Haskell |
| 2025-02-09 23:39:36 +0100 | <haskellbridge> | <Bowuigi> Related, which syntax for visible and invisible foralls is preferred nowadays? |
| 2025-02-09 23:38:01 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
| 2025-02-09 23:25:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-09 23:21:06 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-09 23:07:58 +0100 | tabaqui1 | (~root@87.200.129.102) (Ping timeout: 244 seconds) |
| 2025-02-09 23:05:14 +0100 | <haskellbridge> | <Bowuigi> Gotta continue with my not-grad-student research then lol |
| 2025-02-09 23:04:50 +0100 | <haskellbridge> | <Bowuigi> True lol |
| 2025-02-09 23:04:19 +0100 | <tomsmeding> | anyway we're doing talismanick's grad student's research for them :) |
| 2025-02-09 23:03:41 +0100 | <tomsmeding> | you also have to render whenever the original program _shares_ a monoid value: with `let x = ... ; f y = y ++ y in putStrLn (f x x)`, if you don't take care, you're going to compute x twice (whereas this program as written only computes x once) |
| 2025-02-09 23:03:00 +0100 | <haskellbridge> | <Bowuigi> And if the entire pipeline is exposed to GHC, it can do its magic, as usual |
| 2025-02-09 23:01:50 +0100 | <haskellbridge> | <Bowuigi> Obviously this means that rendering is no longer O(n) but it allows you to keep adding stuff to the monoid afterwards |
| 2025-02-09 23:01:43 +0100 | <tomsmeding> | depends on what exactly is returned from the `case`, but yes, sometimes that works |
| 2025-02-09 23:00:57 +0100 | <haskellbridge> | <Bowuigi> The case can be incorporated into the pipeline by just composing that function with the unrendered value in most cases. As for IO, that's what I mean by "absolutely necessary" |
| 2025-02-09 23:00:56 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-02-09 22:59:04 +0100 | <tomsmeding> | or what if the original program put the String in a `case`? Can't evaluate that `case` without rendering |
| 2025-02-09 22:58:22 +0100 | <haskellbridge> | <Bowuigi> Indeed, the same can be said for the other Cayley transformations |
| 2025-02-09 22:58:20 +0100 | <tomsmeding> | Bowuigi: what if the original program passed the String to `putStrLn`? You'll have to render it at that point. |
| 2025-02-09 22:57:52 +0100 | <tomsmeding> | talismanick: also this is only beneficial for monoids where the wrong associativity is actually slow; doing Cayley to `Sum Int` will only make everything slow |
| 2025-02-09 22:57:26 +0100 | <haskellbridge> | <Bowuigi> You can modify the composition directly, as I've shown before |
| 2025-02-09 22:57:06 +0100 | <tomsmeding> | right, but you're going to auto-transform, you'll have to render sometimes |
| 2025-02-09 22:56:55 +0100 | <haskellbridge> | <Bowuigi> Yeah, tho I'd recommend not rendering unless absolutely necessary |
| 2025-02-09 22:56:38 +0100 | <tomsmeding> | i.e. if you `let x = lit "abc" . lit "def" . lit "ghi" in f (render x) (render x)` then you're doing work twice |
| 2025-02-09 22:56:03 +0100 | <tomsmeding> | it's tricky, because rendering is not O(1), so if you render, you want to continue computation with the rendered value, not the composition you had before |
| 2025-02-09 22:55:27 +0100 | <haskellbridge> | <Bowuigi> Just use the definitions above, doesn't require wrappers or anything like that |
| 2025-02-09 22:54:50 +0100 | <talismanick> | yes, I was thinking about how best to automate that process |
| 2025-02-09 22:54:24 +0100 | <haskellbridge> | <Bowuigi> I call it the Cayley monoid (technically "Cayley monoid of a monoid M", or just "Cayley monoid of M") because of that one theorem |