Logs on 2026-01-15 (liberachat/#haskell)

00:10:52	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:14:29	→	jmcantrell_ joins (~weechat@user/jmcantrell)
00:16:13	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
00:20:40	→	hakutaku joins (~textual@chen.yukari.eu.org)
00:29:05	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:33:48	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
00:37:14	×	Tuplanolla quits (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.)
00:38:59	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:39:56	→	myxos joins (~myxos@174-18-88-231.tcso.qwest.net)
00:43:43	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
00:43:51	→	Lycurgus joins (~juan@user/Lycurgus)
00:46:10	×	xff0x quits (~xff0x@2405:6580:b080:900:dc92:188b:d152:35db) (Ping timeout: 246 seconds)
00:53:36	→	Square joins (~Square@user/square)
00:54:47	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
00:57:43	×	Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org ))
01:01:17	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
01:03:02	→	troydm joins (~troydm@user/troydm)
01:09:40	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...)
01:12:49	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:17:35	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
01:18:39	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
01:24:58	×	divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer)
01:25:05	→	divlamir_ joins (~divlamir@user/divlamir)
01:25:57	divlamir_	is now known as divlamir
01:28:37	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:31:49	×	annamalai quits (~annamalai@157.49.214.71) (Ping timeout: 264 seconds)
01:33:44	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
01:36:55	×	lbseale quits (~quassel@user/ep1ctetus) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
01:37:39	→	lbseale joins (~quassel@user/ep1ctetus)
01:40:32	→	xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
01:44:24	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
01:45:51	→	L29Ah joins (~L29Ah@wikipedia/L29Ah)
01:49:15	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:53:20	→	omidmash2 joins (~omidmash@user/omidmash)
01:54:27	→	housemate_ joins (~housemate@203.56.146.214)
01:54:35	×	housemate quits (~housemate@203.56.146.214) (Read error: Connection reset by peer)
01:55:26	×	omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds)
01:55:26	omidmash2	is now known as omidmash
01:55:35	×	housemate_ quits (~housemate@203.56.146.214) (Max SendQ exceeded)
01:56:08	→	housemate_ joins (~housemate@203.56.146.214)
01:56:50	×	housemate_ quits (~housemate@203.56.146.214) (Max SendQ exceeded)
01:57:20	→	housemate_ joins (~housemate@203.56.146.214)
02:00:13	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:05:00	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
02:15:58	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:20:40	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
02:31:43	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:32:42	×	L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds)
02:36:55	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
02:47:30	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
02:52:07	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
02:53:51	→	annamalai joins (~annamalai@157.49.208.124)
02:56:34	×	acidjnk quits (~acidjnk@p200300d6e7171972cd12b2d062d86876.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
02:56:52	×	annamalai quits (~annamalai@157.49.208.124) (Remote host closed the connection)
02:58:11	→	annamalai joins (~annamalai@2409:4072:629e:6d46::2523:a8b1)
02:59:49	jmcantrell_	is now known as jmcantrell
03:03:17	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:04:14	×	ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
03:04:36	→	ChaiTRex joins (~ChaiTRex@user/chaitrex)
03:07:55	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
03:10:31	×	machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 240 seconds)
03:15:59	×	synchromesh quits (~john@2406:5a00:2412:2c00::144) (Quit: WeeChat 4.1.1)
03:19:05	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:22:11	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
03:24:24	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
03:28:37	→	newmind joins (~newmind@91-133-90-252.dyn.cablelink.at)
03:34:51	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:42:01	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
03:44:25	×	jumper149 quits (~jumper149@base.felixspringer.xyz) (Quit: WeeChat 4.7.1)
03:47:13	→	Guest71 joins (~Guest71@host-67-204-213-15.public.eastlink.ca)
03:47:22	×	Guest71 quits (~Guest71@host-67-204-213-15.public.eastlink.ca) (Client Quit)
03:52:53	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
03:57:01	×	omidmash quits (~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat)
03:57:53	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
04:01:35	→	omidmash joins (~omidmash@user/omidmash)
04:06:10	→	Square2 joins (~Square4@user/square)
04:07:33	×	Square2 quits (~Square4@user/square) (Remote host closed the connection)
04:08:39	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
04:09:17	×	newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Ping timeout: 272 seconds)
04:13:19	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
04:20:24	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
04:20:25	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
04:24:32	→	merijn joins (~merijn@62.45.136.136)
04:29:31	×	merijn quits (~merijn@62.45.136.136) (Ping timeout: 256 seconds)
04:33:35	×	jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 240 seconds)
04:34:31	×	califax quits (~califax@user/califx) (Remote host closed the connection)
04:34:45	→	califax joins (~califax@user/califx)
04:40:06	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
04:44:31	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
04:49:20	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
04:58:03	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:00:07	×	tessier quits (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 240 seconds)
05:02:25	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds)
05:07:41	→	bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex)
05:08:13	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
05:13:26	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:18:15	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
05:29:13	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:29:51	×	chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 244 seconds)
05:30:24	→	chromoblob joins (~chromoblo@user/chromob1ot1c)
05:34:13	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
05:38:53	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:39:37	×	mange quits (~mange@user/mange) (Quit: Quittin' time!)
05:40:44	×	chromoblob quits (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer)
05:41:08	→	chromoblob joins (~chromoblo@user/chromob1ot1c)
05:42:46	×	housemate_ quits (~housemate@203.56.146.214) (Quit: https://ineedsomeacidtocalmmedown.space/)
05:43:10	→	housemate joins (~housemate@203.56.146.214)
05:43:49	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
05:44:00	×	housemate quits (~housemate@203.56.146.214) (Max SendQ exceeded)
05:44:30	→	housemate joins (~housemate@203.56.146.214)
05:44:32	→	michalz joins (~michalz@185.246.207.205)
05:45:19	×	chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds)
05:54:19	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
05:58:57	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
06:09:41	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:12:39	→	chromoblob joins (~chromoblo@user/chromob1ot1c)
06:12:43	→	kimiamania3 joins (~9566fa0a@user/kimiamania)
06:14:43	×	kimiamania quits (~9566fa0a@user/kimiamania) (Ping timeout: 264 seconds)
06:14:44	kimiamania3	is now known as kimiamania
06:15:01	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
06:20:50	→	takuan joins (~takuan@d8D86B9E9.access.telenet.be)
06:25:28	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:27:20	→	jmcantrell_ joins (~weechat@user/jmcantrell)
06:32:22	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
06:34:02	×	jreicher quits (~joelr@user/jreicher) (Quit: Out and about)
06:35:56	×	ft quits (~ft@p4fc2a9d7.dip0.t-ipconnect.de) (Quit: leaving)
06:43:30	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
06:46:41	→	Lycurgus joins (~juan@user/Lycurgus)
06:48:23	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
06:53:30	×	poscat0x04 quits (~poscat@user/poscat) (Remote host closed the connection)
06:55:45	×	jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 245 seconds)
06:56:43	→	poscat joins (~poscat@user/poscat)
06:58:53	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:03:59	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
07:09:22	<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)
07:10:14	<gentauro>	https://github.com/simplex-chat/simplex-chat/blob/stable/docs/CLI.md#in-any-os
07:14:31	→	tromp joins (~textual@2001:1c00:3487:1b00:1931:5674:15e5:cfb0)
07:14:41	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:19:31	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
07:21:38	×	trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
07:21:52	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
07:28:47	×	Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org ))
07:30:28	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:35:23	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds)
07:39:52	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
07:44:42	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
07:47:57	×	ringo__ quits (~ringo@157.230.117.128) (Ping timeout: 250 seconds)
07:50:01	×	annamalai quits (~annamalai@2409:4072:629e:6d46::2523:a8b1) (Ping timeout: 246 seconds)
07:55:39	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
08:00:37	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
08:03:55	→	ringo__ joins (~ringo@157.230.117.128)
08:07:35	×	Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 240 seconds)
08:11:27	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
08:17:55	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
08:19:55	→	durstloescher joins (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3)
08:19:59	×	durstloescher quits (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) (Client Quit)
08:21:23	→	jreicher joins (~joelr@user/jreicher)
08:29:18	→	danza joins (~danza@user/danza)
08:33:10	×	tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:41:12	→	hardyhardhard joins (~guest5000@user/hardyhardhard)
08:49:04	→	Hardyhardhard59 joins (~Hardyhard@user/hardyhardhard)
08:50:29	×	hardyhardhard quits (~guest5000@user/hardyhardhard) (Ping timeout: 272 seconds)
08:51:53	→	chele joins (~chele@user/chele)
08:53:37	→	Maxdamantus joins (~Maxdamant@user/maxdamantus)
08:55:43	×	jreicher quits (~joelr@user/jreicher) (Quit: Gig time)
08:56:56	×	Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
09:05:13	→	peterbecich joins (~Thunderbi@71.84.33.135)
09:05:46	→	merijn joins (~merijn@77.242.116.146)
09:07:24	trickard_	is now known as trickard
09:09:19	×	peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds)
09:16:16	→	infinity0 joins (~infinity0@pwned.gg)
09:23:03	×	infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 265 seconds)
09:26:30	→	acidjnk joins (~acidjnk@p200300d6e7171948e4551533bd5d7598.dip0.t-ipconnect.de)
09:27:03	→	skum joins (~skum@user/skum)
09:29:36	→	Enrico63 joins (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213)
09:31:39	×	Hardyhardhard59 quits (~Hardyhard@user/hardyhardhard) (Ping timeout: 272 seconds)
09:43:41	→	infinity0 joins (~infinity0@pwned.gg)
09:48:31	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds)
09:54:59	→	merijn joins (~merijn@77.242.116.146)
09:58:45	×	Enrico63 quits (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Quit: Client closed)
10:19:06	×	xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
10:21:15	→	durstloescher joins (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3)
10:22:02	×	durstloescher quits (~textual@2a02:8109:1b01:2500:d98f:f3fd:cd44:a6b3) (Client Quit)
10:24:37	→	kuribas joins (~user@2a02-1810-2825-6000-cba-d3d9-b1a1-3dea.ip6.access.telenet.be)
10:27:46	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
10:30:42	→	CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
10:32:06	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 244 seconds)
10:41:35	×	trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 240 seconds)
10:42:10	×	p3n quits (~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in)
10:42:17	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
10:42:50	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
10:44:27	→	bggd joins (~bgg@2a01:e0a:fd5:f510:27fe:a881:1d17:429c)
10:44:27	×	bggd quits (~bgg@2a01:e0a:fd5:f510:27fe:a881:1d17:429c) (Changing host)
10:44:27	→	bggd joins (~bgg@user/bggd)
10:45:19	×	koz quits (~koz@121.99.240.58) (Ping timeout: 264 seconds)
10:51:00	<ncf>	limit the build? to what?
10:51:35	→	p3n joins (~p3n@217.198.124.246)
10:53:24	×	p3n quits (~p3n@217.198.124.246) (Client Quit)
10:53:52	→	p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1)
10:53:56	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
10:56:40	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
11:04:18	→	karenw joins (~karenw@user/karenw)
11:04:19	→	fp joins (~Thunderbi@130.233.70.149)
11:04:57	→	__monty__ joins (~toonn@user/toonn)
11:12:31	→	notzmv joins (~umar@user/notzmv)
11:18:36	→	xff0x joins (~xff0x@2405:6580:b080:900:5f60:7a2f:94c6:623e)
11:21:52	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
11:22:06	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
11:26:27	→	koz joins (~koz@121.99.240.58)
11:29:42	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
11:33:01	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
11:35:39	×	Square quits (~Square@user/square) (Quit: Leaving)
11:46:30	×	kuribas quits (~user@2a02-1810-2825-6000-cba-d3d9-b1a1-3dea.ip6.access.telenet.be) (Ping timeout: 244 seconds)
11:50:51	→	annamalai joins (~annamalai@117.231.194.195)
11:59:55	×	annamalai quits (~annamalai@117.231.194.195) (Ping timeout: 255 seconds)
12:00:18	→	annamalai joins (~annamalai@117.231.194.194)
12:08:32	→	ttybitnik joins (~ttybitnik@user/wolper)
12:10:53	<gentauro>	ncf: only to the `executable simplex-chat` -> https://github.com/simplex-chat/simplex-chat/blob/stable/simplex-chat.cabal#L410
12:11:06	<gentauro>	there are many libs and execs in that .cabal file. I don't need to build `bots` and so.
12:11:37	<gentauro>	like I stated, it's "easy" with `cabal`. But how do I replicate that approach with `nix shell flakes`
12:12:02	<ncf>	nix build .#<tab> will tell you what's available
12:12:13	<ncf>	nix shell doesn't build anything, it spawns a shell with the build dependencies
12:13:42	<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 .`
12:14:21	<ncf>	no it isn't
12:14:27	<gentauro>	I just thought it was the same with other `flake.nix` files. My bad
12:30:01	→	danz65539 joins (~danza@user/danza)
12:32:19	×	danza quits (~danza@user/danza) (Ping timeout: 255 seconds)
12:39:28	×	karenw quits (~karenw@user/karenw) (Ping timeout: 246 seconds)
12:39:55	×	tromp quits (~textual@2001:1c00:3487:1b00:1931:5674:15e5:cfb0) (Ping timeout: 264 seconds)
12:43:13	trickard_	is now known as trickard
12:53:43	×	koz quits (~koz@121.99.240.58) (Ping timeout: 260 seconds)
12:56:37	→	machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net)
13:03:31	×	trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
13:03:45	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
13:08:35	×	fp quits (~Thunderbi@130.233.70.149) (Ping timeout: 240 seconds)
13:09:37	×	annamalai quits (~annamalai@117.231.194.194) (Ping timeout: 264 seconds)
13:13:45	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
13:16:16	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
13:19:22	→	humasect_ joins (~humasect@dyn-192-249-132-90.nexicom.net)
13:21:01	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 264 seconds)
13:21:02	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 256 seconds)
13:23:53	→	FirefoxDeHuk joins (~FirefoxDe@user/FirefoxDeHuk)
13:33:02	→	newmind joins (~newmind@91-133-90-252.dyn.cablelink.at)
13:33:52	→	merijn joins (~merijn@77.242.116.146)
13:35:20	trickard_	is now known as trickard
13:43:31	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
13:46:22	×	FirefoxDeHuk quits (~FirefoxDe@user/FirefoxDeHuk) (Quit: Client closed)
13:48:45	→	merijn joins (~merijn@77.242.116.146)
13:54:36	×	housemate quits (~housemate@203.56.146.214) (Quit: https://ineedsomeacidtocalmmedown.space/)
13:55:28	→	kuribas joins (~user@2a02-1810-2825-6000-b6e0-77f4-472f-1183.ip6.access.telenet.be)
13:58:28	×	rainbyte quits (~rainbyte@186.22.19.214) (Read error: Connection reset by peer)
13:59:01	→	rainbyte joins (~rainbyte@186.22.19.214)
13:59:23	→	housemate joins (~housemate@203.56.146.214)
14:02:32	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
14:02:46	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
14:03:20	→	jreicher joins (~joelr@user/jreicher)
14:08:03	→	annamalai joins (~annamalai@117.231.195.83)
14:09:50	→	durstloescher joins (~textual@2001:638:708:308:c907:7e9e:4d1e:bc5d)
14:09:56	×	durstloescher quits (~textual@2001:638:708:308:c907:7e9e:4d1e:bc5d) (Client Quit)
14:10:52	×	Jackneill_ quits (~Jackneill@94-21-195-8.pool.digikabel.hu) (Quit: Leaving)
14:11:05	→	Jackneill joins (~Jackneill@94-21-195-8.pool.digikabel.hu)
14:20:46	→	karenw joins (~karenw@user/karenw)
14:26:35	×	ystael quits (~ystael@user/ystael) (Ping timeout: 265 seconds)
14:28:02	→	ystael joins (~ystael@user/ystael)
14:34:18	×	humasect_ quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
14:35:25	×	Inline quits (~User@cgn-195-14-218-118.nc.de) (Ping timeout: 264 seconds)
14:39:31	×	ttybitnik quits (~ttybitnik@user/wolper) (Quit: Fading out...)
14:42:55	×	doyougnu- quits (~doyougnu@38.175.72.111) (Ping timeout: 240 seconds)
14:46:05	×	weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
14:46:32	→	L29Ah joins (~L29Ah@wikipedia/L29Ah)
14:46:38	→	doyougnu joins (~doyougnu@38.175.72.111)
14:46:38	×	trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
14:49:19	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
14:52:22	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
14:52:38	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
14:53:04	→	fp joins (~Thunderbi@130.233.70.149)
14:54:29	×	CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds)
14:56:11	→	Jackneill_ joins (~Jackneill@178-164-234-102.pool.digikabel.hu)
14:58:29	×	Jackneill_ quits (~Jackneill@178-164-234-102.pool.digikabel.hu) (Remote host closed the connection)
14:59:07	×	Jackneill quits (~Jackneill@94-21-195-8.pool.digikabel.hu) (Ping timeout: 264 seconds)
15:00:14	→	Jackneill joins (~Jackneill@178-164-234-102.pool.digikabel.hu)
15:07:19	trickard_	is now known as trickard
15:08:08	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 256 seconds)
15:12:25	×	karenw quits (~karenw@user/karenw) (Ping timeout: 246 seconds)
15:13:16	<thenightmail>	why is there no associativity for equality, inequality and comparison operators
15:15:38	→	merijn joins (~merijn@77.242.116.146)
15:16:56	×	newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Quit: Client closed)
15:17:58	<chromoblob>	how would inequality associativity be useful
15:19:21	<chromoblob>	to actually answer: x == y == z is banned because it cannot have the meaning it seems to have
15:19:32	→	qqq joins (~qqq@185.54.21.105)
15:20:10	<chromoblob>	because the result of one comparing is a Bool, thus you would next compare this Bool to another operand
15:20:24	→	Sgeo joins (~Sgeo@user/sgeo)
15:21:22	<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
15:21:34	<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'
15:22:08	×	pavonia quits (~user@user/siracusa) (Quit: Bye!)
15:26:33	<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
15:28:54	×	fp quits (~Thunderbi@130.233.70.149) (Ping timeout: 260 seconds)
15:32:06	×	trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
15:32:06	→	durstloescher joins (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38)
15:32:19	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
15:32:46	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds)
15:34:17	→	merijn joins (~merijn@77.242.116.146)
15:34:37	×	durstloescher quits (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) (Client Quit)
15:35:19	×	EvanR quits (~EvanR@user/evanr) (Ping timeout: 260 seconds)
15:38:32	→	durstloescher joins (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38)
15:42:50	×	durstloescher quits (~textual@2001:638:708:308:b8a0:21c4:c5e4:aa38) (Ping timeout: 245 seconds)
15:46:30	×	Catty quits (~catties@user/meow/catties) (Remote host closed the connection)
15:50:08	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
15:50:23	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
15:52:37	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Client Quit)
15:52:54	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
15:53:38	→	catties joins (~catties@user/meow/catties)
15:54:02	×	itaipu quits (~itaipu@168.121.99.54) (Ping timeout: 256 seconds)
15:54:05	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
15:56:17	→	itaipu joins (~itaipu@168.121.99.54)
16:00:55	×	itaipu quits (~itaipu@168.121.99.54) (Ping timeout: 240 seconds)
16:01:39	×	bggd quits (~bgg@user/bggd) (Remote host closed the connection)
16:03:32	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
16:03:46	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
16:03:56	→	Inline joins (~User@cgn-195-14-218-118.nc.de)
16:05:13	<tomsmeding>	chromoblob: "authors of language" -- authors of _this_ language. The authors of Python did think this was a good idea
16:07:15	→	merijn joins (~merijn@77.242.116.146)
16:12:37	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 264 seconds)
16:14:11	→	merijn joins (~merijn@77.242.116.146)
16:20:51	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
16:23:15	×	chele quits (~chele@user/chele) (Remote host closed the connection)
16:25:08	→	tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
16:25:50	×	rainbyte quits (~rainbyte@186.22.19.214) (Read error: Connection reset by peer)
16:29:11	→	rainbyte joins (~rainbyte@186.22.19.214)
16:29:33	→	Lycurgus joins (~juan@user/Lycurgus)
16:29:40	→	danza joins (~danza@user/danza)
16:30:36	×	danz65539 quits (~danza@user/danza) (Read error: Connection reset by peer)
16:34:18	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...)
16:41:53	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
16:42:06	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
16:42:17	→	ft joins (~ft@p4fc2a9d7.dip0.t-ipconnect.de)
16:51:01	×	merijn quits (~merijn@77.242.116.146) (Ping timeout: 264 seconds)
16:52:13	×	euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
16:55:35	×	doyougnu quits (~doyougnu@38.175.72.111) (Ping timeout: 240 seconds)
16:59:00	→	doyougnu joins (~doyougnu@38.175.72.111)
17:00:07	<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?
17:00:56	<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. :) )
17:01:16	<tomsmeding>	(because == on Bools is <=>)
17:02:20	<monochrom>	It is surprising but handy that both == and /= (xor) are commutative associative and with identities.
17:07:17	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
17:07:44	<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? >:) )
17:08:29	<monochrom>	(Hint: They are pros in math content, but not math syntax.)
17:08:36	<monochrom>	(or any syntax)
17:08:37	<danza>	:t (<=>)
17:08:38	<lambdabot>	error: [GHC-88464]
17:08:38	<lambdabot>	Variable not in scope: <=>
17:08:38	<lambdabot>	Suggested fix:
17:08:49	<monochrom>	Oh, <=> is iff.
17:12:14	→	euphores joins (~SASL_euph@user/euphores)
17:12:52	<danza>	cheers monochrom
17:14:16	×	danza quits (~danza@user/danza) (Remote host closed the connection)
17:22:05	×	Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org ))
17:23:37	→	koz joins (~koz@121.99.240.58)
17:24:20	×	larsivi quits (~larsivi@user/larsivi) (Quit: WeeChat 4.8.1)
17:34:09	→	fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi)
17:43:25	×	kuribas quits (~user@2a02-1810-2825-6000-b6e0-77f4-472f-1183.ip6.access.telenet.be) (Remote host closed the connection)
17:47:10	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...)
17:48:06	→	EvanR joins (~EvanR@user/evanr)
17:57:54	<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.
17:58:05	<dolio>	Not about whether how they're inserted matters.
18:00:24	<dolio>	Even though (==) is associative as an operation on Bool, Haskell will refuse to accept `x == y == z`.
18:01:24	→	ljdarj joins (~Thunderbi@user/ljdarj)
18:04:15	<geekosaur>	that seems pretty obvious to me, since as defined either associativity makes the "other" one a comparison on `Bool`
18:08:01	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:13:16	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
18:20:52	×	elarks quits (~elarks@user/yerrii) (Quit: WeeChat 4.7.1)
18:23:48	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:24:12	×	ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj)
18:25:48	→	ljdarj joins (~Thunderbi@user/ljdarj)
18:30:23	→	Hardyhardhard joins (~Hardyhard@user/hardyhardhard)
18:30:31	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
18:36:28	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
18:36:41	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
18:39:50	→	Everything joins (~Everythin@172-232-54-192.ip.linodeusercontent.com)
18:41:50	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:46:49	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
18:48:21	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
18:53:25	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
19:04:14	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
19:09:19	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
19:11:52	→	Tuplanolla joins (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi)
19:12:25	<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)
19:13:02	<dolio>	Yeah.
19:16:19	<dolio>	The problem is that in situations with other types, the way parentheses are inserted affects whether it's well typed.
19:16:55	<dolio>	And that's kind of a dumb thing to depend on.
19:17:32	<__monty__>	tomsmeding: I'm not so sure, `False == False == True` doesn't seem very useful.
19:17:36	<dolio>	Also the binary operator on booleans is pretty niche.
19:18:44	<__monty__>	Are there any languages where a successful equality check "returns" the value, while an unsuccessful check returns False or something?
19:19:07	<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
19:19:53	<ncf>	(also, logical equivalence is not actually associative constructively, is it?)
19:20:12	<dolio>	This isn't a relation. It's a decision procedure for a relation.
19:20:23	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
19:20:42	<dolio>	The induced operator on booleans calculates parity.
19:22:37	×	Hardyhardhard quits (~Hardyhard@user/hardyhardhard) (Quit: Client closed)
19:23:26	<tomsmeding>	__monty__: sure :p
19:24:05	×	jle` quits (~jle`@2603:8001:3b00:11::1156) (Ping timeout: 245 seconds)
19:24:57	→	Hardyhardhard joins (~Hardyhard@user/hardyhardhard)
19:25:20	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
19:25:33	<dolio>	Or wait, (/=) is parity. (==) is like anti-parity or something.
19:26:12	<dolio>	Parity for the 0 bits instead of 1 bits.
19:26:52	×	jreicher quits (~joelr@user/jreicher) (Quit: In transit)
19:29:33	<__monty__>	Maybe the right type for (==) should be `Eq a => Maybe a -> Maybe a -> Maybe a`? Then we can get associativity.
19:32:11	<monochrom>	A relation is a function. A function is an operator. So a relation is also an operator. >:)
19:33:03	<monochrom>	We have a real type system, so we don't need artificial lines between relations, functions, numbers, values, constants.
19:38:01	→	Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
19:39:00	×	Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
19:39:20	Lord_of_Life_	is now known as Lord_of_Life
19:44:16	×	Hardyhardhard quits (~Hardyhard@user/hardyhardhard) (Quit: Client closed)
19:48:11	<ncf>	have you heard of concepts with attitudes
19:48:28	<ncf>	the intended meaning of a R b R c when R is a relation is a R b ∧ b R c
19:49:08	<ncf>	the intended meaning of a O b O c when O is a (homogeneous, binary, associative) operator is a O (b O c)
19:49:15	<ncf>	those are extremely different!
19:49:21	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
19:50:21	×	bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
19:50:21	<dolio>	ncf: Definitely seems like the associativity is not constructive.
19:50:27	<ncf>	yeah i don't think it is
19:50:38	<ncf>	can you prove a taboo from it?
19:54:18	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
19:59:04	→	ttybitnik joins (~ttybitnik@user/wolper)
20:01:41	<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.
20:04:00	<ncf>	you say continuing operator i say relation
20:04:32	<[exa]>	(binary relations are overrated)
20:05:12	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:06:32	×	ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
20:06:46	<[exa]>	anyway I saw this somewhere with matlabby dots, like (a <. b .< c), it even extended to (a <. b .<. c .< d)
20:06:48	<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.
20:08:27	<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)
20:10:19	<dolio>	Haskell should just extend its rules so that lexing depends not only on parsing, but type checking.
20:10:20	<[exa]>	btw Julia had a special case for that too: Meta.show_sexpr(:(a <= b < c)) == (:comparison, :a, :<=, :b, :<, :c)
20:10:31	<[exa]>	dolio: <3
20:11:40	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
20:11:47	<monochrom>	Speaking of which, how is RecordDot done?
20:12:13	→	ChaiTRex joins (~ChaiTRex@user/chaitrex)
20:13:16	<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
20:13:24	<dolio>	ncf: https://paste.tomsmeding.com/a6qxdKdh
20:13:29	<ncf>	which is a conversation i remember having but don't remember the conclusion
20:13:38	<ncf>	aha
20:14:07	<ncf>	oh right, if you take A = ⊥ you get ¬¬B ↔ B
20:14:14	<ncf>	cool
20:18:18	<monochrom>	Oh nice, one more way to restore classical logic. :)
20:21:17	<davean>	dolio: and end up like C++? Lol
20:21:20	<monochrom>	(I had known of: choose one: EM, double-negation elim, Pierce.)
20:23:15	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:25:54	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
20:26:08	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
20:28:09	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
20:29:41	→	peterbecich joins (~Thunderbi@71.84.33.135)
20:30:37	→	target_i joins (~target_i@user/target-i/x-6023099)
20:30:56	×	collide2954 quits (~collide29@user/collide2954) (Quit: The Lounge - https://thelounge.chat)
20:31:43	→	collide2954 joins (~collide29@user/collide2954)
20:36:01	<dolio>	davean: Does C++ do that, too? I thought that was perl's distinction.
20:36:21	<dolio>	I guess perl has to actually evaluate code.
20:37:42	<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
20:38:47	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:40:35	×	divlamir quits (~divlamir@user/divlamir) (Ping timeout: 240 seconds)
20:41:03	→	humasect joins (~humasect@dyn-192-249-132-90.nexicom.net)
20:42:11	<dolio>	Anyhow, as I said, Haskell can take it to the next level by making lexing undecidable.
20:42:23	<dolio>	That's innovation.
20:42:25	<humasect>	yeah
20:42:52	→	divlamir joins (~divlamir@user/divlamir)
20:42:59	<monochrom>	TypeDirectedLexicalResolution? >:)
20:43:35	→	jreicher joins (~joelr@user/jreicher)
20:43:37	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
20:43:37	→	Enrico63 joins (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213)
20:46:01	<[exa]>	-XLexicalKinds
20:46:48	×	Enrico63 quits (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Client Quit)
20:49:50	×	peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 256 seconds)
20:50:21	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
20:51:08	<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.
20:52:58	<c_wraith>	> LT `compare` GT
20:52:59	<lambdabot>	LT
20:53:03	<c_wraith>	it's closed!
20:53:04	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
20:54:35	<jreicher>	monochrom: a function is a relation, but the converse is not true
20:55:31	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
20:55:46	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
21:01:25	<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!
21:01:55	<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.
21:02:54	<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.
21:03:35	<EvanR>	math entities are a pure construction of the mind
21:03:49	<EvanR>	:D
21:04:33	<EvanR>	how concepts interrelate is more interesting than "what they are really"
21:04:49	<EvanR>	sometimes taking the place of
21:06:56	<dolio>	jreicher: But does every relation contain a function?
21:07:38	<EvanR>	you can get a relation for any function also lets you avoid subtyping
21:08:39	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:09:22	<dolio>	jreicher: Also, relations are functions in that they are maps into a collection of truth values.
21:09:49	<dolio>	Not that every relation from A to B is a function from A to B.
21:12:07	<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.
21:12:55	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
21:13:19	→	Lears joins (~Leary@user/Leary/x-0910699)
21:13:26	<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.
21:13:40	<dolio>	It means there's a sub-relation that is a function.
21:14:14	<jreicher>	dolio: And what do you mean by sub-relation? Does it also mean restricting the domain to a subset?
21:14:35	×	Leary quits (~Leary@user/Leary/x-0910699) (Ping timeout: 240 seconds)
21:15:09	<dolio>	No, R is a sub-relation of S if R(x,y) implies S(x,y) forall x and y.
21:15:28	Lears	is now known as Leary
21:16:18	<dolio>	I guess, you should be able to restrict the domain, too.
21:16:32	<dolio>	Otherwise you could only hope to get a partial function in general.
21:17:26	<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
21:19:37	<monochrom>	jreicher: I am clearly siding with type theory rather than traditional mathematics.
21:22:20	<monochrom>	dolio: To obtain a functional subrelation from a relation with an infinite co-domain, we quickly run into the axiom of choice... :)
21:22:32	<jreicher>	monochrom: what do you mean?
21:22:33	<dolio>	:)
21:23:13	<dolio>	Yeah, that assertion is equivalent to the axiom of choice.
21:23:14	<monochrom>	In type theory, predicates are special cases of functions.
21:23:50	<dolio>	'For every x with multiple related ys, pick one of the ys.'
21:23:57	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:24:11	<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.
21:24:51	×	humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...)
21:24:53	<EvanR>	type theory is logic
21:24:55	<dolio>	Type theory has no need of logic. It has subsumed it.
21:25:06	×	Everything quits (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving)
21:25:28	<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).
21:25:37	<jreicher>	Language and metalanguage.
21:25:54	<EvanR>	if you're proving things about the logic itself
21:26:08	<EvanR>	instead of using it for actual purposes xD
21:26:10	<monochrom>	Traditional mathematics also needs a language and a metalanguage.
21:26:16	→	pavonia joins (~user@user/siracusa)
21:26:31	<jreicher>	Exactly. And to me the original question was about the metalinguistic objects, and not the linguistic ones.
21:26:42	<monochrom>	In fact how about I use HoTT as the metalanguage for defining the language and semantics of set theory?
21:27:11	<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
21:27:40	<jreicher>	When we say a comparison "operator" is a predicate, the operator is linguistic, but the predication is metalinguistic.
21:27:44	<monochrom>	That too. Just look at GHC being written in GHC.
21:28:40	<EvanR>	operator one of the most overloaded terms, in the process also overloading the term operator overloading
21:29:17	<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.
21:29:25	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
21:29:58	<EvanR>	you might have spontaneously created a new platonic semantics for haskell beyond the ones we already had
21:30:09	<jreicher>	Except I'm not a platonist. :p
21:30:26	<monochrom>	HoTT, CoC, Agda, Lean, Haskell all have T and F in the language domain.
21:30:29	<EvanR>	ok then we can reel it back in and have T an F just be haskell T and F
21:31:01	<monochrom>	In Agda, Lean, and Haskell, T and F are even user-definable.
21:31:20	<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
21:31:35	<monochrom>	(Generally in any CoC + user-definable inductive types.)
21:31:58	<monochrom>	Oh, the original language was Haskell.
21:32:07	<davean>	dolio: C++ is undecidable
21:32:18	<monochrom>	Why do we even care about traditional set theory in #haskell? :)
21:32:42	<dolio>	davean: lexing?
21:32:58	<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)
21:33:11	<davean>	dolio: I forget exactly which level of lex vs. parse is undecidable
21:33:18	<EvanR>	this is a bit too dogmatic
21:33:30	<jreicher>	That's why I used the word "unhygienic".
21:33:39	<jreicher>	And also "personally"
21:33:48	<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
21:33:54	→	peterbecich joins (~Thunderbi@71.84.33.135)
21:34:21	<jreicher>	Not sure we want uncountable datatypes in Haskell
21:34:32	<EvanR>	are you sure we don't already?
21:35:01	<dolio>	I'd be a little surprised if the lexing were undecidable, but I'm not much of a C++ guru.
21:35:02	<jreicher>	I can't see how it's possible. You only get countable infinities with recursion.
21:35:03	<EvanR>	datatypes which could not possibly be enumerated (in haskell)
21:35:17	<EvanR>	i.e. make a full list of them
21:35:27	<EvanR>	of the values
21:35:48	<dolio>	Maybe not super surprised.
21:39:45	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:40:00	<davean>	dolio: I just don't recally how they define their boundary
21:41:35	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
21:41:52	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
21:43:44	<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.
21:44:15	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
21:46:06	<jreicher>	monochrom: got a reference? That doesn't sound sensible to me
21:46:37	<monochrom>	I don't have a reference.
21:46:53	<EvanR>	if you disagree that haskell has uncountable datatypes, it's possible normal set theory also doesn't xD
21:47:03	<monochrom>	Not even when that someone is me. I don't bother to write a paper for that.
21:47:06	<jreicher>	I don't disagree. I just can't see how it's possible.
21:47:45	<jreicher>	Uncountability, in a way, "comes from nowhere". It has to be asserted. You can't constructit.
21:47:48	<EvanR>	here is one... data Bitstream = I Bitstream \| O Bitstream
21:47:58	<EvanR>	jreicher, why do you think this xD
21:48:09	<monochrom>	Oh it is asserted. Denotational semantics are seldom constructive.
21:48:10	<jreicher>	EvanR: how is that uncountable?
21:48:27	<EvanR>	you define things and then see if this or that satisfies the definition
21:48:32	<EvanR>	nothing wrong with definitions
21:49:00	<EvanR>	jreicher, there was this guy cantor with this diagonalization argument
21:49:09	<geekosaur>	^
21:49:24	<EvanR>	it made a lot of people very angry and was generally considered a bad idea
21:49:28	<geekosaur>	that was my thought, it either proves countability or provides a recipe to construct uncountably many values
21:49:46	<jreicher>	Yes, but that datatype is not all the reals
21:49:53	<EvanR>	reals?
21:49:55	<jreicher>	You can't make the diagonalisation from it
21:50:06	<EvanR>	that's .. neither here nor there
21:50:22	<jreicher>	Any bitstream value is INDEFINITE length, but it's still FINITE.
21:50:31	<EvanR>	wat
21:50:44	<jreicher>	You can't have an infinite bitstream value
21:50:56	<EvanR>	we're about to jump the shark from uncountability to ultrafinitism
21:51:21	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
21:51:37	<EvanR>	ignoring bottoms there's no way to make a finite Bitstream
21:51:39	<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?
21:52:36	<jreicher>	I'm just after anything that will prove (without question-begging assertions) that BitStream is uncountable. It looks entirely countable to me.
21:52:47	<EvanR>	what makes you say that
21:53:29	<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.
21:53:41	<EvanR>	I don't follow...
21:53:53	<EvanR>	all things constructed are finite?
21:54:02	<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
21:54:40	<dolio>	The type of lazy streams is uncountable.
21:54:55	<jreicher>	dolio: reference? I don't see how that would be the case
21:55:45	<EvanR>	one way to look at countable A is you can make a [A] which contains at some point all possible A values
21:55:57	<EvanR>	possibly infinite
21:56:02	<dolio>	https://hub.darcs.net/dolio/unpossible/browse/src/Cantor/Properties.agda#66
21:56:13	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
21:56:22	<jreicher>	EvanR: Take (as a silly example) data SillyType = I SillyType. Countable or uncountable?
21:56:23	<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...
21:56:46	<jreicher>	monochrom: there aren't any infinite bit strings in the set
21:56:47	<monochrom>	SillyType is countable.
21:56:54	<EvanR>	jreicher, is the only (respectable) value here I (I (I (I ...)))?
21:56:59	<EvanR>	so cardinalty 1
21:57:12	<jreicher>	monochrom: Exactly. So making it a "binary choice" recursion doesn't magically make it uncountable
21:57:57	<monochrom>	You need infinite strings for completeness.
21:58:18	<EvanR>	there's no finite strings by design, so I'm confused by that
21:58:52	<monochrom>	The increasing sequence I bottom, I (I bottom), I (I (I bottom)) ... needs a least upper bound.
21:58:55	×	peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds)
21:59:40	<jreicher>	monochrom: My only point is that none of these recursive datatypes give you infinite strings.
21:59:48	<jreicher>	You have an infinite series of finite strings
21:59:58	<EvanR>	I guess including all these partially defined possibilities is making it even more infinite
22:00:10	EvanR	looks at jreicher
22:00:25	<int-e>	. o O ( it must be nice to have convictions )
22:00:53	<dolio>	> cycle [0,1]
22:00:54	<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...
22:01:01	<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.
22:01:08	<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
22:01:52	<monochrom>	I can respect that you reject denotational semantics altogether, but then you should also be rejecting "bottom".
22:02:17	<jreicher>	I'm not rejecting denotational semantics. I'd just like a pointer to something that explains where/how/why anything uncountable comes in.
22:02:25	<int-e>	But how can you discuss countability in a finitist context? :P
22:02:30	<monochrom>	OK sure. Read my lecture notes first?
22:02:39	<jreicher>	I'm not finitist. I just said infinite series of finite objects.
22:02:48	<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
22:02:58	<EvanR>	jreicher, good xD
22:03:22	<int-e>	(I can defend the idea that streams are countable but it'll involve computability and/or Scott domains)
22:03:29	<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.
22:03:46	<EvanR>	or definability, because you have to write the code, and code is countable
22:03:54	×	Inline quits (~User@cgn-195-14-218-118.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/)
22:04:20	<EvanR>	(but I might be wrong here beacuse of higher order programs)
22:04:26	<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.
22:04:52	<jreicher>	I have to think this through carefully, but I think you are all accepting the existence of infinitely-running programs?
22:05:09	<EvanR>	sounds like operational semantics
22:05:11	<dolio>	Internally to the world of recursive mathematics, Cantor's diagonal argument holds, and the type of infinite bit streams is uncountable.
22:05:23	<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)
22:05:51	<dolio>	Viewed externally as built in classical mathematics, that is the statement, 'the set of recursive bit streams is "computably uncountable."'
22:06:03	<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
22:06:21	<dolio>	I.E. given a computable enumeration of computable bit streams, one can compute a bit stream not in the enumeration.
22:06:25	<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.
22:07:00	<EvanR>	you're trying to say like > repeat 'a' is not an infinite list
22:07:04	<EvanR>	in haskell xD
22:07:09	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:07:25	<int-e>	it's a very finite graph :P
22:07:32	<int-e>	(once fully evaluated)
22:07:39	<EvanR>	in ghc!
22:07:46	<EvanR>	if you're lucky
22:07:56	<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)
22:08:05	<EvanR>	that's the point
22:08:11	<int-e>	EvanR: Well, in isolation, assuming it isn't fused away :P
22:08:33	<EvanR>	you can't generate a stream of all the lists
22:08:34	<monochrom>	I thought I explained that. A model that contains impractical elements can be a useful approximation and/or abstraction.
22:08:47	<EvanR>	some are necessarily missing
22:08:55	<EvanR>	no matter how you go about it
22:09:01	<dolio>	Uncomputable lists aren't real.
22:09:20	<EvanR>	and cantor's proof produces a constructive example list which isn't there
22:09:21	<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)
22:09:21	<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.
22:09:22	<EvanR>	kind of cool
22:09:52	<EvanR>	jreicher, this is like saying any map from N into A necessarily misses some As
22:10:05	<EvanR>	which is what we're trying to say
22:10:05	<jreicher>	Not "some". Most.
22:10:09	<EvanR>	sure
22:10:18	<EvanR>	that's what uncountable is
22:10:42	→	Zemy joins (~Zemy@72.178.108.235)
22:10:58	<dolio>	Every computable map misses many computable streams.
22:11:04	<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?
22:11:21	<EvanR>	sure
22:11:26	<monochrom>	Yes. For example operational semantics.
22:11:44	<jreicher>	OK. So what do we gain from adding the assertion (because we'd need to) that makes it uncountable?
22:11:47	<monochrom>	Another example: Translating Haskell to Turing machines.
22:12:00	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
22:12:03	<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
22:12:03	<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).
22:12:14	<int-e>	It's a simplification.
22:12:18	<EvanR>	jreicher, it's not an assertion, there's a constructive proof xD
22:12:22	<monochrom>	Avoiding the cumbersomeness and missing-the-forest-for-the-trees of operational semantics and Turing machines.
22:12:27	<EvanR>	yielding the missing stream
22:12:57	<jreicher>	EvanR: the proof (like all proofs) starts with axioms. The axioms are the assertions.
22:13:00	<EvanR>	that you can't run a program for infinite time isn't the secret sauce to model it as countable
22:13:04	<EvanR>	that's more like ultrafinitism
22:13:13	<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.
22:13:20	<EvanR>	jreicher, in type theory, we don't always have axioms!
22:13:33	<jreicher>	How can you have a theory without axioms?
22:13:37	<EvanR>	definitions
22:13:40	<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.
22:13:46	<jreicher>	Definitions are axioms
22:13:55	<int-e>	Again, keeping things as mathematically simple as possible.
22:13:57	<EvanR>	well that's muddying things a lot isn't it
22:14:10	<jreicher>	Not for a formal theory, no
22:14:16	<EvanR>	definition is just naming something that you could already say long winded
22:14:22	<EvanR>	to save space
22:14:51	<monochrom>	The hardest example made easy being fs = 1 : 1 : zipWith (+) fs (tail fs).
22:14:53	<jreicher>	int-e: monochrom: I appreciate the use of "extra" infinity as a simplification. Not the first time I've heard that argument.
22:15:12	<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
22:15:21	<EvanR>	introduced*
22:15:24	<monochrom>	Every textbook or tutorial I saw tried to explain it poorly with lazy evaluation.
22:15:24	<jreicher>	"fiar" is "assertion"
22:15:25	×	chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 256 seconds)
22:15:27	<jreicher>	*fiat
22:16:07	<monochrom>	But if you do the denotational "construct the approximation sequence, take limit" it's plain as day.
22:18:26	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
22:20:16	<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).
22:20:31	<dolio>	Cantor's diagonal argument is constructive, ergo bit streams are uncountable.
22:20:41	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
22:20:50	<monochrom>	(About theory with/wo axioms. I don't draw lines between axioms, definitions, inference rules either.)
22:20:54	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
22:20:55	<int-e>	dolio: see me 15 minutes ago ;-)
22:20:56	<dolio>	The only way they look countable is if you believe in classical mathematics and try to build computability within that.
22:21:22	<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
22:21:32	<EvanR>	s/finite/countable/
22:21:56	<dolio>	But in the natural mathematics of computable things, they are uncountable. The ways to count them are not computable.
22:22:17	<dolio>	So reject them.
22:22:56	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:23:26	<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. :)
22:23:54	<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"
22:23:56	<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.
22:24:34	<EvanR>	basically syntactic sugar
22:24:39	<monochrom>	Because classical uncountability gives me a feeling of size, but constructive uncountability doesn't feel like "bigger size", just "unreachable".
22:25:03	<EvanR>	again, isn't this saying more about misunderstanding classical notions ? xD
22:25:03	<dolio>	Yes, the idea that uncountability is about "size" is an erroneous extrapolation from finite sets.
22:25:34	<dolio>	The extended natural numbers are uncountable.
22:25:36	<monochrom>	EvanR, I clone every definition to be an axiom, e.g., definition "x := 4" is cloned so I add an axiom "x = 4".
22:25:42	<dolio>	How many more are there? At most one.
22:25:43	×	takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 240 seconds)
22:25:56	<EvanR>	monochrom, what do you achieve by doing this xD
22:26:02	<EvanR>	twice as many definitions / axioms? xD
22:26:15	<monochrom>	I achieve "they are all axioms".
22:26:17	<dolio>	But infinity + 1 = infinity, right?
22:26:58	<EvanR>	monochrom, it's a slippery slope from there to buffyspeak anything can be anythinged!
22:27:17	<dolio>	(That uncountability part requires more committment to computable principles.)
22:27:31	<monochrom>	Oh sure, I then further consider axioms to be special cases of theorems!
22:28:02	<EvanR>	🤢
22:28:13	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
22:28:24	<int-e>	has anybody said "global assumptions"
22:28:41	<EvanR>	theorems ideally come with proofs, while you wouldn't expect a proof
22:28:45	<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?
22:28:51	<EvanR>	if we don't want anything to mean anything, we can do that I guess xD
22:29:01	<EvanR>	wouldn't expect proof of an axiom*
22:29:23	<EvanR>	and "proving a definition" is itself like a classic fallacy xD
22:30:23	<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...
22:30:32	<monochrom>	WHY SHOULD I CARE. They're all nodes.
22:30:35	<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
22:30:56	<EvanR>	monochrom, really, all these things fit inside a neat tree of life somehow?
22:30:58	<int-e>	EvanR: thereby proving all definitions at once ;-)
22:30:58	<monochrom>	For the simple purpose of traversing or generating that tree, they are all nodes, period.
22:31:03	<EvanR>	I was trying to get away from that with jreicher
22:31:25	<int-e>	@quote
22:31:25	<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.
22:31:26	<monochrom>	Now consider that this tree happens to be my proof tree. So node = theorem. Period.
22:31:27	<EvanR>	no reason everything needs to fit into the same tree
22:31:44	<monochrom>	Oh the root node is also called "axiom". Sure. Whatever.
22:31:59	<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)
22:32:03	<monochrom>	Sure. s/tree/forest/ ?
22:32:48	<monochrom>	Wait, you can run GHC on a 286?!
22:32:49	<EvanR>	everything is in the same forest... as a tree of 1 node... back to the penchant for containerization
22:33:18	<EvanR>	in lambda MOO luckily nodes aren't all required to be in one tree, or even in any tree
22:33:35	<int-e>	monochrom: emulators are a thing you know ;-)
22:33:58	<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`.
22:34:05	<monochrom>	Wait, does that you use a 286 to emulate a 386 then run GHC there?
22:34:15	<monochrom>	s/does that you/does that mean/
22:34:19	<jreicher>	OK. But what about the set he's diagonlising?
22:34:36	<int-e>	monochrom: I don't know. I'm filling in my own details here :P
22:34:42	<monochrom>	Heh
22:35:12	<EvanR>	"wavfunction collapse procedural generation" of anecdotes xD
22:35:22	<dolio>	jreicher: I don't understand the question.
22:35:24	<monochrom>	Because AFAIK GHC assumes a flat/linear 32-bit addressing model i.e. at least 386.
22:35:43	<jreicher>	dolio: I think you're presupposing that the set of reals is "constructive". No?
22:35:44	<int-e>	I don't know that there never was a 16 bit version of GHC.
22:35:56	<EvanR>	who ordered reals
22:36:03	<int-e>	(It does seem rather unlikely though.)
22:36:12	<monochrom>	OK OK April's Fool project: Drastically overhaul GHC to be runnable on 286's segment model!
22:36:18	<dolio>	Reals are too complicated to get into. This is just the bit streams.
22:36:32	<jreicher>	If you have infinite bitstreams, you have all the reals
22:36:33	<int-e>	monochrom: protected mode or real mode?
22:36:36	<monochrom>	(Oh then it probably also runs on 8088 DOS too...)
22:36:40	<jreicher>	Sorry, I should say ALL the infinite bitstreams
22:36:42	×	target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
22:36:44	<dolio>	Reals are a quotient.
22:36:57	<jreicher>	Huh?
22:37:08	<int-e>	dolio: Don't you like Dedekind cuts?
22:37:10	<EvanR>	we're getting off topic trying to jam classical reals into the discussion
22:37:16	<EvanR>	which isn't about them
22:37:28	<int-e>	(so now we're getting off topic, huh)
22:37:30	int-e	runs
22:37:31	<dolio>	jreicher: Like 0.11111... = 1.0 (binary).
22:37:33	<EvanR>	lol
22:37:56	<jreicher>	EvanR: how can you have Cantor's diagonalisation without the reals?
22:38:01	<jreicher>	(Maybe I've misunderstood the idea)
22:38:04	<EvanR>	yes that is what this whole discussion is about
22:38:06	<dolio>	It's actually possible for the (Dedekind) reals to be countable in constructive mathematics.
22:38:10	<EvanR>	was cantor even talking about real numbers
22:38:18	<dolio>	Even though the bit streams are uncountable.
22:38:21	<jreicher>	To begin with I'm pretty sure he was
22:38:22	<monochrom>	I think GCC for DOS could do 32-bit in real mode. I forgot. But just do whatever GCC-for-DOS does.
22:38:42	<jreicher>	dolio: Ok, I'll stick to bistreams. In what way is a non-computable (infinite) bitstream "constructive"?
22:38:44	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:38:52	<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
22:39:04	<dolio>	They aren't. We only need the computable ones.
22:40:15	<jreicher>	And if you only have the computable ones, the set is countable.
22:40:24	<dolio>	No, it isn't.
22:40:45	<EvanR>	at some point doing the proof might help since this is ... mathematical
22:40:55	<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
22:41:00	<dolio>	Cantor's diagonal argument shows every computable enumeration of the computable bit streams misses a computable bit stream.
22:41:05	<EvanR>	a proof is worth 1000 words
22:41:34	<EvanR>	jreicher, I went over that in a few ways above
22:42:03	tomsmeding	. o O ( every _computable_ enumeration -- that bit is relevant here )
22:42:08	<dolio>	Yeah.
22:42:28	<dolio>	If you want to say there's a non-computable enumeration, you have again exited constructive mathematics.
22:42:34	<tomsmeding>	this is not classical set-theoretical "countable", this is "computably countable"
22:42:51	<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.
22:42:59	<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)
22:43:15	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
22:43:25	<tomsmeding>	int-e: right -- I haven't really been following the discussion. You know what, I'll leave you at it :)
22:43:50	<int-e>	tomsmeding: Ah sorry, I'm not complaining!
22:43:53	<EvanR>	if I hook up my Bitstream generator to an external entity then it only makes matters worse
22:44:02	<EvanR>	we're not going to get less bitstreams that way
22:44:08	<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?
22:44:27	<int-e>	tomsmeding: It's in the nature of IRC that discussions become circular, for better or worse.
22:44:33	<tomsmeding>	:D
22:45:09	<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.
22:45:22	<dolio>	Because constructive mathematics is valid for computability.
22:45:26	<EvanR>	whatever the proof means, the proof goes through
22:45:30	<EvanR>	it's valid in of itself
22:45:31	<jreicher>	I don't really understand why that serves as a meanginful notion of uncountability
22:45:33	→	jmcantrell_ joins (~weechat@user/jmcantrell)
22:45:49	<EvanR>	jreicher, you're working on the level of vibes it seems... instead of defining stuff, then proof a theorem
22:46:16	<jreicher>	At the moment I'm just trying to understand dolio's definitions
22:46:17	<EvanR>	for whatever reason you don't like the result, even though it jives exactly with classical math xD
22:46:32	<EvanR>	instead yeah lets understand it on its own terms
22:46:37	<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.
22:46:38	<jreicher>	I know what the definitions and theorems are in classical maths. I don't have a problem with any of that.
22:47:16	<jreicher>	dolio: but why is enumeration important here at all? What's the connection with uncountability, for you?
22:47:29	jmcantrell_	is now known as jmcantrell
22:47:29	<jreicher>	Sorry, I mean computable enumeration
22:47:45	<dolio>	Countability is 'there is a surjection from ℕ'.
22:47:50	<EvanR>	Bitstream is uncountable (in haskell) <-
22:48:12	<dolio>	(Or similar)
22:48:26	<int-e>	if you dislike "countability" you can say that recursive functions are not recursively enumerable ;-)
22:48:29	<dolio>	And I don't believe in uncomputable things. So the surjection is computable.
22:48:41	<jreicher>	Oh. I haven't heard that view before.
22:48:43	→	mange joins (~mange@user/mange)
22:48:58	<EvanR>	which definition are you having issues with again
22:49:05	<dolio>	That is the premise, at least. We are in the world where everything is inherently computable.
22:49:18	<jreicher>	So you don't believe something like Chaitin's omega exists?
22:49:29	×	michalz quits (~michalz@185.246.207.205) (Remote host closed the connection)
22:49:33	<EvanR>	you said you weren't a platonist!
22:49:47	<dolio>	It's not a real number, at least.
22:50:01	<jreicher>	EvanR: :D I'm just trying to use the word "exists" the same way everybody else does
22:50:14	<EvanR>	everybody doesn't sound right...
22:50:25	<jreicher>	Normal people then. :p
22:50:30	<monochrom>	Ugh. But everybody uses a different meaning for "exists"!
22:50:49	<c_wraith>	as if I only use a single meaning
22:50:57	<monochrom>	hehe me too
22:51:05	<jreicher>	dolio: I haven't heard the view that Chaitin's omega is not a real number. Interesting. What kind of object is it then?
22:51:28	<monochrom>	But in this context we only need two: classical math, constructive math
22:51:53	<EvanR>	sometimes that's not the discriminator
22:52:08	<EvanR>	because you can often backport the insights you got from constructive math back to classical and realize it was bogus all along
22:52:23	×	tcard_ quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection)
22:52:39	→	tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303)
22:52:46	<dolio>	I'm not that familiar with what it even does, exactly. You can have a halting relation for Turing machines, but that relation will lack properties that would allow constructing a corresponding real number.
22:53:19	<EvanR>	or it intrinsically requires an unrestricted choice principle
22:54:01	×	fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 264 seconds)
22:54:07	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
22:54:09	<EvanR>	instead accidentally
22:55:52	<int-e>	dolio: Basically you define a prefix code {0,1}^* -> Turing machines. And you map the reals [0,1) to Turing machines via binary expansion and matching a prefix. Assign a non-halting TM to anything that doesn't match a prefix. So now you have a subset of R that corrsponds to halting Turing machines, and you can show classically that it's measurable with measure <= 1. Call that measure "halting...
22:55:58	<int-e>	...probability".
22:57:10	<int-e>	(The arrow there is very much informal.)
22:57:33	<dolio>	Okay, so, not every real has a binary expansion.
22:57:49	<dolio>	Or, there is no mapping from reals to binary expansions, I should say.
22:57:54	<int-e>	you have a set of measure 0 of real numbers that have two expansions.
22:57:58	<jreicher>	Well, the point of Chaitin's omega is that the binary expansion is not computable
22:58:00	<dolio>	There's a ∀∃, but not a function, I think.
22:58:12	<jreicher>	(If you accept that the binary expansion exists in the first place)
22:58:24	<geekosaur>	thinking informally, wouldn't a binary expansion have to be countable length?
22:58:30	<int-e>	I said "classically">
22:59:10	<jreicher>	geekosaur: that might take us back to the start of the debate. :) I think the consensus is that denoting semantics for infinitely executing programs "in principle" simplifies things
22:59:47	<jreicher>	Oh, sorry
22:59:56	<jreicher>	I misread what you wrote! You said "countable" and I read "finite"
23:00:48	<geekosaur>	right, I was abbreviating "countably finite", thought that would be fairly obvious from the ongoing context
23:00:53	<geekosaur>	*infinite
23:01:02	<geekosaur>	damn, fingers ahead of brain again
23:01:58	<monochrom>	Me is even finger-disobeys-brain. (How else do you think I mistyped "you" for "mean"?! :) )
23:02:17	<dolio>	Presumably the prefix code is going to be set up so that there's a unique prefix for each binary expansion.
23:02:27	<dolio>	Hopefully each real number.
23:03:12	<dolio>	So even though the expansions are infinitely long, you only need to look at a finite portion.
23:03:13	<EvanR>	jreicher, classic article in the earth days of modern math, "does every real number have a decimal expansion"
23:03:16	<EvanR>	early*
23:03:37	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
23:04:07	<EvanR>	this was before classical math "won" and "asserted" "yes" xD
23:04:27	<EvanR>	no one will drive us out of the paradise cantor created for us
23:04:34	<jreicher>	EvanR: OK.... Not sure what the point is? (And FYI I don't think classical math has won, but that's a debate for another day/channel)
23:04:51	<EvanR>	around 1940s debate of this sort died out
23:05:01	<EvanR>	resurrected way later
23:05:17	<EvanR>	but hopefully now we can just state our systems and assumptions ahead of time and not debate vibes
23:05:41	<EvanR>	jreicher, the point of the paper? well that's in the paper, and relevant to the above story about chaitin's number
23:05:41	<monochrom>	Leibniz would have loved that.
23:06:03	<jreicher>	EvanR: no, not the point of the paper, the point you are wanting to make by providing the paper
23:06:38	<EvanR>	remarks about about the "construction" hinging on obtaining a digital expansion of any real number
23:06:49	<TMA>	mapping digit sequences of countably infinite lenght to real numbers is a classic way to show that {0,1}^* (or {0..9}^*) is not countable set
23:07:22	<EvanR>	we just did that
23:07:24	<EvanR>	xD
23:07:32	<EvanR>	except skipping the reals
23:07:38	<jreicher>	EvanR: you mean the construction of diagonalisation?
23:07:42	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
23:07:57	→	Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
23:08:26	×	AlexNoo quits (~AlexNoo@5.139.232.54) (Read error: Connection reset by peer)
23:08:48	→	AlexNoo joins (~AlexNoo@5.139.232.54)
23:10:17	<jreicher>	(Because you don't need every real number to have a decimal/binary expansion for that construction)
23:11:48	<EvanR>	you don't even need reals for that, since it's demonstrating uncountability of something, in this case just streams of bits
23:12:08	<jreicher>	Yes, which is why I wasn't entirely understanding why you provided that paper
23:12:19	<EvanR>	you brought up chaitin
23:12:26	<EvanR>	that was being discussed
23:12:35	<EvanR>	that's specifically about reals
23:13:49	<EvanR>	if you keep getting confused thinking stream of bits means "oh reals", and reals means "oh, just a binary expansion", then that equivocation is the point of this old paper
23:14:20	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:14:22	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
23:14:36	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
23:14:38	<EvanR>	if you didn't guess already the argument in the paper is answering "no" to its title... like betteridge's law
23:15:08	<dolio>	Yeah, like I said, there's a paper about a topos where the reals are countable. But the diagonal argument holds in every topos.
23:15:12	<jreicher>	I'm not confused about that. Every bitstream can be interpreted as a numeral corresponding to a number. But that says nothing about the converse, especially since nothing stops you from throwing in all kinds of exotic objects to the set you want to call "the reals"
23:15:39	→	Googulator69 joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
23:15:43	×	Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
23:15:43	<dolio>	So you can't assume that real numbers are the same things as expansions.
23:15:49	<jreicher>	I never have
23:17:34	<EvanR>	I don't doubt you can throw exotic objects in
23:17:49	<EvanR>	but it would seem kind of odd that these objects don't "sit" somewhere on the real line xD
23:18:11	<EvanR>	at least approximately
23:18:19	<jreicher>	yes of course. :)
23:19:04	<jreicher>	I'm pretty sure non-standard analysis does this with asserting the existence of infinitisimals
23:19:05	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
23:19:08	<EvanR>	if were doing vibes, this kind of defeats the point of the real line, and the idea of quantity or ordering
23:19:21	<EvanR>	well you know where infinitesimals are
23:19:26	<EvanR>	at least approximately
23:19:29	<jreicher>	I'm really not doing vibes, so I don't know why you keep saying that
23:19:40	<EvanR>	I'm doing vibes there
23:19:43	<int-e>	EvanR: "real number" is a misnomer :P
23:19:48	<EvanR>	lol
23:20:04	<jreicher>	Fictionalists unite
23:20:08	<monochrom>	My beef is that "imaginary number" is a misnomer. But I digress.
23:20:22	<EvanR>	imaginary numbers are real and real numbers are fictional
23:25:35	<jreicher>	I still don't understand why anyone would say SillyType is countable but BitStream is uncountable.
23:25:59	<jreicher>	Surely they're either both countable, or both uncountable, depending on your "definitions"
23:26:11	<monochrom>	I can prove them, but if you're asking for intuition, I think I don't have any.
23:26:25	<jreicher>	No, prove away, please. I'd like to understand.
23:26:51	<jreicher>	Every proof I sketch out results in an inconsistency.
23:27:29	<monochrom>	I map 0 to the infinite stream z = I z, 1 to bottom, 2 to I bottom, 3 to I (I bottom), etc.
23:28:51	<jreicher>	And so SillyType is countable, yes?
23:29:36	<monochrom>	But intuitively I'm not surprised. Expressing natural numbers in unary requires n units of memory for n; "merely" switching to binary, that drops down to lg n.
23:29:37	<int-e>	Sure. It's morally finite ("morally" being the view where you don't have bottoms)
23:29:43	→	k0zy joins (~user@75-164-179-179.ptld.qwest.net)
23:29:51	×	k0zy quits (~user@75-164-179-179.ptld.qwest.net) (Changing host)
23:29:51	→	k0zy joins (~user@user/k0zy)
23:29:56	×	__monty__ quits (~toonn@user/toonn) (Quit: leaving)
23:30:04	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:30:22	<monochrom>	Generally there are multiple instance when switching from 1 to 2, or 2 to 3, or 3 to 4 makes breaking changes.
23:30:35	<jreicher>	monochrom: hang on, are you now saying bitstream is countable? I was hoping that, having proved SillyType is countable, you'd now prove bitstream is uncountable.
23:30:51	<int-e>	jreicher: NO!
23:30:54	<monochrom>	SillyType is countable, BitStream is uncountable.
23:31:10	<int-e>	bitstream adds additional observations for each natural number.
23:31:21	<monochrom>	2-colourability is polynomial-time, 3-colourability is NP-complete.
23:31:29	<int-e>	1^N has cardinality 1; 2^N or 3^N is uncountable.
23:31:40	<jreicher>	monochrom: what's your preferred proof that bitstream is uncountable? I'm looking for what it uses that SillyType isn't entitled to
23:32:08	<monochrom>	BitStream has more than infinite bit strings.
23:32:25	<monochrom>	(so use Cantor diagonlization again)
23:32:49	<jreicher>	monochrom: am I allowed to say SillyType has more the infinite unary strings?
23:32:53	<monochrom>	(You can also attempt diagonalization on SillyType and get stuck.)
23:33:13	<monochrom>	Sure. That's doesn't get you anywhere per se.
23:33:41	<monochrom>	For BitStream I'm using: if a subset is uncountable, then a superset is also uncountable.
23:33:55	<monochrom>	so "more than" is helpful for me.
23:34:23	<EvanR>	there's other fun stuff like subcountable
23:35:03	<EvanR>	and subfinite
23:35:25	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
23:35:31	<int-e>	jreicher: Anyway, at an intuitive level, SillyType has no bits that you could flip to make Cantor's diagonal argument work.
23:35:52	<int-e>	So it's nothing like a bit stream.
23:36:27	<jreicher>	OK, but depending on what we allow for BitStream, can't I be allowed to construct all the aleph numbers from SillyType? That would make it uncountable i think
23:37:03	×	trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
23:37:17	→	trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au)
23:37:24	<int-e>	you're also stepping beyond what's useful for modelling program semantics
23:37:25	<EvanR>	there's like 1 possible value of SillyType
23:37:38	<EvanR>	if this is uncountable then, I'll eat my hat
23:37:54	<jreicher>	int-e: which is why I queried the use of an "infinitely running program" to begin with. It's an interesting dividing line.
23:38:07	<EvanR>	you're not asking about the number of 1s in the stream
23:38:12	<EvanR>	it's about the number of possible streams
23:38:22	<EvanR>	(like 1)
23:38:43	<int-e>	like, sure, you can pretend that there is an element of SillyType for every ordinal number. Or that there's some other unobservable feature that makes the values more plentiful. There's no purpose to it though, since none of this will be observable.
23:39:02	<jreicher>	...just like infinitely running programs are not observable
23:39:08	<EvanR>	are you sure?
23:39:12	<jreicher>	(I'm just arguing devil's advocate now)
23:39:17	<int-e>	No it's not the same.
23:39:34	<Leary>	jreicher: SillyType caps out at omega since you can only "add 1" on the left to get 1 + omega = omega; there's no omega + 1.
23:39:57	<jreicher>	I know. That's kind of what I mean by "fine line". We seem to be saying we've got "observable", "unobservable", and then something like "observable in principle" (conceivable?)
23:40:09	<int-e>	omega arises naturally as the least upper bound of all natural numbers, corresponding to having computations of arbitrary length
23:40:20	<int-e>	nothing beyond omega arises in this fashion
23:40:24	<EvanR>	that's the point of semantics to define what the values (what the programs mean)
23:40:40	<EvanR>	if you're counting values, you're not counting programs, unless that's the semantics you're using
23:40:45	<EvanR>	or counting runtime behaviors
23:40:52	<jreicher>	Leary: but then why wouldn't we say BitStream caps out at computable streams? (I know it's not the same)
23:41:17	<EvanR>	I missed how we're distinguishing any values of SillyType beyond the obvious 1
23:42:46	<int-e>	EvanR: "we" apparently allow bottoms
23:43:44	<TMA>	ackshually, if we take SillyType as constructed then there is one value in it. if we take the definition as an axiom in a theory, there might exists a nonstandard model, in which there are more members of the SillyType
23:44:29	<EvanR>	so like, bottom, 1 bottom, 1 (1 bottom) etc are all consistent
23:44:37	<EvanR>	so maybe they all count as 1
23:44:53	<jreicher>	Would you prefer data SillyType = I \| I SillyType?
23:45:06	<EvanR>	that would allow finite strings
23:45:11	<int-e>	TMA: You're disallowing bottoms so what you said is not true since we can show coinductively that for all a, b in SillyType, a = b.
23:45:28	<int-e>	IOW, there can't be any distinct non-standard element of that type.
23:45:51	<EvanR>	now you have many distinguishable SillyType strings
23:45:52	→	merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl)
23:46:04	<jreicher>	But still countable?
23:46:11	<EvanR>	looks like yes
23:46:30	<int-e>	Yes, that's still countable.
23:46:34	<EvanR>	exercise write the function from Nat to SillyType which witnesses it
23:46:40	→	Inline joins (~User@2001-4dd6-dd24-0-f7db-3cda-3b52-1dd2.ipv6dyn.netcologne.de)
23:46:51	<TMA>	so the sequence of ω⁺Is could also be in SillyType
23:46:51	<int-e>	(It's an infinite type though so adding non-standard elements will generally work.)
23:46:56	<jreicher>	OK. So I'm still curious why we think it's OK to throw in bitstreams that can't be computed, but we can't throw in sillytype strings that can't be computed
23:47:00	<jreicher>	TMA: exactly
23:47:15	<EvanR>	nobody threw in bitstreams that can't be computed that was iterated like 3 times
23:47:28	<EvanR>	(though I tried to once but everyone ignored me)
23:47:30	int-e	loves moving goalposts btw. Not.
23:48:16	<Leary>	jreicher: You can say that if you want to, but as has already been pointed out, you're "crossing the streams" of two settings. You can model BitStream in either a constructive or a classical setting, but it's uncountable in both /because the notion of countability also depends on the setting/.
23:48:36	<jreicher>	EvanR: sorry, I must be missing something fundamental. I thought bitstream can't be (classically) uncountable without including non-computable streams
23:48:51	<TMA>	but the smallest model contains just one infinite sequence of Is
23:48:53	<EvanR>	well I never brought up classical uncountability
23:49:02	<EvanR>	you're beyond me now
23:50:07	×	merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
23:50:08	<EvanR>	you can map (ok... lazy?) Nat to any SillyType = End \| I SillyType
23:50:20	<EvanR>	I mean, all
23:50:44	<TMA>	jreicher: BitStream is uncountable.
23:50:45	<EvanR>	seems countable
23:51:27	<EvanR>	specifically, f Z = End; f (S n) = I (f n)
23:52:05	<int-e>	(that's borderline stupid; SillyType is obviously isomorphic to Nat)
23:52:12	<EvanR>	if you try that on Bitstream, then somebody can come along and get a counterexample stream
23:52:18	<EvanR>	int-e, looooool
23:52:23	<int-e>	(data Nat = Z \| S N)
23:52:33	<EvanR>	it's borderline Silly
23:52:37	<int-e>	(data SillyType = End \| I SillyType)
23:52:47	<int-e>	EvanR: No, we've crossed that line long ago.
23:53:10	<jreicher>	If we disallow infinite bitstreams, bitstream becomes countable. If we allow infinite bitstreams, why can't we allow transfinite silly strings?
23:53:32	<EvanR>	why didn't cantor think of disallowing infinite streams
23:53:38	<EvanR>	would have saved us a lot of trouble
23:53:42	<int-e>	. o O ( if you disallow inifinte bitstreams, bitstream becomes empty )
23:53:47	<jreicher>	I'm not suggesting we do that. I'm just trying to understand the double standard.
23:53:58	EvanR	boggles
23:54:54	<TMA>	jreicher: there is transfinite silly string... it goes: I I I I I I I I I ...
23:55:24	<Inline>	aye aye aye eye eye aye.......
23:55:29	<int-e>	jreicher: You're insisting that two things are analogous despite strong evidence to the contrary, all of which has been laid out in front of you above.
23:55:38	<Inline>	the egotist set
23:55:43	<Inline>	lol
23:55:43	<EvanR>	jreicher, the original definition of Bitstream and SillyType both have nothing but infinite streams. Not really a double standard
23:55:51	<jreicher>	I'm not insisting anything of the sort. I also don't think they're analogous. I'm just trying to understand why.
23:55:58	<TMA>	jreicher: BUT there is just a single such string in the smallest model of the data SillyType = I SillyType theory
23:56:09	<int-e>	Also has it really been 2 hours of this...
23:56:12	<EvanR>	this is haskell an we have infinite lists
23:56:16	×	ttybitnik quits (~ttybitnik@user/wolper) (Ping timeout: 256 seconds)
23:56:17	<EvanR>	turns out
23:56:41	<jreicher>	But not transfinite lists
23:56:59	<EvanR>	they're not needed to make the original point, just as in cantor
23:57:21	<jreicher>	No, I know. I'm just picking out where the line is.
23:57:24	<EvanR>	though if you want to get into that there's more exotic constructions
23:58:57	trickard_	is now known as trickard

All times are in UTC on 2026-01-15.