Home liberachat/#haskell: Logs Calendar

Logs on 2026-03-12 (liberachat/#haskell)

00:06:15 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:09:04 humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
00:11:15 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
00:22:03 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:27:24 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
00:32:10 AlexZenon_2 joins (~alzenon@5.139.232.240)
00:33:08 × AlexZenon quits (~alzenon@5.139.232.240) (Ping timeout: 244 seconds)
00:33:09 humasect_ joins (~humasect@dyn-192-249-132-90.nexicom.net)
00:33:10 AlexZenon joins (~alzenon@5.139.232.240)
00:33:28 × humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 244 seconds)
00:33:28 × foul_owl quits (~kerry@94.156.149.94) (Ping timeout: 244 seconds)
00:33:59 foul_owl joins (~kerry@94.156.149.94)
00:33:59 × weary-traveler quits (~user@user/user363627) (Ping timeout: 244 seconds)
00:33:59 × ystael quits (~ystael@user/ystael) (Ping timeout: 244 seconds)
00:33:59 × edwtjo quits (~edwtjo@fsf/member/edwtjo) (Ping timeout: 244 seconds)
00:34:12 weary-traveler joins (~user@user/user363627)
00:34:15 ystael joins (~ystael@user/ystael)
00:34:31 × Tuplanolla quits (~Tuplanoll@88-114-89-88.elisa-laajakaista.fi) (Ping timeout: 264 seconds)
00:35:30 edwtjo joins (~edwtjo@fsf/member/edwtjo)
00:36:56 × AlexZenon_2 quits (~alzenon@5.139.232.240) (Ping timeout: 268 seconds)
00:37:50 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:42:46 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
00:53:38 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:00:28 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
01:08:14 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 252 seconds)
01:11:41 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:11:48 × xff0x quits (~xff0x@2405:6580:b080:900:cfba:7074:7dbc:e7e9) (Ping timeout: 264 seconds)
01:16:36 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
01:18:34 × emmanuelux quits (~em@user/emmanuelux) (Read error: Connection reset by peer)
01:18:46 anselmschueler joins (~Thunderbi@user/schuelermine)
01:18:56 × Square quits (~Square4@user/square) (Ping timeout: 244 seconds)
01:19:00 emmanuelux joins (~em@user/emmanuelux)
01:20:55 × acidjnk_new3 quits (~acidjnk@p200300d6e700e503f643e9bea9c15385.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
01:24:43 Square joins (~Square4@user/square)
01:27:29 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:29:20 × emmanuelux quits (~em@user/emmanuelux) (Read error: Connection reset by peer)
01:32:15 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
01:32:36 emmanuelux joins (~em@user/emmanuelux)
01:38:40 × humasect_ quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
01:43:16 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:44:40 humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
01:48:19 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
01:59:03 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:03:53 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
02:05:07 × Googulator44 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
02:05:08 Googulator7 joins (~Googulato@92-249-180-22.pool.digikabel.hu)
02:05:33 × humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
02:06:06 × Googulator7 quits (~Googulato@92-249-180-22.pool.digikabel.hu) (Client Quit)
02:06:12 Googulator89 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:07:13 xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
02:08:44 × tromp quits (~textual@2001:1c00:3487:1b00:2807:b44c:c102:bda9) (Ping timeout: 252 seconds)
02:14:50 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:15:22 Googulator79 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:15:31 × Googulator89 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
02:16:45 × GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 246 seconds)
02:19:23 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
02:26:06 × anselmschueler quits (~Thunderbi@user/schuelermine) (Ping timeout: 244 seconds)
02:27:00 humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
02:29:40 Googulator21 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:30:25 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:30:48 Googulator16 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:30:51 × Googulator21 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit)
02:30:56 × Googulator79 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
02:31:14 × humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 248 seconds)
02:31:55 Googulator99 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:32:11 × Googulator16 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Client Quit)
02:33:45 × machinedgod quits (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 265 seconds)
02:36:57 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
02:42:26 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
02:42:49 × pabs3 quits (~pabs3@user/pabs3) (Read error: Connection reset by peer)
02:44:07 qqq joins (~qqq@185.54.22.246)
02:44:35 ChaiTRex joins (~ChaiTRex@user/chaitrex)
02:48:29 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:49:11 pabs3 joins (~pabs3@user/pabs3)
02:55:02 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
02:55:17 Googulator31 joins (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu)
02:55:17 × Googulator99 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Quit: Client closed)
02:57:01 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:57:11 Googulator10 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
02:59:14 × Googulator10 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Client Quit)
02:59:16 Googulator69 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
03:00:28 × Googulator31 quits (~Googulato@2a01-036d-0106-0119-5d77-22bc-bcbf-a57b.pool6.digikabel.hu) (Ping timeout: 240 seconds)
03:03:18 × czan quits (~czan@user/mange) (Ping timeout: 244 seconds)
03:05:27 Googulator53 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
03:05:31 × Googulator69 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
03:05:59 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:10:32 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
03:21:45 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:26:06 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
03:31:59 Square2 joins (~Square@user/square)
03:34:18 × Square quits (~Square4@user/square) (Ping timeout: 244 seconds)
03:37:09 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:38:07 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 264 seconds)
03:42:18 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
03:52:55 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:54:46 peterbecich joins (~Thunderbi@71.84.33.135)
03:57:55 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
04:08:26 jeremyn joins (~jeremy@user/jeremyn)
04:08:44 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
04:09:23 <jeremyn> \
04:16:00 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
04:24:17 × spew quits (~spew@user/spew) (Quit: nyaa~)
04:26:00 × peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 245 seconds)
04:26:45 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
04:28:12 × Square2 quits (~Square@user/square) (Ping timeout: 255 seconds)
04:31:39 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
04:37:35 × DetourNetworkUK quits (~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer)
04:37:51 DetourNe- joins (~DetourNet@user/DetourNetworkUK)
04:40:05 DetourNe- is now known as DetourNetworkUK
04:42:33 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
04:47:15 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
04:48:15 × kadobanana quits (~mud@user/kadoban) (Quit: quit)
05:07:11 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:09:23 michalz joins (~michalz@185.246.207.203)
05:11:50 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
05:22:58 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:27:55 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
05:33:10 × Googulator53 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
05:33:25 Googulator53 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
05:38:20 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:42:09 × divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer)
05:42:26 divlamir joins (~divlamir@user/divlamir)
05:43:14 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
05:52:23 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:59:07 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
06:09:56 takuan joins (~takuan@d8D86B9E9.access.telenet.be)
06:10:27 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:13:46 × tusko quits (~uwu@user/tusko) (Ping timeout: 258 seconds)
06:15:24 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
06:20:21 × DetourNetworkUK quits (~DetourNet@user/DetourNetworkUK) (Ping timeout: 246 seconds)
06:24:35 × jreicher quits (~joelr@user/jreicher) (Quit: In transit)
06:25:51 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:26:16 × chromoblob quits (~chromoblo@user/chromob1ot1c) (Quit: Quit)
06:26:31 chromoblob joins (~chromoblo@user/chromob1ot1c)
06:30:30 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
06:37:39 AlexNoo_ joins (~AlexNoo@5.139.232.240)
06:41:12 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 264 seconds)
06:41:37 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:46:48 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
06:47:11 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
06:54:55 mud joins (~mud@user/kadoban)
07:03:06 × Googulator53 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
07:03:21 Googulator53 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
07:09:13 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:13:55 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
07:19:37 × mulk quits (~mulk@pd95146df.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
07:20:27 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
07:22:34 × emmanuelux quits (~em@user/emmanuelux) (Quit: bye)
07:22:54 emmanuelux joins (~em@user/emmanuelux)
07:26:30 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
07:26:56 × dolio quits (~dolio@130.44.140.168) (Quit: ZNC 1.10.1 - https://znc.in)
07:27:40 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:28:21 dolio joins (~dolio@130.44.140.168)
07:31:52 × dolio quits (~dolio@130.44.140.168) (Client Quit)
07:32:24 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
07:37:46 dolio joins (~dolio@130.44.140.168)
07:43:14 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:47:48 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
07:54:09 × foul_owl quits (~kerry@94.156.149.94) (Ping timeout: 246 seconds)
07:54:26 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:55:23 × jeremyn quits (~jeremy@user/jeremyn) (Ping timeout: 268 seconds)
07:59:12 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
07:59:33 Enrico63 joins (~Enrico63@host-82-61-84-117.retail.telecomitalia.it)
07:59:52 danza joins (~danza@user/danza)
08:05:26 tusko joins (~uwu@user/tusko)
08:06:51 × Enrico63 quits (~Enrico63@host-82-61-84-117.retail.telecomitalia.it) (Quit: Client closed)
08:07:50 DetourNetworkUK joins (~DetourNet@user/DetourNetworkUK)
08:08:03 foul_owl joins (~kerry@94.156.149.92)
08:09:48 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
08:13:32 acidjnk_new3 joins (~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de)
08:15:07 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
08:18:21 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
08:18:21 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
08:18:21 arandombit joins (~arandombi@user/arandombit)
08:37:35 chele joins (~chele@user/chele)
08:41:32 kimiamania40 joins (~b4b260c9@user/kimiamania)
08:42:04 × kimiamania4 quits (~b4b260c9@user/kimiamania) (Read error: Connection reset by peer)
08:42:04 kimiamania40 is now known as kimiamania4
08:45:13 × emmanuelux quits (~em@user/emmanuelux) (Quit: bye)
08:49:08 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:50:10 AlexNoo_ is now known as AlexNoo
08:50:31 merijn joins (~merijn@77.242.116.146)
08:57:44 akegalj joins (~akegalj@78-2-210-167.adsl.net.t-com.hr)
09:06:49 qqq joins (~qqq@185.54.22.246)
09:14:26 jreicher joins (~joelr@user/jreicher)
09:15:33 oskarw joins (~user@user/oskarw)
09:38:32 × danza quits (~danza@user/danza) (Read error: Connection reset by peer)
09:38:50 danz14649 joins (~danza@user/danza)
09:48:13 fp1 joins (~Thunderbi@2001:708:20:1406::10c5)
09:54:18 fp2 joins (~Thunderbi@2001:708:20:1406::10c5)
09:54:45 × fp1 quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds)
09:56:36 fp2 is now known as fp1
09:58:39 × bionade24 quits (~quassel@server2.oscloud.info) (Read error: Connection reset by peer)
09:59:04 bionade24 joins (~quassel@server2.oscloud.info)
10:01:48 × AlexZenon quits (~alzenon@5.139.232.240) (Ping timeout: 244 seconds)
10:04:02 dhil joins (~dhil@5.151.29.139)
10:07:21 AlexZenon joins (~alzenon@5.139.232.240)
10:09:12 poscat joins (~poscat@user/poscat)
10:11:26 × poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 268 seconds)
10:14:15 × danz14649 quits (~danza@user/danza) (Remote host closed the connection)
10:14:57 danza joins (~danza@user/danza)
10:17:23 × danza quits (~danza@user/danza) (Remote host closed the connection)
10:17:43 danza joins (~danza@user/danza)
10:18:19 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 264 seconds)
10:19:41 × xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 265 seconds)
10:49:03 acidjnk_new joins (~acidjnk@p200300d6e700e551a4c32391cc3108f5.dip0.t-ipconnect.de)
10:51:53 × acidjnk_new3 quits (~acidjnk@p200300d6e700e5038fcc42959c1b3c05.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
10:55:35 × fp1 quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 245 seconds)
10:57:11 × danza quits (~danza@user/danza) (Remote host closed the connection)
10:57:16 __monty__ joins (~toonn@user/toonn)
11:00:33 × takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
11:01:44 takuan joins (~takuan@d8D86B9E9.access.telenet.be)
11:15:43 GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano)
11:17:37 xff0x joins (~xff0x@2405:6580:b080:900:855c:3368:d601:eb86)
11:34:42 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 248 seconds)
11:37:42 × noctux quits (~noctux@user/noctux) (Read error: Connection reset by peer)
11:40:12 noctux joins (~noctux@user/noctux)
11:40:35 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds)
11:47:56 poscat0x04 joins (~poscat@user/poscat)
11:48:14 × dhil quits (~dhil@5.151.29.139) (Ping timeout: 244 seconds)
11:49:13 × poscat quits (~poscat@user/poscat) (Quit: Bye)
11:52:34 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
11:52:34 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
11:52:34 arandombit joins (~arandombi@user/arandombit)
11:57:28 × preflex quits (~preflex@user/mauke/bot/preflex) (Read error: Connection reset by peer)
11:57:28 × mauke quits (~mauke@user/mauke) (Read error: Connection reset by peer)
12:00:05 preflex joins (~preflex@user/mauke/bot/preflex)
12:00:51 dhil joins (~dhil@5.151.29.139)
12:03:11 mauke joins (~mauke@user/mauke)
12:16:51 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds)
12:21:18 anselmschueler joins (~Thunderbi@user/schuelermine)
12:23:18 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
12:31:46 haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8)
12:31:46 × haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host)
12:31:46 haritz joins (~hrtz@user/haritz)
12:31:57 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
12:31:57 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
12:31:57 arandombit joins (~arandombi@user/arandombit)
12:33:17 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
12:41:58 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds)
12:51:11 × AlexZenon quits (~alzenon@5.139.232.240) (Quit: ;-)
12:51:41 × Alex_delenda_est quits (~al_test@5.139.232.240) (Quit: ;-)
12:52:11 × AlexNoo quits (~AlexNoo@5.139.232.240) (Quit: Leaving)
13:06:14 qqq joins (~qqq@185.54.22.246)
13:09:05 AlexNoo joins (~AlexNoo@5.139.232.240)
13:09:20 × anselmschueler quits (~Thunderbi@user/schuelermine) (Ping timeout: 245 seconds)
13:13:22 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
13:16:04 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 244 seconds)
13:22:49 AlexZenon joins (~alzenon@5.139.232.240)
13:28:02 Alex_delenda_est joins (~al_test@5.139.232.240)
13:33:00 arandombit joins (~arandombi@user/arandombit)
13:35:36 qqq joins (~qqq@185.54.22.246)
13:38:03 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 272 seconds)
13:49:10 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
13:49:10 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
13:49:10 arandombit joins (~arandombi@user/arandombit)
13:54:03 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds)
13:59:14 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 248 seconds)
14:04:08 _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
14:05:44 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
14:05:44 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
14:05:44 arandombit joins (~arandombi@user/arandombit)
14:10:19 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds)
14:22:01 arandombit joins (~arandombi@user/arandombit)
14:23:30 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/> )
14:23:43 Square2 joins (~Square@user/square)
14:24:26 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds)
14:24:38 jeremyn joins (~jeremy@user/jeremyn)
14:26:26 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 248 seconds)
14:27:15 <mesaoptimizer> good for her
14:33:54 arandombit joins (~arandombi@user/arandombit)
14:46:01 jmcantrell_ joins (~weechat@user/jmcantrell)
14:46:01 jmcantrell_ is now known as jmcantrell
14:49:04 × jeremyn quits (~jeremy@user/jeremyn) (Ping timeout: 244 seconds)
14:49:04 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
14:50:54 kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
14:56:45 Digitteknohippie joins (~user@user/digit)
14:56:48 × Digit quits (~user@user/digit) (Ping timeout: 264 seconds)
15:09:13 × oskarw quits (~user@user/oskarw) (Ping timeout: 244 seconds)
15:35:56 machinedgod joins (~machinedg@d172-219-48-230.abhsia.telus.net)
15:36:52 ChaiTRex joins (~ChaiTRex@user/chaitrex)
15:38:14 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
15:43:19 × myme quits (~myme@2a01:799:d5e:5f00:332d:919:8ee8:93eb) (Ping timeout: 244 seconds)
15:44:21 myme joins (~myme@2a01:799:d5e:5f00:303a:da6f:3ef4:dbc1)
15:48:04 Wygulmage joins (~Wygulmage@user/Wygulmage)
15:48:53 <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?
15:49:25 <Wygulmage> I'd comment on Discourse but apparently my non-AI browser is not supported...
15:50:26 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 252 seconds)
16:05:14 arandombit joins (~arandombi@user/arandombit)
16:07:34 × chele quits (~chele@user/chele) (Remote host closed the connection)
16:08:59 kupi joins (uid212005@id-212005.hampstead.irccloud.com)
16:10:46 <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
16:10:47 <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`.
16:12:02 × Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 248 seconds)
16:16:11 <Wygulmage> Sorry. Is IRC dead, or did I just come at a bad time?
16:19:33 × somemathguy quits (~somemathg@user/somemathguy) (Ping timeout: 246 seconds)
16:20:27 <haskellbridge> <sm> it has quiet and busy times. Definitely not dead here, but you may need to wait more than 5m
16:20:50 <haskellbridge> <sm> s/but.*//
16:21:58 <haskellbridge> <sm> do you have javascript disabled in your browser ?
16:22:11 <Wygulmage> Thanks, sm. Just got worried that all the humans had left. *deep breaths*
16:22:23 <Wygulmage> Not for haskell.org.
16:22:44 <haskellbridge> <sm> :) we're still here
16:23:24 <haskellbridge> <sm> I wondered why you couldn't comment at discourse. It requires js I see.
16:23:56 somemathguy joins (~somemathg@user/somemathguy)
16:24:32 <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.
16:25:56 <Wygulmage> And possibly a Discourse problem.
16:27:13 Digitteknohippie is now known as Digit
16:29:04 Ranhir joins (~Ranhir@157.97.53.139)
16:30:19 <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
16:30:20 <Wygulmage> `deriving via WrapMonad M instance Applicative M` ?
16:43:59 <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
16:44:45 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds)
16:47:27 ski coughs and stares at `Read' and `Show'
16:51:10 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)
16:51:30 chewybread joins (~chewybrea@user/chewybread)
16:51:33 <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.
16:51:41 <EvanR> Wygulmage, the humans are dead
16:52:02 <EvanR> 🤖
16:52:58 <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 ;(
16:53:45 <Wygulmage> Which, judging by the AI slop in his youtube feed...
16:55:07 <davean> Wygulmage: Haha, the AI slop in his youtube feed is a very specific thing and I want more of it ...
16:55:40 <davean> Wygulmage: assume the AI slop is an inside joke thing.
16:56:00 <Wygulmage> \O/
16:56:30 <davean> He's entertaining a specific few of us with a specific project
16:56:31 <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
16:56:46 <davean> You wouldn't have the context to enjoy it. Its public because it was being posted in a facebook group.
16:58:42 <Wygulmage> davean: Thanks for outing yourself as part of the SkyNet that replaced Ed.
16:58:53 <EvanR> having a vector add to something other than a vector is cringe
16:59:16 <haskellbridge> <ijouw> I believe number hirarchies should be displayed as tree/graph for quick overview.
16:59:48 EvanR looks at newmind
16:59:58 <newmind> hi
16:59:59 <EvanR> seems to be some sort of bot PMming me
17:00:09 × akegalj quits (~akegalj@78-2-210-167.adsl.net.t-com.hr) (Ping timeout: 255 seconds)
17:00:12 <newmind> not a bot
17:00:57 humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
17:01:21 <newmind> just wasn't related to this conversation, but rather something you asked in a different channel yesterday
17:01:42 <EvanR> I haven't been in that channel in maybe 8 years
17:01:50 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 245 seconds)
17:01:51 Anarchos joins (~Anarchos@91-161-254-16.subs.proxad.net)
17:02:08 <haskellbridge> <ijouw> Maybe a bot impersonating you?
17:02:22 × Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 244 seconds)
17:02:30 <EvanR> unlikely
17:02:48 <newmind> oh, sorry, misread the nick, >.> terribly sorry
17:02:55 <EvanR> oh ok
17:03:11 <newmind> was a 'RyanR'
17:03:12 <mesaoptimizer> strange
17:03:14 <EvanR> lol
17:03:30 <newmind> so,, the distinct uppercase R at the end triggered a bit of a pattern match :D
17:03:35 <EvanR> tbf your message was relevant to the conversion "AI slop" xD
17:03:36 Wygulmage4 joins (~Wygulmage@user/Wygulmage)
17:03:43 <EvanR> conversation
17:03:52 <haskellbridge> <ijouw> if y == v then all but the first char match.
17:03:59 × bionade24 quits (~quassel@server2.oscloud.info) (Quit: Apocalypse Incoming!)
17:04:20 <Wygulmage4> And I think they should have started with a right near semiring rather than an "additive" semigroup.
17:04:30 bionade24 joins (~quassel@server2.oscloud.info)
17:04:54 <ski> Wygulmage4 : like <https://cokmett.github.io/cokmett/> (click on image) ?
17:05:02 <newmind> again, sorry for the disturbance, my fault >.>
17:05:15 <haskellbridge> <ijouw> Do we have somewhere explaining English terminology for that stuff?
17:06:00 <haskellbridge> <ijouw> Like an overview over names of math concepts relating to numbers?
17:06:02 <EvanR> I wonder if any of that is real
17:06:10 <Wygulmage4> ski: :')
17:06:18 <newmind> you... want logs?
17:06:28 × Wygulmage quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
17:06:36 <haskellbridge> <ijouw> No, i have enough wood?
17:06:37 <Wygulmage4> ijouw: Almost all math terminology is terrible, and you just kind of accept it.
17:07:09 <haskellbridge> <ijouw> I just do not know it.
17:07:14 <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
17:08:01 <Wygulmage4> Damn. That hurts. But yeah, why does NixOS keep arbitrarily renaming options???
17:08:43 <davean> hy does nix make modularizing something take 3x the code of just doing the thing in the first place?
17:08:43 <Wygulmage4> Still, semigroup is to group as semilattice is to ???????
17:09:59 <ski> "semi-" here is basically "not quite"
17:10:00 <EvanR> not sure that makes any sense
17:10:03 <Wygulmage4> Don't think I'll survive these truth bombs.
17:12:04 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
17:12:45 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 255 seconds)
17:13:08 <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.
17:13:26 <EvanR> you should rename it
17:13:36 <EvanR> will be very confusing it
17:14:13 <EvanR> (ring terminology already has some jargon decay in places where it depends who's talking about it means)
17:14:20 anselmschueler joins (~Thunderbi@user/schuelermine)
17:14:48 <EvanR> some of my words seem to not making it through the tubes
17:15:31 Ranhir joins (~Ranhir@157.97.53.139)
17:15:41 <Wygulmage4> I have not heard "jargon decay"; that's it exactly.
17:17:14 <Wygulmage4> But being precise and calling something a "right ringoid with additive and multiplicative associativity"... I don't know if that's better.
17:17:37 <EvanR> what is this in relation to
17:18:33 × anselmschueler quits (~Thunderbi@user/schuelermine) (Ping timeout: 248 seconds)
17:19:13 <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
17:19:46 <Wygulmage4> Or if you have access to university libraries, have them reserve you a textbook.
17:22:08 mulk joins (~mulk@pd95146df.dip0.t-ipconnect.de)
17:23:23 <haskellbridge> <ijouw> Thank you
17:25:12 <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.
17:25:27 merijn joins (~merijn@77.242.116.146)
17:27:39 Sgeo joins (~Sgeo@user/sgeo)
17:30:38 × Googulator53 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
17:31:01 Googulator53 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
17:31:38 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
17:32:26 euphores joins (~SASL_euph@user/euphores)
17:35:46 qqq joins (~qqq@185.54.22.246)
17:39:12 AlexNoo joins (~AlexNoo@5.139.232.240)
17:39:43 anselmschueler joins (~Thunderbi@user/schuelermine)
17:39:57 AlexNoo_ joins (~AlexNoo@5.139.232.240)
17:40:40 × anselmschueler quits (~Thunderbi@user/schuelermine) (Client Quit)
17:40:41 AlexNoo__ joins (~AlexNoo@5.139.232.240)
17:42:43 Tuplanolla joins (~Tuplanoll@88-114-89-88.elisa-laajakaista.fi)
17:43:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:44:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:44:42 AlexNoo joins (~AlexNoo@5.139.232.240)
17:44:50 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:45:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
17:46:09 AlexNoo__ joins (~AlexNoo@5.139.232.240)
17:47:21 oskarw joins (~user@user/oskarw)
17:49:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:49:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:49:39 <gentauro> % :t readMaybe
17:49:39 <yahb2> <interactive>:1:1: error: [GHC-88464] ; Variable not in scope: readMaybe
17:49:51 <gentauro> % import Text.Read
17:49:51 <yahb2> <no output>
17:49:53 <gentauro> % :t readMaybe
17:49:53 <yahb2> readMaybe :: Read a => String -> Maybe a
17:50:02 AlexNoo joins (~AlexNoo@5.139.232.240)
17:50:07 <EvanR> that's a good one
17:50:25 <gentauro> % data FooBar = Foo | Bar deriving Read
17:50:25 <yahb2> <no output>
17:50:35 <gentauro> % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar)
17:50:35 <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...
17:50:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:50:44 AlexNoo_ joins (~AlexNoo@5.139.232.240)
17:51:09 <gentauro> > :i (+)
17:51:11 <lambdabot> <hint>:1:1: error: parse error on input `:'
17:51:20 <gentauro> > import Text.Read
17:51:21 <lambdabot> <hint>:1:1: error: parse error on input `import'
17:51:24 <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>)
17:51:28 AlexNoo__ joins (~AlexNoo@5.139.232.240)
17:51:32 <ski> @let import Text.Read
17:51:33 <lambdabot> Defined.
17:51:54 <gentauro> > :i readMaybe
17:51:55 <lambdabot> <hint>:1:1: error: parse error on input `:'
17:51:57 <gentauro> :|
17:52:04 <ski> @type readMaybe
17:52:05 <lambdabot> Read a => String -> Maybe a
17:52:09 <EvanR> :i readMaybe
17:52:30 <ski> (there is no `@info' with lambdabot)
17:52:47 <gentauro> ski: got it
17:53:00 × dhil quits (~dhil@5.151.29.139) (Ping timeout: 244 seconds)
17:53:11 <ski> % :set -XLambdaCase
17:53:11 <yahb2> <no output>
17:53:16 <gentauro> :o
17:53:20 <ski> % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar)
17:53:20 <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
17:53:32 <ski> % :m + Data.Char
17:53:32 <yahb2> <no output>
17:53:35 <ski> % let readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar)
17:53:35 <yahb2> <no output>
17:53:47 <gentauro> % readFoobar "foo"
17:53:47 <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...
17:53:56 <gentauro> % data FooBar = Foo | Bar deriving (Read, Show)
17:53:56 <yahb2> <no output>
17:53:58 <gentauro> % readFoobar "foo"
17:53:58 <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: ; ...
17:54:13 <gentauro> % readFoobar = (\case [] -> Nothing; c:cs -> readMaybe (toUpper c : map toLower cs) :: Maybe FooBar)
17:54:13 <yahb2> <no output>
17:54:16 <gentauro> % readFoobar "foo"
17:54:16 <yahb2> Just Foo
17:54:18 <gentauro> nice
17:54:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:54:44 <ski> % (reads :: ReadS FooBar) "foo bar"
17:54:44 <yahb2> []
17:54:55 <ski> % (reads :: ReadS FooBar) "Foo Bar"
17:54:55 <yahb2> [(Foo," Bar")]
17:54:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:55:22 AlexNoo joins (~AlexNoo@5.139.232.240)
17:56:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
17:56:05 AlexNoo_ joins (~AlexNoo@5.139.232.240)
17:56:12 × chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 264 seconds)
17:56:48 AlexNoo__ joins (~AlexNoo@5.139.232.240)
17:59:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:00:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:00:42 AlexNoo joins (~AlexNoo@5.139.232.240)
18:01:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:01:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:02:08 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:02:16 <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.
18:03:01 <ski> galois connections / adjunctions
18:03:01 <haskellbridge> <ijouw> monus >> minus?
18:03:05 <ski> no
18:03:29 <ski> <https://en.wikipedia.org/wiki/Monus>
18:03:53 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
18:04:45 <ski> m ∸ o ≤ n
18:04:46 <ski> ⇔ m ≤ n + o
18:05:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:05:34 × Wygulmage4 quits (~Wygulmage@user/Wygulmage) (Quit: Client closed)
18:05:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:06:00 <ski> in words, ⌜m ∸ o⌝ is the least ⌜n⌝ such that ⌜m ≤ n + o⌝ (⌜n⌝ added to ⌜m⌝ is at least ⌜o⌝)
18:06:01 AlexNoo joins (~AlexNoo@5.139.232.240)
18:06:02 <haskellbridge> <ijouw> Seems useful
18:06:20 Wygulmage joins (~Wygulmage@user/Wygulmage)
18:06:26 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds)
18:06:27 <ski> two consequences (unit & counit) of that galois connection / adjunction are
18:06:42 <ski> m ≤ (m ∸ o) + o
18:06:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:06:44 <ski> and
18:06:44 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:06:58 <ski> (n + o) ∸ o ≤ n
18:07:19 <ski> for natural numbers (and subsets), the latter is actually an equality
18:07:37 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:07:54 <ski> for natural numbers, monus is also called cut-off / saturated / truncated subtraction
18:07:55 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
18:07:55 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
18:07:55 arandombit joins (~arandombi@user/arandombit)
18:08:42 <Wygulmage> And conveniently it's closed for natural numbers, unlike subtraction.
18:08:47 <ski> (and ⌜m ∸ o⌝ can be described as ⌜max 0 (m − o)⌝)
18:09:12 jeremyn joins (~jeremy@user/jeremyn)
18:10:19 <ski> in total programming environments, people often use monus, instead of minus, just to get it totally defined
18:10:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:10:41 <Wygulmage> But of course it doesn't work for `Int`.
18:10:42 <ski> (i've seen people define "reciprocal" of zero as zero, for similar reasons ..)
18:10:51 <Wygulmage> *shudder*
18:10:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:11:08 <ski> yea, i was thinking of stuff like recursive functions (a la Kleene)
18:11:22 AlexNoo joins (~AlexNoo@5.139.232.240)
18:12:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:12:05 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:12:20 <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
18:13:07 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:13:17 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds)
18:15:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:16:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:16:42 AlexNoo joins (~AlexNoo@5.139.232.240)
18:17:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:17:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:17:56 <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.
18:18:02 <ski> "preimage"/"inverse image", where you start with a subset of the codomain)))
18:18:05 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 245 seconds)
18:18:06 peterbecich joins (~Thunderbi@71.84.33.135)
18:18:09 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:18:37 × kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
18:20:16 qqq joins (~qqq@185.54.22.246)
18:21:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:21:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:22:02 AlexNoo joins (~AlexNoo@5.139.232.240)
18:22:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:22:45 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:23:29 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:23:31 Googulator22 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
18:23:54 × Googulator53 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
18:24:23 <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
18:24:48 <ski> (well, the version i was pondering was dependently typed, but you could also have non-dependently typed versions)
18:26:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:26:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:27:22 AlexNoo joins (~AlexNoo@5.139.232.240)
18:28:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:28:05 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:28:49 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:29:15 <Wygulmage> What would a non-dependently typed version look like?
18:29:45 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:29:55 <Wygulmage> (I'm reading up on Brzozowski derivatives and quotients of formal languages.)
18:30:39 someb joins (~someb@24.42.43.79)
18:30:57 <someb> hello?
18:31:02 <someb> anyone online?
18:31:40 <ski> Wygulmage : the version i showed above
18:31:41 wbrawner joins (~wbrawner@129.146.105.153)
18:31:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:31:56 <ski> someb : don't ask to ask, just ask
18:32:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:32:42 AlexNoo joins (~AlexNoo@5.139.232.240)
18:33:10 someb parts (~someb@24.42.43.79) ()
18:33:16 × Googulator22 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
18:33:17 Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
18:33:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:33:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:33:42 ski shrugs
18:34:04 <Wygulmage> Me a couple hours ago: <Wygulmage>     Sorry. Is IRC dead, or did I just come at a bad time?
18:34:09 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:34:39 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
18:36:24 <Wygulmage> ski: So that's using the type-level Nat?
18:36:46 <ski> no, that's a normal (value-level) `Nat'
18:37:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:37:37 <Wygulmage> And the side conditions produce type errors if they can't be proven at compile time?
18:37:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:38:02 AlexNoo joins (~AlexNoo@5.139.232.240)
18:38:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:38:45 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:39:23 <ski> dependently typed version would be `k - m : Fin n | k ?< m : Fin m -| m : Nat , n : Nat , k : Fin (m + n)'
18:39:29 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:39:41 <ski> Wygulmage : side conditions ?
18:40:07 arandombit joins (~arandombi@user/arandombit)
18:40:10 <ski> it's simultaneously defining two operations, `-' and `?<' such that they together (on the same inputs) are total
18:40:27 × jeremyn quits (~jeremy@user/jeremyn) (Quit: Konversation terminated!)
18:40:41 jeremyn joins (~jeremy@user/jeremyn)
18:40:59 <Wygulmage> Oh! I see. That would be nice. Like requiring a `null` test to use `tail`.
18:41:53 <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)
18:42:20 <Wygulmage> Right.
18:42:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:42:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:43:22 AlexNoo joins (~AlexNoo@5.139.232.240)
18:43:23 <ski> operationally, it's similar to `(-?<) : Either Nat ()' (or the dependently typed version), and using `case'-`of' to dispatch on that
18:44:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:44:05 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:44:28 <Wygulmage> So is `<?` equivalent to Haskell's `<` or does it produce a sum type?
18:44:48 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 246 seconds)
18:44:49 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:45:20 <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'
18:45:27 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:45:38 <ski> (quick, what's the result of `k / 0' and `k % 0' ?)
18:45:59 <ski> Wygulmage : neither
18:46:56 <ski> `?<' (if it terminates, is not partial) provides evidence of the `<' relation between the inputs
18:47:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:47:50 × Googulator38 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
18:47:52 <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
18:48:05 Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
18:48:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:48:18 × peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds)
18:48:42 AlexNoo joins (~AlexNoo@5.139.232.240)
18:49:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:49:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:49:32 <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"")
18:50:07 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
18:50:08 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:51:05 <ski> Wygulmage : if you want to, you could say `Right (k - m) | Left (k ?< m)' produces a sum type (`Fin m + Fin n')
18:52:15 <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: : - ?< , | -|
18:53:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:53:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:53:39 <ski> ("-" | "?<") , ("|" , ",") , "-|"
18:54:01 AlexNoo joins (~AlexNoo@5.139.232.240)
18:54:12 <ski> ((m - n) : Nat) | ((m ?< n) : ()) -| ((m : Nat) , (n : Nat))
18:54:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:54:44 AlexNoo_ joins (~AlexNoo@5.139.232.240)
18:54:50 <Wygulmage> Thanks, I was not parsing it like that.
18:55:22 <ski> (((k - m) : Fin n) | ((k ?< m) : Fin m)) -| ((m : Nat) , (n : Nat) , (k : Fin (m + n)))
18:55:28 AlexNoo__ joins (~AlexNoo@5.139.232.240)
18:55:54 <ski> (((k / n) : Fin m) , ((k % n) : Fin n)) -| ((m : Nat) , (n : Nat) , (k : Fin (m * n)))
18:56:19 <ski> er, forgot to insert the `:' ..
18:56:28 <ski> ("-" | "?<") , ":" , ("|" , ",") , "-|"
18:58:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:58:28 <EvanR> oof ok
18:58:41 × Googulator38 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
18:58:47 <ski> if you prefer a more C-like syntax :
18:58:51 <ski> nat minus(m,n) | void under(m,n)
18:58:57 Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
18:58:58 <ski> nat m,n;
18:58:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
18:59:02 <ski> { ... }
18:59:11 arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
18:59:11 × arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
18:59:11 arandombit joins (~arandombi@user/arandombit)
18:59:21 AlexNoo joins (~AlexNoo@5.139.232.240)
18:59:38 <EvanR> where is the { ... } in the original notation
18:59:54 <ski> it wasn't shown. i just showed the type signature, not the implementation
19:00:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:00:04 AlexNoo_ joins (~AlexNoo@5.139.232.240)
19:00:30 <EvanR> the implementation of what exactly, both these operators?
19:00:48 AlexNoo__ joins (~AlexNoo@5.139.232.240)
19:02:46 Wygulmage88 joins (~Wygulmage@user/Wygulmage)
19:02:58 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
19:03:29 <ski> yes
19:03:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:03:50 <EvanR> oh
19:03:51 <ski> m - Zero = m | _ ?< Zero = ‾
19:03:57 <ski> _ - Succ _ = ‾ | _ ?< Succ _ = ()
19:04:00 <ski> Succ m - Succ n = m - n | Succ m ?< Succ n = m ?< n
19:04:08 <ski> is the implementation
19:04:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:04:20 <EvanR> oh
19:04:29 <Wygulmage88> Got to change locations. Gonna check the log.
19:04:42 <EvanR> I was expecting to see - defined using ?< and ?< defined using - xD
19:04:42 AlexNoo joins (~AlexNoo@5.139.232.240)
19:05:00 <EvanR> what is ‾
19:05:20 <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
19:05:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:05:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
19:05:49 <ski> (but i allow using it in expressions, as well)
19:05:58 × Wygulmage quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
19:06:09 AlexNoo__ joins (~AlexNoo@5.139.232.240)
19:06:44 <ski> (in Haskell, you'd use `case ... of {}' for the absurd pattern case, e.g. with GADTs)
19:07:24 <ski> it is the neutral element of the ambiguous operator `|'
19:08:20 <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)
19:09:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:09:19 <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)
19:09:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:10:02 AlexNoo joins (~AlexNoo@5.139.232.240)
19:10:19 <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
19:10:28 × Wygulmage88 quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
19:10:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:10:45 AlexNoo_ joins (~AlexNoo@5.139.232.240)
19:11:29 AlexNoo__ joins (~AlexNoo@5.139.232.240)
19:13:24 <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)
19:14:25 <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)')
19:14:26 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:14:58 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:15:22 AlexNoo joins (~AlexNoo@5.139.232.240)
19:15:24 <EvanR> Zero - Succ _ = undefined
19:15:38 <EvanR> so the program will crash or
19:16:02 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:16:05 AlexNoo_ joins (~AlexNoo@5.139.232.240)
19:16:49 <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
19:16:49 AlexNoo__ joins (~AlexNoo@5.139.232.240)
19:17:02 <ski> (if you're just using one of them, it would be partial, yes)
19:17:19 <EvanR> what does applying both operators look like
19:19:46 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:20:18 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:20:20 <ski> m / n = Succ ((m - n) / n) | let () = m ?< n in Zero ; m % n = (m - n) % n | let () = m ?< n in m
19:20:42 AlexNoo joins (~AlexNoo@5.139.232.240)
19:20:51 × Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 246 seconds)
19:20:51 <ski> (that does not terminate for `n = 0'. dependently typed version i hinted at above is total, though)
19:21:22 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:21:25 AlexNoo_ joins (~AlexNoo@5.139.232.240)
19:22:09 AlexNoo__ joins (~AlexNoo@5.139.232.240)
19:22:25 <EvanR> so the Succ ((m - n) / n) will be "tried" first and if it's undefined go to the thing right of |
19:23:02 <EvanR> and the types don't have to match immediately
19:24:25 <ski> types have to match
19:24:34 <ski> and `|' is commutative
19:24:41 <EvanR> oh
19:25:06 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:25:13 <ski> operational semantics should be as if you executed `(-?<) :: Nat -> Nat -> Either () Nat'
19:25:13 <EvanR> is the commutativity guaranteed somehow by the compiler
19:25:29 <monochrom> <3 unordered alternation
19:25:31 <ski> they are not independent operations, one tried after the other
19:25:38 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:25:40 <ski> they are tried, simultaneously
19:25:52 <ski> (and so the recursion pattern of them both must align)
19:25:59 <EvanR> similar to lub
19:26:25 <ski> oh, and yes, the system would ensure that both are not defined at the same time
19:26:33 AlexNoo joins (~AlexNoo@5.139.232.240)
19:26:42 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:26:51 <monochrom> There is a Curry compiler, Curry2Go, which compiles non-determinism to Go multi-threading so all alternatives are literally tried concurrently.
19:27:11 <ski> breadth-first ?
19:27:25 <monochrom> Yeah
19:28:49 <ski> how does it handle trying to communicate a result non-locally out of an alternative ?
19:29:28 <monochrom> I don't know.
19:29:50 <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)
19:30:13 <ski> (the CTM book talks about this, in the chapter about constraint programming)
19:30:37 ski was (re)reading it recently (didn't get to that part yet, though)
19:30:58 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:31:08 AlexNoo joins (~AlexNoo@5.139.232.240)
19:31:10 <monochrom> Yeah I'm thinking "what's there to handle?" because the only thing left to do is collecting results.
19:31:29 target_i joins (~target_i@user/target-i/x-6023099)
19:34:05 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> )
19:34:07 <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.
19:34:59 <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)
19:35:00 × remedan quits (~remedan@78-80-95-79.customers.tmcz.cz) (Quit: Bye!)
19:35:04 <monochrom> It doesn't even have Prolog's cut, so you can't even kill your sibling!
19:35:10 <EvanR> the Sagrada Família on the cover is great
19:35:14 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
19:35:29 <EvanR> *your code project is going this well*
19:35:46 × target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 248 seconds)
19:36:20 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds)
19:36:41 <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
19:36:48 target_i joins (~target_i@user/target-i/x-6023099)
19:37:06 Ranhir joins (~Ranhir@157.97.53.139)
19:41:15 × target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 255 seconds)
19:41:48 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 264 seconds)
19:42:08 target_i joins (~target_i@user/target-i/x-6023099)
19:43:53 chewybread joins (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170)
19:43:53 × chewybread quits (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host)
19:43:53 chewybread joins (~chewybrea@user/chewybread)
19:44:45 <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.
19:45:24 <monochrom> I have a feeling that when there are no mutable variables, you have confluence so it doesn't matter what you do.
19:45:45 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
19:46:19 <ski> yea, Oz has declaratie concurrency for this
19:46:37 <ski> (operations block until their inputs are instantiated)
19:47:08 <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
19:49:44 Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
19:50:17 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds)
19:52:23 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.html> )
19:52:37 Lord_of_Life_ is now known as Lord_of_Life
19:54:09 <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)
19:54:14 <ski> @hackage lvish
19:54:14 <lambdabot> https://hackage.haskell.org/package/lvish
19:54:49 akegalj joins (~akegalj@141-138-62-190.dsl.iskon.hr)
19:58:00 arandombit joins (~arandombi@user/arandombit)
20:09:04 × Square2 quits (~Square@user/square) (Quit: Leaving)
20:09:19 × akegalj quits (~akegalj@141-138-62-190.dsl.iskon.hr) (Quit: leaving)
20:09:21 Square joins (~Square@user/square)
20:13:29 <gentauro> ski: every now and then uni's change their websistes and all papers linking are gone
20:13:38 <gentauro> :(
20:14:15 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:18:54 <ski> similar to many large applications or GUI systems or web sites changing, "just because", presumably to justify having interface designers or somesuch ?
20:20:46 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
20:21:15 <geekosaur> there's also this business of unis asserting ownership of other uni's web namespaces because they're better known or w/e
20:26:06 × humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
20:31:22 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:33:53 <gentauro> I'm stuck in a terminal with black background and greenish/limeish foreground. I don't understand the fuzz :-\
20:35:26 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
20:35:35 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
20:36:10 <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 :(
20:36:16 <gentauro> now that's saD
20:38:11 <haskellbridge> <sm> is it open source ?
20:39:38 AlexNoo joins (~AlexNoo@5.139.232.240)
20:40:23 AlexNoo_ joins (~AlexNoo@5.139.232.240)
20:41:07 AlexNoo__ joins (~AlexNoo@5.139.232.240)
20:42:17 × chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 248 seconds)
20:42:54 <gentauro> yeah. AGPLv3.0
20:44:02 × AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
20:44:34 × AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
20:45:38 × AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
20:46:44 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:47:13 pavonia joins (~user@user/siracusa)
20:51:27 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
20:57:06 chewybread joins (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170)
20:57:06 × chewybread quits (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host)
20:57:06 chewybread joins (~chewybrea@user/chewybread)
21:01:36 × chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 264 seconds)
21:02:00 <sm> so you know what to do :-)
21:02:05 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:03:38 <jreicher> gentauro: what's the protocol (and server?) architecture?
21:06:55 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
21:09:23 chewybread joins (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170)
21:09:23 × chewybread quits (~chewybrea@240b:10:9502:4100:80a2:daac:f3ad:170) (Changing host)
21:09:23 chewybread joins (~chewybrea@user/chewybread)
21:16:16 humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
21:17:27 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:21:45 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
21:26:34 × machinedgod quits (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 245 seconds)
21:28:14 × oskarw quits (~user@user/oskarw) (Remote host closed the connection)
21:28:37 remedan joins (~remedan@78-80-95-79.customers.tmcz.cz)
21:32:49 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:37:46 <aka_dude> How to concatenate to lists on type level?
21:37:47 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
21:39:56 <aka_dude> I implemented a type family for that but hoped there is something in base for that
21:40:01 <aka_dude> Can't find though
21:43:48 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
21:46:52 <geekosaur> https://downloads.haskell.org/ghc/latest/docs/libraries/base-4.22.0.0-66f8/GHC-TypeLits.html#t:AppendSymbol
21:47:23 <geekosaur> "For now, this module is the API for working with type-level literals."
21:47:39 <geekosaur> oh wait, lists, sorry
21:47:53 <geekosaur> not sure there's anything specifically for type level lists
21:48:15 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:49:09 <geekosaur> I think various effects libraries provide such but they're likely to be specialized to their types
21:53:00 × takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
21:54:11 takuan joins (~takuan@d8D86B9E9.access.telenet.be)
21:54:45 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
21:59:17 × preflex quits (~preflex@user/mauke/bot/preflex) (Remote host closed the connection)
21:59:20 × michalz quits (~michalz@185.246.207.203) (Remote host closed the connection)
21:59:54 preflex joins (~preflex@user/mauke/bot/preflex)
22:04:37 qqq joins (~qqq@185.54.22.246)
22:06:14 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:08:09 × takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
22:09:21 takuan joins (~takuan@d8D86B9E9.access.telenet.be)
22:10:40 × takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
22:10:49 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
22:12:39 × img quits (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in)
22:13:46 takuan joins (~takuan@d8D86B9E9.access.telenet.be)
22:13:53 img joins (~img@user/img)
22:20:32 × takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
22:21:42 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:25:54 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
22:27:53 × chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 248 seconds)
22:32:50 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:32:52 gmg joins (~user@user/gehmehgeh)
22:35:12 × Anarchos quits (~Anarchos@91-161-254-16.subs.proxad.net) (Ping timeout: 264 seconds)
22:37:00 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:42:04 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
22:52:21 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:56:48 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
23:07:41 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:08:30 × jzargo2 quits (~jzargo@user/jzargo) (Read error: Connection reset by peer)
23:12:18 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
23:23:05 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:29:56 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
23:30:19 × qqq quits (~qqq@185.54.22.246) (Ping timeout: 264 seconds)
23:41:08 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:41:14 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
23:44:26 × arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds)
23:45:01 qqq joins (~qqq@185.54.22.246)
23:45:36 × merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
23:46:44 peterbecich joins (~Thunderbi@71.84.33.135)
23:50:02 chewybread joins (~chewybrea@user/chewybread)
23:50:32 arandombit joins (~arandombi@user/arandombit)
23:51:24 × jreicher quits (~joelr@user/jreicher) (Ping timeout: 246 seconds)
23:53:04 jreicher joins (~joelr@user/jreicher)
23:54:51 Square2 joins (~Square4@user/square)
23:55:13 × Googulator38 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
23:55:29 Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
23:56:30 merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:57:15 × Square quits (~Square@user/square) (Ping timeout: 244 seconds)
23:57:24 × chewybread quits (~chewybrea@user/chewybread) (Ping timeout: 264 seconds)

All times are in UTC on 2026-03-12.