| 2026-03-12 00:01:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 00:02:48 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) (Ping timeout: 264 seconds) |
| 2026-03-12 00:04:32 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-03-12 00:06:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-03-12 00:07:44 +0100 | Guest34 | (~Guest34@134.197.0.20) |
| 2026-03-12 00:08:13 +0100 | Guest34 | (~Guest34@134.197.0.20) (Client Quit) |
| 2026-03-12 00:13:45 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-03-12 00:15:43 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 2026-03-12 00:16:47 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-03-12 00:16:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 00:19:48 +0100 | stackdroid18 | (~stackdroi@user/stackdroid) () |
| 2026-03-12 00:22:26 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2026-03-12 00:23:33 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 00:34:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 00:39:54 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 00:39:59 +0100 | czan | (~czan@user/mange) czan |
| 2026-03-12 00:40:43 +0100 | Square | (~Square4@user/square) Square |
| 2026-03-12 00:43:36 +0100 | Square2 | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2026-03-12 00:45:25 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-03-12 00:50:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 00:53:33 +0100 | Pozyomka | (~pyon@user/pyon) (Read error: Connection reset by peer) |
| 2026-03-12 00:54:43 +0100 | Pozyomka | (~pyon@user/pyon) pyon |
| 2026-03-12 00:55:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-03-12 01:06:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 01:09:04 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 01:11:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 01:22:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 01:27:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 01:32:10 +0100 | AlexZenon_2 | (~alzenon@5.139.232.240) |
| 2026-03-12 01:33:08 +0100 | AlexZenon | (~alzenon@5.139.232.240) (Ping timeout: 244 seconds) |
| 2026-03-12 01:33:09 +0100 | humasect_ | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 01:33:10 +0100 | AlexZenon | (~alzenon@5.139.232.240) |
| 2026-03-12 01:33:28 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 244 seconds) |
| 2026-03-12 01:33:28 +0100 | foul_owl | (~kerry@94.156.149.94) (Ping timeout: 244 seconds) |
| 2026-03-12 01:33:59 +0100 | foul_owl | (~kerry@94.156.149.94) foul_owl |
| 2026-03-12 01:33:59 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 244 seconds) |
| 2026-03-12 01:33:59 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 244 seconds) |
| 2026-03-12 01:33:59 +0100 | edwtjo | (~edwtjo@fsf/member/edwtjo) (Ping timeout: 244 seconds) |
| 2026-03-12 01:34:12 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-03-12 01:34:15 +0100 | ystael | (~ystael@user/ystael) ystael |
| 2026-03-12 01:34:31 +0100 | Tuplanolla | (~Tuplanoll@88-114-89-88.elisa-laajakaista.fi) (Ping timeout: 264 seconds) |
| 2026-03-12 01:35:30 +0100 | edwtjo | (~edwtjo@fsf/member/edwtjo) edwtjo |
| 2026-03-12 01:36:56 +0100 | AlexZenon_2 | (~alzenon@5.139.232.240) (Ping timeout: 268 seconds) |
| 2026-03-12 01:37:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 01:42:46 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 01:53:38 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 02:00:28 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-03-12 02:08:14 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 252 seconds) |
| 2026-03-12 02:11:41 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 02:11:48 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cfba:7074:7dbc:e7e9) (Ping timeout: 264 seconds) |
| 2026-03-12 02:16:36 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 02:18:34 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-03-12 02:18:46 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-03-12 02:18:56 +0100 | Square | (~Square4@user/square) (Ping timeout: 244 seconds) |
| 2026-03-12 02:19:00 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-03-12 02:20:55 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e700e503f643e9bea9c15385.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2026-03-12 02:24:43 +0100 | Square | (~Square4@user/square) Square |
| 2026-03-12 02:27:29 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 02:29:20 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-03-12 02:32:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 02:32:36 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-03-12 02:38:40 +0100 | humasect_ | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-03-12 02:43:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 02:44:40 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 02:48:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 02:59:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 03:03:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 03:05:07 +0100 | Googulator44 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 03:05:08 +0100 | Googulator7 | (~Googulato@92-249-180-22.pool.digikabel.hu) |
| 2026-03-12 03:05:33 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-03-12 03:06:06 +0100 | Googulator7 | (~Googulato@92-249-180-22.pool.digikabel.hu) (Client Quit) |
| 2026-03-12 03:06:12 +0100 | Googulator89 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:07:13 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-03-12 03:08:44 +0100 | tromp | (~textual@2001:1c00:3487:1b00:2807:b44c:c102:bda9) (Ping timeout: 252 seconds) |
| 2026-03-12 03:14:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 03:15:22 +0100 | Googulator79 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:15:31 +0100 | Googulator89 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 03:16:45 +0100 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 246 seconds) |
| 2026-03-12 03:19:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 03:26:06 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) (Ping timeout: 244 seconds) |
| 2026-03-12 03:27:00 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 03:29:40 +0100 | Googulator21 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:30:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 03:30:48 +0100 | Googulator16 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:30:51 +0100 | Googulator21 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit) |
| 2026-03-12 03:30:56 +0100 | Googulator79 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 03:31:14 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 248 seconds) |
| 2026-03-12 03:31:55 +0100 | Googulator99 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:32:11 +0100 | Googulator16 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit) |
| 2026-03-12 03:33:45 +0100 | machinedgod | (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 2026-03-12 03:36:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 03:42:26 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2026-03-12 03:42:49 +0100 | pabs3 | (~pabs3@user/pabs3) (Read error: Connection reset by peer) |
| 2026-03-12 03:44:07 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 03:44:35 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-03-12 03:48:29 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 03:49:11 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2026-03-12 03:55:02 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 03:55:17 +0100 | Googulator31 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) |
| 2026-03-12 03:55:17 +0100 | Googulator99 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 03:57:01 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-03-12 03:57:11 +0100 | Googulator10 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 03:59:14 +0100 | Googulator10 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Client Quit) |
| 2026-03-12 03:59:16 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 04:00:28 +0100 | Googulator31 | (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Ping timeout: 240 seconds) |
| 2026-03-12 04:03:18 +0100 | czan | (~czan@user/mange) (Ping timeout: 244 seconds) |
| 2026-03-12 04:05:27 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 04:05:31 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 04:05:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 04:10:32 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 04:21:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 04:26:06 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 04:31:59 +0100 | Square2 | (~Square@user/square) Square |
| 2026-03-12 04:34:18 +0100 | Square | (~Square4@user/square) (Ping timeout: 244 seconds) |
| 2026-03-12 04:37:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 04:38:07 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 264 seconds) |
| 2026-03-12 04:42:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 04:52:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 04:54:46 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-03-12 04:57:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 05:08:26 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 05:08:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 05:09:23 +0100 | <jeremyn> | \ |
| 2026-03-12 05:16:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 05:24:17 +0100 | spew | (~spew@user/spew) (Quit: nyaa~) |
| 2026-03-12 05:26:00 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 245 seconds) |
| 2026-03-12 05:26:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 05:28:12 +0100 | Square2 | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2026-03-12 05:31:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 05:37:35 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 2026-03-12 05:37:51 +0100 | DetourNe- | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-03-12 05:40:05 +0100 | DetourNe- | DetourNetworkUK |
| 2026-03-12 05:42:33 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 05:47:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-03-12 05:48:15 +0100 | kadobanana | (~mud@user/kadoban) (Quit: quit) |
| 2026-03-12 06:07:11 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 06:09:23 +0100 | michalz | (~michalz@185.246.207.203) |
| 2026-03-12 06:11:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 06:22:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 06:27:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-03-12 06:33:10 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 06:33:25 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 06:38:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 06:42:09 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-03-12 06:42:26 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-03-12 06:43:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 06:52:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 06:59:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 07:09:56 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-03-12 07:10:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 07:13:46 +0100 | tusko | (~uwu@user/tusko) (Ping timeout: 258 seconds) |
| 2026-03-12 07:15:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 07:20:21 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) (Ping timeout: 246 seconds) |
| 2026-03-12 07:24:35 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-03-12 07:25:51 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 07:26:16 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Quit: Quit) |
| 2026-03-12 07:26:31 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-03-12 07:30:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-03-12 07:37:39 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 07:41:12 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 264 seconds) |
| 2026-03-12 07:41:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 07:46:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 07:47:11 +0100 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-03-12 07:54:55 +0100 | mud | (~mud@user/kadoban) kadoban |
| 2026-03-12 08:03:06 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 08:03:21 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 08:09:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 08:13:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 08:19:37 +0100 | mulk | (~mulk@pd95146df.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2026-03-12 08:20:27 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2026-03-12 08:22:34 +0100 | emmanuelux | (~em@user/emmanuelux) (Quit: bye) |
| 2026-03-12 08:22:54 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-03-12 08:26:30 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-03-12 08:26:56 +0100 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-03-12 08:27:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 08:28:21 +0100 | dolio | (~dolio@130.44.140.168) dolio |
| 2026-03-12 08:31:52 +0100 | dolio | (~dolio@130.44.140.168) (Client Quit) |
| 2026-03-12 08:32:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 08:37:46 +0100 | dolio | (~dolio@130.44.140.168) dolio |
| 2026-03-12 08:43:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 08:47:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 08:54:09 +0100 | foul_owl | (~kerry@94.156.149.94) (Ping timeout: 246 seconds) |
| 2026-03-12 08:54:26 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 08:55:23 +0100 | jeremyn | (~jeremy@user/jeremyn) (Ping timeout: 268 seconds) |
| 2026-03-12 08:59:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 08:59:33 +0100 | Enrico63 | (~Enrico63@host-82-61-84-117.retail.telecomitalia.it) Enrico63 |
| 2026-03-12 08:59:52 +0100 | danza | (~danza@user/danza) danza |
| 2026-03-12 09:05:26 +0100 | tusko | (~uwu@user/tusko) tusko |
| 2026-03-12 09:06:51 +0100 | Enrico63 | (~Enrico63@host-82-61-84-117.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-03-12 09:07:50 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-03-12 09:08:03 +0100 | foul_owl | (~kerry@94.156.149.92) foul_owl |
| 2026-03-12 09:09:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 09:13:32 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de) |
| 2026-03-12 09:15:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2026-03-12 09:18:21 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 09:18:21 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 09:18:21 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 09:37:35 +0100 | chele | (~chele@user/chele) chele |
| 2026-03-12 09:41:32 +0100 | kimiamania40 | (~b4b260c9@user/kimiamania) kimiamania |
| 2026-03-12 09:42:04 +0100 | kimiamania4 | (~b4b260c9@user/kimiamania) (Read error: Connection reset by peer) |
| 2026-03-12 09:42:04 +0100 | kimiamania40 | kimiamania4 |
| 2026-03-12 09:45:13 +0100 | emmanuelux | (~em@user/emmanuelux) (Quit: bye) |
| 2026-03-12 09:49:08 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2026-03-12 09:50:10 +0100 | AlexNoo_ | AlexNoo |
| 2026-03-12 09:50:31 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-03-12 09:57:44 +0100 | akegalj | (~akegalj@78-2-210-167.adsl.net.t-com.hr) akegalj |
| 2026-03-12 10:06:49 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 10:14:26 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-03-12 10:15:33 +0100 | oskarw | (~user@user/oskarw) oskarw |
| 2026-03-12 10:38:32 +0100 | danza | (~danza@user/danza) (Read error: Connection reset by peer) |
| 2026-03-12 10:38:50 +0100 | danz14649 | (~danza@user/danza) danza |
| 2026-03-12 10:48:13 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2026-03-12 10:54:18 +0100 | fp2 | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2026-03-12 10:54:45 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds) |
| 2026-03-12 10:56:36 +0100 | fp2 | fp1 |
| 2026-03-12 10:58:39 +0100 | bionade24 | (~quassel@server2.oscloud.info) (Read error: Connection reset by peer) |
| 2026-03-12 10:59:04 +0100 | bionade24 | (~quassel@server2.oscloud.info) bionade24 |
| 2026-03-12 11:01:48 +0100 | AlexZenon | (~alzenon@5.139.232.240) (Ping timeout: 244 seconds) |
| 2026-03-12 11:04:02 +0100 | dhil | (~dhil@5.151.29.139) dhil |
| 2026-03-12 11:07:21 +0100 | AlexZenon | (~alzenon@5.139.232.240) |
| 2026-03-12 11:09:12 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2026-03-12 11:11:26 +0100 | poscat0x04 | (~poscat@user/poscat) (Ping timeout: 268 seconds) |
| 2026-03-12 11:14:15 +0100 | danz14649 | (~danza@user/danza) (Remote host closed the connection) |
| 2026-03-12 11:14:57 +0100 | danza | (~danza@user/danza) danza |
| 2026-03-12 11:17:23 +0100 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-03-12 11:17:43 +0100 | danza | (~danza@user/danza) danza |
| 2026-03-12 11:18:19 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 264 seconds) |
| 2026-03-12 11:19:41 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 265 seconds) |
| 2026-03-12 11:49:03 +0100 | acidjnk_new | (~acidjnk@p200300d6e700e551a4c32391cc3108f5.dip0.t-ipconnect.de) |
| 2026-03-12 11:51:53 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2026-03-12 11:55:35 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds) |
| 2026-03-12 11:57:11 +0100 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-03-12 11:57:16 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-03-12 12:00:33 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2026-03-12 12:01:44 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-03-12 12:15:43 +0100 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2026-03-12 12:17:37 +0100 | xff0x | (~xff0x@2405:6580:b080:900:855c:3368:d601:eb86) |
| 2026-03-12 12:34:42 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 248 seconds) |
| 2026-03-12 12:37:42 +0100 | noctux | (~noctux@user/noctux) (Read error: Connection reset by peer) |
| 2026-03-12 12:40:12 +0100 | noctux | (~noctux@user/noctux) noctux |
| 2026-03-12 12:40:35 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds) |
| 2026-03-12 12:47:56 +0100 | poscat0x04 | (~poscat@user/poscat) poscat |
| 2026-03-12 12:48:14 +0100 | dhil | (~dhil@5.151.29.139) (Ping timeout: 244 seconds) |
| 2026-03-12 12:49:13 +0100 | poscat | (~poscat@user/poscat) (Quit: Bye) |
| 2026-03-12 12:52:34 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 12:52:34 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 12:52:34 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 12:57:28 +0100 | preflex | (~preflex@user/mauke/bot/preflex) (Read error: Connection reset by peer) |
| 2026-03-12 12:57:28 +0100 | mauke | (~mauke@user/mauke) (Read error: Connection reset by peer) |
| 2026-03-12 13:00:05 +0100 | preflex | (~preflex@user/mauke/bot/preflex) preflex |
| 2026-03-12 13:00:51 +0100 | dhil | (~dhil@5.151.29.139) dhil |
| 2026-03-12 13:03:11 +0100 | mauke | (~mauke@user/mauke) mauke |
| 2026-03-12 13:16:51 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-03-12 13:21:18 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-03-12 13:23:18 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2026-03-12 13:31:46 +0100 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2026-03-12 13:31:46 +0100 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2026-03-12 13:31:46 +0100 | haritz | (~hrtz@user/haritz) haritz |
| 2026-03-12 13:31:57 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 13:31:57 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 13:31:57 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 13:33:17 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2026-03-12 13:41:58 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-03-12 13:51:11 +0100 | AlexZenon | (~alzenon@5.139.232.240) (Quit: ;-) |
| 2026-03-12 13:51:41 +0100 | Alex_delenda_est | (~al_test@5.139.232.240) (Quit: ;-) |
| 2026-03-12 13:52:11 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Quit: Leaving) |
| 2026-03-12 14:06:14 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 14:09:05 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 14:09:20 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) (Ping timeout: 245 seconds) |
| 2026-03-12 14:13:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 14:16:04 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 244 seconds) |
| 2026-03-12 14:22:49 +0100 | AlexZenon | (~alzenon@5.139.232.240) |
| 2026-03-12 14:28:02 +0100 | Alex_delenda_est | (~al_test@5.139.232.240) |
| 2026-03-12 14:33:00 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 14:35:36 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 14:38:03 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 272 seconds) |
| 2026-03-12 14:49:10 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 14:49:10 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 14:49:10 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 14:54:03 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-03-12 14:59:14 +0100 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 248 seconds) |
| 2026-03-12 15:04:08 +0100 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) {-d0t-} |
| 2026-03-12 15:05:44 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 15:05:44 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 15:05:44 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 15:10:19 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-03-12 15:22:01 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 15:23:30 +0100 | ski | . o O ( "A break from programming languages" by Alexis King in 2025-05-29 at <https://lexi-lambda.github.io/blog/2025/05/29/a-break-from-programming-languages/> ) |
| 2026-03-12 15:23:43 +0100 | Square2 | (~Square@user/square) Square |
| 2026-03-12 15:24:26 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds) |
| 2026-03-12 15:24:38 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 15:26:26 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 248 seconds) |
| 2026-03-12 15:27:15 +0100 | <mesaoptimizer> | good for her |
| 2026-03-12 15:33:54 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 15:46:01 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-03-12 15:46:01 +0100 | jmcantrell_ | jmcantrell |
| 2026-03-12 15:49:04 +0100 | jeremyn | (~jeremy@user/jeremyn) (Ping timeout: 244 seconds) |
| 2026-03-12 15:49:04 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds) |
| 2026-03-12 15:50:54 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
| 2026-03-12 15:56:45 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2026-03-12 15:56:48 +0100 | Digit | (~user@user/digit) (Ping timeout: 264 seconds) |
| 2026-03-12 16:09:13 +0100 | oskarw | (~user@user/oskarw) (Ping timeout: 244 seconds) |
| 2026-03-12 16:35:56 +0100 | machinedgod | (~machinedg@d172-219-48-230.abhsia.telus.net) machinedgod |
| 2026-03-12 16:36:52 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-03-12 16:38:14 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2026-03-12 16:43:19 +0100 | myme | (~myme@2a01:799:d5e:5f00:332d:919:8ee8:93eb) (Ping timeout: 244 seconds) |
| 2026-03-12 16:44:21 +0100 | myme | (~myme@2a01:799:d5e:5f00:303a:da6f:3ef4:dbc1) myme |
| 2026-03-12 16:48:04 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2026-03-12 16:48:53 +0100 | <Wygulmage> | Has anyone else looked at https://discourse.haskell.org/t/sneak-peek-bolt-math/13766 and thinks it's well intentioned but unworkable as written? |
| 2026-03-12 16:49:25 +0100 | <Wygulmage> | I'd comment on Discourse but apparently my non-AI browser is not supported... |
| 2026-03-12 16:50:26 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 252 seconds) |
| 2026-03-12 17:05:14 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 17:07:34 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2026-03-12 17:08:59 +0100 | kupi | (uid212005@id-212005.hampstead.irccloud.com) kupi |
| 2026-03-12 17:10:46 +0100 | <Wygulmage> | Clearly not. So, for example, say you have an instance of `AdditiveSemigroup`. Presumably the only law is that it's a semigroup. Cool. So you define `instance AdditiveSemigroup Integer where add = (*)`. Why not? It satisfies the law. And then you define `instance MultiplicativeSemigroup Integer where mul = (*)` Again, it satisfies the law. And |
| 2026-03-12 17:10:47 +0100 | <Wygulmage> | they're both monoidal, with `one = 1` and `zero = one`. Again, the laws are still satisfied. And then the library claims you have a `Semiring`, and perhaps assumes that `zero` (1) is annihilative for `mul`. |
| 2026-03-12 17:12:02 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 248 seconds) |
| 2026-03-12 17:16:11 +0100 | <Wygulmage> | Sorry. Is IRC dead, or did I just come at a bad time? |
| 2026-03-12 17:19:33 +0100 | somemathguy | (~somemathg@user/somemathguy) (Ping timeout: 246 seconds) |
| 2026-03-12 17:20:27 +0100 | <haskellbridge> | <sm> it has quiet and busy times. Definitely not dead here, but you may need to wait more than 5m |
| 2026-03-12 17:20:50 +0100 | <haskellbridge> | <sm> s/but.*// |
| 2026-03-12 17:21:58 +0100 | <haskellbridge> | <sm> do you have javascript disabled in your browser ? |
| 2026-03-12 17:22:11 +0100 | <Wygulmage> | Thanks, sm. Just got worried that all the humans had left. *deep breaths* |
| 2026-03-12 17:22:23 +0100 | <Wygulmage> | Not for haskell.org. |
| 2026-03-12 17:22:44 +0100 | <haskellbridge> | <sm> :) we're still here |
| 2026-03-12 17:23:24 +0100 | <haskellbridge> | <sm> I wondered why you couldn't comment at discourse. It requires js I see. |
| 2026-03-12 17:23:56 +0100 | somemathguy | (~somemathg@user/somemathguy) somemathguy |
| 2026-03-12 17:24:32 +0100 | <Wygulmage> | When I look at what I have blocked, both for discourse-cdn and haskell.org, everything is enabled. But yeah, I won't try to make #haskell into my IT helpers. Clearly that's a me problem. |
| 2026-03-12 17:25:56 +0100 | <Wygulmage> | And possibly a Discourse problem. |
| 2026-03-12 17:27:13 +0100 | Digitteknohippie | Digit |
| 2026-03-12 17:29:04 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
| 2026-03-12 17:30:19 +0100 | <Wygulmage> | I do have another question that's vaguely related to my initial rant. Are there any major roadblocks in GHC preventing class alias definitions or automatic defaulted superclasses? For example, allowing someone to just write `instance Monad M where...` and let GHC silently take care of `Functor` and `Applicative`, without even having to write |
| 2026-03-12 17:30:20 +0100 | <Wygulmage> | `deriving via WrapMonad M instance Applicative M` ? |
| 2026-03-12 17:43:59 +0100 | <ski> | Wygulmage : i was just (before i read your responses) about to comment on the same issue with not having a single place in the source which takes resposibility for ensuring that distributivity holds |
| 2026-03-12 17:44:45 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2026-03-12 17:47:27 +0100 | ski | coughs and stares at `Read' and `Show' |
| 2026-03-12 17:51:10 +0100 | ski | . o O ( "Class Alias Proposal for Haskell" <http://repetae.net/recent/out/classalias.html>,"Supertyping Suggestion for Haskell" <http://repetae.net/recent/out/supertyping.html>, both by jmeacham) |
| 2026-03-12 17:51:30 +0100 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2026-03-12 17:51:33 +0100 | <Wygulmage> | That's a totally fair point about `Read` and `Show` , but I think they're more clearly "utility" classes that don't have to follow any laws. But you REALLY want your numeric hierarchy to follow well defined laws. |
| 2026-03-12 17:51:41 +0100 | <EvanR> | Wygulmage, the humans are dead |
| 2026-03-12 17:52:02 +0100 | <EvanR> | 🤖 |
| 2026-03-12 17:52:58 +0100 | <Wygulmage> | I'm OK with that as long as Edward Kmett has been replaced with a sufficiently advanced chatbot that I can't tell the difference ;( |
| 2026-03-12 17:53:45 +0100 | <Wygulmage> | Which, judging by the AI slop in his youtube feed... |
| 2026-03-12 17:55:07 +0100 | <davean> | Wygulmage: Haha, the AI slop in his youtube feed is a very specific thing and I want more of it ... |
| 2026-03-12 17:55:40 +0100 | <davean> | Wygulmage: assume the AI slop is an inside joke thing. |
| 2026-03-12 17:56:00 +0100 | <Wygulmage> | \O/ |
| 2026-03-12 17:56:30 +0100 | <davean> | He's entertaining a specific few of us with a specific project |
| 2026-03-12 17:56:31 +0100 | <haskellbridge> | <ijouw> I was experimenting with naming my class of things to add (+) (using type operators) and using functional dependencies to make sure the compiler can infer the types (if 2 of (left arg, right arg, result) type are known). That does limit it to Vector a + a = Vector a or Vector a + Vector a = Vector a |
| 2026-03-12 17:56:46 +0100 | <davean> | You wouldn't have the context to enjoy it. Its public because it was being posted in a facebook group. |
| 2026-03-12 17:58:42 +0100 | <Wygulmage> | davean: Thanks for outing yourself as part of the SkyNet that replaced Ed. |
| 2026-03-12 17:58:53 +0100 | <EvanR> | having a vector add to something other than a vector is cringe |
| 2026-03-12 17:59:16 +0100 | <haskellbridge> | <ijouw> I believe number hirarchies should be displayed as tree/graph for quick overview. |
| 2026-03-12 17:59:48 +0100 | EvanR | looks at newmind |
| 2026-03-12 17:59:58 +0100 | <newmind> | hi |
| 2026-03-12 17:59:59 +0100 | <EvanR> | seems to be some sort of bot PMming me |
| 2026-03-12 18:00:09 +0100 | akegalj | (~akegalj@78-2-210-167.adsl.net.t-com.hr) (Ping timeout: 255 seconds) |
| 2026-03-12 18:00:12 +0100 | <newmind> | not a bot |
| 2026-03-12 18:00:57 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 18:01:21 +0100 | <newmind> | just wasn't related to this conversation, but rather something you asked in a different channel yesterday |
| 2026-03-12 18:01:42 +0100 | <EvanR> | I haven't been in that channel in maybe 8 years |
| 2026-03-12 18:01:50 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 245 seconds) |
| 2026-03-12 18:01:51 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-03-12 18:02:08 +0100 | <haskellbridge> | <ijouw> Maybe a bot impersonating you? |
| 2026-03-12 18:02:22 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 244 seconds) |
| 2026-03-12 18:02:30 +0100 | <EvanR> | unlikely |
| 2026-03-12 18:02:48 +0100 | <newmind> | oh, sorry, misread the nick, >.> terribly sorry |
| 2026-03-12 18:02:55 +0100 | <EvanR> | oh ok |
| 2026-03-12 18:03:11 +0100 | <newmind> | was a 'RyanR' |
| 2026-03-12 18:03:12 +0100 | <mesaoptimizer> | strange |
| 2026-03-12 18:03:14 +0100 | <EvanR> | lol |
| 2026-03-12 18:03:30 +0100 | <newmind> | so,, the distinct uppercase R at the end triggered a bit of a pattern match :D |
| 2026-03-12 18:03:35 +0100 | <EvanR> | tbf your message was relevant to the conversion "AI slop" xD |
| 2026-03-12 18:03:36 +0100 | Wygulmage4 | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2026-03-12 18:03:43 +0100 | <EvanR> | conversation |
| 2026-03-12 18:03:52 +0100 | <haskellbridge> | <ijouw> if y == v then all but the first char match. |
| 2026-03-12 18:03:59 +0100 | bionade24 | (~quassel@server2.oscloud.info) (Quit: Apocalypse Incoming!) |
| 2026-03-12 18:04:20 +0100 | <Wygulmage4> | And I think they should have started with a right near semiring rather than an "additive" semigroup. |
| 2026-03-12 18:04:30 +0100 | bionade24 | (~quassel@server2.oscloud.info) bionade24 |
| 2026-03-12 18:04:54 +0100 | <ski> | Wygulmage4 : like <https://cokmett.github.io/cokmett/> (click on image) ? |
| 2026-03-12 18:05:02 +0100 | <newmind> | again, sorry for the disturbance, my fault >.> |
| 2026-03-12 18:05:15 +0100 | <haskellbridge> | <ijouw> Do we have somewhere explaining English terminology for that stuff? |
| 2026-03-12 18:06:00 +0100 | <haskellbridge> | <ijouw> Like an overview over names of math concepts relating to numbers? |
| 2026-03-12 18:06:02 +0100 | <EvanR> | I wonder if any of that is real |
| 2026-03-12 18:06:10 +0100 | <Wygulmage4> | ski: :') |
| 2026-03-12 18:06:18 +0100 | <newmind> | you... want logs? |
| 2026-03-12 18:06:28 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 18:06:36 +0100 | <haskellbridge> | <ijouw> No, i have enough wood? |
| 2026-03-12 18:06:37 +0100 | <Wygulmage4> | ijouw: Almost all math terminology is terrible, and you just kind of accept it. |
| 2026-03-12 18:07:09 +0100 | <haskellbridge> | <ijouw> I just do not know it. |
| 2026-03-12 18:07:14 +0100 | <EvanR> | at least math people stick to it and don't go about renaming everything randomly every 6 months like programming language of the week people |
| 2026-03-12 18:08:01 +0100 | <Wygulmage4> | Damn. That hurts. But yeah, why does NixOS keep arbitrarily renaming options??? |
| 2026-03-12 18:08:43 +0100 | <davean> | hy does nix make modularizing something take 3x the code of just doing the thing in the first place? |
| 2026-03-12 18:08:43 +0100 | <Wygulmage4> | Still, semigroup is to group as semilattice is to ??????? |
| 2026-03-12 18:09:59 +0100 | <ski> | "semi-" here is basically "not quite" |
| 2026-03-12 18:10:00 +0100 | <EvanR> | not sure that makes any sense |
| 2026-03-12 18:10:03 +0100 | <Wygulmage4> | Don't think I'll survive these truth bombs. |
| 2026-03-12 18:12:04 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-03-12 18:12:45 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 255 seconds) |
| 2026-03-12 18:13:08 +0100 | <Wygulmage4> | I'm not really being fair to mathematicians. But I want a "right semiring" to be two associative operations where one distributes over the other from the right. And that simply isn't true. |
| 2026-03-12 18:13:26 +0100 | <EvanR> | you should rename it |
| 2026-03-12 18:13:36 +0100 | <EvanR> | will be very confusing it |
| 2026-03-12 18:14:13 +0100 | <EvanR> | (ring terminology already has some jargon decay in places where it depends who's talking about it means) |
| 2026-03-12 18:14:20 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-03-12 18:14:48 +0100 | <EvanR> | some of my words seem to not making it through the tubes |
| 2026-03-12 18:15:31 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
| 2026-03-12 18:15:41 +0100 | <Wygulmage4> | I have not heard "jargon decay"; that's it exactly. |
| 2026-03-12 18:17:14 +0100 | <Wygulmage4> | But being precise and calling something a "right ringoid with additive and multiplicative associativity"... I don't know if that's better. |
| 2026-03-12 18:17:37 +0100 | <EvanR> | what is this in relation to |
| 2026-03-12 18:18:33 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) (Ping timeout: 248 seconds) |
| 2026-03-12 18:19:13 +0100 | <Wygulmage4> | ijouw: For basic definitions, I usually go to Wolfram MathWorld, Planet Math, or Wikipedia. Here's Planet Math on Brouwerian lattices: https://planetmath.org/brouwerianlattice |
| 2026-03-12 18:19:46 +0100 | <Wygulmage4> | Or if you have access to university libraries, have them reserve you a textbook. |
| 2026-03-12 18:22:08 +0100 | mulk | (~mulk@pd95146df.dip0.t-ipconnect.de) mulk |
| 2026-03-12 18:23:23 +0100 | <haskellbridge> | <ijouw> Thank you |
| 2026-03-12 18:25:12 +0100 | <Wygulmage4> | No problem. Being employed by a university is a real lifehack for that kind of stuff. You can be in IT or a janitor an they'll still send you a copy of Residuated Structures in Algebra and Logic. |
| 2026-03-12 18:25:27 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-03-12 18:27:39 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-03-12 18:30:38 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 18:31:01 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 18:31:38 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-03-12 18:32:26 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2026-03-12 18:35:46 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 18:39:12 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:39:43 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-03-12 18:39:57 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:40:40 +0100 | anselmschueler | (~Thunderbi@user/schuelermine) (Client Quit) |
| 2026-03-12 18:40:41 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:42:43 +0100 | Tuplanolla | (~Tuplanoll@88-114-89-88.elisa-laajakaista.fi) Tuplanolla |
| 2026-03-12 18:43:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:44:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:44:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:44:50 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:45:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:46:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:47:21 +0100 | oskarw | (~user@user/oskarw) oskarw |
| 2026-03-12 18:49:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:49:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:49:39 +0100 | <gentauro> | % :t readMaybe |
| 2026-03-12 18:49:39 +0100 | <yahb2> | <interactive>:1:1: error: [GHC-88464] ; Variable not in scope: readMaybe |
| 2026-03-12 18:49:51 +0100 | <gentauro> | % import Text.Read |
| 2026-03-12 18:49:51 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:49:53 +0100 | <gentauro> | % :t readMaybe |
| 2026-03-12 18:49:53 +0100 | <yahb2> | readMaybe :: Read a => String -> Maybe a |
| 2026-03-12 18:50:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:50:07 +0100 | <EvanR> | that's a good one |
| 2026-03-12 18:50:25 +0100 | <gentauro> | % data FooBar = Foo | Bar deriving Read |
| 2026-03-12 18:50:25 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:50:35 +0100 | <gentauro> | % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 18:50:35 +0100 | <yahb2> | <interactive>:47:16: error: [GHC-51179] ; Illegal \case ; Suggested fix: ; Perhaps you intended to use the ‘LambdaCase’ extension ; You may enable this language extension in GHC... |
| 2026-03-12 18:50:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:50:44 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:51:09 +0100 | <gentauro> | > :i (+) |
| 2026-03-12 18:51:11 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input `:' |
| 2026-03-12 18:51:20 +0100 | <gentauro> | > import Text.Read |
| 2026-03-12 18:51:21 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input `import' |
| 2026-03-12 18:51:24 +0100 | <ski> | residuated lattices reminds me of ordered (intuitionistic) logic (see "Ordered Linear Logic and Applications" by Jeffrey E. Polakow in 2001-08 at <https://www.cs.cmu.edu/~jpolakow/diss.ps>,(draft) <https://web.archive.org/web/20010614031936/http://www.cs.cmu.edu:80/~jpolakow/diss.pdf>) |
| 2026-03-12 18:51:28 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:51:32 +0100 | <ski> | @let import Text.Read |
| 2026-03-12 18:51:33 +0100 | <lambdabot> | Defined. |
| 2026-03-12 18:51:54 +0100 | <gentauro> | > :i readMaybe |
| 2026-03-12 18:51:55 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input `:' |
| 2026-03-12 18:51:57 +0100 | <gentauro> | :| |
| 2026-03-12 18:52:04 +0100 | <ski> | @type readMaybe |
| 2026-03-12 18:52:05 +0100 | <lambdabot> | Read a => String -> Maybe a |
| 2026-03-12 18:52:09 +0100 | <EvanR> | :i readMaybe |
| 2026-03-12 18:52:30 +0100 | <ski> | (there is no `@info' with lambdabot) |
| 2026-03-12 18:52:47 +0100 | <gentauro> | ski: got it |
| 2026-03-12 18:53:00 +0100 | dhil | (~dhil@5.151.29.139) (Ping timeout: 244 seconds) |
| 2026-03-12 18:53:11 +0100 | <ski> | % :set -XLambdaCase |
| 2026-03-12 18:53:11 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:53:16 +0100 | <gentauro> | :o |
| 2026-03-12 18:53:20 +0100 | <ski> | % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 18:53:20 +0100 | <yahb2> | <interactive>:51:59: error: [GHC-88464] ; Variable not in scope: toUpper :: a -> Char ; ; <interactive>:51:75: error: [GHC-88464] ; Variable not in scope: toLower :: a -> Char |
| 2026-03-12 18:53:32 +0100 | <ski> | % :m + Data.Char |
| 2026-03-12 18:53:32 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:53:35 +0100 | <ski> | % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 18:53:35 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:53:47 +0100 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 18:53:47 +0100 | <yahb2> | <interactive>:57:1: error: [GHC-39999] ; • No instance for ‘Show FooBar’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; • In a stmt of an interactive GHCi command: ; Yah... |
| 2026-03-12 18:53:56 +0100 | <gentauro> | % data FooBar = Foo | Bar deriving (Read, Show) |
| 2026-03-12 18:53:56 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:53:58 +0100 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 18:53:58 +0100 | <yahb2> | <interactive>:61:1: error: [GHC-39999] ; • No instance for ‘Show Ghci8.FooBar’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; There are instances for similar types: ; ... |
| 2026-03-12 18:54:13 +0100 | <gentauro> | % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar) |
| 2026-03-12 18:54:13 +0100 | <yahb2> | <no output> |
| 2026-03-12 18:54:16 +0100 | <gentauro> | % readFoobar "foo" |
| 2026-03-12 18:54:16 +0100 | <yahb2> | Just Foo |
| 2026-03-12 18:54:18 +0100 | <gentauro> | nice |
| 2026-03-12 18:54:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:54:44 +0100 | <ski> | % (reads :: ReadS FooBar) "foo bar" |
| 2026-03-12 18:54:44 +0100 | <yahb2> | [] |
| 2026-03-12 18:54:55 +0100 | <ski> | % (reads :: ReadS FooBar) "Foo Bar" |
| 2026-03-12 18:54:55 +0100 | <yahb2> | [(Foo," Bar")] |
| 2026-03-12 18:54:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:55:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:56:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:56:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:56:12 +0100 | chewybread | (~chewybrea@user/chewybread) (Ping timeout: 264 seconds) |
| 2026-03-12 18:56:48 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:59:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:00:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:00:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:01:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:01:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:02:08 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:02:16 +0100 | <Wygulmage4> | ski: Is there any formal relation between a monoid (or semigroup) with monus and a residuated lattice (or residuated semilattice)? They seem to be doing similar things w.r.t. generalized division and subtraction. |
| 2026-03-12 19:03:01 +0100 | <ski> | galois connections / adjunctions |
| 2026-03-12 19:03:01 +0100 | <haskellbridge> | <ijouw> monus >> minus? |
| 2026-03-12 19:03:05 +0100 | <ski> | no |
| 2026-03-12 19:03:29 +0100 | <ski> | <https://en.wikipedia.org/wiki/Monus> |
| 2026-03-12 19:03:53 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2026-03-12 19:04:45 +0100 | <ski> | m ∸ o ≤ n |
| 2026-03-12 19:04:46 +0100 | <ski> | ⇔ m ≤ n + o |
| 2026-03-12 19:05:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:05:34 +0100 | Wygulmage4 | (~Wygulmage@user/Wygulmage) (Quit: Client closed) |
| 2026-03-12 19:05:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:06:00 +0100 | <ski> | in words, ⌜m ∸ o⌝ is the least ⌜n⌝ such that ⌜m ≤ n + o⌝ (⌜n⌝ added to ⌜m⌝ is at least ⌜o⌝) |
| 2026-03-12 19:06:01 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:06:02 +0100 | <haskellbridge> | <ijouw> Seems useful |
| 2026-03-12 19:06:20 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2026-03-12 19:06:26 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-03-12 19:06:27 +0100 | <ski> | two consequences (unit & counit) of that galois connection / adjunction are |
| 2026-03-12 19:06:42 +0100 | <ski> | m ≤ (m ∸ o) + o |
| 2026-03-12 19:06:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:06:44 +0100 | <ski> | and |
| 2026-03-12 19:06:44 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:06:58 +0100 | <ski> | (n + o) ∸ o ≤ n |
| 2026-03-12 19:07:19 +0100 | <ski> | for natural numbers (and subsets), the latter is actually an equality |
| 2026-03-12 19:07:37 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:07:54 +0100 | <ski> | for natural numbers, monus is also called cut-off / saturated / truncated subtraction |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:08:42 +0100 | <Wygulmage> | And conveniently it's closed for natural numbers, unlike subtraction. |
| 2026-03-12 19:08:47 +0100 | <ski> | (and ⌜m ∸ o⌝ can be described as ⌜max 0 (m − o)⌝) |
| 2026-03-12 19:09:12 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 19:10:19 +0100 | <ski> | in total programming environments, people often use monus, instead of minus, just to get it totally defined |
| 2026-03-12 19:10:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:10:41 +0100 | <Wygulmage> | But of course it doesn't work for `Int`. |
| 2026-03-12 19:10:42 +0100 | <ski> | (i've seen people define "reciprocal" of zero as zero, for similar reasons ..) |
| 2026-03-12 19:10:51 +0100 | <Wygulmage> | *shudder* |
| 2026-03-12 19:10:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:11:08 +0100 | <ski> | yea, i was thinking of stuff like recursive functions (a la Kleene) |
| 2026-03-12 19:11:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:12:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:12:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:12:20 +0100 | <ski> | exercise for the reader : figure out an appropriate galois connection for division in relational algebra, and determine what the result of dividing by the empty relation here amounts to |
| 2026-03-12 19:13:07 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:13:17 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-03-12 19:15:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:16:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:16:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:17:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:17:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:17:56 +0100 | <ski> | (also stuff like <https://en.wikipedia.org/wiki/Brzozowski_derivative> (for formal languages, and regexen). figure out how this relates to an appropriate galois connection, and how it *differs* from <https://en.wikipedia.org/wiki/Quotient_of_a_formal_language>, while it relates to "universal image" (as opposed to "existential image"/"(direct) image") of a function on a subset of its domain (cf. |
| 2026-03-12 19:18:02 +0100 | <ski> | "preimage"/"inverse image", where you start with a subset of the codomain))) |
| 2026-03-12 19:18:05 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 245 seconds) |
| 2026-03-12 19:18:06 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-03-12 19:18:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:18:37 +0100 | kupi | (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-03-12 19:20:16 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 19:21:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:21:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:22:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:22:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:23:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:23:31 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:23:54 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:24:23 +0100 | <ski> | .. in my imagined functional language, from a while ago, you can write stuff like `m - n : Nat | m ?< n : () -| m : Nat , n : Nat', where either `m - n' or `m ?< n' is well-defined |
| 2026-03-12 19:24:48 +0100 | <ski> | (well, the version i was pondering was dependently typed, but you could also have non-dependently typed versions) |
| 2026-03-12 19:26:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:26:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:27:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:28:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:28:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:28:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:29:15 +0100 | <Wygulmage> | What would a non-dependently typed version look like? |
| 2026-03-12 19:29:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 19:29:55 +0100 | <Wygulmage> | (I'm reading up on Brzozowski derivatives and quotients of formal languages.) |
| 2026-03-12 19:30:39 +0100 | someb | (~someb@24.42.43.79) |
| 2026-03-12 19:30:57 +0100 | <someb> | hello? |
| 2026-03-12 19:31:02 +0100 | <someb> | anyone online? |
| 2026-03-12 19:31:40 +0100 | <ski> | Wygulmage : the version i showed above |
| 2026-03-12 19:31:41 +0100 | wbrawner | (~wbrawner@129.146.105.153) wbrawner |
| 2026-03-12 19:31:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:31:56 +0100 | <ski> | someb : don't ask to ask, just ask |
| 2026-03-12 19:32:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:32:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:33:10 +0100 | someb | (~someb@24.42.43.79) () |
| 2026-03-12 19:33:16 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:33:17 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:33:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:33:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:33:42 +0100 | ski | shrugs |
| 2026-03-12 19:34:04 +0100 | <Wygulmage> | Me a couple hours ago: <Wygulmage> Sorry. Is IRC dead, or did I just come at a bad time? |
| 2026-03-12 19:34:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:34:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 19:36:24 +0100 | <Wygulmage> | ski: So that's using the type-level Nat? |
| 2026-03-12 19:36:46 +0100 | <ski> | no, that's a normal (value-level) `Nat' |
| 2026-03-12 19:37:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:37:37 +0100 | <Wygulmage> | And the side conditions produce type errors if they can't be proven at compile time? |
| 2026-03-12 19:37:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:38:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:38:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:38:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:39:23 +0100 | <ski> | dependently typed version would be `k - m : Fin n | k ?< m : Fin m -| m : Nat , n : Nat , k : Fin (m + n)' |
| 2026-03-12 19:39:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:39:41 +0100 | <ski> | Wygulmage : side conditions ? |
| 2026-03-12 19:40:07 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:40:10 +0100 | <ski> | it's simultaneously defining two operations, `-' and `?<' such that they together (on the same inputs) are total |
| 2026-03-12 19:40:27 +0100 | jeremyn | (~jeremy@user/jeremyn) (Quit: Konversation terminated!) |
| 2026-03-12 19:40:41 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 19:40:59 +0100 | <Wygulmage> | Oh! I see. That would be nice. Like requiring a `null` test to use `tail`. |
| 2026-03-12 19:41:53 +0100 | <ski> | so, you can write an expression like `..(k - m).. | ..(k <? m)..', and these two occurances of `k - m' respectively `k ?< m' will correspond to a single procedure call at run-time which can end with one or another return path, activating either the left or the right side of the `... | ...' (making the other side undefined) |
| 2026-03-12 19:42:20 +0100 | <Wygulmage> | Right. |
| 2026-03-12 19:42:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:42:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:43:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:43:23 +0100 | <ski> | operationally, it's similar to `(-?<) : Either Nat ()' (or the dependently typed version), and using `case'-`of' to dispatch on that |
| 2026-03-12 19:44:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:44:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:44:28 +0100 | <Wygulmage> | So is `<?` equivalent to Haskell's `<` or does it produce a sum type? |
| 2026-03-12 19:44:48 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 246 seconds) |
| 2026-03-12 19:44:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:45:20 +0100 | <ski> | there's also a version `k / n : Fin m , k % n : Fin n -| m : Nat , n : Nat , k : Fin (m * n)', where the joint operation `/' & `%' here corresponds to a single Haskell call `divMod' |
| 2026-03-12 19:45:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 19:45:38 +0100 | <ski> | (quick, what's the result of `k / 0' and `k % 0' ?) |
| 2026-03-12 19:45:59 +0100 | <ski> | Wygulmage : neither |
| 2026-03-12 19:46:56 +0100 | <ski> | `?<' (if it terminates, is not partial) provides evidence of the `<' relation between the inputs |
| 2026-03-12 19:47:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:47:50 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:47:52 +0100 | <ski> | in the dependently typed version, `k ?< m : Fin m', but you could, if you wanted, make that `k ?< m : k < m' (modulo an inclusion from `Fin (m + n)' to `Nat' for the `k'), instead |
| 2026-03-12 19:48:05 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:48:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:48:18 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds) |
| 2026-03-12 19:48:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:49:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:49:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:49:32 +0100 | <ski> | (there's a reason why i'm making some of the arguments `Nat's and others `Fin o's for various `o's, here, but it's a bit incidental to the general idea of "simultaneous alternative definitions"") |
| 2026-03-12 19:50:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 19:50:08 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:51:05 +0100 | <ski> | Wygulmage : if you want to, you could say `Right (k - m) | Left (k ?< m)' produces a sum type (`Fin m + Fin n') |
| 2026-03-12 19:52:15 +0100 | <EvanR> | there's so much punctuation in m - n : Nat | m ?< n : () -| m : Nat , n : Nat let me try to guess the precedence from highest to lowest: : - ?< , | -| |
| 2026-03-12 19:53:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:53:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:53:39 +0100 | <ski> | ("-" | "?<") , ("|" , ",") , "-|" |
| 2026-03-12 19:54:01 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:54:12 +0100 | <ski> | ((m - n) : Nat) | ((m ?< n) : ()) -| ((m : Nat) , (n : Nat)) |
| 2026-03-12 19:54:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:54:44 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:54:50 +0100 | <Wygulmage> | Thanks, I was not parsing it like that. |
| 2026-03-12 19:55:22 +0100 | <ski> | (((k - m) : Fin n) | ((k ?< m) : Fin m)) -| ((m : Nat) , (n : Nat) , (k : Fin (m + n))) |
| 2026-03-12 19:55:28 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:55:54 +0100 | <ski> | (((k / n) : Fin m) , ((k % n) : Fin n)) -| ((m : Nat) , (n : Nat) , (k : Fin (m * n))) |
| 2026-03-12 19:56:19 +0100 | <ski> | er, forgot to insert the `:' .. |
| 2026-03-12 19:56:28 +0100 | <ski> | ("-" | "?<") , ":" , ("|" , ",") , "-|" |
| 2026-03-12 19:58:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:58:28 +0100 | <EvanR> | oof ok |
| 2026-03-12 19:58:41 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:58:47 +0100 | <ski> | if you prefer a more C-like syntax : |
| 2026-03-12 19:58:51 +0100 | <ski> | nat minus(m,n) | void under(m,n) |
| 2026-03-12 19:58:57 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:58:58 +0100 | <ski> | nat m,n; |
| 2026-03-12 19:58:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:59:02 +0100 | <ski> | { ... } |
| 2026-03-12 19:59:11 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 19:59:11 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 19:59:11 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:59:21 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:59:38 +0100 | <EvanR> | where is the { ... } in the original notation |
| 2026-03-12 19:59:54 +0100 | <ski> | it wasn't shown. i just showed the type signature, not the implementation |
| 2026-03-12 20:00:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:00:04 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:00:30 +0100 | <EvanR> | the implementation of what exactly, both these operators? |
| 2026-03-12 20:00:48 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:02:46 +0100 | Wygulmage88 | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2026-03-12 20:02:58 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2026-03-12 20:03:29 +0100 | <ski> | yes |
| 2026-03-12 20:03:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:03:50 +0100 | <EvanR> | oh |
| 2026-03-12 20:03:51 +0100 | <ski> | m - Zero = m | _ ?< Zero = ‾ |
| 2026-03-12 20:03:57 +0100 | <ski> | _ - Succ _ = ‾ | _ ?< Succ _ = () |
| 2026-03-12 20:04:00 +0100 | <ski> | Succ m - Succ n = m - n | Succ m ?< Succ n = m ?< n |
| 2026-03-12 20:04:08 +0100 | <ski> | is the implementation |
| 2026-03-12 20:04:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:04:20 +0100 | <EvanR> | oh |
| 2026-03-12 20:04:29 +0100 | <Wygulmage88> | Got to change locations. Gonna check the log. |
| 2026-03-12 20:04:42 +0100 | <EvanR> | I was expecting to see - defined using ?< and ?< defined using - xD |
| 2026-03-12 20:04:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:05:00 +0100 | <EvanR> | what is ‾ |
| 2026-03-12 20:05:20 +0100 | <ski> | `‾' means "undefined". in a pattern, in Agda, it's known as "absurd pattern", and spelled `()', used to indicate that we know no possible constructor could match |
| 2026-03-12 20:05:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:05:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:05:49 +0100 | <ski> | (but i allow using it in expressions, as well) |
| 2026-03-12 20:05:58 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 20:06:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:06:44 +0100 | <ski> | (in Haskell, you'd use `case ... of {}' for the absurd pattern case, e.g. with GADTs) |
| 2026-03-12 20:07:24 +0100 | <ski> | it is the neutral element of the ambiguous operator `|' |
| 2026-03-12 20:08:20 +0100 | <ski> | just like `_' is the neutral element of the `&' conjunctive pattern (generalization of `@' where both sides are allowed to be arbitrary patterns. e.g. useful with view patterns, pattern synonyms) |
| 2026-03-12 20:09:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:09:19 +0100 | <ski> | (i also used `|' above to separate alternative definitions, largely for suggestive effect. one could dispense with this use of it, letting the system infer which defining equations together are total on the given inputs) |
| 2026-03-12 20:09:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:10:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:10:19 +0100 | <ski> | "I was expecting to see - defined using ?< and ?< defined using - xD" -- you could have that for some other pair of alternative operations, i suppose |
| 2026-03-12 20:10:28 +0100 | Wygulmage88 | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 20:10:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:10:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:11:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:13:24 +0100 | <ski> | oh .. sorry, i just realized the left argument of the middle equations should be `Zero', not `_' (was taking this from memory). hopefully that makes more sense (removing the inadvertent overlap between the equations) |
| 2026-03-12 20:14:25 +0100 | <ski> | (btw, for the dependently typed version, you'd replace the latter two right side definitions by `Zero ?< Succ _ = Zero' and `Succ m ?< Succ n = Succ (m ?< n)', so `k ?< m' here is equal to `k', but restricted to be an element of `Fin m', rather than an element of `Fin (m + n)') |
| 2026-03-12 20:14:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:14:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:15:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:15:24 +0100 | <EvanR> | Zero - Succ _ = undefined |
| 2026-03-12 20:15:38 +0100 | <EvanR> | so the program will crash or |
| 2026-03-12 20:16:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:16:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:16:49 +0100 | <ski> | nope, because you're supposed to pair up an application of `-', with an application of `?<' so that one of them will be defined, succeed |
| 2026-03-12 20:16:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:17:02 +0100 | <ski> | (if you're just using one of them, it would be partial, yes) |
| 2026-03-12 20:17:19 +0100 | <EvanR> | what does applying both operators look like |
| 2026-03-12 20:19:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:20:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:20:20 +0100 | <ski> | m / n = Succ ((m - n) / n) | let () = m ?< n in Zero ; m % n = (m - n) % n | let () = m ?< n in m |
| 2026-03-12 20:20:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:20:51 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 246 seconds) |
| 2026-03-12 20:20:51 +0100 | <ski> | (that does not terminate for `n = 0'. dependently typed version i hinted at above is total, though) |
| 2026-03-12 20:21:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:21:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:22:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:22:25 +0100 | <EvanR> | so the Succ ((m - n) / n) will be "tried" first and if it's undefined go to the thing right of | |
| 2026-03-12 20:23:02 +0100 | <EvanR> | and the types don't have to match immediately |
| 2026-03-12 20:24:25 +0100 | <ski> | types have to match |
| 2026-03-12 20:24:34 +0100 | <ski> | and `|' is commutative |
| 2026-03-12 20:24:41 +0100 | <EvanR> | oh |
| 2026-03-12 20:25:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:25:13 +0100 | <ski> | operational semantics should be as if you executed `(-?<) :: Nat -> Nat -> Either () Nat' |
| 2026-03-12 20:25:13 +0100 | <EvanR> | is the commutativity guaranteed somehow by the compiler |
| 2026-03-12 20:25:29 +0100 | <monochrom> | <3 unordered alternation |
| 2026-03-12 20:25:31 +0100 | <ski> | they are not independent operations, one tried after the other |
| 2026-03-12 20:25:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:25:40 +0100 | <ski> | they are tried, simultaneously |
| 2026-03-12 20:25:52 +0100 | <ski> | (and so the recursion pattern of them both must align) |
| 2026-03-12 20:25:59 +0100 | <EvanR> | similar to lub |
| 2026-03-12 20:26:25 +0100 | <ski> | oh, and yes, the system would ensure that both are not defined at the same time |
| 2026-03-12 20:26:33 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:26:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:26:51 +0100 | <monochrom> | There is a Curry compiler, Curry2Go, which compiles non-determinism to Go multi-threading so all alternatives are literally tried concurrently. |
| 2026-03-12 20:27:11 +0100 | <ski> | breadth-first ? |
| 2026-03-12 20:27:25 +0100 | <monochrom> | Yeah |
| 2026-03-12 20:28:49 +0100 | <ski> | how does it handle trying to communicate a result non-locally out of an alternative ? |
| 2026-03-12 20:29:28 +0100 | <monochrom> | I don't know. |
| 2026-03-12 20:29:50 +0100 | <ski> | presumably the alternation acts as a barrier, where information can flow into the "engine", but not out of (except at the end of the computation, collecting results) |
| 2026-03-12 20:30:13 +0100 | <ski> | (the CTM book talks about this, in the chapter about constraint programming) |
| 2026-03-12 20:30:37 +0100 | ski | was (re)reading it recently (didn't get to that part yet, though) |
| 2026-03-12 20:30:58 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:31:08 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:31:10 +0100 | <monochrom> | Yeah I'm thinking "what's there to handle?" because the only thing left to do is collecting results. |
| 2026-03-12 20:31:29 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-03-12 20:34:05 +0100 | ski | . o O ( "Concepts, Techniques, and Models of Computer Programming" by Peter Van Roy,Seif Haridi in 2003-06-05 at <https://webperso.info.ucl.ac.be/~pvr/book.html>,<https://webperso.info.ucl.ac.be/~pvr/VanRoyHaridi2003-book.pdf> ) |
| 2026-03-12 20:34:07 +0100 | <monochrom> | Given that non-determinism cannot be used with mutable variables, you have a multiple-world semantics, such that there is no communication between two sibling worlds. |
| 2026-03-12 20:34:59 +0100 | <ski> | (at first, i was thinking of the two different flavors of AND-parallelism (merge-at-join vs. communicate), but presumably they're only doing OR-parallelism) |
| 2026-03-12 20:35:00 +0100 | remedan | (~remedan@78-80-95-79.customers.tmcz.cz) (Quit: Bye!) |
| 2026-03-12 20:35:04 +0100 | <monochrom> | It doesn't even have Prolog's cut, so you can't even kill your sibling! |
| 2026-03-12 20:35:10 +0100 | <EvanR> | the Sagrada Família on the cover is great |
| 2026-03-12 20:35:14 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:35:29 +0100 | <EvanR> | *your code project is going this well* |
| 2026-03-12 20:35:46 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Ping timeout: 248 seconds) |
| 2026-03-12 20:36:20 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-03-12 20:36:41 +0100 | <ski> | i heard something about the rate at continuing with Sagrada Familia going up, recently, due to being able to use prefab pieces, designed to fit, constructed elsewhere |
| 2026-03-12 20:36:48 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-03-12 20:37:06 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
| 2026-03-12 20:41:15 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Ping timeout: 255 seconds) |
| 2026-03-12 20:41:48 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 264 seconds) |
| 2026-03-12 20:42:08 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-03-12 20:43:53 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) |
| 2026-03-12 20:43:53 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host) |
| 2026-03-12 20:43:53 +0100 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2026-03-12 20:44:45 +0100 | <monochrom> | For AND, Curry only requires this: Let x be a logic variable, then "x>=5 AND unify(x,10)" and "unify(x,10) AND x>=5" behave the same, both should discover x=10 and compute 10>=5. |
| 2026-03-12 20:45:24 +0100 | <monochrom> | I have a feeling that when there are no mutable variables, you have confluence so it doesn't matter what you do. |
| 2026-03-12 20:45:45 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-03-12 20:46:19 +0100 | <ski> | yea, Oz has declaratie concurrency for this |
| 2026-03-12 20:46:37 +0100 | <ski> | (operations block until their inputs are instantiated) |
| 2026-03-12 20:47:08 +0100 | <ski> | it's also possible to construct a "read-only view" of a dataflow variable (logic variable), so that you can't instantiate through it |
| 2026-03-12 20:49:44 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-03-12 20:50:17 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 2026-03-12 20:52:23 +0100 | ski | . o O ( "Dataflow Parallelism: The Par Monad" (chapter 4, "Parallel and Concurrent Programming in Haskell" by Simon Marlow in 2013) <https://web.archive.org/web/20180108044627/http:/chimera.labs.oreilly.com/books/1230000000929/ch04…> ) |
| 2026-03-12 20:52:37 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2026-03-12 20:54:09 +0100 | <ski> | (you get non-declarative concurrency, when you allow race conditions, non-deterministic merging of multiple concurrent channels. i guess lvish is a principled way to keep declarativity, in some of those cases) |
| 2026-03-12 20:54:14 +0100 | <ski> | @hackage lvish |
| 2026-03-12 20:54:14 +0100 | <lambdabot> | https://hackage.haskell.org/package/lvish |
| 2026-03-12 20:54:49 +0100 | akegalj | (~akegalj@141-138-62-190.dsl.iskon.hr) |
| 2026-03-12 20:58:00 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 21:09:04 +0100 | Square2 | (~Square@user/square) (Quit: Leaving) |
| 2026-03-12 21:09:19 +0100 | akegalj | (~akegalj@141-138-62-190.dsl.iskon.hr) (Quit: leaving) |
| 2026-03-12 21:09:21 +0100 | Square | (~Square@user/square) Square |
| 2026-03-12 21:13:29 +0100 | <gentauro> | ski: every now and then uni's change their websistes and all papers linking are gone |
| 2026-03-12 21:13:38 +0100 | <gentauro> | :( |
| 2026-03-12 21:14:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 21:18:54 +0100 | <ski> | similar to many large applications or GUI systems or web sites changing, "just because", presumably to justify having interface designers or somesuch ? |
| 2026-03-12 21:20:46 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 21:21:15 +0100 | <geekosaur> | there's also this business of unis asserting ownership of other uni's web namespaces because they're better known or w/e |
| 2026-03-12 21:26:06 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-03-12 21:31:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 21:33:53 +0100 | <gentauro> | I'm stuck in a terminal with black background and greenish/limeish foreground. I don't understand the fuzz :-\ |
| 2026-03-12 21:35:26 +0100 | gentauro | «Hello, the CLI version is only intended for developer use right now, we do not plan to improve its usability much for regular users, the GUI desktop app is focused on regular users. Thank you for the suggestion» -- SimpleX Chat |
| 2026-03-12 21:35:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 21:36:10 +0100 | <gentauro> | probably the best chat app (non IRC based) and written in Haskell, with a terminal CLI, is not gonna invest anymore effort into the terminal CLI :( |
| 2026-03-12 21:36:16 +0100 | <gentauro> | now that's saD |
| 2026-03-12 21:38:11 +0100 | <haskellbridge> | <sm> is it open source ? |
| 2026-03-12 21:39:38 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 21:40:23 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 21:41:07 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 21:42:17 +0100 | chewybread | (~chewybrea@user/chewybread) (Ping timeout: 248 seconds) |
| 2026-03-12 21:42:54 +0100 | <gentauro> | yeah. AGPLv3.0 |
| 2026-03-12 21:44:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 21:44:34 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 21:45:38 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 21:46:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 21:47:13 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2026-03-12 21:51:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 21:57:06 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) |
| 2026-03-12 21:57:06 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host) |
| 2026-03-12 21:57:06 +0100 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2026-03-12 22:01:36 +0100 | chewybread | (~chewybrea@user/chewybread) (Ping timeout: 264 seconds) |
| 2026-03-12 22:02:00 +0100 | <sm> | so you know what to do :-) |
| 2026-03-12 22:02:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 22:03:38 +0100 | <jreicher> | gentauro: what's the protocol (and server?) architecture? |
| 2026-03-12 22:06:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 22:09:23 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) |
| 2026-03-12 22:09:23 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host) |
| 2026-03-12 22:09:23 +0100 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2026-03-12 22:16:16 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-03-12 22:17:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 22:21:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-03-12 22:26:34 +0100 | machinedgod | (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 2026-03-12 22:28:14 +0100 | oskarw | (~user@user/oskarw) (Remote host closed the connection) |
| 2026-03-12 22:28:37 +0100 | remedan | (~remedan@78-80-95-79.customers.tmcz.cz) remedan |
| 2026-03-12 22:32:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 22:37:46 +0100 | <aka_dude> | How to concatenate to lists on type level? |
| 2026-03-12 22:37:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2026-03-12 22:39:56 +0100 | <aka_dude> | I implemented a type family for that but hoped there is something in base for that |
| 2026-03-12 22:40:01 +0100 | <aka_dude> | Can't find though |
| 2026-03-12 22:43:48 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-03-12 22:46:52 +0100 | <geekosaur> | https://downloads.haskell.org/ghc/latest/docs/libraries/base-4.22.0.0-66f8/GHC-TypeLits.html#t:App… |
| 2026-03-12 22:47:23 +0100 | <geekosaur> | "For now, this module is the API for working with type-level literals." |
| 2026-03-12 22:47:39 +0100 | <geekosaur> | oh wait, lists, sorry |
| 2026-03-12 22:47:53 +0100 | <geekosaur> | not sure there's anything specifically for type level lists |
| 2026-03-12 22:48:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 22:49:09 +0100 | <geekosaur> | I think various effects libraries provide such but they're likely to be specialized to their types |
| 2026-03-12 22:53:00 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2026-03-12 22:54:11 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-03-12 22:54:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-03-12 22:59:17 +0100 | preflex | (~preflex@user/mauke/bot/preflex) (Remote host closed the connection) |
| 2026-03-12 22:59:20 +0100 | michalz | (~michalz@185.246.207.203) (Remote host closed the connection) |
| 2026-03-12 22:59:54 +0100 | preflex | (~preflex@user/mauke/bot/preflex) preflex |
| 2026-03-12 23:04:37 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 23:06:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 23:08:09 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2026-03-12 23:09:21 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-03-12 23:10:40 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2026-03-12 23:10:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-03-12 23:12:39 +0100 | img | (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-03-12 23:13:46 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-03-12 23:13:53 +0100 | img | (~img@user/img) img |
| 2026-03-12 23:20:32 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2026-03-12 23:21:42 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 23:25:54 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-03-12 23:27:53 +0100 | chewybread | (~chewybrea@user/chewybread) (Ping timeout: 248 seconds) |
| 2026-03-12 23:32:50 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-03-12 23:32:52 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-03-12 23:35:12 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Ping timeout: 264 seconds) |
| 2026-03-12 23:37:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 23:42:04 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-03-12 23:52:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 23:56:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |