| 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 |
| 2026-01-15 23:01:52 +0100 | <monochrom> | I can respect that you reject denotational semantics altogether, but then you should also be rejecting "bottom". |
| 2026-01-15 23:02:17 +0100 | <jreicher> | I'm not rejecting denotational semantics. I'd just like a pointer to something that explains where/how/why anything uncountable comes in. |
| 2026-01-15 23:02:25 +0100 | <int-e> | But how can you discuss countability in a finitist context? :P |
| 2026-01-15 23:02:30 +0100 | <monochrom> | OK sure. Read my lecture notes first? |
| 2026-01-15 23:02:39 +0100 | <jreicher> | I'm not finitist. I just said infinite series of finite objects. |
| 2026-01-15 23:02:48 +0100 | <EvanR> | you first need to know what Bitstreams even are, and then you can progress to the cantor style proof which mirrors the classic version for binary strings |
| 2026-01-15 23:02:58 +0100 | <EvanR> | jreicher, good xD |
| 2026-01-15 23:03:22 +0100 | <int-e> | (I can defend the idea that streams are countable but it'll involve computability and/or Scott domains) |
| 2026-01-15 23:03:29 +0100 | <dolio> | jreicher: The only way to believe that being recursive makes things countable is by not taking recursion seriously enough. When you set up your mathematics such that everything is inherently recursive, some things in that mathematics become uncountable again. |
| 2026-01-15 23:03:46 +0100 | <EvanR> | or definability, because you have to write the code, and code is countable |
| 2026-01-15 23:03:54 +0100 | Inline | (~User@cgn-195-14-218-118.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 2026-01-15 23:04:20 +0100 | <EvanR> | (but I might be wrong here beacuse of higher order programs) |
| 2026-01-15 23:04:26 +0100 | <dolio> | E.G. if you build recursive things in classical mathematics, it will appear that the set of recursively definable streams is countable. But the enumeration of all such streams is not recursive. |
| 2026-01-15 23:04:52 +0100 | <jreicher> | I have to think this through carefully, but I think you are all accepting the existence of infinitely-running programs? |
| 2026-01-15 23:05:09 +0100 | <EvanR> | sounds like operational semantics |
| 2026-01-15 23:05:11 +0100 | <dolio> | Internally to the world of recursive mathematics, Cantor's diagonal argument holds, and the type of infinite bit streams is uncountable. |
| 2026-01-15 23:05:23 +0100 | <int-e> | And a clear distinction between object and meta levels, because at the object level, for any sequence of sequences f :: Nat -> (Nat -> Bool) you can apply Cantor's diagonal construction, s n = not (f n n) to obtain a sequence that's not in the enumeration. (I'll skip how Nat -> Bool is equivalent to streams of bools) |
| 2026-01-15 23:05:51 +0100 | <dolio> | Viewed externally as built in classical mathematics, that is the statement, 'the set of recursive bit streams is "computably uncountable."' |
| 2026-01-15 23:06:03 +0100 | <EvanR> | i.e. the only thing that is real is a real running program on a computer, which will never be infinite, because the universe is purely finite or something. Which is the kind of stuff I'd like to use math to avoid entirely |
| 2026-01-15 23:06:21 +0100 | <dolio> | I.E. given a computable enumeration of computable bit streams, one can compute a bit stream not in the enumeration. |
| 2026-01-15 23:06:25 +0100 | <jreicher> | If we say infinite bitstreams exist, then the type is uncountable. I'm not arguing with that. But in practice (and I hesitate as I say that) you're never going to have an infinite bitstream, so I'm not sure this is a sensible thing to say. |
| 2026-01-15 23:07:00 +0100 | <EvanR> | you're trying to say like > repeat 'a' is not an infinite list |
| 2026-01-15 23:07:04 +0100 | <EvanR> | in haskell xD |
| 2026-01-15 23:07:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:07:25 +0100 | <int-e> | it's a very finite graph :P |
| 2026-01-15 23:07:32 +0100 | <int-e> | (once fully evaluated) |
| 2026-01-15 23:07:39 +0100 | <EvanR> | in ghc! |
| 2026-01-15 23:07:46 +0100 | <EvanR> | if you're lucky |
| 2026-01-15 23:07:56 +0100 | <jreicher> | EvanR: I don't think so, no. I'm saying something more like you can't generate ALL infinite lists that way (e.g. uncomputable ones) |
| 2026-01-15 23:08:05 +0100 | <EvanR> | that's the point |
| 2026-01-15 23:08:11 +0100 | <int-e> | EvanR: Well, in isolation, assuming it isn't fused away :P |
| 2026-01-15 23:08:33 +0100 | <EvanR> | you can't generate a stream of all the lists |
| 2026-01-15 23:08:34 +0100 | <monochrom> | I thought I explained that. A model that contains impractical elements can be a useful approximation and/or abstraction. |
| 2026-01-15 23:08:47 +0100 | <EvanR> | some are necessarily missing |
| 2026-01-15 23:08:55 +0100 | <EvanR> | no matter how you go about it |
| 2026-01-15 23:09:01 +0100 | <dolio> | Uncomputable lists aren't real. |
| 2026-01-15 23:09:20 +0100 | <EvanR> | and cantor's proof produces a constructive example list which isn't there |
| 2026-01-15 23:09:21 +0100 | <jreicher> | And if they're missing, how is it meaningful to say the type is uncountable? (I feel like this is hitting downward lowenheim-skolem somehow) |
| 2026-01-15 23:09:21 +0100 | <int-e> | If you don't model this mathematically, countability doesn't even come up; there is no set whose cardinality you could possibly discuss. |
| 2026-01-15 23:09:22 +0100 | <EvanR> | kind of cool |
| 2026-01-15 23:09:52 +0100 | <EvanR> | jreicher, this is like saying any map from N into A necessarily misses some As |
| 2026-01-15 23:10:05 +0100 | <EvanR> | which is what we're trying to say |
| 2026-01-15 23:10:05 +0100 | <jreicher> | Not "some". Most. |
| 2026-01-15 23:10:09 +0100 | <EvanR> | sure |
| 2026-01-15 23:10:18 +0100 | <EvanR> | that's what uncountable is |
| 2026-01-15 23:10:42 +0100 | Zemy | (~Zemy@72.178.108.235) |
| 2026-01-15 23:10:58 +0100 | <dolio> | Every computable map misses many computable streams. |
| 2026-01-15 23:11:04 +0100 | <jreicher> | So let me re-ask the question. Do you think it's possible to model all this mathematically such that BitStream is a countable infinite type? |
| 2026-01-15 23:11:21 +0100 | <EvanR> | sure |
| 2026-01-15 23:11:26 +0100 | <monochrom> | Yes. For example operational semantics. |
| 2026-01-15 23:11:44 +0100 | <jreicher> | OK. So what do we gain from adding the assertion (because we'd need to) that makes it uncountable? |
| 2026-01-15 23:11:47 +0100 | <monochrom> | Another example: Translating Haskell to Turing machines. |
| 2026-01-15 23:12:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 23:12:03 +0100 | <EvanR> | this is why I began by phrasing the whole thing as "are you sure" about not having uncountable things, it depends on how you think about it |
| 2026-01-15 23:12:03 +0100 | <int-e> | When you model programs mathematically, you typically do not impose a running time bound up front, so the modelled program behavior is effectively infinite (since you can run it to any arbitrary length, giving you a state after n steps for all natural numbers n). |
| 2026-01-15 23:12:14 +0100 | <int-e> | It's a simplification. |
| 2026-01-15 23:12:18 +0100 | <EvanR> | jreicher, it's not an assertion, there's a constructive proof xD |
| 2026-01-15 23:12:22 +0100 | <monochrom> | Avoiding the cumbersomeness and missing-the-forest-for-the-trees of operational semantics and Turing machines. |
| 2026-01-15 23:12:27 +0100 | <EvanR> | yielding the missing stream |
| 2026-01-15 23:12:57 +0100 | <jreicher> | EvanR: the proof (like all proofs) starts with axioms. The axioms are the assertions. |
| 2026-01-15 23:13:00 +0100 | <EvanR> | that you can't run a program for infinite time isn't the secret sauce to model it as countable |
| 2026-01-15 23:13:04 +0100 | <EvanR> | that's more like ultrafinitism |
| 2026-01-15 23:13:13 +0100 | <monochrom> | My lecture notes also shows that if you use this "unrealistic" (but still sound) denotational approach, it is easier to predict the outcome of certain recursive definitions. |
| 2026-01-15 23:13:20 +0100 | <EvanR> | jreicher, in type theory, we don't always have axioms! |
| 2026-01-15 23:13:33 +0100 | <jreicher> | How can you have a theory without axioms? |
| 2026-01-15 23:13:37 +0100 | <EvanR> | definitions |
| 2026-01-15 23:13:40 +0100 | <int-e> | And, correspondingly, the easiest model for streams of Bools gives you an arbitrary boolean value for the n-th element of the stream, for each natural number N. The set of all these functions is uncountable. |
| 2026-01-15 23:13:46 +0100 | <jreicher> | Definitions are axioms |
| 2026-01-15 23:13:55 +0100 | <int-e> | Again, keeping things as mathematically simple as possible. |
| 2026-01-15 23:13:57 +0100 | <EvanR> | well that's muddying things a lot isn't it |
| 2026-01-15 23:14:10 +0100 | <jreicher> | Not for a formal theory, no |
| 2026-01-15 23:14:16 +0100 | <EvanR> | definition is just naming something that you could already say long winded |
| 2026-01-15 23:14:22 +0100 | <EvanR> | to save space |
| 2026-01-15 23:14:51 +0100 | <monochrom> | The hardest example made easy being fs = 1 : 1 : zipWith (+) fs (tail fs). |
| 2026-01-15 23:14:53 +0100 | <jreicher> | int-e: monochrom: I appreciate the use of "extra" infinity as a simplification. Not the first time I've heard that argument. |
| 2026-01-15 23:15:12 +0100 | <EvanR> | an example of an axiom in type theory is the law of excluded middle. Introduces by fiat. As opposed to proven as a theorem somehow |
| 2026-01-15 23:15:21 +0100 | <EvanR> | introduced* |
| 2026-01-15 23:15:24 +0100 | <monochrom> | Every textbook or tutorial I saw tried to explain it poorly with lazy evaluation. |
| 2026-01-15 23:15:24 +0100 | <jreicher> | "fiar" is "assertion" |
| 2026-01-15 23:15:25 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 256 seconds) |
| 2026-01-15 23:15:27 +0100 | <jreicher> | *fiat |
| 2026-01-15 23:16:07 +0100 | <monochrom> | But if you do the denotational "construct the approximation sequence, take limit" it's plain as day. |
| 2026-01-15 23:18:26 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-15 23:20:16 +0100 | <dolio> | All you need to do to have uncountable bit streams is live within constructive mathematics, recognizing that it holds for computable things (computability allows extra principles on top of bare constructive mathematics, actually). |
| 2026-01-15 23:20:31 +0100 | <dolio> | Cantor's diagonal argument is constructive, ergo bit streams are uncountable. |
| 2026-01-15 23:20:41 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 23:20:50 +0100 | <monochrom> | (About theory with/wo axioms. I don't draw lines between axioms, definitions, inference rules either.) |
| 2026-01-15 23:20:54 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 23:20:55 +0100 | <int-e> | dolio: see me 15 minutes ago ;-) |
| 2026-01-15 23:20:56 +0100 | <dolio> | The only way they look countable is if you believe in classical mathematics and try to build computability within that. |
| 2026-01-15 23:21:22 +0100 | <EvanR> | another thing, my kneejerk devil's advocate arguement for the countable Bitstream is that you can only have finite many programs. However in haskell you can obtain Bitstream other ways... which perhaps also avoids computability |
| 2026-01-15 23:21:32 +0100 | <EvanR> | s/finite/countable/ |
| 2026-01-15 23:21:56 +0100 | <dolio> | But in the natural mathematics of computable things, they are uncountable. The ways to count them are not computable. |
| 2026-01-15 23:22:17 +0100 | <dolio> | So reject them. |
| 2026-01-15 23:22:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:23:26 +0100 | <monochrom> | That gives very different feel... But I confess I'm classical in my core, I only pretend to be intuitionistic when it's convenient. :) |
| 2026-01-15 23:23:54 +0100 | <EvanR> | monochrom, I'm calling definitions shorthand that expands to something we already had. Unlike e.g. "the answer to any LEM question you name" |
| 2026-01-15 23:23:56 +0100 | <dolio> | The diagonal argument shows that any computable way to enumerate computable bit streams misses some of the computable bit streams. You don't need uncomputable ones for the enumeration to be incomplete. |
| 2026-01-15 23:24:34 +0100 | <EvanR> | basically syntactic sugar |
| 2026-01-15 23:24:39 +0100 | <monochrom> | Because classical uncountability gives me a feeling of size, but constructive uncountability doesn't feel like "bigger size", just "unreachable". |
| 2026-01-15 23:25:03 +0100 | <EvanR> | again, isn't this saying more about misunderstanding classical notions ? xD |
| 2026-01-15 23:25:03 +0100 | <dolio> | Yes, the idea that uncountability is about "size" is an erroneous extrapolation from finite sets. |
| 2026-01-15 23:25:34 +0100 | <dolio> | The extended natural numbers are uncountable. |
| 2026-01-15 23:25:36 +0100 | <monochrom> | EvanR, I clone every definition to be an axiom, e.g., definition "x := 4" is cloned so I add an axiom "x = 4". |
| 2026-01-15 23:25:42 +0100 | <dolio> | How many more are there? At most one. |
| 2026-01-15 23:25:43 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 240 seconds) |
| 2026-01-15 23:25:56 +0100 | <EvanR> | monochrom, what do you achieve by doing this xD |
| 2026-01-15 23:26:02 +0100 | <EvanR> | twice as many definitions / axioms? xD |
| 2026-01-15 23:26:15 +0100 | <monochrom> | I achieve "they are all axioms". |
| 2026-01-15 23:26:17 +0100 | <dolio> | But infinity + 1 = infinity, right? |
| 2026-01-15 23:26:58 +0100 | <EvanR> | monochrom, it's a slippery slope from there to buffyspeak anything can be anythinged! |
| 2026-01-15 23:27:17 +0100 | <dolio> | (That uncountability part requires more committment to computable principles.) |
| 2026-01-15 23:27:31 +0100 | <monochrom> | Oh sure, I then further consider axioms to be special cases of theorems! |
| 2026-01-15 23:28:02 +0100 | <EvanR> | 🤢 |
| 2026-01-15 23:28:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 23:28:24 +0100 | <int-e> | has anybody said "global assumptions" |
| 2026-01-15 23:28:41 +0100 | <EvanR> | theorems ideally come with proofs, while you wouldn't expect a proof |
| 2026-01-15 23:28:45 +0100 | <monochrom> | But I stop there. When I prove something, I only need a line between theorems and non-theorems. Why should I care about further distinctions between "different kinds" of theorems? |
| 2026-01-15 23:28:51 +0100 | <EvanR> | if we don't want anything to mean anything, we can do that I guess xD |
| 2026-01-15 23:29:01 +0100 | <EvanR> | wouldn't expect proof of an axiom* |
| 2026-01-15 23:29:23 +0100 | <EvanR> | and "proving a definition" is itself like a classic fallacy xD |
| 2026-01-15 23:30:23 +0100 | <monochrom> | Consider a tree as in computer science or programming. There are root nodes, there are children nodes, there are greatgreatgrandganddaughter nodes, you can make infinitely many artificial distinctions between nodes living at different positions in the tree... |
| 2026-01-15 23:30:32 +0100 | <monochrom> | WHY SHOULD I CARE. They're all nodes. |
| 2026-01-15 23:30:35 +0100 | <int-e> | EvanR: You can prove that adding a definitional axiom (of the shape <new name> = <expression>) is a conservative extension for any [add suitable adjective] logic |
| 2026-01-15 23:30:56 +0100 | <EvanR> | monochrom, really, all these things fit inside a neat tree of life somehow? |
| 2026-01-15 23:30:58 +0100 | <int-e> | EvanR: thereby proving all definitions at once ;-) |
| 2026-01-15 23:30:58 +0100 | <monochrom> | For the simple purpose of traversing or generating that tree, they are all nodes, period. |
| 2026-01-15 23:31:03 +0100 | <EvanR> | I was trying to get away from that with jreicher |
| 2026-01-15 23:31:25 +0100 | <int-e> | @quote |
| 2026-01-15 23:31:25 +0100 | <lambdabot> | cjeris says: vincenz: no, on a 286 GHC feels warm, like a little fire you can warm your hands at. wait, that smells funny. wait, that was my CPU. |
| 2026-01-15 23:31:26 +0100 | <monochrom> | Now consider that this tree happens to be my proof tree. So node = theorem. Period. |
| 2026-01-15 23:31:27 +0100 | <EvanR> | no reason everything needs to fit into the same tree |
| 2026-01-15 23:31:44 +0100 | <monochrom> | Oh the root node is also called "axiom". Sure. Whatever. |
| 2026-01-15 23:31:59 +0100 | <jreicher> | dolio: what do you mean when you say that uncountability comes "naturally" from "constructive" mathematics? (I'm probably paraphasing badly, and I'm not disagreeing; I'm just trying to understand your idea) |
| 2026-01-15 23:32:03 +0100 | <monochrom> | Sure. s/tree/forest/ ? |
| 2026-01-15 23:32:48 +0100 | <monochrom> | Wait, you can run GHC on a 286?! |
| 2026-01-15 23:32:49 +0100 | <EvanR> | everything is in the same forest... as a tree of 1 node... back to the penchant for containerization |
| 2026-01-15 23:33:18 +0100 | <EvanR> | in lambda MOO luckily nodes aren't all required to be in one tree, or even in any tree |
| 2026-01-15 23:33:35 +0100 | <int-e> | monochrom: emulators are a thing you know ;-) |
| 2026-01-15 23:33:58 +0100 | <dolio> | jreicher: Cantor's diagonal argument is constructive. It's basically what I linked. Given `enum : ℕ → (ℕ → 2)`, one can construct a `ℕ → 2` that is not in the image of `enum`. |
| 2026-01-15 23:34:05 +0100 | <monochrom> | Wait, does that you use a 286 to emulate a 386 then run GHC there? |
| 2026-01-15 23:34:15 +0100 | <monochrom> | s/does that you/does that mean/ |
| 2026-01-15 23:34:19 +0100 | <jreicher> | OK. But what about the set he's diagonlising? |
| 2026-01-15 23:34:36 +0100 | <int-e> | monochrom: I don't know. I'm filling in my own details here :P |
| 2026-01-15 23:34:42 +0100 | <monochrom> | Heh |
| 2026-01-15 23:35:12 +0100 | <EvanR> | "wavfunction collapse procedural generation" of anecdotes xD |
| 2026-01-15 23:35:22 +0100 | <dolio> | jreicher: I don't understand the question. |
| 2026-01-15 23:35:24 +0100 | <monochrom> | Because AFAIK GHC assumes a flat/linear 32-bit addressing model i.e. at least 386. |
| 2026-01-15 23:35:43 +0100 | <jreicher> | dolio: I think you're presupposing that the set of reals is "constructive". No? |
| 2026-01-15 23:35:44 +0100 | <int-e> | I don't know that there never was a 16 bit version of GHC. |
| 2026-01-15 23:35:56 +0100 | <EvanR> | who ordered reals |
| 2026-01-15 23:36:03 +0100 | <int-e> | (It does seem rather unlikely though.) |
| 2026-01-15 23:36:12 +0100 | <monochrom> | OK OK April's Fool project: Drastically overhaul GHC to be runnable on 286's segment model! |
| 2026-01-15 23:36:18 +0100 | <dolio> | Reals are too complicated to get into. This is just the bit streams. |
| 2026-01-15 23:36:32 +0100 | <jreicher> | If you have infinite bitstreams, you have all the reals |
| 2026-01-15 23:36:33 +0100 | <int-e> | monochrom: protected mode or real mode? |
| 2026-01-15 23:36:36 +0100 | <monochrom> | (Oh then it probably also runs on 8088 DOS too...) |
| 2026-01-15 23:36:40 +0100 | <jreicher> | Sorry, I should say ALL the infinite bitstreams |
| 2026-01-15 23:36:42 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-01-15 23:36:44 +0100 | <dolio> | Reals are a quotient. |
| 2026-01-15 23:36:57 +0100 | <jreicher> | Huh? |
| 2026-01-15 23:37:08 +0100 | <int-e> | dolio: Don't you like Dedekind cuts? |
| 2026-01-15 23:37:10 +0100 | <EvanR> | we're getting off topic trying to jam classical reals into the discussion |
| 2026-01-15 23:37:16 +0100 | <EvanR> | which isn't about them |
| 2026-01-15 23:37:28 +0100 | <int-e> | (so *now* we're getting off topic, huh) |
| 2026-01-15 23:37:30 +0100 | int-e | runs |
| 2026-01-15 23:37:31 +0100 | <dolio> | jreicher: Like 0.11111... = 1.0 (binary). |
| 2026-01-15 23:37:33 +0100 | <EvanR> | lol |
| 2026-01-15 23:37:56 +0100 | <jreicher> | EvanR: how can you have Cantor's diagonalisation without the reals? |
| 2026-01-15 23:38:01 +0100 | <jreicher> | (Maybe I've misunderstood the idea) |
| 2026-01-15 23:38:04 +0100 | <EvanR> | yes that is what this whole discussion is about |
| 2026-01-15 23:38:06 +0100 | <dolio> | It's actually possible for the (Dedekind) reals to be countable in constructive mathematics. |
| 2026-01-15 23:38:10 +0100 | <EvanR> | was cantor even talking about real numbers |
| 2026-01-15 23:38:18 +0100 | <dolio> | Even though the bit streams are uncountable. |
| 2026-01-15 23:38:21 +0100 | <jreicher> | To begin with I'm pretty sure he was |
| 2026-01-15 23:38:22 +0100 | <monochrom> | I think GCC for DOS could do 32-bit in real mode. I forgot. But just do whatever GCC-for-DOS does. |
| 2026-01-15 23:38:42 +0100 | <jreicher> | dolio: Ok, I'll stick to bistreams. In what way is a non-computable (infinite) bitstream "constructive"? |
| 2026-01-15 23:38:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:38:52 +0100 | <EvanR> | at that time, it wasn't appreciated the subtleties that binary streams created for defining reals... but a stream of bits is pretty simple |
| 2026-01-15 23:39:04 +0100 | <dolio> | They aren't. We only need the computable ones. |
| 2026-01-15 23:40:15 +0100 | <jreicher> | And if you only have the computable ones, the set is countable. |
| 2026-01-15 23:40:24 +0100 | <dolio> | No, it isn't. |
| 2026-01-15 23:40:45 +0100 | <EvanR> | at some point doing the proof might help since this is ... mathematical |
| 2026-01-15 23:40:55 +0100 | <jreicher> | "computable" can be understood as "generated by a program", and all program texts are finite. So the set of all program texts is countable, and so is the set of computable outputs |
| 2026-01-15 23:41:00 +0100 | <dolio> | Cantor's diagonal argument shows every computable enumeration of the computable bit streams misses a computable bit stream. |
| 2026-01-15 23:41:05 +0100 | <EvanR> | a proof is worth 1000 words |
| 2026-01-15 23:41:34 +0100 | <EvanR> | jreicher, I went over that in a few ways above |
| 2026-01-15 23:42:03 +0100 | tomsmeding | . o O ( every _computable_ enumeration -- that bit is relevant here ) |
| 2026-01-15 23:42:08 +0100 | <dolio> | Yeah. |
| 2026-01-15 23:42:28 +0100 | <dolio> | If you want to say there's a non-computable enumeration, you have again exited constructive mathematics. |
| 2026-01-15 23:42:34 +0100 | <tomsmeding> | this is not classical set-theoretical "countable", this is "computably countable" |
| 2026-01-15 23:42:51 +0100 | <int-e> | tomsmeding: But the only reason we are in this mess is that we pretend that "everything" is computable. As I said earlier, you need to be very clear about object and meta levels for this discussion to be meaningful. |
| 2026-01-15 23:42:59 +0100 | <EvanR> | another way to say that, already said, Bitstream is uncountable (in haskell). (Assuming a lot about what kind of haskell you are allowed to write) |
| 2026-01-15 23:43:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-15 23:43:25 +0100 | <tomsmeding> | int-e: right -- I haven't really been following the discussion. You know what, I'll leave you at it :) |
| 2026-01-15 23:43:50 +0100 | <int-e> | tomsmeding: Ah sorry, I'm not complaining! |
| 2026-01-15 23:43:53 +0100 | <EvanR> | if I hook up my Bitstream generator to an external entity then it only makes matters worse |
| 2026-01-15 23:44:02 +0100 | <EvanR> | we're not going to get less bitstreams that way |
| 2026-01-15 23:44:08 +0100 | <jreicher> | dolio: You're saying that because the set of computable numbers is not itself computably enumrable, that it's "constructively" uncountable? Something like that? |
| 2026-01-15 23:44:27 +0100 | <int-e> | tomsmeding: It's in the nature of IRC that discussions become circular, for better or worse. |
| 2026-01-15 23:44:33 +0100 | <tomsmeding> | :D |
| 2026-01-15 23:45:09 +0100 | <dolio> | jreicher: Something like that. Maybe it's backwards. The constructive proof of its uncountability 'means' that the computable bit streams are not computably enumerable. |
| 2026-01-15 23:45:22 +0100 | <dolio> | Because constructive mathematics is valid for computability. |
| 2026-01-15 23:45:26 +0100 | <EvanR> | whatever the proof means, the proof goes through |
| 2026-01-15 23:45:30 +0100 | <EvanR> | it's valid in of itself |
| 2026-01-15 23:45:31 +0100 | <jreicher> | I don't really understand why that serves as a meanginful notion of uncountability |
| 2026-01-15 23:45:33 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-15 23:45:49 +0100 | <EvanR> | jreicher, you're working on the level of vibes it seems... instead of defining stuff, then proof a theorem |
| 2026-01-15 23:46:16 +0100 | <jreicher> | At the moment I'm just trying to understand dolio's definitions |
| 2026-01-15 23:46:17 +0100 | <EvanR> | for whatever reason you don't like the result, even though it jives exactly with classical math xD |
| 2026-01-15 23:46:32 +0100 | <EvanR> | instead yeah lets understand it on its own terms |
| 2026-01-15 23:46:37 +0100 | <dolio> | The reason the 'program text' thing won't work is that the computable bit streams are (at best) a quotient of program texts. So being able to enumerate program texts won't help you enumerate all the bit streams. |
| 2026-01-15 23:46:38 +0100 | <jreicher> | I know what the definitions and theorems are in classical maths. I don't have a problem with any of that. |
| 2026-01-15 23:47:16 +0100 | <jreicher> | dolio: but why is enumeration important here at all? What's the connection with uncountability, for you? |
| 2026-01-15 23:47:29 +0100 | jmcantrell_ | jmcantrell |
| 2026-01-15 23:47:29 +0100 | <jreicher> | Sorry, I mean computable enumeration |
| 2026-01-15 23:47:45 +0100 | <dolio> | Countability is 'there is a surjection from â„•'. |
| 2026-01-15 23:47:50 +0100 | <EvanR> | Bitstream is uncountable (in haskell) <- |
| 2026-01-15 23:48:12 +0100 | <dolio> | (Or similar) |
| 2026-01-15 23:48:26 +0100 | <int-e> | if you dislike "countability" you can say that recursive functions are not recursively enumerable ;-) |
| 2026-01-15 23:48:29 +0100 | <dolio> | And I don't believe in uncomputable things. So the surjection is computable. |
| 2026-01-15 23:48:41 +0100 | <jreicher> | Oh. I haven't heard that view before. |
| 2026-01-15 23:48:43 +0100 | mange | (~mange@user/mange) mange |
| 2026-01-15 23:48:58 +0100 | <EvanR> | which definition are you having issues with again |
| 2026-01-15 23:49:05 +0100 | <dolio> | That is the premise, at least. We are in the world where everything is inherently computable. |
| 2026-01-15 23:49:18 +0100 | <jreicher> | So you don't believe something like Chaitin's omega exists? |
| 2026-01-15 23:49:29 +0100 | michalz | (~michalz@185.246.207.205) (Remote host closed the connection) |
| 2026-01-15 23:49:33 +0100 | <EvanR> | you said you weren't a platonist! |