IRCBrowse

2026/03/12

2026-03-12 00:01:10 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 00:02:48 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) (Ping timeout: 264 seconds)
2026-03-12 00:04:32 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) DetourNetworkUK
2026-03-12 00:06:00 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-03-12 00:07:44 +0100Guest34(~Guest34@134.197.0.20)
2026-03-12 00:08:13 +0100Guest34(~Guest34@134.197.0.20) (Client Quit)
2026-03-12 00:13:45 +0100gmg(~user@user/gehmehgeh) gehmehgeh
2026-03-12 00:15:43 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer)
2026-03-12 00:16:47 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) DetourNetworkUK
2026-03-12 00:16:56 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 00:19:48 +0100stackdroid18(~stackdroi@user/stackdroid) ()
2026-03-12 00:22:26 +0100Anarchos(~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!)
2026-03-12 00:23:33 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2026-03-12 00:34:59 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 00:39:54 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 00:39:59 +0100czan(~czan@user/mange) czan
2026-03-12 00:40:43 +0100Square(~Square4@user/square) Square
2026-03-12 00:43:36 +0100Square2(~Square@user/square) (Ping timeout: 264 seconds)
2026-03-12 00:45:25 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2026-03-12 00:50:45 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 00:53:33 +0100Pozyomka(~pyon@user/pyon) (Read error: Connection reset by peer)
2026-03-12 00:54:43 +0100Pozyomka(~pyon@user/pyon) pyon
2026-03-12 00:55:34 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2026-03-12 01:06:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 01:09:04 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2026-03-12 01:11:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 01:22:03 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 01:27:24 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 01:32:10 +0100AlexZenon_2(~alzenon@5.139.232.240)
2026-03-12 01:33:08 +0100AlexZenon(~alzenon@5.139.232.240) (Ping timeout: 244 seconds)
2026-03-12 01:33:09 +0100humasect_(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2026-03-12 01:33:10 +0100AlexZenon(~alzenon@5.139.232.240)
2026-03-12 01:33:28 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 244 seconds)
2026-03-12 01:33:28 +0100foul_owl(~kerry@94.156.149.94) (Ping timeout: 244 seconds)
2026-03-12 01:33:59 +0100foul_owl(~kerry@94.156.149.94) foul_owl
2026-03-12 01:33:59 +0100weary-traveler(~user@user/user363627) (Ping timeout: 244 seconds)
2026-03-12 01:33:59 +0100ystael(~ystael@user/ystael) (Ping timeout: 244 seconds)
2026-03-12 01:33:59 +0100edwtjo(~edwtjo@fsf/member/edwtjo) (Ping timeout: 244 seconds)
2026-03-12 01:34:12 +0100weary-traveler(~user@user/user363627) user363627
2026-03-12 01:34:15 +0100ystael(~ystael@user/ystael) ystael
2026-03-12 01:34:31 +0100Tuplanolla(~Tuplanoll@88-114-89-88.elisa-laajakaista.fi) (Ping timeout: 264 seconds)
2026-03-12 01:35:30 +0100edwtjo(~edwtjo@fsf/member/edwtjo) edwtjo
2026-03-12 01:36:56 +0100AlexZenon_2(~alzenon@5.139.232.240) (Ping timeout: 268 seconds)
2026-03-12 01:37:50 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 01:42:46 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 01:53:38 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 02:00:28 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2026-03-12 02:08:14 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 252 seconds)
2026-03-12 02:11:41 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 02:11:48 +0100xff0x(~xff0x@2405:6580:b080:900:cfba:7074:7dbc:e7e9) (Ping timeout: 264 seconds)
2026-03-12 02:16:36 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 02:18:34 +0100emmanuelux(~em@user/emmanuelux) (Read error: Connection reset by peer)
2026-03-12 02:18:46 +0100anselmschueler(~Thunderbi@user/schuelermine) schuelermine
2026-03-12 02:18:56 +0100Square(~Square4@user/square) (Ping timeout: 244 seconds)
2026-03-12 02:19:00 +0100emmanuelux(~em@user/emmanuelux) emmanuelux
2026-03-12 02:20:55 +0100acidjnk_new3(~acidjnk@p200300d6e700e503f643e9bea9c15385.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
2026-03-12 02:24:43 +0100Square(~Square4@user/square) Square
2026-03-12 02:27:29 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 02:29:20 +0100emmanuelux(~em@user/emmanuelux) (Read error: Connection reset by peer)
2026-03-12 02:32:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 02:32:36 +0100emmanuelux(~em@user/emmanuelux) emmanuelux
2026-03-12 02:38:40 +0100humasect_(~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
2026-03-12 02:43:16 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 02:44:40 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2026-03-12 02:48:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 02:59:03 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 03:03:53 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 03:05:07 +0100Googulator44(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 03:05:08 +0100Googulator7(~Googulato@92-249-180-22.pool.digikabel.hu)
2026-03-12 03:05:33 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
2026-03-12 03:06:06 +0100Googulator7(~Googulato@92-249-180-22.pool.digikabel.hu) (Client Quit)
2026-03-12 03:06:12 +0100Googulator89(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:07:13 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2026-03-12 03:08:44 +0100tromp(~textual@2001:1c00:3487:1b00:2807:b44c:c102:bda9) (Ping timeout: 252 seconds)
2026-03-12 03:14:50 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 03:15:22 +0100Googulator79(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:15:31 +0100Googulator89(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 03:16:45 +0100GdeVolpiano(~GdeVolpia@user/GdeVolpiano) (Ping timeout: 246 seconds)
2026-03-12 03:19:23 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 03:26:06 +0100anselmschueler(~Thunderbi@user/schuelermine) (Ping timeout: 244 seconds)
2026-03-12 03:27:00 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2026-03-12 03:29:40 +0100Googulator21(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:30:25 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 03:30:48 +0100Googulator16(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:30:51 +0100Googulator21(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit)
2026-03-12 03:30:56 +0100Googulator79(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 03:31:14 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 248 seconds)
2026-03-12 03:31:55 +0100Googulator99(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:32:11 +0100Googulator16(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit)
2026-03-12 03:33:45 +0100machinedgod(~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 265 seconds)
2026-03-12 03:36:57 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 03:42:26 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2026-03-12 03:42:49 +0100pabs3(~pabs3@user/pabs3) (Read error: Connection reset by peer)
2026-03-12 03:44:07 +0100qqq(~qqq@185.54.22.246)
2026-03-12 03:44:35 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2026-03-12 03:48:29 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 03:49:11 +0100pabs3(~pabs3@user/pabs3) pabs3
2026-03-12 03:55:02 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 03:55:17 +0100Googulator31(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
2026-03-12 03:55:17 +0100Googulator99(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 03:57:01 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2026-03-12 03:57:11 +0100Googulator10(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 03:59:14 +0100Googulator10(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Client Quit)
2026-03-12 03:59:16 +0100Googulator69(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 04:00:28 +0100Googulator31(~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Ping timeout: 240 seconds)
2026-03-12 04:03:18 +0100czan(~czan@user/mange) (Ping timeout: 244 seconds)
2026-03-12 04:05:27 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 04:05:31 +0100Googulator69(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 04:05:59 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 04:10:32 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 04:21:45 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 04:26:06 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2026-03-12 04:31:59 +0100Square2(~Square@user/square) Square
2026-03-12 04:34:18 +0100Square(~Square4@user/square) (Ping timeout: 244 seconds)
2026-03-12 04:37:09 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 04:38:07 +0100qqq(~qqq@185.54.22.246) (Ping timeout: 264 seconds)
2026-03-12 04:42:18 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2026-03-12 04:52:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 04:54:46 +0100peterbecich(~Thunderbi@71.84.33.135) peterbecich
2026-03-12 04:57:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 05:08:26 +0100jeremyn(~jeremy@user/jeremyn) jeremyn
2026-03-12 05:08:44 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 05:09:23 +0100 <jeremyn> \
2026-03-12 05:16:00 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 05:24:17 +0100spew(~spew@user/spew) (Quit: nyaa~)
2026-03-12 05:26:00 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 245 seconds)
2026-03-12 05:26:45 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 05:28:12 +0100Square2(~Square@user/square) (Ping timeout: 255 seconds)
2026-03-12 05:31:39 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-03-12 05:37:35 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer)
2026-03-12 05:37:51 +0100DetourNe-(~DetourNet@user/DetourNetworkUK) DetourNetworkUK
2026-03-12 05:40:05 +0100DetourNe-DetourNetworkUK
2026-03-12 05:42:33 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 05:47:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-03-12 05:48:15 +0100kadobanana(~mud@user/kadoban) (Quit: quit)
2026-03-12 06:07:11 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 06:09:23 +0100michalz(~michalz@185.246.207.203)
2026-03-12 06:11:50 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 06:22:58 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 06:27:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2026-03-12 06:33:10 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 06:33:25 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 06:38:20 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 06:42:09 +0100divlamir(~divlamir@user/divlamir) (Read error: Connection reset by peer)
2026-03-12 06:42:26 +0100divlamir(~divlamir@user/divlamir) divlamir
2026-03-12 06:43:14 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 06:52:23 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 06:59:07 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 07:09:56 +0100takuan(~takuan@d8D86B9E9.access.telenet.be)
2026-03-12 07:10:27 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 07:13:46 +0100tusko(~uwu@user/tusko) (Ping timeout: 258 seconds)
2026-03-12 07:15:24 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 07:20:21 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) (Ping timeout: 246 seconds)
2026-03-12 07:24:35 +0100jreicher(~joelr@user/jreicher) (Quit: In transit)
2026-03-12 07:25:51 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 07:26:16 +0100chromoblob(~chromoblo@user/chromob1ot1c) (Quit: Quit)
2026-03-12 07:26:31 +0100chromoblob(~chromoblo@user/chromob1ot1c) chromoblob\0
2026-03-12 07:30:30 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-03-12 07:37:39 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 07:41:12 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 264 seconds)
2026-03-12 07:41:37 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 07:46:48 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2026-03-12 07:47:11 +0100haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2026-03-12 07:54:55 +0100mud(~mud@user/kadoban) kadoban
2026-03-12 08:03:06 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 08:03:21 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 08:09:13 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 08:13:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 08:19:37 +0100mulk(~mulk@pd95146df.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2026-03-12 08:20:27 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2026-03-12 08:22:34 +0100emmanuelux(~em@user/emmanuelux) (Quit: bye)
2026-03-12 08:22:54 +0100emmanuelux(~em@user/emmanuelux) emmanuelux
2026-03-12 08:26:30 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2026-03-12 08:26:56 +0100dolio(~dolio@130.44.140.168) (Quit: ZNC 1.10.1 - https://znc.in)
2026-03-12 08:27:40 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 08:28:21 +0100dolio(~dolio@130.44.140.168) dolio
2026-03-12 08:31:52 +0100dolio(~dolio@130.44.140.168) (Client Quit)
2026-03-12 08:32:24 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-03-12 08:37:46 +0100dolio(~dolio@130.44.140.168) dolio
2026-03-12 08:43:14 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 08:47:48 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 08:54:09 +0100foul_owl(~kerry@94.156.149.94) (Ping timeout: 246 seconds)
2026-03-12 08:54:26 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 08:55:23 +0100jeremyn(~jeremy@user/jeremyn) (Ping timeout: 268 seconds)
2026-03-12 08:59:12 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 08:59:33 +0100Enrico63(~Enrico63@host-82-61-84-117.retail.telecomitalia.it) Enrico63
2026-03-12 08:59:52 +0100danza(~danza@user/danza) danza
2026-03-12 09:05:26 +0100tusko(~uwu@user/tusko) tusko
2026-03-12 09:06:51 +0100Enrico63(~Enrico63@host-82-61-84-117.retail.telecomitalia.it) (Quit: Client closed)
2026-03-12 09:07:50 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) DetourNetworkUK
2026-03-12 09:08:03 +0100foul_owl(~kerry@94.156.149.92) foul_owl
2026-03-12 09:09:48 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 09:13:32 +0100acidjnk_new3(~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de)
2026-03-12 09:15:07 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2026-03-12 09:18:21 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 09:18:21 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 09:18:21 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 09:37:35 +0100chele(~chele@user/chele) chele
2026-03-12 09:41:32 +0100kimiamania40(~b4b260c9@user/kimiamania) kimiamania
2026-03-12 09:42:04 +0100kimiamania4(~b4b260c9@user/kimiamania) (Read error: Connection reset by peer)
2026-03-12 09:42:04 +0100kimiamania40kimiamania4
2026-03-12 09:45:13 +0100emmanuelux(~em@user/emmanuelux) (Quit: bye)
2026-03-12 09:49:08 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2026-03-12 09:50:10 +0100AlexNoo_AlexNoo
2026-03-12 09:50:31 +0100merijn(~merijn@77.242.116.146) merijn
2026-03-12 09:57:44 +0100akegalj(~akegalj@78-2-210-167.adsl.net.t-com.hr) akegalj
2026-03-12 10:06:49 +0100qqq(~qqq@185.54.22.246)
2026-03-12 10:14:26 +0100jreicher(~joelr@user/jreicher) jreicher
2026-03-12 10:15:33 +0100oskarw(~user@user/oskarw) oskarw
2026-03-12 10:38:32 +0100danza(~danza@user/danza) (Read error: Connection reset by peer)
2026-03-12 10:38:50 +0100danz14649(~danza@user/danza) danza
2026-03-12 10:48:13 +0100fp1(~Thunderbi@2001:708:20:1406::10c5) fp
2026-03-12 10:54:18 +0100fp2(~Thunderbi@2001:708:20:1406::10c5) fp
2026-03-12 10:54:45 +0100fp1(~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds)
2026-03-12 10:56:36 +0100fp2fp1
2026-03-12 10:58:39 +0100bionade24(~quassel@server2.oscloud.info) (Read error: Connection reset by peer)
2026-03-12 10:59:04 +0100bionade24(~quassel@server2.oscloud.info) bionade24
2026-03-12 11:01:48 +0100AlexZenon(~alzenon@5.139.232.240) (Ping timeout: 244 seconds)
2026-03-12 11:04:02 +0100dhil(~dhil@5.151.29.139) dhil
2026-03-12 11:07:21 +0100AlexZenon(~alzenon@5.139.232.240)
2026-03-12 11:09:12 +0100poscat(~poscat@user/poscat) poscat
2026-03-12 11:11:26 +0100poscat0x04(~poscat@user/poscat) (Ping timeout: 268 seconds)
2026-03-12 11:14:15 +0100danz14649(~danza@user/danza) (Remote host closed the connection)
2026-03-12 11:14:57 +0100danza(~danza@user/danza) danza
2026-03-12 11:17:23 +0100danza(~danza@user/danza) (Remote host closed the connection)
2026-03-12 11:17:43 +0100danza(~danza@user/danza) danza
2026-03-12 11:18:19 +0100qqq(~qqq@185.54.22.246) (Ping timeout: 264 seconds)
2026-03-12 11:19:41 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 265 seconds)
2026-03-12 11:49:03 +0100acidjnk_new(~acidjnk@p200300d6e700e551a4c32391cc3108f5.dip0.t-ipconnect.de)
2026-03-12 11:51:53 +0100acidjnk_new3(~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2026-03-12 11:55:35 +0100fp1(~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds)
2026-03-12 11:57:11 +0100danza(~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 +0100takuan(~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
2026-03-12 12:01:44 +0100takuan(~takuan@d8D86B9E9.access.telenet.be)
2026-03-12 12:15:43 +0100GdeVolpiano(~GdeVolpia@user/GdeVolpiano) GdeVolpiano
2026-03-12 12:17:37 +0100xff0x(~xff0x@2405:6580:b080:900:855c:3368:d601:eb86)
2026-03-12 12:34:42 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 248 seconds)
2026-03-12 12:37:42 +0100noctux(~noctux@user/noctux) (Read error: Connection reset by peer)
2026-03-12 12:40:12 +0100noctux(~noctux@user/noctux) noctux
2026-03-12 12:40:35 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds)
2026-03-12 12:47:56 +0100poscat0x04(~poscat@user/poscat) poscat
2026-03-12 12:48:14 +0100dhil(~dhil@5.151.29.139) (Ping timeout: 244 seconds)
2026-03-12 12:49:13 +0100poscat(~poscat@user/poscat) (Quit: Bye)
2026-03-12 12:52:34 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 12:52:34 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 12:52:34 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 12:57:28 +0100preflex(~preflex@user/mauke/bot/preflex) (Read error: Connection reset by peer)
2026-03-12 12:57:28 +0100mauke(~mauke@user/mauke) (Read error: Connection reset by peer)
2026-03-12 13:00:05 +0100preflex(~preflex@user/mauke/bot/preflex) preflex
2026-03-12 13:00:51 +0100dhil(~dhil@5.151.29.139) dhil
2026-03-12 13:03:11 +0100mauke(~mauke@user/mauke) mauke
2026-03-12 13:16:51 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 268 seconds)
2026-03-12 13:21:18 +0100anselmschueler(~Thunderbi@user/schuelermine) schuelermine
2026-03-12 13:23:18 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2026-03-12 13:31:46 +0100haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8)
2026-03-12 13:31:46 +0100haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host)
2026-03-12 13:31:46 +0100haritz(~hrtz@user/haritz) haritz
2026-03-12 13:31:57 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 13:31:57 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 13:31:57 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 13:33:17 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2026-03-12 13:41:58 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 244 seconds)
2026-03-12 13:51:11 +0100AlexZenon(~alzenon@5.139.232.240) (Quit: ;-)
2026-03-12 13:51:41 +0100Alex_delenda_est(~al_test@5.139.232.240) (Quit: ;-)
2026-03-12 13:52:11 +0100AlexNoo(~AlexNoo@5.139.232.240) (Quit: Leaving)
2026-03-12 14:06:14 +0100qqq(~qqq@185.54.22.246)
2026-03-12 14:09:05 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 14:09:20 +0100anselmschueler(~Thunderbi@user/schuelermine) (Ping timeout: 245 seconds)
2026-03-12 14:13:22 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 14:16:04 +0100qqq(~qqq@185.54.22.246) (Ping timeout: 244 seconds)
2026-03-12 14:22:49 +0100AlexZenon(~alzenon@5.139.232.240)
2026-03-12 14:28:02 +0100Alex_delenda_est(~al_test@5.139.232.240)
2026-03-12 14:33:00 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 14:35:36 +0100qqq(~qqq@185.54.22.246)
2026-03-12 14:38:03 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 272 seconds)
2026-03-12 14:49:10 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 14:49:10 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 14:49:10 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 14:54:03 +0100arandombit(~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 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 15:05:44 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 15:05:44 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 15:10:19 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 244 seconds)
2026-03-12 15:22:01 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 15:23:30 +0100ski. 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 +0100Square2(~Square@user/square) Square
2026-03-12 15:24:26 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds)
2026-03-12 15:24:38 +0100jeremyn(~jeremy@user/jeremyn) jeremyn
2026-03-12 15:26:26 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 248 seconds)
2026-03-12 15:27:15 +0100 <mesaoptimizer> good for her
2026-03-12 15:33:54 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 15:46:01 +0100jmcantrell_(~weechat@user/jmcantrell) jmcantrell
2026-03-12 15:46:01 +0100jmcantrell_jmcantrell
2026-03-12 15:49:04 +0100jeremyn(~jeremy@user/jeremyn) (Ping timeout: 244 seconds)
2026-03-12 15:49:04 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
2026-03-12 15:50:54 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be) kuribas
2026-03-12 15:56:45 +0100Digitteknohippie(~user@user/digit) Digit
2026-03-12 15:56:48 +0100Digit(~user@user/digit) (Ping timeout: 264 seconds)
2026-03-12 16:09:13 +0100oskarw(~user@user/oskarw) (Ping timeout: 244 seconds)
2026-03-12 16:35:56 +0100machinedgod(~machinedg@d172-219-48-230.abhsia.telus.net) machinedgod
2026-03-12 16:36:52 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2026-03-12 16:38:14 +0100euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2026-03-12 16:43:19 +0100myme(~myme@2a01:799:d5e:5f00:332d:919:8ee8:93eb) (Ping timeout: 244 seconds)
2026-03-12 16:44:21 +0100myme(~myme@2a01:799:d5e:5f00:303a:da6f:3ef4:dbc1) myme
2026-03-12 16:48:04 +0100Wygulmage(~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 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 252 seconds)
2026-03-12 17:05:14 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 17:07:34 +0100chele(~chele@user/chele) (Remote host closed the connection)
2026-03-12 17:08:59 +0100kupi(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 +0100Ranhir(~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 +0100somemathguy(~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 +0100somemathguy(~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 +0100DigitteknohippieDigit
2026-03-12 17:29:04 +0100Ranhir(~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 +0100merijn(~merijn@77.242.116.146) (Ping timeout: 245 seconds)
2026-03-12 17:47:27 +0100skicoughs and stares at `Read' and `Show'
2026-03-12 17:51:10 +0100ski. 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 +0100chewybread(~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 +0100EvanRlooks 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 +0100akegalj(~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 +0100humasect(~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 +0100qqq(~qqq@185.54.22.246) (Ping timeout: 245 seconds)
2026-03-12 18:01:51 +0100Anarchos(~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 +0100Ranhir(~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 +0100Wygulmage4(~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 +0100bionade24(~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 +0100bionade24(~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 +0100Wygulmage(~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 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2026-03-12 18:12:45 +0100kuribas(~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 +0100anselmschueler(~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 +0100Ranhir(~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 +0100anselmschueler(~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 +0100mulk(~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 +0100merijn(~merijn@77.242.116.146) merijn
2026-03-12 18:27:39 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2026-03-12 18:30:38 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 18:31:01 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 18:31:38 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2026-03-12 18:32:26 +0100euphores(~SASL_euph@user/euphores) euphores
2026-03-12 18:35:46 +0100qqq(~qqq@185.54.22.246)
2026-03-12 18:39:12 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 18:39:43 +0100anselmschueler(~Thunderbi@user/schuelermine) schuelermine
2026-03-12 18:39:57 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 18:40:40 +0100anselmschueler(~Thunderbi@user/schuelermine) (Client Quit)
2026-03-12 18:40:41 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 18:42:43 +0100Tuplanolla(~Tuplanoll@88-114-89-88.elisa-laajakaista.fi) Tuplanolla
2026-03-12 18:43:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:44:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:44:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 18:44:50 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:45:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 18:46:09 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 18:47:21 +0100oskarw(~user@user/oskarw) oskarw
2026-03-12 18:49:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:49:38 +0100AlexNoo_(~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 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:50:44 +0100AlexNoo_(~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 +0100AlexNoo__(~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 +0100dhil(~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 +0100AlexNoo(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:55:22 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 18:56:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 18:56:05 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 18:56:12 +0100chewybread(~chewybrea@user/chewybread) (Ping timeout: 264 seconds)
2026-03-12 18:56:48 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 18:59:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:00:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:00:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:01:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:01:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:02:08 +0100AlexNoo__(~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 +0100merijn(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:05:34 +0100Wygulmage4(~Wygulmage@user/Wygulmage) (Quit: Client closed)
2026-03-12 19:05:38 +0100AlexNoo_(~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 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:06:02 +0100 <haskellbridge> <ijouw> Seems useful
2026-03-12 19:06:20 +0100Wygulmage(~Wygulmage@user/Wygulmage) Wygulmage
2026-03-12 19:06:26 +0100arandombit(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:06:44 +0100 <ski> and
2026-03-12 19:06:44 +0100AlexNoo_(~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 +0100AlexNoo__(~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 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 19:07:55 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 19:07:55 +0100arandombit(~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 +0100jeremyn(~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 +0100AlexNoo(~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 +0100AlexNoo_(~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 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:12:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:12:05 +0100AlexNoo_(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:13:17 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 268 seconds)
2026-03-12 19:15:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:16:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:16:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:17:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:17:25 +0100AlexNoo_(~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 +0100qqq(~qqq@185.54.22.246) (Ping timeout: 245 seconds)
2026-03-12 19:18:06 +0100peterbecich(~Thunderbi@71.84.33.135) peterbecich
2026-03-12 19:18:09 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:18:37 +0100kupi(uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2026-03-12 19:20:16 +0100qqq(~qqq@185.54.22.246)
2026-03-12 19:21:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:21:38 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:22:02 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:22:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:22:45 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:23:29 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:23:31 +0100Googulator22(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:23:54 +0100Googulator53(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:26:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:27:22 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:28:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:28:05 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:28:49 +0100AlexNoo__(~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 +0100merijn(~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 +0100someb(~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 +0100wbrawner(~wbrawner@129.146.105.153) wbrawner
2026-03-12 19:31:46 +0100AlexNoo(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:32:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:33:10 +0100someb(~someb@24.42.43.79) ()
2026-03-12 19:33:16 +0100Googulator22(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:33:17 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:33:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:33:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:33:42 +0100skishrugs
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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:34:39 +0100merijn(~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 +0100AlexNoo(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:38:02 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:38:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:38:45 +0100AlexNoo_(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:39:41 +0100 <ski> Wygulmage : side conditions ?
2026-03-12 19:40:07 +0100arandombit(~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 +0100jeremyn(~jeremy@user/jeremyn) (Quit: Konversation terminated!)
2026-03-12 19:40:41 +0100jeremyn(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:42:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:43:22 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:44:05 +0100AlexNoo_(~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 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 246 seconds)
2026-03-12 19:44:49 +0100AlexNoo__(~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 +0100merijn(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:47:50 +0100Googulator38(~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 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:48:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:48:18 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds)
2026-03-12 19:48:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:49:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:49:25 +0100AlexNoo_(~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 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 19:50:08 +0100AlexNoo__(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:53:38 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:53:39 +0100 <ski> ("-" | "?<") , ("|" , ",") , "-|"
2026-03-12 19:54:01 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:54:44 +0100AlexNoo_(~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 +0100AlexNoo__(~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 +0100AlexNoo(~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 +0100Googulator38(~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 +0100Googulator38(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:59:02 +0100 <ski> { ... }
2026-03-12 19:59:11 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 19:59:11 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 19:59:11 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 19:59:21 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:00:04 +0100AlexNoo_(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 20:02:46 +0100Wygulmage88(~Wygulmage@user/Wygulmage) Wygulmage
2026-03-12 20:02:58 +0100CiaoSen(~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 +0100AlexNoo(~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 +0100AlexNoo_(~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 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:05:25 +0100AlexNoo_(~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 +0100Wygulmage(~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
2026-03-12 20:06:09 +0100AlexNoo__(~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 +0100AlexNoo(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:10:02 +0100AlexNoo(~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 +0100Wygulmage88(~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
2026-03-12 20:10:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:10:45 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:11:29 +0100AlexNoo__(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:14:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:15:22 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:16:05 +0100AlexNoo_(~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 +0100AlexNoo__(~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 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:20:18 +0100AlexNoo_(~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 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 20:20:51 +0100Ranhir(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:21:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:22:09 +0100AlexNoo__(~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