Newest at the top
| 2025-11-07 20:23:19 +0100 | michalz | (~michalz@185.246.207.215) (Remote host closed the connection) |
| 2025-11-07 20:18:43 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-11-07 20:18:14 +0100 | haritz | (~hrtz@user/haritz) haritz |
| 2025-11-07 20:18:14 +0100 | haritz | (~hrtz@140.228.70.141) (Changing host) |
| 2025-11-07 20:18:14 +0100 | haritz | (~hrtz@140.228.70.141) |
| 2025-11-07 20:16:13 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-11-07 20:16:02 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-11-07 20:13:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-07 20:09:40 +0100 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-11-07 20:08:07 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 264 seconds) |
| 2025-11-07 20:07:32 +0100 | peterbecich | (~Thunderbi@172.222.148.214) peterbecich |
| 2025-11-07 20:06:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-11-07 20:05:25 +0100 | synchromesh | (~john@2406:5a00:2412:2c00:ad6b:d7bc:cf6f:605a) synchromesh |
| 2025-11-07 20:04:21 +0100 | synchromesh | (~john@2406:5a00:2412:2c00:ad6b:d7bc:cf6f:605a) (Read error: Connection reset by peer) |
| 2025-11-07 20:01:59 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-07 19:59:17 +0100 | ZLima12_ | (~zlima12@user/meow/ZLima12) () |
| 2025-11-07 19:51:13 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-07 19:49:24 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-11-07 19:46:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-07 19:45:32 +0100 | <tomsmeding> | there you can just return a dependent pair of whatever existential you want and call it a day |
| 2025-11-07 19:45:14 +0100 | <tomsmeding> | this CPS stuff is yet another reason I should have written this in Agda I guess |
| 2025-11-07 19:39:45 +0100 | <tomsmeding> | them successfully continuing work on this codebase, on the other hand... |
| 2025-11-07 19:39:31 +0100 | <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 19:38:34 +0100 | <tomsmeding> | e |
| 2025-11-07 19:38:32 +0100 | <tomsmeding> | I've seen a phd student working on prior student projects and they were miserabl |
| 2025-11-07 19:37:54 +0100 | <[exa]> | "future phd student working on something" yeah I love listening to fairy tales :D |
| 2025-11-07 19:37:09 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-11-07 19:34:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-11-07 19:33:58 +0100 | <tomsmeding> | s/of future/of/ (why can't I type today) |
| 2025-11-07 19:33:46 +0100 | <tomsmeding> | my advisor sometimes speaks of future a future phd student continuing work on this codebase |
| 2025-11-07 19:30:52 +0100 | Googulator53 | (~Googulato@team.broadbit.hu) |
| 2025-11-07 19:30:48 +0100 | Googulator41 | (~Googulato@team.broadbit.hu) (Quit: Client closed) |
| 2025-11-07 19:30:38 +0100 | <[exa]> | yeah like, I might need a week to properly soak that in |
| 2025-11-07 19:29:44 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-11-07 19:29:03 +0100 | Googulator68 | (~Googulato@team.broadbit.hu) (Ping timeout: 250 seconds) |
| 2025-11-07 19:28:53 +0100 | Square3 | (~Square@user/square) Square |
| 2025-11-07 19:28:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-07 19:26:04 +0100 | <tomsmeding> | s/-/_/ |
| 2025-11-07 19:25:58 +0100 | <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 19:25:42 +0100 | Googulator41 | (~Googulato@team.broadbit.hu) |
| 2025-11-07 19:25:09 +0100 | <tomsmeding> | and I feel like if I hadn't, that probability would have been <5% |
| 2025-11-07 19:24:51 +0100 | <tomsmeding> | the former is "because it means that when I manage to make the bloody thing typecheck it has an 80% chance of being correct" |
| 2025-11-07 19:24:32 +0100 | <tomsmeding> | s/lolo/lol/ |
| 2025-11-07 19:24:26 +0100 | <tomsmeding> | the latter is "because this is phd research lolo" |
| 2025-11-07 19:24:18 +0100 | <tomsmeding> | then I proceeded to implement complicated algorithms in it |
| 2025-11-07 19:23:55 +0100 | <tomsmeding> | I made the decision to make the embedded language in this compiler strongly typed |
| 2025-11-07 19:23:26 +0100 | <[exa]> | y u so complex programs |
| 2025-11-07 19:22:34 +0100 | <tomsmeding> | ^ |
| 2025-11-07 19:22:30 +0100 | <tomsmeding> | I can write a custom data type for each of these functions, but I don't think that's better |
| 2025-11-07 19:22:29 +0100 | <int-e> | (CPS isn't that horrible, compared to having ad-hoc existential data types) |