Newest at the top
| 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) |
| 2025-11-07 19:22:03 +0100 | <tomsmeding> | if I put 'Identity' in that continuation then GHC complains on the use of 'Identity' that it can't match variables "because type variable ‘env'1’ would escape its scope" |
| 2025-11-07 19:22:00 +0100 | <int-e> | yeah I don't think you'll get rid of that conveniently |
| 2025-11-07 19:21:22 +0100 | <tomsmeding> | int-e: I have functions that return stuff with existentials; I implement them currently in CPS style by having them take a continuation with some foralls |
| 2025-11-07 19:21:05 +0100 | <int-e> | but isn't nice :P |
| 2025-11-07 19:20:55 +0100 | <int-e> | `Refl <- pure ...` should have a chance |
| 2025-11-07 19:20:29 +0100 | <tomsmeding> | [exa]: I tried just now, doesn't seem to eat the existentials |
| 2025-11-07 19:19:51 +0100 | <int-e> | IIUC you can't let-bind type evidence |
| 2025-11-07 19:19:16 +0100 | <[exa]> | might be arrows. |
| 2025-11-07 19:18:45 +0100 | <[exa]> | other than that no actual idea, it's brutal |
| 2025-11-07 19:18:36 +0100 | <[exa]> | in Identity do? |
| 2025-11-07 19:18:30 +0100 | <[exa]> | could you run the whole thing in Identity, replace the single-cases with binding? |
| 2025-11-07 19:17:56 +0100 | <tomsmeding> | 15 was actually an understatement, getting 20 levels here |
| 2025-11-07 19:17:43 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-11-07 19:16:28 +0100 | <tomsmeding> | [exa]: I ran hindent on the thing, is this better? https://paste.tomsmeding.com/OgCpjy7u |
| 2025-11-07 19:15:43 +0100 | Googulator68 | (~Googulato@team.broadbit.hu) |
| 2025-11-07 19:15:40 +0100 | Googulator69 | (~Googulato@team.broadbit.hu) (Quit: Client closed) |
| 2025-11-07 19:15:30 +0100 | haritz | (~hrtz@user/haritz) (Remote host closed the connection) |
| 2025-11-07 19:15:23 +0100 | img | (~img@user/img) img |
| 2025-11-07 19:15:07 +0100 | <[exa]> | tomsmeding: oh wait ok I see |
| 2025-11-07 19:14:41 +0100 | haritz | (~hrtz@user/haritz) haritz |
| 2025-11-07 19:14:41 +0100 | haritz | (~hrtz@140.228.70.141) (Changing host) |
| 2025-11-07 19:14:41 +0100 | haritz | (~hrtz@140.228.70.141) |
| 2025-11-07 19:14:35 +0100 | <tomsmeding> | semantically it's just a long list of let bindings, it's just that the language forces me to make some of those callbacks because of existentials |
| 2025-11-07 19:14:07 +0100 | <tomsmeding> | or even organise this |
| 2025-11-07 19:14:05 +0100 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-11-07 19:14:04 +0100 | <tomsmeding> | [exa]: I'm honestly open for suggestions how to properly format this |
| 2025-11-07 19:13:52 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-11-07 19:13:14 +0100 | <tomsmeding> | [exa]: and end up with 15 levels deep indentation? |
| 2025-11-07 19:12:54 +0100 | comonad | (~comonad@p200300d02741a000c6934c09e8b46dfd.dip0.t-ipconnect.de) |
| 2025-11-07 19:12:41 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-07 19:06:55 +0100 | <[exa]> | tomsmeding: you should run hindent on that thing, it reads .... less chaotically I guess |
| 2025-11-07 19:06:08 +0100 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-11-07 19:05:40 +0100 | <[exa]> | I'll simply write a note for myself here to never try to golf contT into this :D |