Logs: liberachat/#haskell
| 2025-11-07 18:25:58 | <tomsmeding> | this is a code transformation where the types in the output code depend quite significantly on the precise structure of the input _terms- |
| 2025-11-07 18:26:04 | <tomsmeding> | s/-/_/ |
| 2025-11-07 18:28:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 18:28:53 | → | Square3 joins (~Square@user/square) |
| 2025-11-07 18:29:03 | × | Googulator68 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-07 18:29:44 | → | gmg joins (~user@user/gehmehgeh) |
| 2025-11-07 18:30:38 | <[exa]> | yeah like, I might need a week to properly soak that in |
| 2025-11-07 18:30:48 | × | Googulator41 quits (~Googulato@team.broadbit.hu) (Quit: Client closed) |
| 2025-11-07 18:30:52 | → | Googulator53 joins (~Googulato@team.broadbit.hu) |
| 2025-11-07 18:33:46 | <tomsmeding> | my advisor sometimes speaks of future a future phd student continuing work on this codebase |
| 2025-11-07 18:33:58 | <tomsmeding> | s/of future/of/ (why can't I type today) |
| 2025-11-07 18:34:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-11-07 18:37:09 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-11-07 18:37:54 | <[exa]> | "future phd student working on something" yeah I love listening to fairy tales :D |
| 2025-11-07 18:38:32 | <tomsmeding> | I've seen a phd student working on prior student projects and they were miserabl |
| 2025-11-07 18:38:34 | <tomsmeding> | e |
| 2025-11-07 18:39:31 | <tomsmeding> | there being a future phd student is actually less of a fiction than you might think in this case, he has a grant and is hiring |
| 2025-11-07 18:39:45 | <tomsmeding> | them successfully continuing work on this codebase, on the other hand... |
| 2025-11-07 18:45:14 | <tomsmeding> | this CPS stuff is yet another reason I should have written this in Agda I guess |
| 2025-11-07 18:45:32 | <tomsmeding> | there you can just return a dependent pair of whatever existential you want and call it a day |
| 2025-11-07 18:46:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 18:49:24 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-11-07 18:51:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-07 18:59:17 | × | ZLima12_ quits (~zlima12@user/meow/ZLima12) () |
| 2025-11-07 19:01:59 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 19:04:21 | × | synchromesh quits (~john@2406:5a00:2412:2c00:ad6b:d7bc:cf6f:605a) (Read error: Connection reset by peer) |
| 2025-11-07 19:05:25 | → | synchromesh joins (~john@2406:5a00:2412:2c00:ad6b:d7bc:cf6f:605a) |
| 2025-11-07 19:06:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-11-07 19:07:32 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-11-07 19:08:07 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 264 seconds) |
| 2025-11-07 19:09:40 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 2025-11-07 19:13:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 19:16:02 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-11-07 19:16:13 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 2025-11-07 19:18:14 | → | haritz joins (~hrtz@140.228.70.141) |
| 2025-11-07 19:18:14 | × | haritz quits (~hrtz@140.228.70.141) (Changing host) |
| 2025-11-07 19:18:14 | → | haritz joins (~hrtz@user/haritz) |
| 2025-11-07 19:18:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-11-07 19:23:19 | × | michalz quits (~michalz@185.246.207.215) (Remote host closed the connection) |
| 2025-11-07 19:27:03 | × | haritz quits (~hrtz@user/haritz) (Remote host closed the connection) |
| 2025-11-07 19:29:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 19:34:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-07 19:45:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 19:47:09 | × | biberu quits (~biberu@user/biberu) (Quit: ZNC - https://znc.in) |
| 2025-11-07 19:49:19 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 240 seconds) |
| 2025-11-07 19:50:12 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 2025-11-07 19:50:42 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-11-07 19:51:03 | → | ZLima12 joins (~zlima12@user/meow/ZLima12) |
| 2025-11-07 19:54:24 | <monochrom> | I would consider not indenting. E.g., line n column k: "foo \i ->", line (n+1) column k: "bar \j ->", line (n+2) column k: "x y z i j" |
| 2025-11-07 19:54:39 | <tomsmeding> | yep, that's exactly what I ended up doing |
| 2025-11-07 19:55:35 | <monochrom> | Another way (mostly to appease other people's rigid style guides) is to use ContT or Codensity, then it's just a do-block. :) |
| 2025-11-07 19:55:55 | <tomsmeding> | monochrom: does ContT really work? |
| 2025-11-07 19:56:02 | <tomsmeding> | pls teach me |
| 2025-11-07 19:56:56 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 2025-11-07 19:58:29 | <tomsmeding> | monochrom: can you write this with some monad trick? https://play.haskell.org/saved/REvWXlQd |
| 2025-11-07 19:58:43 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2025-11-07 19:58:43 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2025-11-07 19:58:43 | → | haritz joins (~hrtz@user/haritz) |
| 2025-11-07 19:59:10 | <monochrom> | Nice, I'll work with that. |
| 2025-11-07 20:00:38 | → | yauhsien joins (~Yau-Hsien@118-168-140-77.dynamic-ip.hinet.net) |
| 2025-11-07 20:01:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 20:01:41 | <EvanR> | It's a monad. I know this. </jurassicpark> |
| 2025-11-07 20:02:07 | <monochrom> | onoes there are 2 arguments! |
| 2025-11-07 20:02:28 | <monochrom> | "now there are two of them!" </phantom menace> |
| 2025-11-07 20:02:38 | <tomsmeding> | monochrom: I think that's not the biggest problem there -- you can just use a tuple |
| 2025-11-07 20:02:39 | <glguy> | uncurry it to get back to one |
| 2025-11-07 20:02:41 | <tomsmeding> | the problem is the existential |
| 2025-11-07 20:03:15 | <monochrom> | Yeah the forall may require Codensity. |
| 2025-11-07 20:03:33 | <monochrom> | err no, Codensity does forall on the other guy. |
| 2025-11-07 20:05:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-07 20:05:55 | → | Googulator34 joins (~Googulato@team.broadbit.hu) |
| 2025-11-07 20:09:08 | → | Googulator13 joins (~Googulato@team.broadbit.hu) |
| 2025-11-07 20:09:09 | × | Googulator53 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-07 20:09:09 | <Leary> | tomsmeding: https://paste.tomsmeding.com/phEkL7cc |
| 2025-11-07 20:09:27 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 2025-11-07 20:10:05 | <tomsmeding> | oh that's delightful |
| 2025-11-07 20:10:20 | <monochrom> | Intreresting |
| 2025-11-07 20:10:44 | × | Googulator13 quits (~Googulato@team.broadbit.hu) (Client Quit) |
| 2025-11-07 20:10:50 | → | Googulator11 joins (~Googulato@team.broadbit.hu) |
| 2025-11-07 20:11:28 | <EvanR> | because of that I'm now using ImpredicativeTypes everywhere |
| 2025-11-07 20:11:45 | <tomsmeding> | what makes it better is that that type for >>= is completely different from what >>= is normally supposed to be |
| 2025-11-07 20:11:46 | <monochrom> | heh |
| 2025-11-07 20:12:03 | <EvanR> | how I learned to stop worrying and love ImpredicativeTypes |
| 2025-11-07 20:13:03 | × | Googulator34 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-07 20:14:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 20:17:49 | × | Googulator11 quits (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-07 20:19:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-11-07 20:20:24 | [exa] | discovers QualifiedDo |
| 2025-11-07 20:20:29 | <tomsmeding> | Leary: it doesn't seem possible to write a generic adaptor for two-result functions like my original 'foo' to one-result functions, right? |
| 2025-11-07 20:23:58 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 2025-11-07 20:27:11 | <monochrom> | Here is the worst of both worlds, just for laughs: https://play.haskell.org/saved/YfoP6M4d |
| 2025-11-07 20:27:18 | <[exa]> | Leary: ok turns out the QualifiedDo completely solves my previous concerns, thanks again :D |
| 2025-11-07 20:28:59 | <tomsmeding> | monochrom: https://play.haskell.org/saved/VMQbllqc :p |
| 2025-11-07 20:29:11 | <tomsmeding> | once you have a data type no more cruft is necessary |
| 2025-11-07 20:29:49 | <tomsmeding> | [exa]: do you seriously think that a wacky utterly-not-a-monad QualifiedDo thing is better than nested wrapper functions |
| 2025-11-07 20:30:20 | <[exa]> | well, there's 10 levels of indentation on the table |
| 2025-11-07 20:30:26 | <monochrom> | Actually "foo :: Int -> E" and "E x1 f1 <- Identity (foo n)" is simpler. |
| 2025-11-07 20:30:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-07 20:31:00 | <monochrom> | Anyway please turn on BlockArguments >:) |
| 2025-11-07 20:31:37 | <tomsmeding> | monochrom: don't even need the Identity, in fact https://play.haskell.org/saved/clzWP2pe |
All times are in UTC.