Newest at the top
| 2025-12-28 22:07:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-28 22:07:17 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-12-28 22:04:10 +0100 | tromp | (~textual@user/tromp) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-12-28 22:02:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 22:00:44 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2025-12-28 21:50:38 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-12-28 21:47:34 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2025-12-28 21:46:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 21:45:57 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) Everything |
| 2025-12-28 21:42:57 +0100 | Square2 | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2025-12-28 21:35:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-28 21:31:50 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) stefan-__ |
| 2025-12-28 21:31:24 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) (Remote host closed the connection) |
| 2025-12-28 21:30:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 21:27:06 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) stefan-__ |
| 2025-12-28 21:26:43 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) (Remote host closed the connection) |
| 2025-12-28 21:18:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-28 21:16:30 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-12-28 21:14:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 21:13:09 +0100 | <machinedgod> | ncf: The proposal has much more information than manual - this is great, thank you again. |
| 2025-12-28 21:11:49 +0100 | <machinedgod> | Oh, I see! I didn't even notice the Consumable constraint! Thank you, now I know at least my intuition was at the right place. |
| 2025-12-28 21:11:15 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) stefan-__ |
| 2025-12-28 21:09:34 +0100 | stefan-__ | (~m-yh2rcc@42dots.de) (Remote host closed the connection) |
| 2025-12-28 21:03:33 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-12-28 20:58:24 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 252 seconds) |
| 2025-12-28 20:51:34 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2025-12-28 20:46:52 +0100 | zfnmxt | (~m-gkkevi@209.209.10.107) (Ping timeout: 246 seconds) |
| 2025-12-28 20:44:51 +0100 | <ncf> | the fst and snd from linear-base have a Consumable constraint on the field that's being discarded, so there's no magic there |
| 2025-12-28 20:44:23 +0100 | <ncf> | machinedgod: record projections take an unrestricted record unless there's only a single field, see https://ghc-proposals.readthedocs.io/en/latest/proposals/0111-linear-types.html#records-and-projec… |
| 2025-12-28 20:43:56 +0100 | wennefer0_ | (~wennefer0@user/wennefer0) (Client Quit) |
| 2025-12-28 20:41:44 +0100 | wennefer0_ | (~wennefer0@user/wennefer0) wennefer0 |
| 2025-12-28 20:39:27 +0100 | <machinedgod> | (sorry for the wall of text - didn't realize how much I wrote) |
| 2025-12-28 20:39:13 +0100 | <machinedgod> | and snd from linear-base do just that. Is this meant to help bridge the gaps with nonlinear code, or is linear code actually supposed to be like that? Thank you upfront. |
| 2025-12-28 20:39:07 +0100 | <machinedgod> | Hi everyone. Linear types question (mostly theoretical curiosity but practical solution is appreciated too): is it possible to make a linear function that acts just like a record selector on data? The reason I ask is because, my intuition says - I will have to ignore (consume) all the fields except the one I need when I pattern match, therefore it violates linearity. However, linear versions of fst |
| 2025-12-28 20:37:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-28 20:37:42 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-12-28 20:35:20 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
| 2025-12-28 20:33:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 20:22:01 +0100 | earthy | (~arthurvl@2a02-a469-f5e2-1-83d2-ca43-57a2-dc81.fixed6.kpn.net) (Quit: ein reboot macht gut) |
| 2025-12-28 20:20:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-28 20:18:25 +0100 | bionade24 | (~quassel@server2.oscloud.info) bionade24 |
| 2025-12-28 20:13:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 20:12:26 +0100 | sroso | (~sroso@user/SrOso) SrOso |
| 2025-12-28 20:06:58 +0100 | edmerry | edm |
| 2025-12-28 20:05:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-12-28 20:02:05 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-12-28 20:01:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 19:51:32 +0100 | tromp | (~textual@user/tromp) tromp |
| 2025-12-28 19:49:27 +0100 | Square2 | (~Square@user/square) Square |
| 2025-12-28 19:47:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |