| 2026-01-15 00:01:49 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 264 seconds) |
| 2026-01-15 00:03:09 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-15 00:05:28 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 00:11:53 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-01-15 00:12:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 00:19:37 +0100 | Googulator15 | Googulator |
| 2026-01-15 00:21:53 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-01-15 00:23:31 +0100 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-01-15 00:28:11 +0100 | merijn | (~merijn@62.45.136.136) (Ping timeout: 244 seconds) |
| 2026-01-15 00:29:56 +0100 | mange | (~mange@user/mange) mange |
| 2026-01-15 00:39:24 +0100 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-01-15 00:43:08 +0100 | fwam | rensenwxre |
| 2026-01-15 00:43:55 +0100 | merijn | (~merijn@62.45.136.136) (Ping timeout: 240 seconds) |
| 2026-01-15 00:45:45 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 244 seconds) |
| 2026-01-15 00:48:04 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) gabriel_sevecek |
| 2026-01-15 00:54:07 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-01-15 00:55:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 00:59:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-15 01:10:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 01:14:29 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-15 01:16:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 01:20:40 +0100 | hakutaku | (~textual@chen.yukari.eu.org) |
| 2026-01-15 01:29:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 01:33:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 01:37:14 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-15 01:38:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 01:39:56 +0100 | myxos | (~myxos@174-18-88-231.tcso.qwest.net) myxokephale |
| 2026-01-15 01:43:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 01:43:51 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-15 01:46:10 +0100 | xff0x | (~xff0x@2405:6580:b080:900:dc92:188b:d152:35db) (Ping timeout: 246 seconds) |
| 2026-01-15 01:53:36 +0100 | Square | (~Square@user/square) Square |
| 2026-01-15 01:54:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 01:57:43 +0100 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-15 02:01:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 02:03:02 +0100 | troydm | (~troydm@user/troydm) troydm |
| 2026-01-15 02:09:40 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 02:12:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 02:17:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 02:18:39 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-15 02:24:58 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-15 02:25:05 +0100 | divlamir_ | (~divlamir@user/divlamir) divlamir |
| 2026-01-15 02:25:57 +0100 | divlamir_ | divlamir |
| 2026-01-15 02:28:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 02:31:49 +0100 | annamalai | (~annamalai@157.49.214.71) (Ping timeout: 264 seconds) |
| 2026-01-15 02:33:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-15 02:36:55 +0100 | lbseale | (~quassel@user/ep1ctetus) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2026-01-15 02:37:39 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2026-01-15 02:40:32 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-15 02:44:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 02:45:51 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-01-15 02:49:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-15 02:53:20 +0100 | omidmash2 | (~omidmash@user/omidmash) omidmash |
| 2026-01-15 02:54:27 +0100 | housemate_ | (~housemate@203.56.146.214) housemate |
| 2026-01-15 02:54:35 +0100 | housemate | (~housemate@203.56.146.214) (Read error: Connection reset by peer) |
| 2026-01-15 02:55:26 +0100 | omidmash | (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-15 02:55:26 +0100 | omidmash2 | omidmash |
| 2026-01-15 02:55:35 +0100 | housemate_ | (~housemate@203.56.146.214) (Max SendQ exceeded) |
| 2026-01-15 02:56:08 +0100 | housemate_ | (~housemate@203.56.146.214) housemate |
| 2026-01-15 02:56:50 +0100 | housemate_ | (~housemate@203.56.146.214) (Max SendQ exceeded) |
| 2026-01-15 02:57:20 +0100 | housemate_ | (~housemate@203.56.146.214) housemate |
| 2026-01-15 03:00:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 03:05:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 03:15:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 03:20:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 03:31:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 03:32:42 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
| 2026-01-15 03:36:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 03:47:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 03:52:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 03:53:51 +0100 | annamalai | (~annamalai@157.49.208.124) annamalai |
| 2026-01-15 03:56:34 +0100 | acidjnk | (~acidjnk@p200300d6e7171972cd12b2d062d86876.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2026-01-15 03:56:52 +0100 | annamalai | (~annamalai@157.49.208.124) (Remote host closed the connection) |
| 2026-01-15 03:58:11 +0100 | annamalai | (~annamalai@2409:4072:629e:6d46::2523:a8b1) annamalai |
| 2026-01-15 03:59:49 +0100 | jmcantrell_ | jmcantrell |
| 2026-01-15 04:03:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 04:04:14 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-15 04:04:36 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-15 04:07:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 04:10:31 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 2026-01-15 04:15:59 +0100 | synchromesh | (~john@2406:5a00:2412:2c00::144) (Quit: WeeChat 4.1.1) |
| 2026-01-15 04:19:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 04:22:11 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-15 04:24:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 04:28:37 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) |
| 2026-01-15 04:34:51 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 04:42:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 04:44:25 +0100 | jumper149 | (~jumper149@base.felixspringer.xyz) (Quit: WeeChat 4.7.1) |
| 2026-01-15 04:47:13 +0100 | Guest71 | (~Guest71@host-67-204-213-15.public.eastlink.ca) |
| 2026-01-15 04:47:22 +0100 | Guest71 | (~Guest71@host-67-204-213-15.public.eastlink.ca) (Client Quit) |
| 2026-01-15 04:52:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 04:57:01 +0100 | omidmash | (~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat) |
| 2026-01-15 04:57:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 05:01:35 +0100 | omidmash | (~omidmash@user/omidmash) omidmash |
| 2026-01-15 05:06:10 +0100 | Square2 | (~Square4@user/square) Square |
| 2026-01-15 05:07:33 +0100 | Square2 | (~Square4@user/square) (Remote host closed the connection) |
| 2026-01-15 05:08:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 05:09:17 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) (Ping timeout: 272 seconds) |
| 2026-01-15 05:13:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 05:20:24 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 05:20:25 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-15 05:24:32 +0100 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-01-15 05:29:31 +0100 | merijn | (~merijn@62.45.136.136) (Ping timeout: 256 seconds) |
| 2026-01-15 05:33:35 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 240 seconds) |
| 2026-01-15 05:34:31 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2026-01-15 05:34:45 +0100 | califax | (~califax@user/califx) califx |
| 2026-01-15 05:40:06 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 05:44:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 05:49:20 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-01-15 05:58:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 06:00:07 +0100 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 240 seconds) |
| 2026-01-15 06:02:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-01-15 06:07:41 +0100 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-15 06:08:13 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2026-01-15 06:13:26 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 06:18:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 06:29:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 06:29:51 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 244 seconds) |
| 2026-01-15 06:30:24 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-01-15 06:34:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 06:38:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 06:39:37 +0100 | mange | (~mange@user/mange) (Quit: Quittin' time!) |
| 2026-01-15 06:40:44 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer) |
| 2026-01-15 06:41:08 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-01-15 06:42:46 +0100 | housemate_ | (~housemate@203.56.146.214) (Quit: https://ineedsomeacidtocalmmedown.space/) |
| 2026-01-15 06:43:10 +0100 | housemate | (~housemate@203.56.146.214) housemate |
| 2026-01-15 06:43:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 06:44:00 +0100 | housemate | (~housemate@203.56.146.214) (Max SendQ exceeded) |
| 2026-01-15 06:44:30 +0100 | housemate | (~housemate@203.56.146.214) housemate |
| 2026-01-15 06:44:32 +0100 | michalz | (~michalz@185.246.207.205) |
| 2026-01-15 06:45:19 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds) |
| 2026-01-15 06:54:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 06:58:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-15 07:09:41 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 07:12:39 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-01-15 07:12:43 +0100 | kimiamania3 | (~9566fa0a@user/kimiamania) kimiamania |
| 2026-01-15 07:14:43 +0100 | kimiamania | (~9566fa0a@user/kimiamania) (Ping timeout: 264 seconds) |
| 2026-01-15 07:14:44 +0100 | kimiamania3 | kimiamania |
| 2026-01-15 07:15:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 07:20:50 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-01-15 07:25:28 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 07:27:20 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-15 07:32:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 07:34:02 +0100 | jreicher | (~joelr@user/jreicher) (Quit: Out and about) |
| 2026-01-15 07:35:56 +0100 | ft | (~ft@p4fc2a9d7.dip0.t-ipconnect.de) (Quit: leaving) |
| 2026-01-15 07:43:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 07:46:41 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-15 07:48:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-15 07:53:30 +0100 | poscat0x04 | (~poscat@user/poscat) (Remote host closed the connection) |
| 2026-01-15 07:55:45 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) (Ping timeout: 245 seconds) |
| 2026-01-15 07:56:43 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2026-01-15 07:58:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 08:03:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 08:09:22 +0100 | <gentauro> | anybody know what to pass to `nix shell --extra-experimental-features flakes--extra-experimental-features nix-command--inputs-from .` (https://github.com/simplex-chat/simplex-chat/blob/stable/flake.nix) if I only want to limit the build? In cabal it would be to the CLI: `cabal install simplex-chat` (https://github.com/simplex-chat/simplex-chat/blob/stable/simplex-chat.cabal#L410) |
| 2026-01-15 08:10:14 +0100 | <gentauro> | https://github.com/simplex-chat/simplex-chat/blob/stable/docs/CLI.md#in-any-os |
| 2026-01-15 08:14:31 +0100 | tromp | (~textual@2001:1c00:3487:1b00:1931:5674:15e5:cfb0) |
| 2026-01-15 08:14:41 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 08:19:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 08:21:38 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 08:21:52 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 08:28:47 +0100 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-15 08:30:28 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 08:35:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-01-15 08:39:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 08:44:42 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-15 08:47:57 +0100 | ringo__ | (~ringo@157.230.117.128) (Ping timeout: 250 seconds) |
| 2026-01-15 08:50:01 +0100 | annamalai | (~annamalai@2409:4072:629e:6d46::2523:a8b1) (Ping timeout: 246 seconds) |
| 2026-01-15 08:55:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 09:00:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 09:03:55 +0100 | ringo__ | (~ringo@157.230.117.128) ringo_ |
| 2026-01-15 09:07:35 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 240 seconds) |
| 2026-01-15 09:11:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 09:17:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 09:19:55 +0100 | durstloescher | (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) |
| 2026-01-15 09:19:59 +0100 | durstloescher | (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) (Client Quit) |
| 2026-01-15 09:21:23 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-01-15 09:29:18 +0100 | danza | (~danza@user/danza) danza |
| 2026-01-15 09:33:10 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2026-01-15 09:41:12 +0100 | hardyhardhard | (~guest5000@user/hardyhardhard) hardyhardhard |
| 2026-01-15 09:49:04 +0100 | Hardyhardhard59 | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-15 09:50:29 +0100 | hardyhardhard | (~guest5000@user/hardyhardhard) (Ping timeout: 272 seconds) |
| 2026-01-15 09:51:53 +0100 | chele | (~chele@user/chele) chele |
| 2026-01-15 09:53:37 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) Maxdamantus |
| 2026-01-15 09:55:43 +0100 | jreicher | (~joelr@user/jreicher) (Quit: Gig time) |
| 2026-01-15 09:56:56 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-01-15 10:05:13 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-01-15 10:05:46 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 10:07:24 +0100 | trickard_ | trickard |
| 2026-01-15 10:09:19 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 2026-01-15 10:16:16 +0100 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2026-01-15 10:23:03 +0100 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 265 seconds) |
| 2026-01-15 10:26:30 +0100 | acidjnk | (~acidjnk@p200300d6e7171948e4551533bd5d7598.dip0.t-ipconnect.de) acidjnk |
| 2026-01-15 10:27:03 +0100 | skum | (~skum@user/skum) skum |
| 2026-01-15 10:29:36 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) Enrico63 |
| 2026-01-15 10:31:39 +0100 | Hardyhardhard59 | (~Hardyhard@user/hardyhardhard) (Ping timeout: 272 seconds) |
| 2026-01-15 10:43:41 +0100 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2026-01-15 10:48:31 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 2026-01-15 10:54:59 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 10:58:45 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Quit: Client closed) |
| 2026-01-15 11:19:06 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2026-01-15 11:21:15 +0100 | durstloescher | (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) |
| 2026-01-15 11:22:02 +0100 | durstloescher | (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) (Client Quit) |
| 2026-01-15 11:24:37 +0100 | kuribas | (~user@2a02-1810-2825-6000-cba-d3d9-b1a1-3dea.ip6.access.telenet.be) kuribas |
| 2026-01-15 11:27:46 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 11:30:42 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2026-01-15 11:32:06 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 244 seconds) |
| 2026-01-15 11:41:35 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 240 seconds) |
| 2026-01-15 11:42:10 +0100 | p3n | (~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-01-15 11:42:17 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 11:42:50 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 11:44:27 +0100 | bggd | (~bgg@2a01:e0a:fd5:f510:27fe:a881:1d17:429c) |
| 2026-01-15 11:44:27 +0100 | bggd | (~bgg@2a01:e0a:fd5:f510:27fe:a881:1d17:429c) (Changing host) |
| 2026-01-15 11:44:27 +0100 | bggd | (~bgg@user/bggd) bggd |
| 2026-01-15 11:45:19 +0100 | koz | (~koz@121.99.240.58) (Ping timeout: 264 seconds) |
| 2026-01-15 11:51:00 +0100 | <ncf> | limit the build? to what? |
| 2026-01-15 11:51:35 +0100 | p3n | (~p3n@217.198.124.246) p3n |
| 2026-01-15 11:53:24 +0100 | p3n | (~p3n@217.198.124.246) (Client Quit) |
| 2026-01-15 11:53:52 +0100 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) p3n |
| 2026-01-15 11:53:56 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 11:56:40 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 12:04:18 +0100 | karenw | (~karenw@user/karenw) karenw |
| 2026-01-15 12:04:19 +0100 | fp | (~Thunderbi@130.233.70.149) fp |
| 2026-01-15 12:04:57 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-01-15 12:12:31 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2026-01-15 12:18:36 +0100 | xff0x | (~xff0x@2405:6580:b080:900:5f60:7a2f:94c6:623e) |
| 2026-01-15 12:21:52 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 12:22:06 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 12:26:27 +0100 | koz | (~koz@121.99.240.58) |
| 2026-01-15 12:29:42 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 12:33:01 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 12:35:39 +0100 | Square | (~Square@user/square) (Quit: Leaving) |
| 2026-01-15 12:46:30 +0100 | kuribas | (~user@2a02-1810-2825-6000-cba-d3d9-b1a1-3dea.ip6.access.telenet.be) (Ping timeout: 244 seconds) |
| 2026-01-15 12:50:51 +0100 | annamalai | (~annamalai@117.231.194.195) annamalai |
| 2026-01-15 12:59:55 +0100 | annamalai | (~annamalai@117.231.194.195) (Ping timeout: 255 seconds) |
| 2026-01-15 13:00:18 +0100 | annamalai | (~annamalai@117.231.194.194) annamalai |
| 2026-01-15 13:08:32 +0100 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2026-01-15 13:10:53 +0100 | <gentauro> | ncf: only to the `executable simplex-chat` -> https://github.com/simplex-chat/simplex-chat/blob/stable/simplex-chat.cabal#L410 |
| 2026-01-15 13:11:06 +0100 | <gentauro> | there are many libs and execs in that .cabal file. I don't need to build `bots` and so. |
| 2026-01-15 13:11:37 +0100 | <gentauro> | like I stated, it's "easy" with `cabal`. But how do I replicate that approach with `nix shell flakes` |
| 2026-01-15 13:12:02 +0100 | <ncf> | nix build .#<tab> will tell you what's available |
| 2026-01-15 13:12:13 +0100 | <ncf> | nix shell doesn't build anything, it spawns a shell with the build dependencies |
| 2026-01-15 13:13:42 +0100 | <gentauro> | ncf: well, this is how I build `opencode` from its `latest` branch: `nix shell --extra-experimental-features flakes --extra-experimental-features nix-command --inputs-from .` |
| 2026-01-15 13:14:21 +0100 | <ncf> | no it isn't |
| 2026-01-15 13:14:27 +0100 | <gentauro> | I just thought it was the same with other `flake.nix` files. My bad |
| 2026-01-15 13:30:01 +0100 | danz65539 | (~danza@user/danza) danza |
| 2026-01-15 13:32:19 +0100 | danza | (~danza@user/danza) (Ping timeout: 255 seconds) |
| 2026-01-15 13:39:28 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 246 seconds) |
| 2026-01-15 13:39:55 +0100 | tromp | (~textual@2001:1c00:3487:1b00:1931:5674:15e5:cfb0) (Ping timeout: 264 seconds) |
| 2026-01-15 13:43:13 +0100 | trickard_ | trickard |
| 2026-01-15 13:53:43 +0100 | koz | (~koz@121.99.240.58) (Ping timeout: 260 seconds) |
| 2026-01-15 13:56:37 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2026-01-15 14:03:31 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 14:03:45 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 14:08:35 +0100 | fp | (~Thunderbi@130.233.70.149) (Ping timeout: 240 seconds) |
| 2026-01-15 14:09:37 +0100 | annamalai | (~annamalai@117.231.194.194) (Ping timeout: 264 seconds) |
| 2026-01-15 14:13:45 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 14:16:16 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 14:19:22 +0100 | humasect_ | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 14:21:01 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 264 seconds) |
| 2026-01-15 14:21:02 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2026-01-15 14:23:53 +0100 | FirefoxDeHuk | (~FirefoxDe@user/FirefoxDeHuk) FirefoxDeHuk |
| 2026-01-15 14:33:02 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) |
| 2026-01-15 14:33:52 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 14:35:20 +0100 | trickard_ | trickard |
| 2026-01-15 14:43:31 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2026-01-15 14:46:22 +0100 | FirefoxDeHuk | (~FirefoxDe@user/FirefoxDeHuk) (Quit: Client closed) |
| 2026-01-15 14:48:45 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 14:54:36 +0100 | housemate | (~housemate@203.56.146.214) (Quit: https://ineedsomeacidtocalmmedown.space/) |
| 2026-01-15 14:55:28 +0100 | kuribas | (~user@2a02-1810-2825-6000-b6e0-77f4-472f-1183.ip6.access.telenet.be) kuribas |
| 2026-01-15 14:58:28 +0100 | rainbyte | (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 2026-01-15 14:59:01 +0100 | rainbyte | (~rainbyte@186.22.19.214) rainbyte |
| 2026-01-15 14:59:23 +0100 | housemate | (~housemate@203.56.146.214) housemate |
| 2026-01-15 15:02:32 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 15:02:46 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 15:03:20 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-01-15 15:08:03 +0100 | annamalai | (~annamalai@117.231.195.83) annamalai |
| 2026-01-15 15:09:50 +0100 | durstloescher | (~textual@2001:638:708:308:c907:7e9e:4d1e:bc5d) |
| 2026-01-15 15:09:56 +0100 | durstloescher | (~textual@2001:638:708:308:c907:7e9e:4d1e:bc5d) (Client Quit) |
| 2026-01-15 15:10:52 +0100 | Jackneill_ | (~Jackneill@94-21-195-8.pool.digikabel.hu) (Quit: Leaving) |
| 2026-01-15 15:11:05 +0100 | Jackneill | (~Jackneill@94-21-195-8.pool.digikabel.hu) Jackneill |
| 2026-01-15 15:20:46 +0100 | karenw | (~karenw@user/karenw) karenw |
| 2026-01-15 15:26:35 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 265 seconds) |
| 2026-01-15 15:28:02 +0100 | ystael | (~ystael@user/ystael) ystael |
| 2026-01-15 15:34:18 +0100 | humasect_ | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-01-15 15:35:25 +0100 | Inline | (~User@cgn-195-14-218-118.nc.de) (Ping timeout: 264 seconds) |
| 2026-01-15 15:39:31 +0100 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2026-01-15 15:42:55 +0100 | doyougnu- | (~doyougnu@38.175.72.111) (Ping timeout: 240 seconds) |
| 2026-01-15 15:46:05 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2026-01-15 15:46:32 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-01-15 15:46:38 +0100 | doyougnu | (~doyougnu@38.175.72.111) doyougnu |
| 2026-01-15 15:46:38 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 15:49:19 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 15:52:22 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 15:52:38 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 15:53:04 +0100 | fp | (~Thunderbi@130.233.70.149) fp |
| 2026-01-15 15:54:29 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
| 2026-01-15 15:56:11 +0100 | Jackneill_ | (~Jackneill@178-164-234-102.pool.digikabel.hu) |
| 2026-01-15 15:58:29 +0100 | Jackneill_ | (~Jackneill@178-164-234-102.pool.digikabel.hu) (Remote host closed the connection) |
| 2026-01-15 15:59:07 +0100 | Jackneill | (~Jackneill@94-21-195-8.pool.digikabel.hu) (Ping timeout: 264 seconds) |
| 2026-01-15 16:00:14 +0100 | Jackneill | (~Jackneill@178-164-234-102.pool.digikabel.hu) |
| 2026-01-15 16:07:19 +0100 | trickard_ | trickard |
| 2026-01-15 16:08:08 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2026-01-15 16:12:25 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 246 seconds) |
| 2026-01-15 16:13:16 +0100 | <thenightmail> | why is there no associativity for equality, inequality and comparison operators |
| 2026-01-15 16:15:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 16:16:56 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) (Quit: Client closed) |
| 2026-01-15 16:17:58 +0100 | <chromoblob> | how would inequality associativity be useful |
| 2026-01-15 16:19:21 +0100 | <chromoblob> | to actually answer: x == y == z is banned because it cannot have the meaning it seems to have |
| 2026-01-15 16:19:32 +0100 | qqq | (~qqq@185.54.21.105) |
| 2026-01-15 16:20:10 +0100 | <chromoblob> | because the result of one comparing is a Bool, thus you would next compare this Bool to another operand |
| 2026-01-15 16:20:24 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-01-15 16:21:22 +0100 | <chromoblob> | and authors of language didn't think that it would be a good idea to forego rule and special-case these operators so that it means what you want it to mean |
| 2026-01-15 16:21:34 +0100 | <thenightmail> | i see, this question is a problem from a book. the hint is to 'write down the simplest expression you can think of that would require the associativity rules to resolve the precedence of comparison operators and try to make sense of it' |
| 2026-01-15 16:22:08 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-01-15 16:26:33 +0100 | <thenightmail> | I'm not fully grasping it, maybe x == y == z is what they are referring to, but I will move on for now in case it makes sense later with more context. thanks for the answers |
| 2026-01-15 16:28:54 +0100 | fp | (~Thunderbi@130.233.70.149) (Ping timeout: 260 seconds) |
| 2026-01-15 16:32:06 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 16:32:06 +0100 | durstloescher | (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) |
| 2026-01-15 16:32:19 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 16:32:46 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2026-01-15 16:34:17 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 16:34:37 +0100 | durstloescher | (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) (Client Quit) |
| 2026-01-15 16:35:19 +0100 | EvanR | (~EvanR@user/evanr) (Ping timeout: 260 seconds) |
| 2026-01-15 16:38:32 +0100 | durstloescher | (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) |
| 2026-01-15 16:42:50 +0100 | durstloescher | (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) (Ping timeout: 245 seconds) |
| 2026-01-15 16:46:30 +0100 | Catty | (~catties@user/meow/catties) (Remote host closed the connection) |
| 2026-01-15 16:50:08 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 16:50:23 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 16:52:37 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Client Quit) |
| 2026-01-15 16:52:54 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 16:53:38 +0100 | catties | (~catties@user/meow/catties) catties |
| 2026-01-15 16:54:02 +0100 | itaipu | (~itaipu@168.121.99.54) (Ping timeout: 256 seconds) |
| 2026-01-15 16:54:05 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2026-01-15 16:56:17 +0100 | itaipu | (~itaipu@168.121.99.54) itaipu |
| 2026-01-15 17:00:55 +0100 | itaipu | (~itaipu@168.121.99.54) (Ping timeout: 240 seconds) |
| 2026-01-15 17:01:39 +0100 | bggd | (~bgg@user/bggd) (Remote host closed the connection) |
| 2026-01-15 17:03:32 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 17:03:46 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 17:03:56 +0100 | Inline | (~User@cgn-195-14-218-118.nc.de) Inline |
| 2026-01-15 17:05:13 +0100 | <tomsmeding> | chromoblob: "authors of language" -- authors of _this_ language. The authors of Python did think this was a good idea |
| 2026-01-15 17:07:15 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 17:12:37 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 2026-01-15 17:14:11 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-01-15 17:20:51 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 17:23:15 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2026-01-15 17:25:08 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2026-01-15 17:25:50 +0100 | rainbyte | (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 2026-01-15 17:29:11 +0100 | rainbyte | (~rainbyte@186.22.19.214) rainbyte |
| 2026-01-15 17:29:33 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-15 17:29:40 +0100 | danza | (~danza@user/danza) danza |
| 2026-01-15 17:30:36 +0100 | danz65539 | (~danza@user/danza) (Read error: Connection reset by peer) |
| 2026-01-15 17:34:18 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 17:41:53 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 17:42:06 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 17:42:17 +0100 | ft | (~ft@p4fc2a9d7.dip0.t-ipconnect.de) ft |
| 2026-01-15 17:51:01 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 2026-01-15 17:52:13 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2026-01-15 17:55:35 +0100 | doyougnu | (~doyougnu@38.175.72.111) (Ping timeout: 240 seconds) |
| 2026-01-15 17:59:00 +0100 | doyougnu | (~doyougnu@38.175.72.111) |
| 2026-01-15 18:00:07 +0100 | <monochrom> | "associativity" talks about whether "(x == y) == z" and "x == (y == z)" are the same or not. So those are the two expressions the hint wants you to look at. If they were the same, can you see a type error? |
| 2026-01-15 18:00:56 +0100 | <monochrom> | (Fun fact: But if x,y,z are all Bool, then they are the same. Draw a truth table to see and be shocked. :) ) |
| 2026-01-15 18:01:16 +0100 | <tomsmeding> | (because == on Bools is <=>) |
| 2026-01-15 18:02:20 +0100 | <monochrom> | It is surprising but handy that both == and /= (xor) are commutative associative and with identities. |
| 2026-01-15 18:07:17 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 18:07:44 +0100 | <monochrom> | Alternatively, you can legalize "x == y == z" but you say it does not mean "(x == y) == z" or "x == (y == z)". You say it means "x == y && y == z". This is what mathematicians did. (You can trust that they are pros and they know what they're doing, right? Right? >:) ) |
| 2026-01-15 18:08:29 +0100 | <monochrom> | (Hint: They are pros in math content, but not math syntax.) |
| 2026-01-15 18:08:36 +0100 | <monochrom> | (or any syntax) |
| 2026-01-15 18:08:37 +0100 | <danza> | :t (<=>) |
| 2026-01-15 18:08:38 +0100 | <lambdabot> | error: [GHC-88464] |
| 2026-01-15 18:08:38 +0100 | <lambdabot> | Variable not in scope: <=> |
| 2026-01-15 18:08:38 +0100 | <lambdabot> | Suggested fix: |
| 2026-01-15 18:08:49 +0100 | <monochrom> | Oh, <=> is iff. |
| 2026-01-15 18:12:14 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2026-01-15 18:12:52 +0100 | <danza> | cheers monochrom |
| 2026-01-15 18:14:16 +0100 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-01-15 18:22:05 +0100 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-15 18:23:37 +0100 | koz | (~koz@121.99.240.58) |
| 2026-01-15 18:24:20 +0100 | larsivi | (~larsivi@user/larsivi) (Quit: WeeChat 4.8.1) |
| 2026-01-15 18:34:09 +0100 | fp | (~Thunderbi@89-27-10-140.bb.dnainternet.fi) fp |
| 2026-01-15 18:43:25 +0100 | kuribas | (~user@2a02-1810-2825-6000-b6e0-77f4-472f-1183.ip6.access.telenet.be) (Remote host closed the connection) |
| 2026-01-15 18:47:10 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 18:48:06 +0100 | EvanR | (~EvanR@user/evanr) EvanR |
| 2026-01-15 18:57:54 +0100 | <dolio> | I expect the "associativity" in the question is not about that associativity. It sounds like it's asking about the rules on how parentheses are automatically inserted. |
| 2026-01-15 18:58:05 +0100 | <dolio> | Not about whether how they're inserted matters. |
| 2026-01-15 19:00:24 +0100 | <dolio> | Even though (==) is associative as an operation on Bool, Haskell will refuse to accept `x == y == z`. |
| 2026-01-15 19:01:24 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2026-01-15 19:04:15 +0100 | <geekosaur> | that seems pretty obvious to me, since as defined either associativity makes the "other" one a comparison on `Bool` |
| 2026-01-15 19:08:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 19:13:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-15 19:20:52 +0100 | elarks | (~elarks@user/yerrii) (Quit: WeeChat 4.7.1) |
| 2026-01-15 19:23:48 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 19:24:12 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 2026-01-15 19:25:48 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2026-01-15 19:30:23 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-15 19:30:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 19:36:28 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 19:36:41 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 19:39:50 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) Everything |
| 2026-01-15 19:41:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 19:46:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 19:48:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 19:53:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 20:04:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 20:09:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 20:11:52 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) Tuplanolla |
| 2026-01-15 20:12:25 +0100 | <tomsmeding> | I feel like the nonassociativity of the (==) operator in haskell is mostly because it is polymorphic. Had it been monomorphic for Bool, I'm sure it would have been made associative (in some direction) |
| 2026-01-15 20:13:02 +0100 | <dolio> | Yeah. |
| 2026-01-15 20:16:19 +0100 | <dolio> | The problem is that in situations with other types, the way parentheses are inserted affects whether it's well typed. |
| 2026-01-15 20:16:55 +0100 | <dolio> | And that's kind of a dumb thing to depend on. |
| 2026-01-15 20:17:32 +0100 | <__monty__> | tomsmeding: I'm not so sure, `False == False == True` doesn't seem very useful. |
| 2026-01-15 20:17:36 +0100 | <dolio> | Also the binary operator on booleans is pretty niche. |
| 2026-01-15 20:18:44 +0100 | <__monty__> | Are there any languages where a successful equality check "returns" the value, while an unsuccessful check returns False or something? |
| 2026-01-15 20:19:07 +0100 | <ncf> | equality is a relation, not an operator. asking whether a relation is associative is usually a type error, except in the case where the relation is on propositions (in this case decidable ones), but that doesn't mean it's a good idea to do it |
| 2026-01-15 20:19:53 +0100 | <ncf> | (also, logical equivalence is not actually associative constructively, is it?) |
| 2026-01-15 20:20:12 +0100 | <dolio> | This isn't a relation. It's a decision procedure for a relation. |
| 2026-01-15 20:20:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 20:20:42 +0100 | <dolio> | The induced operator on booleans calculates parity. |
| 2026-01-15 20:22:37 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) (Quit: Client closed) |
| 2026-01-15 20:23:26 +0100 | <tomsmeding> | __monty__: sure :p |
| 2026-01-15 20:24:05 +0100 | jle` | (~jle`@2603:8001:3b00:11::1156) (Ping timeout: 245 seconds) |
| 2026-01-15 20:24:57 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-15 20:25:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-15 20:25:33 +0100 | <dolio> | Or wait, (/=) is parity. (==) is like anti-parity or something. |
| 2026-01-15 20:26:12 +0100 | <dolio> | Parity for the 0 bits instead of 1 bits. |
| 2026-01-15 20:26:52 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-01-15 20:29:33 +0100 | <__monty__> | Maybe the right type for (==) should be `Eq a => Maybe a -> Maybe a -> Maybe a`? Then we can get associativity. |
| 2026-01-15 20:32:11 +0100 | <monochrom> | A relation is a function. A function is an operator. So a relation is also an operator. >:) |
| 2026-01-15 20:33:03 +0100 | <monochrom> | We have a real type system, so we don't need artificial lines between relations, functions, numbers, values, constants. |
| 2026-01-15 20:38:01 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-01-15 20:39:00 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2026-01-15 20:39:20 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2026-01-15 20:44:16 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) (Quit: Client closed) |
| 2026-01-15 20:48:11 +0100 | <ncf> | have you heard of concepts with attitudes |
| 2026-01-15 20:48:28 +0100 | <ncf> | the intended meaning of a R b R c when R is a relation is a R b ∧ b R c |
| 2026-01-15 20:49:08 +0100 | <ncf> | the intended meaning of a O b O c when O is a (homogeneous, binary, associative) operator is a O (b O c) |
| 2026-01-15 20:49:15 +0100 | <ncf> | those are extremely different! |
| 2026-01-15 20:49:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 20:50:21 +0100 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-15 20:50:21 +0100 | <dolio> | ncf: Definitely seems like the associativity is not constructive. |
| 2026-01-15 20:50:27 +0100 | <ncf> | yeah i don't think it is |
| 2026-01-15 20:50:38 +0100 | <ncf> | can you prove a taboo from it? |
| 2026-01-15 20:54:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 20:59:04 +0100 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2026-01-15 21:01:41 +0100 | <monochrom> | I have not heard of concepts with attitudes. But my thesis supervisor coined "continuing" for R in the 1990's. (E.g., https://www.cs.toronto.edu/~hehner/aPToP/aPToP.pdf last page.) We can do this by invoking "syntax sugar" on a per-operator basis. We don't need anything more profound or advanced. |
| 2026-01-15 21:04:00 +0100 | <ncf> | you say continuing operator i say relation |
| 2026-01-15 21:04:32 +0100 | <[exa]> | (binary relations are overrated) |
| 2026-01-15 21:05:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:06:32 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-15 21:06:46 +0100 | <[exa]> | anyway I saw this somewhere with matlabby dots, like (a <. b .< c), it even extended to (a <. b .<. c .< d) |
| 2026-01-15 21:06:48 +0100 | <monochrom> | The difference between yours and mine is that I say that a continuing operator is still an operator, just that it enjoys syntax sugar, whereas you say that it is not even an operator. |
| 2026-01-15 21:08:27 +0100 | <geekosaur> | Icon lets you do this chaining, but it's not using a mechanism Haskell could make use of (it's solidly based in its "failure" semantic) |
| 2026-01-15 21:10:19 +0100 | <dolio> | Haskell should just extend its rules so that lexing depends not only on parsing, but type checking. |
| 2026-01-15 21:10:20 +0100 | <[exa]> | btw Julia had a special case for that too: Meta.show_sexpr(:(a <= b < c)) == (:comparison, :a, :<=, :b, :<, :c) |
| 2026-01-15 21:10:31 +0100 | <[exa]> | dolio: <3 |
| 2026-01-15 21:11:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 21:11:47 +0100 | <monochrom> | Speaking of which, how is RecordDot done? |
| 2026-01-15 21:12:13 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-15 21:13:16 +0100 | <ncf> | dolio: by yoneda this reduces to ((A ↔ B) ↔ A) ↔ B and the nontrivial direction is →, which is almost curry's paradox except with A ↔ B instead of A → B |
| 2026-01-15 21:13:24 +0100 | <dolio> | ncf: https://paste.tomsmeding.com/a6qxdKdh |
| 2026-01-15 21:13:29 +0100 | <ncf> | which is a conversation i remember having but don't remember the conclusion |
| 2026-01-15 21:13:38 +0100 | <ncf> | aha |
| 2026-01-15 21:14:07 +0100 | <ncf> | oh right, if you take A = ⊥ you get ¬¬B ↔ B |
| 2026-01-15 21:14:14 +0100 | <ncf> | cool |
| 2026-01-15 21:18:18 +0100 | <monochrom> | Oh nice, one more way to restore classical logic. :) |
| 2026-01-15 21:21:17 +0100 | <davean> | dolio: and end up like C++? Lol |
| 2026-01-15 21:21:20 +0100 | <monochrom> | (I had known of: choose one: EM, double-negation elim, Pierce.) |
| 2026-01-15 21:23:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:25:54 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 21:26:08 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 21:28:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 21:29:41 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-01-15 21:30:37 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-01-15 21:30:56 +0100 | collide2954 | (~collide29@user/collide2954) (Quit: The Lounge - https://thelounge.chat) |
| 2026-01-15 21:31:43 +0100 | collide2954 | (~collide29@user/collide2954) collide2954 |
| 2026-01-15 21:36:01 +0100 | <dolio> | davean: Does C++ do that, too? I thought that was perl's distinction. |
| 2026-01-15 21:36:21 +0100 | <dolio> | I guess perl has to actually evaluate code. |
| 2026-01-15 21:37:42 +0100 | <davean> | dolio: https://blog.reverberate.org/2013/08/parsing-c-is-literally-undecidable.html "C++ grammar: the type name vs object name issue" and others |
| 2026-01-15 21:38:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:40:35 +0100 | divlamir | (~divlamir@user/divlamir) (Ping timeout: 240 seconds) |
| 2026-01-15 21:41:03 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-15 21:42:11 +0100 | <dolio> | Anyhow, as I said, Haskell can take it to the next level by making lexing undecidable. |
| 2026-01-15 21:42:23 +0100 | <dolio> | That's innovation. |
| 2026-01-15 21:42:25 +0100 | <humasect> | yeah |
| 2026-01-15 21:42:52 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-01-15 21:42:59 +0100 | <monochrom> | TypeDirectedLexicalResolution? >:) |
| 2026-01-15 21:43:35 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-01-15 21:43:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 21:43:37 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) Enrico63 |
| 2026-01-15 21:46:01 +0100 | <[exa]> | -XLexicalKinds |
| 2026-01-15 21:46:48 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Client Quit) |
| 2026-01-15 21:49:50 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 256 seconds) |
| 2026-01-15 21:50:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:51:08 +0100 | <jreicher> | thenightmail: I'm fairly sure in mathematics the comparison "operators" are not operators at all. In algebra an operator on a set produces another element from the same set. Comparison, on the other hand, is a predicate. |
| 2026-01-15 21:52:58 +0100 | <c_wraith> | > LT `compare` GT |
| 2026-01-15 21:52:59 +0100 | <lambdabot> | LT |
| 2026-01-15 21:53:03 +0100 | <c_wraith> | it's closed! |
| 2026-01-15 21:53:04 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 21:54:35 +0100 | <jreicher> | monochrom: a function is a relation, but the converse is not true |
| 2026-01-15 21:55:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 21:55:46 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 22:01:25 +0100 | <EvanR> | you can get a relation for any function, then functions don't need to be implemented as literal relations if you don't want them to be! |
| 2026-01-15 22:01:55 +0100 | <int-e> | "in mathematics" - there is no such thing really; mathematicians will take whatever view is most convenient in a context. In classical logic, predicates can and will be used as functions. Logicians who want to allow logics without the law of excluded middle will disagree. |
| 2026-01-15 22:02:54 +0100 | <int-e> | First-order logic has many-sorted variants. There are algebras with more than one carrier set and operators that aren't homogenous either, like vector spaces. |
| 2026-01-15 22:03:35 +0100 | <EvanR> | math entities are a pure construction of the mind |
| 2026-01-15 22:03:49 +0100 | <EvanR> | :D |
| 2026-01-15 22:04:33 +0100 | <EvanR> | how concepts interrelate is more interesting than "what they are really" |
| 2026-01-15 22:04:49 +0100 | <EvanR> | sometimes taking the place of |
| 2026-01-15 22:06:56 +0100 | <dolio> | jreicher: But does every relation contain a function? |
| 2026-01-15 22:07:38 +0100 | <EvanR> | you can get a relation for any function also lets you avoid subtyping |
| 2026-01-15 22:08:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:09:22 +0100 | <dolio> | jreicher: Also, relations are functions in that they are maps into a collection of truth values. |
| 2026-01-15 22:09:49 +0100 | <dolio> | Not that every relation from A to B is a function from A to B. |
| 2026-01-15 22:12:07 +0100 | <jreicher> | dolio: I'm not sure what you mean by "contain", but I'm fairly sure the answer will be "no", regardless of what meaning you choose. |
| 2026-01-15 22:12:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 22:13:19 +0100 | Lears | (~Leary@user/Leary/x-0910699) Leary |
| 2026-01-15 22:13:26 +0100 | <jreicher> | int-e: I suspect you underestimate the significance of "most convenient". Mathematical definitions are language design in much the same way that programming languages are designed. So if a mathematician says something is "convenient", it means it's a good design. And mathematicians have been working on this much longer than computer scientists. |
| 2026-01-15 22:13:40 +0100 | <dolio> | It means there's a sub-relation that is a function. |
| 2026-01-15 22:14:14 +0100 | <jreicher> | dolio: And what do you mean by sub-relation? Does it also mean restricting the domain to a subset? |
| 2026-01-15 22:14:35 +0100 | Leary | (~Leary@user/Leary/x-0910699) (Ping timeout: 240 seconds) |
| 2026-01-15 22:15:09 +0100 | <dolio> | No, R is a sub-relation of S if R(x,y) implies S(x,y) forall x and y. |
| 2026-01-15 22:15:28 +0100 | Lears | Leary |
| 2026-01-15 22:16:18 +0100 | <dolio> | I guess, you should be able to restrict the domain, too. |
| 2026-01-15 22:16:32 +0100 | <dolio> | Otherwise you could only hope to get a partial function in general. |
| 2026-01-15 22:17:26 +0100 | <jreicher> | Yes partial functions will definitely happen. But maybe we can accept those. The bigger problem is that if there are many y for a given x for which S(x,y) then a sub relation that is a function will not really resemble S in any meaningful way |
| 2026-01-15 22:19:37 +0100 | <monochrom> | jreicher: I am clearly siding with type theory rather than traditional mathematics. |
| 2026-01-15 22:22:20 +0100 | <monochrom> | dolio: To obtain a functional subrelation from a relation with an infinite co-domain, we quickly run into the axiom of choice... :) |
| 2026-01-15 22:22:32 +0100 | <jreicher> | monochrom: what do you mean? |
| 2026-01-15 22:22:33 +0100 | <dolio> | :) |
| 2026-01-15 22:23:13 +0100 | <dolio> | Yeah, that assertion is equivalent to the axiom of choice. |
| 2026-01-15 22:23:14 +0100 | <monochrom> | In type theory, predicates are special cases of functions. |
| 2026-01-15 22:23:50 +0100 | <dolio> | 'For every x with multiple related ys, pick one of the ys.' |
| 2026-01-15 22:23:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:24:11 +0100 | <jreicher> | I think that mixes up language levels. Type theory itself needs to be written in logic, which means predicates are used to describe it. It will be different predicates that are objects within type theory. |
| 2026-01-15 22:24:51 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 22:24:53 +0100 | <EvanR> | type theory *is* logic |
| 2026-01-15 22:24:55 +0100 | <dolio> | Type theory has no need of logic. It has subsumed it. |
| 2026-01-15 22:25:06 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2026-01-15 22:25:28 +0100 | <jreicher> | Yes, but you then have two logics. The logic which is the object of study (proof), and the logic being used to study it (prove things about it). |
| 2026-01-15 22:25:37 +0100 | <jreicher> | Language and metalanguage. |
| 2026-01-15 22:25:54 +0100 | <EvanR> | if you're proving things about the logic itself |
| 2026-01-15 22:26:08 +0100 | <EvanR> | instead of using it for actual purposes xD |
| 2026-01-15 22:26:10 +0100 | <monochrom> | Traditional mathematics also needs a language and a metalanguage. |
| 2026-01-15 22:26:16 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2026-01-15 22:26:31 +0100 | <jreicher> | Exactly. And to me the original question was about the metalinguistic objects, and not the linguistic ones. |
| 2026-01-15 22:26:42 +0100 | <monochrom> | In fact how about I use HoTT as the metalanguage for defining the language and semantics of set theory? |
| 2026-01-15 22:27:11 +0100 | <EvanR> | it's relative right, you could have two of the same theories one standing for metatheory one for theory but they're the same language |
| 2026-01-15 22:27:40 +0100 | <jreicher> | When we say a comparison "operator" is a predicate, the operator is linguistic, but the predication is metalinguistic. |
| 2026-01-15 22:27:44 +0100 | <monochrom> | That too. Just look at GHC being written in GHC. |
| 2026-01-15 22:28:40 +0100 | <EvanR> | operator one of the most overloaded terms, in the process also overloading the term operator overloading |
| 2026-01-15 22:29:17 +0100 | <jreicher> | Put another way, when the "output" of the "operator" is T or F, those values don't exist in the language domain. They are the semantic values in the metalanguage. |
| 2026-01-15 22:29:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 22:29:58 +0100 | <EvanR> | you might have spontaneously created a new platonic semantics for haskell beyond the ones we already had |
| 2026-01-15 22:30:09 +0100 | <jreicher> | Except I'm not a platonist. :p |
| 2026-01-15 22:30:26 +0100 | <monochrom> | HoTT, CoC, Agda, Lean, Haskell all have T and F in the language domain. |
| 2026-01-15 22:30:29 +0100 | <EvanR> | ok then we can reel it back in and have T an F just be haskell T and F |
| 2026-01-15 22:31:01 +0100 | <monochrom> | In Agda, Lean, and Haskell, T and F are even user-definable. |
| 2026-01-15 22:31:20 +0100 | <jreicher> | monochrom: yes, and so that's a different kind of language. It all depends on how you understand the original question about "where" in the language comparison "operators" are |
| 2026-01-15 22:31:35 +0100 | <monochrom> | (Generally in any CoC + user-definable inductive types.) |
| 2026-01-15 22:31:58 +0100 | <monochrom> | Oh, the original language was Haskell. |
| 2026-01-15 22:32:07 +0100 | <davean> | dolio: C++ is undecidable |
| 2026-01-15 22:32:18 +0100 | <monochrom> | Why do we even care about traditional set theory in #haskell? :) |
| 2026-01-15 22:32:42 +0100 | <dolio> | davean: lexing? |
| 2026-01-15 22:32:58 +0100 | <jreicher> | Personally I think it's unhygienic to talk about a logistic language as a logic. A logic is a logic when it's used for proof, and so it can only be a metalanguage. But because it is a formal system it can be "reflected" as a language, but when that's done it shouldn't be called a logic (in my opinion) |
| 2026-01-15 22:33:11 +0100 | <davean> | dolio: I forget exactly which level of lex vs. parse is undecidable |
| 2026-01-15 22:33:18 +0100 | <EvanR> | this is a bit too dogmatic |
| 2026-01-15 22:33:30 +0100 | <jreicher> | That's why I used the word "unhygienic". |
| 2026-01-15 22:33:39 +0100 | <jreicher> | And also "personally" |
| 2026-01-15 22:33:48 +0100 | <EvanR> | you could make the case to come up with semantics to mediate between haskell and set theory if that was relevant, but it's often not xD |
| 2026-01-15 22:33:54 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-01-15 22:34:21 +0100 | <jreicher> | Not sure we want uncountable datatypes in Haskell |
| 2026-01-15 22:34:32 +0100 | <EvanR> | are you sure we don't already? |
| 2026-01-15 22:35:01 +0100 | <dolio> | I'd be a little surprised if the lexing were undecidable, but I'm not much of a C++ guru. |
| 2026-01-15 22:35:02 +0100 | <jreicher> | I can't see how it's possible. You only get countable infinities with recursion. |
| 2026-01-15 22:35:03 +0100 | <EvanR> | datatypes which could not possibly be enumerated (in haskell) |
| 2026-01-15 22:35:17 +0100 | <EvanR> | i.e. make a full list of them |
| 2026-01-15 22:35:27 +0100 | <EvanR> | of the values |
| 2026-01-15 22:35:48 +0100 | <dolio> | Maybe not super surprised. |
| 2026-01-15 22:39:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:40:00 +0100 | <davean> | dolio: I just don't recally how they define their boundary |
| 2026-01-15 22:41:35 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 22:41:52 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 22:43:44 +0100 | <monochrom> | Denotational semantics for lazy infinite streams are full of uncountable data types. So someone wants it. But that someone also acknowledges that it is just a model, and it is chosen for a trade-off. Uncontability is weird and unrealistic, but it buys simplcity for something else. |
| 2026-01-15 22:44:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 22:46:06 +0100 | <jreicher> | monochrom: got a reference? That doesn't sound sensible to me |
| 2026-01-15 22:46:37 +0100 | <monochrom> | I don't have a reference. |
| 2026-01-15 22:46:53 +0100 | <EvanR> | if you disagree that haskell has uncountable datatypes, it's possible normal set theory also doesn't xD |
| 2026-01-15 22:47:03 +0100 | <monochrom> | Not even when that someone is me. I don't bother to write a paper for that. |
| 2026-01-15 22:47:06 +0100 | <jreicher> | I don't disagree. I just can't see how it's possible. |
| 2026-01-15 22:47:45 +0100 | <jreicher> | Uncountability, in a way, "comes from nowhere". It has to be asserted. You can't constructit. |
| 2026-01-15 22:47:48 +0100 | <EvanR> | here is one... data Bitstream = I Bitstream | O Bitstream |
| 2026-01-15 22:47:58 +0100 | <EvanR> | jreicher, why do you think this xD |
| 2026-01-15 22:48:09 +0100 | <monochrom> | Oh it is asserted. Denotational semantics are seldom constructive. |
| 2026-01-15 22:48:10 +0100 | <jreicher> | EvanR: how is that uncountable? |
| 2026-01-15 22:48:27 +0100 | <EvanR> | you define things and then see if this or that satisfies the definition |
| 2026-01-15 22:48:32 +0100 | <EvanR> | nothing wrong with definitions |
| 2026-01-15 22:49:00 +0100 | <EvanR> | jreicher, there was this guy cantor with this diagonalization argument |
| 2026-01-15 22:49:09 +0100 | <geekosaur> | ^ |
| 2026-01-15 22:49:24 +0100 | <EvanR> | it made a lot of people very angry and was generally considered a bad idea |
| 2026-01-15 22:49:28 +0100 | <geekosaur> | that was my thought, it either proves countability or provides a recipe to construct uncountably many values |
| 2026-01-15 22:49:46 +0100 | <jreicher> | Yes, but that datatype is not all the reals |
| 2026-01-15 22:49:53 +0100 | <EvanR> | reals? |
| 2026-01-15 22:49:55 +0100 | <jreicher> | You can't make the diagonalisation from it |
| 2026-01-15 22:50:06 +0100 | <EvanR> | that's .. neither here nor there |
| 2026-01-15 22:50:22 +0100 | <jreicher> | Any bitstream value is INDEFINITE length, but it's still FINITE. |
| 2026-01-15 22:50:31 +0100 | <EvanR> | wat |
| 2026-01-15 22:50:44 +0100 | <jreicher> | You can't have an infinite bitstream value |
| 2026-01-15 22:50:56 +0100 | <EvanR> | we're about to jump the shark from uncountability to ultrafinitism |
| 2026-01-15 22:51:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:51:37 +0100 | <EvanR> | ignoring bottoms there's no way to make a finite Bitstream |
| 2026-01-15 22:51:39 +0100 | <monochrom> | Consider the usual denotational sematnics of BitStream, as opposed to the usual operational semantics of it in Haskell? So do you mean that you seek materials for teaching denotational semantics? |
| 2026-01-15 22:52:36 +0100 | <jreicher> | I'm just after anything that will prove (without question-begging assertions) that BitStream is uncountable. It looks entirely countable to me. |
| 2026-01-15 22:52:47 +0100 | <EvanR> | what makes you say that |
| 2026-01-15 22:53:29 +0100 | <jreicher> | I've already explained. The "recursion" of the construction is infinite, but all the things constructed are finite. So you don't get diagonalisation. |
| 2026-01-15 22:53:41 +0100 | <EvanR> | I don't follow... |
| 2026-01-15 22:53:53 +0100 | <EvanR> | all things constructed are finite? |
| 2026-01-15 22:54:02 +0100 | <monochrom> | Well here goes shameless plug. This is my lecture notes for this stuff: https://www.cs.utoronto.ca/~trebla/CSCC24-latest/partial-order-recursion.html |
| 2026-01-15 22:54:40 +0100 | <dolio> | The type of lazy streams is uncountable. |
| 2026-01-15 22:54:55 +0100 | <jreicher> | dolio: reference? I don't see how that would be the case |
| 2026-01-15 22:55:45 +0100 | <EvanR> | one way to look at countable A is you can make a [A] which contains at some point all possible A values |
| 2026-01-15 22:55:57 +0100 | <EvanR> | possibly infinite |
| 2026-01-15 22:56:02 +0100 | <dolio> | https://hub.darcs.net/dolio/unpossible/browse/src/Cantor/Properties.agda#66 |
| 2026-01-15 22:56:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 22:56:22 +0100 | <jreicher> | EvanR: Take (as a silly example) data SillyType = I SillyType. Countable or uncountable? |
| 2026-01-15 22:56:23 +0100 | <monochrom> | With my notes, you can either take the watered-down take in the first half, where I just assert that all infinite bit strings are in the set for the type, then use the usual diagonizable argument; or use the second half where I describe the recipe for the set for non-strict ADTs in general, then do it for BitStream yourself... |
| 2026-01-15 22:56:46 +0100 | <jreicher> | monochrom: there aren't any infinite bit strings in the set |
| 2026-01-15 22:56:47 +0100 | <monochrom> | SillyType is countable. |
| 2026-01-15 22:56:54 +0100 | <EvanR> | jreicher, is the only (respectable) value here I (I (I (I ...)))? |
| 2026-01-15 22:56:59 +0100 | <EvanR> | so cardinalty 1 |
| 2026-01-15 22:57:12 +0100 | <jreicher> | monochrom: Exactly. So making it a "binary choice" recursion doesn't magically make it uncountable |
| 2026-01-15 22:57:57 +0100 | <monochrom> | You need infinite strings for completeness. |
| 2026-01-15 22:58:18 +0100 | <EvanR> | there's no finite strings by design, so I'm confused by that |
| 2026-01-15 22:58:52 +0100 | <monochrom> | The increasing sequence I bottom, I (I bottom), I (I (I bottom)) ... needs a least upper bound. |
| 2026-01-15 22:58:55 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 2026-01-15 22:59:40 +0100 | <jreicher> | monochrom: My only point is that none of these recursive datatypes give you infinite strings. |
| 2026-01-15 22:59:48 +0100 | <jreicher> | You have an infinite series of finite strings |
| 2026-01-15 22:59:58 +0100 | <EvanR> | I guess including all these partially defined possibilities is making it even more infinite |
| 2026-01-15 23:00:10 +0100 | EvanR | looks at jreicher |
| 2026-01-15 23:00:25 +0100 | <int-e> | . o O ( it must be nice to have convictions ) |
| 2026-01-15 23:00:53 +0100 | <dolio> | > cycle [0,1] |
| 2026-01-15 23:00:54 +0100 | <lambdabot> | [0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1... |
| 2026-01-15 23:01:01 +0100 | <monochrom> | If you don't complain that I said "bottom", then you have accepted that I am doing a denotational semantics model, and therefore there are infinite strings in the model. |
| 2026-01-15 23:01:08 +0100 | <EvanR> | the corresponding complaint about infinite objects in normal math is getting worse than I thought, though allowing "infinite" versions of each value at least isn't ultrafinite |