Logs on 2022-03-27 (liberachat/#haskell)

00:01:29	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
00:05:05	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
00:14:12	×	harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Ping timeout: 240 seconds)
00:14:26	→	azimut_ joins (~azimut@gateway/tor-sasl/azimut)
00:14:38	→	raehik joins (~raehik@82.21.176.157)
00:16:15	×	azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds)
00:17:35	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
00:19:48	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
00:20:45	×	kaph_ quits (~kaph@net-109-116-124-149.cust.vodafonedsl.it) (Read error: Connection reset by peer)
00:24:15	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
00:26:40	→	harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67)
00:27:02	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
00:27:46	→	AlexNoo_ joins (~AlexNoo@178.34.150.116)
00:27:57	×	AlexNoo quits (~AlexNoo@178.34.150.116) (Read error: Connection reset by peer)
00:30:28	→	wroathe joins (~wroathe@ee4.ips.PaulBunyan.net)
00:30:28	×	wroathe quits (~wroathe@ee4.ips.PaulBunyan.net) (Changing host)
00:30:28	→	wroathe joins (~wroathe@user/wroathe)
00:31:55	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds)
00:32:15	×	raehik quits (~raehik@82.21.176.157) (Ping timeout: 256 seconds)
00:32:19	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
00:33:57	×	zyklotomic quits (~ethan@res388d-128-61-91-192.res.gatech.edu) (Ping timeout: 256 seconds)
00:35:36	→	zyklotomic joins (~ethan@r4-128-61-94-5.res.gatech.edu)
00:35:42	×	epolanski quits (uid312403@id-312403.helmsley.irccloud.com) (Quit: Connection closed for inactivity)
00:37:24	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer)
00:37:33	→	rawley_ joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
00:38:17	×	rawley_ quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Remote host closed the connection)
00:38:42	→	rawley_ joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
00:39:02	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
00:40:19	×	pnotequalnp quits (~kevin@user/pnotequalnp) (Ping timeout: 260 seconds)
00:42:56	×	Tuplanolla quits (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) (Quit: Leaving.)
00:47:44	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
00:48:06	→	chenqisu1 joins (~chenqisu1@183.217.201.88)
00:50:13	×	cyphase quits (~cyphase@user/cyphase) (Ping timeout: 268 seconds)
00:54:36	→	cyphase joins (~cyphase@user/cyphase)
00:55:51	×	DNH quits (~DNH@8.44.0.63) (Quit: My MacBook has gone to sleep. ZZZzzz…)
01:06:32	→	Jeanne-Kamikaze joins (~Jeanne-Ka@142.147.89.202)
01:15:47	×	aliosablack quits (~chomwitt@2a02:587:dc18:da00:eb71:868b:3400:4636) (Ping timeout: 260 seconds)
01:17:25	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Ping timeout: 240 seconds)
01:22:07	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
01:26:42	×	Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 272 seconds)
01:27:19	→	Maxdamantus joins (~Maxdamant@user/maxdamantus)
01:28:37	×	rawley_ quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Quit: Leaving)
01:28:56	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
01:29:50	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Client Quit)
01:30:03	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
01:30:06	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
01:31:00	×	mvk quits (~mvk@2607:fea8:5cc3:7e00::7980) (Ping timeout: 240 seconds)
01:33:10	→	rustacean joins (~quassel@117.254.34.143)
01:33:29	×	rustacean quits (~quassel@117.254.34.143) (Client Quit)
01:33:43	→	razetime joins (~quassel@117.254.34.143)
01:34:26	→	alp joins (~alp@user/alp)
01:34:37	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 268 seconds)
01:37:09	→	vglfr joins (~vglfr@37.73.58.115)
01:38:35	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds)
01:40:08	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
01:40:14	→	rekahsoft joins (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com)
01:41:13	×	rekahsoft quits (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com) (Remote host closed the connection)
01:41:18	×	xkuru quits (~xkuru@user/xkuru) (Read error: Connection reset by peer)
01:41:33	→	rekahsoft joins (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com)
01:43:10	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 272 seconds)
01:45:10	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
01:47:52	×	rekahsoft quits (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com) (Remote host closed the connection)
01:47:57	×	xff0x quits (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp) (Ping timeout: 256 seconds)
01:50:26	×	zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection)
01:51:05	→	rekahsoft joins (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com)
01:51:19	×	rekahsoft quits (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com) (Remote host closed the connection)
01:51:44	→	rekahsoft joins (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com)
01:52:24	→	zaquest joins (~notzaques@5.130.79.72)
01:55:57	×	joo-_ quits (~joo-_@fsf/member/joo--) (Ping timeout: 252 seconds)
01:57:34	→	joo-_ joins (~joo-_@80-62-117-54-mobile.dk.customer.tdc.net)
01:57:34	×	joo-_ quits (~joo-_@80-62-117-54-mobile.dk.customer.tdc.net) (Changing host)
01:57:34	→	joo-_ joins (~joo-_@fsf/member/joo--)
02:02:13	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds)
02:04:06	→	wroathe joins (~wroathe@ee4.ips.PaulBunyan.net)
02:04:06	×	wroathe quits (~wroathe@ee4.ips.PaulBunyan.net) (Changing host)
02:04:06	→	wroathe joins (~wroathe@user/wroathe)
02:04:13	×	vglfr quits (~vglfr@37.73.58.115) (Ping timeout: 268 seconds)
02:10:14	→	vglfr joins (~vglfr@37.73.58.115)
02:10:57	<razetime>	hi, i'm trying to install a package with cabal but get this weird error:
02:10:57	<razetime>	cabal: Error: some packages failed to install:
02:10:57	<razetime>	ghc-lib-parser-8.10.7.20220219-7xoqX1liclfEDk8lJQn5pT failed during the
02:10:57	<razetime>	configure step. The exception was:
02:10:57	<razetime>	ExitFailure 1
02:10:57	<razetime>	ormolu-0.1.4.1-IQBEtLLThqGE3isZmjbrfL depends on ormolu-0.1.4.1 which failed
02:10:59	<razetime>	to install.
02:18:01	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Read error: Connection reset by peer)
02:18:07	→	awschnap joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
02:20:36	×	jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection)
02:24:49	→	jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
02:25:06	→	AlexNoo__ joins (~AlexNoo@94.233.240.35)
02:25:13	→	xff0x joins (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp)
02:25:17	×	Katarushisu quits (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) (Read error: Connection reset by peer)
02:26:12	×	razetime quits (~quassel@117.254.34.143) (Ping timeout: 240 seconds)
02:26:37	×	AlexZenon quits (~alzenon@178.34.150.116) (Ping timeout: 240 seconds)
02:26:56	→	razetime joins (~quassel@117.254.34.170)
02:27:34	→	Katarushisu joins (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net)
02:27:39	×	Alex_test quits (~al_test@178.34.150.116) (Ping timeout: 250 seconds)
02:28:17	×	vglfr quits (~vglfr@37.73.58.115) (Ping timeout: 240 seconds)
02:28:17	×	AlexNoo_ quits (~AlexNoo@178.34.150.116) (Ping timeout: 240 seconds)
02:30:28	→	AlexZenon joins (~alzenon@94.233.240.35)
02:31:34	→	Alex_test joins (~al_test@94.233.240.35)
02:39:14	×	harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving)
02:40:24	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
02:41:41	→	finn_elija joins (~finn_elij@user/finn-elija/x-0085643)
02:41:42	×	FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
02:41:42	finn_elija	is now known as FinnElija
02:42:36	×	wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Quit: Lost terminal)
02:44:36	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
02:54:47	×	alp quits (~alp@user/alp) (Ping timeout: 268 seconds)
02:55:57	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds)
02:58:53	→	wroathe joins (~wroathe@user/wroathe)
03:01:17	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds)
03:01:23	→	deadmarshal_ joins (~deadmarsh@95.38.230.121)
03:02:36	→	kaph joins (~kaph@net-109-116-124-149.cust.vodafonedsl.it)
03:06:46	<DigitalKiwi>	razetime: is ormolu the package you want to install or something else
03:07:00	<razetime>	it is the package i want to install
03:08:14	→	cdman joins (~dcm@user/dmc/x-4369397)
03:08:27	<DigitalKiwi>	nix-shell -p ormolu
03:08:28	<DigitalKiwi>	[nix-shell:~]$ ormolu --version
03:08:30	<DigitalKiwi>	ormolu 0.1.4.1 UNKNOWN UNKNOWN
03:08:32	<DigitalKiwi>	using ghc-lib-parser 8.10.7.20210828
03:09:54	→	_dmc_ joins (~dcm@27.2.216.148)
03:13:11	×	cdman quits (~dcm@user/dmc/x-4369397) (Ping timeout: 256 seconds)
03:17:37	×	Hash quits (~Hash@hey.howstoned.ru) (Ping timeout: 240 seconds)
03:18:14	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
03:23:01	×	rekahsoft quits (~rekahsoft@cpe001b21a2fd89-cm64777ddc63a0.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds)
03:24:21	→	wyrd joins (~wyrd@gateway/tor-sasl/wyrd)
03:25:05	×	Jeanne-Kamikaze quits (~Jeanne-Ka@142.147.89.202) (Quit: Leaving)
03:26:12	<DigitalKiwi>	razetime: when was your last `cabal update`?
03:26:32	<razetime>	about a minute before i ran cabal install ormolu
03:27:42	<ProfSimm>	How does Haskell disambiguate these: a -b as in "apply -b to function a" vs "subtract b from a"
03:36:29	<dsal>	`a -b` is "call the function (-) on `a` and `b`"
03:37:35	<ProfSimm>	dsal: what about the other case, where I was trying to pass -b to a
03:37:47	<dsal>	That's not what that does, though.
03:37:47	<ProfSimm>	dsal: for example print -5
03:37:56	<dsal>	> print (-5)
03:37:57	<lambdabot>	<IO ()>
03:38:00	<ProfSimm>	Sure but
03:38:03	<dsal>	% print (-5)
03:38:03	<yahb>	dsal: -5
03:38:04	<ProfSimm>	Isn't this error prone
03:38:06	<DigitalKiwi>	lol weird i get ormolu-0.4.0.0 with cabal
03:38:26	<dsal>	It's not error prone in the sense that it'll cause runtime problems. It's not ambiguous.
03:38:30	<ProfSimm>	%print -5
03:38:51	<dsal>	There's a GHC extension to make it work a little more like you'd expect, but then that'd break some other things.
03:38:55	<dsal>	% print -5
03:38:55	<yahb>	dsal: ; <interactive>:28:1: error:; * No instance for (Num (() -> IO ())) arising from a use of `it'; (maybe you haven't applied a function to enough arguments?); * In the first argument of `print', namely `it'; In a stmt of an interactive GHCi command: print it
03:39:09	<ProfSimm>	Hm
03:39:31	<ProfSimm>	dsal: why have such an extension
03:39:47	<dsal>	Because people keep trying to do the syntactic thing that you're trying to do and it can work in many cases.
03:40:08	<ProfSimm>	dsal: in that case how do they do the other variant
03:40:12	<ProfSimm>	a - b
03:40:53	<dsal>	When do you want to call `(-) a b` ? That's almost every time I use `(-)`. I'm having a little trouble relating.
03:41:14	<ProfSimm>	OK
03:41:16	<ProfSimm>	thanks
03:41:46	<dsal>	This is the extension: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/negative_literals.html
03:43:07	<boxscape_>	ProfSimm: be clear (though maybe it is already), even with the extension, `a - b` is still parsed as `(-) a b`, just `a -b` is parsed as `a (-b)`
03:43:12	<boxscape_>	s/be/to be
03:43:34	<dsal>	It's OK to demand clarity of me.
03:45:35	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
03:46:58	×	Topsi quits (~Tobias@dyndsl-095-033-022-251.ewe-ip-backbone.de) (Read error: Connection reset by peer)
03:48:55	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
03:49:43	<abastro[m]>	Tbh quite ambiguous with `a-b`
03:50:04	<boxscape_>	that's parsed as `(-) a b` also
03:50:13	<abastro[m]>	Oh thats nice
03:50:20	<abastro[m]>	At cost of parsing overhead
03:50:29	<abastro[m]>	Hm actually, haskell is hard to parse right
03:50:40	<boxscape_>	I think so yeah
03:50:42	<abastro[m]>	I think it is one of problems of haskell
03:52:07	<dsal>	> 1+5
03:52:09	<lambdabot>	6
03:52:21	×	[itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 250 seconds)
03:52:25	<dsal>	> "a"<>"b"
03:52:27	<lambdabot>	"ab"
03:53:00	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds)
03:56:34	→	[itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
04:01:14	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
04:01:21	→	vglfr joins (~vglfr@46.96.151.207)
04:02:45	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
04:04:35	×	stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds)
04:06:57	→	stiell joins (~stiell@gateway/tor-sasl/stiell)
04:07:02	<abastro[m]>	That parsing error message is rather poor
04:08:57	<boxscape_>	% % (proc a -> (\| id (\x -> returnA -< x) \|) 4 5 6) "foo" -- update, I asked yesterday whether this is a bug, because the command seems to be getting more arguments than it requires - I now think it isn't, turns out commands just get a stack of arguments, and I suppose more values can be added onto that stack
04:08:57	<yahb>	boxscape_: ; <interactive>:34:1: error: parse error on input `%'
04:09:00	<boxscape_>	whoops
04:09:04	<boxscape_>	% (proc a -> (\| id (\x -> returnA -< x) \|) 4 5 6) "foo"
04:09:04	<yahb>	boxscape_: 4
04:12:25	→	vysn joins (~vysn@user/vysn)
04:14:05	→	nicbk joins (~nicbk@user/nicbk)
04:15:27	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 260 seconds)
04:15:55	×	deadmarshal_ quits (~deadmarsh@95.38.230.121) (Ping timeout: 260 seconds)
04:16:26	×	vglfr quits (~vglfr@46.96.151.207) (Ping timeout: 272 seconds)
04:19:07	×	_dmc_ quits (~dcm@27.2.216.148) (Changing host)
04:19:07	→	_dmc_ joins (~dcm@user/dmc/x-4369397)
04:19:22	×	_dmc_ quits (~dcm@user/dmc/x-4369397) (Quit: Leaving)
04:19:49	→	cdman joins (~dcm@user/dmc/x-4369397)
04:20:39	×	lambdap2 quits (~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: lambdap2)
04:21:15	→	lambdap2 joins (~lambdap@static.167.190.119.168.clients.your-server.de)
04:22:08	→	nate1 joins (~nate@98.45.167.61)
04:22:31	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
04:22:35	→	pnotequalnp joins (~kevin@user/pnotequalnp)
04:25:34	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
04:28:07	→	dyeplexer joins (~dyeplexer@user/dyeplexer)
04:29:28	→	_dmc_ joins (~dcm@27.2.216.148)
04:29:28	×	_dmc_ quits (~dcm@27.2.216.148) (Changing host)
04:29:28	→	_dmc_ joins (~dcm@user/dmc/x-4369397)
04:30:22	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Remote host closed the connection)
04:30:25	×	_dmc_ quits (~dcm@user/dmc/x-4369397) (Remote host closed the connection)
04:36:35	×	lumberjack123 quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
04:39:57	×	chenqisu1 quits (~chenqisu1@183.217.201.88) (Ping timeout: 240 seconds)
04:42:45	×	HotblackDesiato_ quits (~HotblackD@gateway/tor-sasl/hotblackdesiato) (Remote host closed the connection)
04:43:00	→	HotblackDesiato joins (~HotblackD@gateway/tor-sasl/hotblackdesiato)
04:48:01	→	lumberjack123 joins (~alMalsamo@gateway/tor-sasl/almalsamo)
04:51:15	×	[itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
04:54:06	×	pgib quits (~textual@173.38.117.75) (Ping timeout: 245 seconds)
04:59:30	×	jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 272 seconds)
05:00:57	→	Guest2747 joins (~Guest27@2601:281:d47f:1590::6b90)
05:09:15	×	nicbk quits (~nicbk@user/nicbk) (Quit: nicbk)
05:15:58	×	nate1 quits (~nate@98.45.167.61) (Ping timeout: 272 seconds)
05:16:34	→	sloorush joins (~sloorush@136.233.9.99)
05:26:55	×	sloorush quits (~sloorush@136.233.9.99) (Ping timeout: 256 seconds)
05:28:21	×	Unicorn_Princess quits (~Unicorn_P@93-103-228-248.dynamic.t-2.net) (Remote host closed the connection)
05:29:48	×	vysn quits (~vysn@user/vysn) (Ping timeout: 240 seconds)
05:29:59	×	Guest2747 quits (~Guest27@2601:281:d47f:1590::6b90) (Quit: Client closed)
05:32:39	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
05:33:30	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
05:35:29	→	Everything joins (~Everythin@37.115.210.35)
05:41:53	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
05:45:02	→	jdm joins (jesse@c-68-62-216-212.hsd1.al.comcast.net)
05:47:23	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds)
05:48:15	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
05:49:24	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
05:50:15	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
05:51:48	×	awschnap quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
05:53:54	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
05:54:28	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
05:57:30	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
05:59:13	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
06:00:16	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
06:05:37	×	pnotequalnp quits (~kevin@user/pnotequalnp) (Ping timeout: 240 seconds)
06:06:19	×	YoungFrog quits (~youngfrog@2a02:a03f:c21b:f900:d813:4914:1c90:9409) (Remote host closed the connection)
06:06:38	→	YoungFrog joins (~youngfrog@2a02:a03f:c21b:f900:84e3:4a12:bce1:8082)
06:09:19	×	kaph quits (~kaph@net-109-116-124-149.cust.vodafonedsl.it) (Ping timeout: 260 seconds)
06:11:15	→	Pickchea joins (~private@user/pickchea)
06:13:48	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
06:14:05	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
06:19:23	→	vglfr joins (~vglfr@46.96.151.207)
06:22:51	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
06:23:19	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds)
06:24:23	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
06:36:07	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
06:36:54	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
06:37:27	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
06:40:17	×	leah2 quits (~leah@vuxu.org) (Ping timeout: 252 seconds)
06:41:43	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
06:45:00	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
06:45:14	×	lagash quits (lagash@lagash.shelltalk.net) (Ping timeout: 252 seconds)
06:48:03	→	lagooned joins (~lagooned@108-208-149-42.lightspeed.hstntx.sbcglobal.net)
06:49:15	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
06:52:01	×	mtjm quits (~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection)
06:53:05	→	mtjm joins (~mutantmel@2604:a880:2:d0::208b:d001)
06:53:40	→	kaph joins (~kaph@net-109-116-124-149.cust.vodafonedsl.it)
07:04:02	×	Pickchea quits (~private@user/pickchea) (Quit: Leaving)
07:04:43	→	dextaa_ joins (~dextaa@user/dextaa)
07:07:50	→	AlexZenon_2 joins (~alzenon@94.233.240.35)
07:09:29	×	AlexZenon quits (~alzenon@94.233.240.35) (Ping timeout: 256 seconds)
07:10:50	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Remote host closed the connection)
07:10:57	→	pacc joins (~dylan@c-98-212-49-222.hsd1.il.comcast.net)
07:11:16	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
07:11:59	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
07:12:13	→	vysn joins (~vysn@user/vysn)
07:15:49	→	Midjak joins (~Midjak@82.66.147.146)
07:17:17	×	pacc quits (~dylan@c-98-212-49-222.hsd1.il.comcast.net) (Quit: WeeChat 3.0)
07:21:48	→	takuan joins (~takuan@178-116-218-225.access.telenet.be)
07:23:31	→	acidjnk joins (~acidjnk@pd9e0b763.dip0.t-ipconnect.de)
07:23:52	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
07:25:57	×	tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz)
07:27:15	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds)
07:27:53	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
07:28:58	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
07:40:34	→	chenqisu1 joins (~chenqisu1@183.217.201.88)
07:42:36	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds)
07:43:47	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
07:47:20	<joel135>	do you know some unexpected way of implementing division with remainder in pure lambda calculus?
07:47:20	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:47:35	→	Dorkside joins (~dorkside@208.190.197.222)
07:47:36	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:47:50	→	Dorkside joins (~dorkside@208.190.197.222)
07:47:51	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:48:05	→	Dorkside joins (~dorkside@208.190.197.222)
07:48:06	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:48:19	→	Dorkside joins (~dorkside@208.190.197.222)
07:48:19	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:48:32	→	Dorkside joins (~dorkside@208.190.197.222)
07:48:33	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:48:46	→	Dorkside joins (~dorkside@208.190.197.222)
07:48:46	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:48:55	×	lumberjack123 quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
07:48:59	→	Dorkside joins (~dorkside@208.190.197.222)
07:49:00	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:49:13	→	Dorkside joins (~dorkside@208.190.197.222)
07:49:13	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:49:26	→	Dorkside joins (~dorkside@208.190.197.222)
07:49:26	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:49:39	→	Dorkside joins (~dorkside@208.190.197.222)
07:49:39	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:49:53	→	Dorkside joins (~dorkside@208.190.197.222)
07:49:54	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:50:08	→	Dorkside joins (~dorkside@208.190.197.222)
07:50:09	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:50:23	→	Dorkside joins (~dorkside@208.190.197.222)
07:50:24	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:50:28	<joel135>	(mostly interested in the remainder part, but i figure the quotient shouldn't be much harder)
07:50:36	→	Dorkside joins (~dorkside@208.190.197.222)
07:50:37	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:50:50	→	Dorkside joins (~dorkside@208.190.197.222)
07:50:50	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:51:03	→	Dorkside joins (~dorkside@208.190.197.222)
07:51:03	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:51:04	→	Tuplanolla joins (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi)
07:51:16	→	Dorkside joins (~dorkside@208.190.197.222)
07:51:17	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:51:31	→	Dorkside joins (~dorkside@208.190.197.222)
07:51:32	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:51:45	→	Dorkside joins (~dorkside@208.190.197.222)
07:51:46	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:52:04	→	Dorkside joins (~dorkside@208.190.197.222)
07:52:04	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:52:18	→	Dorkside joins (~dorkside@208.190.197.222)
07:52:19	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:52:32	→	Dorkside joins (~dorkside@208.190.197.222)
07:52:33	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:52:46	→	Dorkside joins (~dorkside@208.190.197.222)
07:52:46	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:52:59	→	Dorkside joins (~dorkside@208.190.197.222)
07:52:59	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:53:13	→	Dorkside joins (~dorkside@208.190.197.222)
07:53:14	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:53:28	→	Dorkside joins (~dorkside@208.190.197.222)
07:53:29	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:53:42	→	Dorkside joins (~dorkside@208.190.197.222)
07:53:42	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:53:55	→	Dorkside joins (~dorkside@208.190.197.222)
07:53:55	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:54:08	→	Dorkside joins (~dorkside@208.190.197.222)
07:54:09	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:54:21	→	Dorkside joins (~dorkside@208.190.197.222)
07:54:21	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:54:34	→	Dorkside joins (~dorkside@208.190.197.222)
07:54:34	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:54:42	<joel135>	maybe i should give mendler encoding another go
07:54:47	→	Dorkside joins (~dorkside@208.190.197.222)
07:54:48	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:54:58	<boxscape_>	% :t \f xs ys z -> foldr (uncurry f) z $ zip xs ys
07:54:58	<yahb>	boxscape_: (a -> b1 -> b2 -> b2) -> [a] -> [b1] -> b2 -> b2
07:55:00	→	Dorkside joins (~dorkside@208.190.197.222)
07:55:01	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:55:02	<boxscape_>	is there a function like this in hackage?
07:55:14	→	Dorkside joins (~dorkside@208.190.197.222)
07:55:14	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:55:19	→	deadmarshal_ joins (~deadmarsh@95.38.230.121)
07:55:32	<boxscape_>	I guess it might not cross the Fairbairn threshold
07:55:33	→	Dorkside joins (~dorkside@208.190.197.222)
07:55:33	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:55:47	→	Dorkside joins (~dorkside@208.190.197.222)
07:55:48	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:56:01	→	Dorkside joins (~dorkside@208.190.197.222)
07:56:02	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:56:16	→	Dorkside joins (~dorkside@208.190.197.222)
07:56:17	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:56:30	→	Dorkside joins (~dorkside@208.190.197.222)
07:56:30	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:56:43	→	Dorkside joins (~dorkside@208.190.197.222)
07:56:43	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:56:56	→	Dorkside joins (~dorkside@208.190.197.222)
07:56:57	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:57:10	→	Dorkside joins (~dorkside@208.190.197.222)
07:57:11	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:57:14	→	gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk)
07:57:25	→	Dorkside joins (~dorkside@208.190.197.222)
07:57:26	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:57:39	→	Dorkside joins (~dorkside@208.190.197.222)
07:57:40	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:57:53	→	Dorkside joins (~dorkside@208.190.197.222)
07:57:54	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:58:07	→	Dorkside joins (~dorkside@208.190.197.222)
07:58:07	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:58:21	→	Dorkside joins (~dorkside@208.190.197.222)
07:58:21	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:58:34	→	Dorkside joins (~dorkside@208.190.197.222)
07:58:34	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:58:47	→	Dorkside joins (~dorkside@208.190.197.222)
07:58:47	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:59:00	→	Dorkside joins (~dorkside@208.190.197.222)
07:59:00	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:59:13	→	Dorkside joins (~dorkside@208.190.197.222)
07:59:13	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
07:59:27	→	Dorkside joins (~dorkside@208.190.197.222)
07:59:28	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:59:41	→	Dorkside joins (~dorkside@208.190.197.222)
07:59:42	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
07:59:55	×	deadmarshal_ quits (~deadmarsh@95.38.230.121) (Ping timeout: 260 seconds)
07:59:56	→	Dorkside joins (~dorkside@208.190.197.222)
07:59:57	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:00:11	→	Dorkside joins (~dorkside@208.190.197.222)
08:00:12	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:00:26	→	Dorkside joins (~dorkside@208.190.197.222)
08:00:27	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:00:41	→	Dorkside joins (~dorkside@208.190.197.222)
08:00:41	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:00:54	→	Dorkside joins (~dorkside@208.190.197.222)
08:00:55	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:01:16	→	Dorkside joins (~dorkside@208.190.197.222)
08:01:16	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:01:29	→	Dorkside joins (~dorkside@208.190.197.222)
08:01:30	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:01:42	→	Dorkside joins (~dorkside@208.190.197.222)
08:01:43	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:01:56	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
08:01:57	→	Dorkside joins (~dorkside@208.190.197.222)
08:01:58	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:02:12	→	Dorkside joins (~dorkside@208.190.197.222)
08:02:13	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:02:26	→	Dorkside joins (~dorkside@208.190.197.222)
08:02:27	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:02:45	→	Dorkside joins (~dorkside@208.190.197.222)
08:02:45	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:03:00	→	Dorkside joins (~dorkside@208.190.197.222)
08:03:01	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:03:13	→	Dorkside joins (~dorkside@208.190.197.222)
08:03:13	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:03:27	→	Dorkside joins (~dorkside@208.190.197.222)
08:03:27	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:03:39	→	Dorkside joins (~dorkside@208.190.197.222)
08:03:39	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:03:52	→	Dorkside joins (~dorkside@208.190.197.222)
08:03:53	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:04:06	→	Dorkside joins (~dorkside@208.190.197.222)
08:04:06	×	Dorkside quits (~dorkside@208.190.197.222) (Read error: Connection reset by peer)
08:04:19	→	Dorkside joins (~dorkside@208.190.197.222)
08:04:19	×	Dorkside quits (~dorkside@208.190.197.222) (Remote host closed the connection)
08:04:32	→	Dorkside joins (~dorkside@208.190.197.222)
08:05:39	→	leah2 joins (~leah@vuxu.org)
08:07:34	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
08:10:22	→	aliosablack joins (~chomwitt@2a02:587:dc18:da00:e2ec:eb52:4039:9bfe)
08:12:31	<tomsmeding>	periodic reminder that ghcup is great, just updated my haskell installation on a machine I haven't touched in a while, `ghcup tui` and we roll
08:14:25	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 256 seconds)
08:15:15	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
08:19:54	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
08:20:00	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
08:21:48	×	leah2 quits (~leah@vuxu.org) (Ping timeout: 240 seconds)
08:24:59	×	Batzy quits (~quassel@user/batzy) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
08:27:23	→	Batzy joins (~quassel@user/batzy)
08:27:27	×	vglfr quits (~vglfr@46.96.151.207) (Ping timeout: 260 seconds)
08:34:08	<energizer>	if a,b are types then "either a or b" is another type. sometimes people say that's "addition", i guess because the cardinalities match up or something
08:35:13	<energizer>	but types are kinda like sets too, so isn't it more like "union"; and also types are supposedly like propositions so isn't it more like "or"
08:35:25	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds)
08:36:31	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
08:36:46	<energizer>	so why is it + instead of ∪ or \|
08:36:48	<abastro[m]>	Which is why ppl use the term `Tagged union` as well
08:37:25	<abastro[m]>	Btw iirc in boolean logic, OR was using notation `+`
08:38:01	→	leah2 joins (~leah@vuxu.org)
08:38:25	<energizer>	can i take two types and add them together?
08:39:29	<tomsmeding>	energizer: what's "either Int or In"
08:39:35	<tomsmeding>	*Int
08:39:41	<tomsmeding>	That's Int + Int, not Int, right?
08:39:41	<energizer>	that's just Int
08:39:50	<tomsmeding>	Which is why it is the disjoint union, not the union
08:40:08	<tomsmeding>	Ah, if you say that's Int, then indeed you're talking about union, but then those are not sum types
08:40:15	<energizer>	+ is disjoint union and \| is regular union?
08:40:27	<tomsmeding>	Sum types do a disjoint union, also (in imperative programming land) a tagged union
08:40:49	<tomsmeding>	+ in type theory is disjoint union, \| in boolean logic is union :p
08:41:07	<energizer>	is there a plain union in type theory?
08:41:14	<tomsmeding>	Some languages, e.g. python and typescript, have actual union types
08:41:41	<tomsmeding>	Not the basic type theory I know, but I wouldn't be surprised if someone found an encoding for union in TT
08:42:35	<tomsmeding>	If union is \cup, then the cardinalities are weird though; #(a \cup b) is not really expressible in terms of #a and #b
08:42:51	<tomsmeding>	So the "algebraic" data types analogy doesn't hold for them
08:44:01	<tomsmeding>	(c.f. abastro[m]'s remark: in boolean logic, union (OR) is saturating addition: 1+1=1)
08:44:36	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
08:44:58	<energizer>	isnt it just #a + #b - #(a∩b)
08:45:11	×	acidjnk quits (~acidjnk@pd9e0b763.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
08:45:17	<abastro[m]>	Yes, saturating addition
08:45:20	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
08:47:02	<abastro[m]>	Anyway notation usage of math is quite liberal
08:47:09	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
08:48:28	<tomsmeding>	energizer: yes indeed, but #(a \cap b) is not a really simple operation
08:49:10	<boxscape_>	the main problem with union types AFAIK is that type inference is hard
08:49:20	<boxscape_>	...as with all forms of subtyping
08:49:25	<boxscape_>	(okay maybe not literally all)
08:49:37	<energizer>	does that refer to global type inference?
08:50:28	<boxscape_>	I haven't actually heard the term "global type inference" before but I suspect if global and local type inference exist it's hard for both of them, I don't see a reason why they would be different here
08:51:22	<energizer>	iirc mypy only cares about one function at a time
08:52:06	<energizer>	tomsmeding: is #a + #b - #(a∩b) somehow a representation of saturating addition?
08:52:57	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
08:53:39	<abastro[m]>	Apparently many ppl do not care much about type inference
08:53:41	<tomsmeding>	energizer: yes
08:53:52	<tomsmeding>	Thing is that saturating addition of integers is easy
08:53:58	<abastro[m]>	I've heard many ppl saying that it is better to be enforced to specify types
08:54:02	<tomsmeding>	But saturating addition of sets is... kinda weird
08:54:10	<boxscape_>	energizer judging by https://stackoverflow.com/questions/4304003/what-does-no-global-type-inference-mean-regarding-scala it does sound like local inference might be fine with subtyping, though I guess there probably isn't a single definition of "local" inference
08:54:17	<tomsmeding>	You can define it, and it works, but it's not super simple to work with
08:54:52	<abastro[m]>	Local inference is possible with subtyping but hard and also limited iirc
08:55:02	<abastro[m]>	Got bitten a lot by that
08:55:06	<boxscape_>	I see
08:55:56	<tomsmeding>	Also union types are, in some sense, not really compositional: where a * b and a + b are defined in terms of a and b, a \cup b is defined in terms of a, b _and_ a \cap b
08:56:02	<abastro[m]>	`((_.foo) compose (bar))` and type errors go broke
08:56:26	<tomsmeding>	And type theory is otherwise very compositional
08:57:02	<boxscape_>	tomsmeding doesn't that depend on how you define your primitives? As in, you could say union is primitive, and sum types are union + a \cap b
08:57:41	<tomsmeding>	Of course
08:58:10	<tomsmeding>	But disjoint union is very nice, and in fact not even primitive in TT: it's a sigma type over a boolean
08:58:20	<boxscape_>	hm that's fair
08:58:53	<abastro[m]>	But then more complex one is primitive
08:59:01	<abastro[m]>	Namely, sigma and pi
08:59:04	<boxscape_>	what is "complexity"
08:59:26	<abastro[m]>	Idk, more symbols
08:59:35	<abastro[m]>	You need to introduce a binding
08:59:36	<tomsmeding>	abastro[m]: more complex maybe, but also a very small set
08:59:37	<boxscape_>	though in any case that doesn't matter if you need sigma and pi anyway for other reasons
08:59:48	<abastro[m]>	Well yea
09:00:33	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
09:00:35	<boxscape_>	your compiler will be less complex overall if you have fewer primitives
09:01:27	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 256 seconds)
09:01:31	<abastro[m]>	That was my illusion but type checking and inference of dependent languages told me otherwise
09:01:47	<tomsmeding>	Type theory is, in basis, math
09:02:13	<tomsmeding>	It's math chosen such that it has a nice correspondence with programming, but it's still math
09:02:22	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
09:02:31	<boxscape_>	abastro[m] yeah I was being unclear in that - I didn't mean if you have a smaller set of primitives, I meant if you have a strict subset of primitives
09:02:43	<tomsmeding>	Your compiler will be simpler if it only supports * and +, but then it wouldn't support dependently typed languages
09:03:21	<tomsmeding>	Your compiler will be simpler with fewer prinitives _assuming that you must implement a dependently typed language_
09:03:39	<tomsmeding>	Also what boxscape_ just said lol
09:04:44	×	yushyin quits (NwWjaFh18p@mail.karif.server-speed.net) (Quit: WeeChat 3.4)
09:04:44	×	noctuks quits (pS9vLLhgiV@user/noctux) (Quit: WeeChat 3.4)
09:04:44	×	sviermsung quits (owJr4HCxlX@user/s4msung) (Quit: sviermsung)
09:05:37	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
09:07:05	→	noctuks joins (9wxBRvrIcP@user/noctux)
09:07:06	→	s4msung joins (iMiZICJOVw@user/s4msung)
09:07:07	→	yushyin joins (klVu03SvEu@mail.karif.server-speed.net)
09:08:12	<energizer>	found a paper that says untagged union is denoted \vee b
09:08:21	<energizer>	s/b//
09:11:01	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
09:11:05	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
09:11:09	<abastro[m]>	Oh, I see
09:11:32	<abastro[m]>	Indeed strict subset is easier to implement
09:11:35	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
09:12:26	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
09:12:36	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Remote host closed the connection)
09:13:01	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
09:15:16	<abastro[m]>	I wonder how type theory survived in programming where set theory became dominant in math
09:16:48	<Maxdamantus>	Presumably by being computable.
09:16:53	<Maxdamantus>	Which is important for computers.
09:16:53	<[exa]>	+1 ^
09:17:19	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
09:17:39	<Maxdamantus>	"became dominant in math", it already was dominant.
09:17:58	<Maxdamantus>	type theory arose as an alternative solution to problems in type theory.
09:18:19	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
09:18:35	<Maxdamantus>	the non-alternative solution was ZFC, which is still set theory.
09:18:57	<tomsmeding>	Disjoint union is also much more useful in programming than union I think: think of tree structures. Almost all of programming is dealing with tree structures, and trees are necessarily inductive disjoint unions, not set-theory unions
09:19:14	<Maxdamantus>	(in particular, problems raised by Bertrand Russell in the early 1900s. he was the one that started "type theory")
09:19:33	<abastro[m]>	<del>Type theory to solve problems in type theory</del>
09:19:46	<Maxdamantus>	er, meant to say "problems in set theory"
09:20:01	<energizer>	tomsmeding: ehh hammer/nail
09:20:03	<abastro[m]>	sorry..
09:20:19	<abastro[m]>	Sometimes I be that pedant
09:21:15	<Maxdamantus>	In programming, using "sets" is something extra. Related to what tomsmeding is saying, in programming you would normally go for an array/list as the computationally simple thing.
09:21:37	<Maxdamantus>	It's only in special cases that you actually want set behaviour, where you want your members to be deduplicated.
09:22:36	<Maxdamantus>	(naturally in Haskell, you can have a list of values of any type, but if you want a set, you need to demand a constraint, `Ord a`)
09:22:51	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
09:23:11	<energizer>	what does it have to do with ordering?
09:23:20	<boxscape_>	technically Eq a is enough
09:23:25	<boxscape_>	but Ord a allows you to make it more efficient
09:23:43	→	ProfSimm joins (~ProfSimm@87.227.196.109)
09:24:05	<abastro[m]>	So Russel was not great enough in his reputation to turn entire mathematics towards TT
09:24:10	<boxscape_>	(easier to search for duplicate values if you can make a binary search tree)
09:24:11	<Maxdamantus>	Sure, there could be different sorts of constraints, but you're always going to have an extra constraint that is not required for lists.
09:24:47	<energizer>	lists are in an order, which is odd
09:24:52	<Maxdamantus>	abastro[m]: well, I don't think Russell is the only one involved in the push for TT.
09:25:07	<[exa]>	why would entire mathematics need type theory?
09:25:10	<abastro[m]>	(Java has hashCode for every classes - hm)
09:25:39	<[exa]>	that would be just grossly impractical
09:25:48	<abastro[m]>	Precision
09:25:54	<Maxdamantus>	Because it's computable.
09:26:01	<abastro[m]>	That as well
09:26:09	<tomsmeding>	energizer: reminder that programming existed before type theory got any significant influence there :p
09:26:14	<[exa]>	good luck expressing basic calculus with that :D
09:26:19	<Maxdamantus>	You don't have to rely as much on people carefully reviewing proofs.
09:26:29	<abastro[m]>	(I think you could still deal with uncomputable objects in TT but anyway)
09:26:51	<abastro[m]>	Idk, basic calculus does not seem that hard to express
09:26:56	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
09:27:22	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
09:27:23	<abastro[m]>	Possibly you could use concepts from manifolds
09:27:23	<[exa]>	abastro[m]: even the most basic theorems there require reaching to infinity and assuming whatever happens there
09:27:28	<abastro[m]>	Manifold analysis*
09:27:30	<tomsmeding>	I mean, the `union` keyword in C is a bloody disjoint union
09:27:47	<tomsmeding>	It just misses a tag to be a proper sum type
09:28:13	<abastro[m]>	Reaching to infinity? Im quite sure it is doable
09:28:21	<energizer>	forall (e : real), exists (d : real), forall x ... this isnt hard
09:28:30	<Maxdamantus>	tomsmeding: `union` in C would usually be considered a non-disjoint union.
09:28:33	<abastro[m]>	Ye
09:28:36	<Maxdamantus>	tomsmeding: since it doesn't include a tag.
09:28:41	×	chenqisu1 quits (~chenqisu1@183.217.201.88) (Quit: Leaving)
09:28:46	<abastro[m]>	Problem is with topology, rather.
09:29:00	<Maxdamantus>	tomsmeding: `union { int a; int b; }` is not very useful.
09:29:03	<[exa]>	abastro[m]: what's the type of a real that is a product of 2 such limits?
09:29:18	<[exa]>	(-> can you then type reals?)
09:29:24	<abastro[m]>	You have "extended reals"
09:29:31	<abastro[m]>	Which includes infinity
09:29:37	<tomsmeding>	Hm, good point, I messed up there
09:29:58	<abastro[m]>	Instead compromises product and such
09:30:43	<abastro[m]>	IIRC quite huge parts of math is formalized in Coq and Lean
09:30:45	<[exa]>	abastro[m]: I expect you will find many surprising truths about the computability of real numbers
09:31:32	<abastro[m]>	I mean, you can either represent computable real numbers or deal with uncomputables
09:31:41	<abastro[m]>	Which is quite doable actually
09:31:51	<abastro[m]>	Just restrict evaluating the term
09:32:04	→	DNH joins (~DNH@2a09:bac0:48::82b:7a48)
09:33:29	<[exa]>	that sounds much like "let's take rational numbers and pretend they are real"
09:33:48	<joel135>	does someone have a copy of "mendler 1987 recursive types and type constraints in second-order lambda calculus" ?
09:34:43	<[exa]>	joel135: you mean this? https://core.ac.uk/download/pdf/81989173.pdf
09:34:44	<abastro[m]>	Well you do know how real number is defined from quotients right?
09:35:03	<abastro[m]>	You can do that and sacrifice a bit of compitability
09:35:16	<[exa]>	wait what
09:35:49	<boxscape_>	you can define computable real numbers in terms of limits of rational numbers, i.e. Cauchy sequences
09:35:55	<joel135>	it is not the same article but maybe it will do :)
09:36:01	<abastro[m]>	Acrually I found this
09:36:03	<abastro[m]>	https://www.cs.umd.edu/~rrand/vqc/Real.html
09:36:21	<abastro[m]>	They found that cauchy seq is not good enough, so gone for axiomatic formulation
09:37:02	<boxscape_>	fair enough
09:37:23	→	zer0bitz_ joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
09:37:26	<abastro[m]>	Yea I mean they could use cauchy seq ofc
09:37:37	<abastro[m]>	But it was slightly cumbersome they say
09:37:49	<boxscape_>	riht
09:37:57	<boxscape_>	s/h/gh/
09:38:17	×	zer0bitz quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 240 seconds)
09:38:30	<energizer>	in the big theorem provers they use much more abstract math that has undergraduate-level material as a very very very special case
09:38:33	<abastro[m]>	Can I ask what is s/h/gh
09:38:52	<energizer>	it means substitute, in place of h, gh
09:39:05	<abastro[m]>	Oh, interesting
09:39:07	<energizer>	because boxscape_ did a typo
09:39:19	<abastro[m]>	I learned a new chat expression
09:39:23	<energizer>	it's the syntax from sed
09:39:38	<boxscape_>	fun fact discord even supports it
09:39:45	<boxscape_>	i.e. will actually edit your last message
09:40:02	<joel135>	you can try this in your terminal "echo foobar\| sed 's/foo/chocolate /'"
09:40:10	<abastro[m]>	Oh wow
09:40:44	<abastro[m]>	I hope it's not regex
09:41:06	<boxscape_>	I haven't seen people use regex in IRC for that
09:41:10	<boxscape_>	but they sure do in sed
09:41:20	<abastro[m]>	Oh nooooooo
09:41:42	<[exa]>	luckily people here interpret regex flawlessly right? :D
09:41:56	<boxscape_>	of course
09:42:03	<[exa]>	abastro[m]: you're invited to try proving the bolzano-weierstrass theorem on that structure
09:42:54	<abastro[m]>	I don't think B-W would be hard even
09:42:57	<joel135>	see also http://www.paultaylor.eu/ASD/analysis
09:43:20	×	Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
09:44:12	<ProfSimm>	dsal: thanks for the link. It's odd Haskell overlooked this problem when making their syntax
09:44:36	<abastro[m]>	Okay it does take some space in coq stdlib
09:45:35	→	zer0bitz joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
09:45:43	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
09:46:43	<Maxdamantus>	I usually treat my s/// lines as actual regex.
09:47:00	<Maxdamantus>	eg, I'll often use \< and \> as word delimeters.
09:47:15	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds)
09:47:58	<abastro[m]>	https://github.com/coq/coq/blob/master/theories/Reals/Rtopology.v
09:48:09	<Maxdamantus>	$ grep 's/.*$\\<\\|\\>$' ~/irclogs/Libera/#haskell.log
09:48:09	<Maxdamantus>	17:19 < Maxdamantus> s/\<their\>/they're/
09:48:10	→	zer0bitz__ joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
09:48:14	<Maxdamantus>	Maybe I'm the only one.
09:49:07	×	zer0bitz_ quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 260 seconds)
09:49:16	<boxscape_>	you even bother to escape the <>s
09:49:44	<Maxdamantus>	Of course, otherwise it would require a literal less than and greater than sign.
09:50:16	<Maxdamantus>	s/\<a //; s/\<sign\>/signs/
09:50:30	→	_ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl)
09:50:40	<boxscape_>	I usually set up my tools to make me escape literals when I want to search for them
09:50:42	→	deadmarshal_ joins (~deadmarsh@95.38.230.121)
09:50:58	<Maxdamantus>	Wait, you mean in my grep command?
09:51:16	<boxscape_>	no
09:51:33	<boxscape_>	but I would just assume other people's brains are set up the way I set up my tools when convenient
09:51:37	<boxscape_>	to save myself some characters
09:51:55	<Maxdamantus>	`s/<a//` and `s/\<a//` mean something quite different in sed.
09:51:55	×	zer0bitz quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 260 seconds)
09:52:06	<Maxdamantus>	\< is a leading word delimeter.
09:52:10	<Maxdamantus>	< is just a less than sign.
09:52:28	<boxscape_>	right I don't know that you can change it in sed but e.g. in vim I have it the other way around
09:52:54	<Maxdamantus>	Oh, so you've selected ereg or PCRE or something.
09:53:16	<boxscape_>	alas, there's no setting for it, it requires a plugin
09:53:41	<Maxdamantus>	Personally, I find it annoying that some tools (eg, `less`) use different syntaxes.
09:53:58	<boxscape_>	understandable
09:54:26	<abastro[m]>	Price to pay with composability
09:55:14	<Maxdamantus>	imo the breg syntax is more logical anyway.
09:56:07	<abastro[m]>	Hm I guess I am weird for not using these utilities
09:56:43	<Maxdamantus>	I've always suspected that if people prefer the symbols to be treated as special by default (ie, without requiring a backslash), it's just because they initially used regexes that did that, eg, ones in popular programming languages like JS.
09:57:30	×	DNH quits (~DNH@2a09:bac0:48::82b:7a48) (Quit: My MacBook has gone to sleep. ZZZzzz…)
09:57:41	<Maxdamantus>	I would even like it if breg went further and made it so '.' matches a literal dot while '\.' matches any byte. similarly, '*' should match an asterisk.
09:58:15	<Maxdamantus>	but too late for that, and those are the only exceptions you need to remember afaict.
09:58:51	<abastro[m]>	Well I don't see difference of the characters by rendering
09:59:10	<boxscape_>	does matrix remove backslashes?
09:59:24	<boxscape_>	\. . <- this is two dots without a backslash?
09:59:24	<Maxdamantus>	Oh, there's also ^ $ []
09:59:39	<Maxdamantus>	22:59:24 < boxscape_> \. . <- this is two dots without a backslash?
09:59:50	<Maxdamantus>	Oh, nvm. I'm not on Matrix.
10:00:07	<Maxdamantus>	(I thought you were wondering if your Matrix connection did something)
10:00:23	<abastro[m]>	Yes, matrix removes backslash
10:00:28	<boxscape_>	interesting
10:00:46	<abastro[m]>	Can't blame matrix, right
10:03:35	→	dsrt^ joins (~dsrt@96-91-136-49-static.hfc.comcastbusiness.net)
10:05:35	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
10:08:00	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
10:09:42	<[exa]>	is there some nice haskell library one could use for syntax highlighting? (i.e., it tells me some meta information about what each piece of a given source code string is, and has support for at least some languages so that I don't need to write the definitions myself)
10:10:02	→	DNH joins (~DNH@8.43.122.72)
10:12:50	bcoppens_	is now known as bcoppens
10:13:59	<[exa]>	whew, there's skylighting
10:16:39	→	rustacean joins (~quassel@117.254.34.170)
10:16:48	×	razetime quits (~quassel@117.254.34.170) (Ping timeout: 272 seconds)
10:18:25	×	califax quits (~califax@user/califx) (Remote host closed the connection)
10:19:28	→	califax joins (~califax@user/califx)
10:21:06	×	dsrt^ quits (~dsrt@96-91-136-49-static.hfc.comcastbusiness.net) (Remote host closed the connection)
10:21:31	→	dsrt^ joins (~dsrt@96-91-136-49-static.hfc.comcastbusiness.net)
10:21:37	×	dsrt^ quits (~dsrt@96-91-136-49-static.hfc.comcastbusiness.net) (Remote host closed the connection)
10:22:32	<Franciman>	[exa]: there are also tree-sitter bindings
10:23:26	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
10:26:36	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
10:27:51	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
10:27:52	<sshine>	[exa], I'd go with tree-sitter just because it seems like a great project.
10:31:18	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Ping timeout: 252 seconds)
10:31:20	<[exa]>	hm yeah that looks cool
10:31:35	<[exa]>	is it somehow easily accessible from hackage?
10:32:35	<sshine>	except for the tree-sitter package saying "We strongly recommend against depending on this library at this time", hmm... ;)
10:32:47	<sshine>	and hasn't been updated in two years.
10:33:12	→	xkuru joins (~xkuru@user/xkuru)
10:33:20	<sshine>	it feels like a group of people had a hope two years ago, but abandoned it.
10:33:45	<sshine>	where/how do you plan to display syntax-highlighted code?
10:34:52	<sshine>	my guess is that most syntax-highlighting happens in javascript nowadays.
10:34:55	<[exa]>	I'm not really after syntax highlighting, just trying to get a decent set of code tokenizers for free
10:35:00	<sshine>	ah!
10:35:16	<[exa]>	(related to a problem that I was trying to solve here repeatedly several times already, haha)
10:35:31	<sshine>	ah, didn't catch the general problem.
10:35:46	<[exa]>	technically I'm just trying to cut the code (and possibly other stuff) into separate tokens and whitespace
10:36:13	<sshine>	is it a variable set of syntaxes you want to tokenize?
10:36:32	<sshine>	it's possible that writing your own crude tokenizers is cheap if you don't need the syntax trees.
10:37:31	→	gehmehgeh joins (~user@user/gehmehgeh)
10:38:26	<sshine>	I like the approach of tree-sitter because it tries to solve a problem across languages and provide FFI, so there's one place to put a parser, rather than to write a parser in each language for each language.
10:38:48	<sshine>	I'm surprised the tree-sitter package isn't in use.
10:39:05	<sshine>	it might be, and the warning is just a scare tactic. ;)
10:39:13	<abastro[m]>	Wouldn't writing own tokenizer be quite a burden
10:39:31	<[exa]>	the higher-level goal is that I have a nice diff&patch&diff3 tool here that is able to reasonably merge diffs with messed up whitespace and tokenization (think an effortless git merge of source formatted by hindent into source formatted by ormolu), and I'm struggling to get a generic way of parsing many interesting text formats easily (ranging from .txt to markdown, latex, CSVs all the way to normal
10:39:37	<[exa]>	programming)
10:39:54	<sshine>	also, eh, the tree-sitter package is littered with 'Ptr' types... seems very shallowly embedded.
10:41:03	<[exa]>	I was trying to come up with some kinda user-specifiable regex tokenizer but it's not as easy as one would expect, notably given the opinions hardcoded in current regex libraries
10:41:52	<sshine>	so... a whitespace remover that doesn't break programs for arbitrary syntaxes?
10:41:56	<[exa]>	then I thought it would be nice to have a runtime lexer library, literally flex that you can load directly into haskell
10:42:16	<[exa]>	and today I woke up remembering about them syntax highlighters
10:42:56	<[exa]>	unfortunately apparently this is okay for syntax highlighters: tokenize ... "int a = 5;" ==> [[(DataTypeTok,"int"),(NormalTok," a "),(OperatorTok,"="), ...]
10:43:04	<sshine>	so... I played around a lot with syntax highlighting in gedit and vim many years ago, and I remember that most syntax-highlighting libraries do things with regex and simple state machines, not lexing.
10:43:08	<[exa]>	so yeah the search continues!
10:45:25	<[exa]>	I mostly wanted to avoid problems from e.g. not recognizing the spaces in strings as actual content, and recognizing "actually required" spacing like the haskell "function application space"
10:47:16	<[exa]>	like, I guess most people would probably do with a simple C-like tokenizer, but that's a highly simplifying assumption (similar to the assumption of current difftools, "code is just lines")
10:48:04	<[exa]>	actually would it be possible to use vim as a library for this?
10:51:43	<[exa]>	tree-sitter has no distinction for whitespace either I see :(
10:52:06	<sshine>	sounds like it wouldn't be able to construct syntax tree for whitespace-sensitive languages then...
10:52:36	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 240 seconds)
10:52:54	<[exa]>	it does (it can do python) but the whitespace is marked very implicitly
10:53:23	<[exa]>	"1 + 2" seems to parse into: operator expression "1 + 2" that contains left operand "1" and right operand "2"
10:54:07	<sshine>	ah, and you want whitespace tokens.
10:54:13	<[exa]>	the " + " in the middle can be kinda deduced but man, is the whitespace significant?
10:54:22	<[exa]>	(is it even whitespace there?)
10:54:38	<[exa]>	ok nvm as I said, The Search Continues! :]
10:55:56	<sshine>	any interest in adding a reference to #haskell-beginners in #haskell's topic again? it was removed some years ago because the channel's topic was consistently used for advertising for a particular book, I believe. but it isn't any more.
10:58:40	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
10:59:09	<abastro[m]>	Used for advertising??
11:00:32	→	eotdlt^ joins (~eotdlt@96-91-136-49-static.hfc.comcastbusiness.net)
11:00:48	<[exa]>	sshine: I thought it is here mainly as a spillover for "ok let's move this to -beginners" for longer conversations here
11:00:56	<sshine>	so on freenode, I think #haskell-beginners was registered by bitemyapp, and he put a link to buy his book in the topic. I remember the day when the reference to the channel was removed because it seemed partisan, or something.
11:01:33	<sshine>	[exa], it is here for whatever :) I see some pretty advanced stuff going on in #haskell-beginners, since it's mostly a self-assessment thing whether you're a beginner.
11:02:09	<sshine>	[exa], but I think the one thing that the channel does is let people ask how to get the nth element of a list, because the name implies all questions are allowed.
11:02:44	<sshine>	[exa], nobody would frown at such questions here, but psychology, meh. :)
11:02:54	<[exa]>	yeah
11:03:07	<[exa]>	like, there's still plenty of space in the topic right?
11:03:08	<sshine>	the reference used to be there
11:06:22	→	AlexZenon joins (~alzenon@94.233.240.35)
11:08:03	×	AlexZenon_2 quits (~alzenon@94.233.240.35) (Ping timeout: 256 seconds)
11:08:42	→	acidjnk joins (~acidjnk@p200300d0c7049f825551b1368b4030e6.dip0.t-ipconnect.de)
11:13:09	×	benin quits (~benin@183.82.24.110) (Quit: The Lounge - https://thelounge.chat)
11:22:02	×	econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity)
11:24:03	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
11:25:19	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
11:30:12	<abastro[m]>	Sometimes `!! n` is useful tho
11:36:27	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Ping timeout: 260 seconds)
11:39:00	<sm>	a good article on [Infinite] Category Theory: https://news.ycombinator.com/item?id=30809385
11:40:50	×	DNH quits (~DNH@8.43.122.72) (Quit: My MacBook has gone to sleep. ZZZzzz…)
11:42:35	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds)
11:42:48	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 252 seconds)
11:43:13	<sm>	AFAIK #haskell-beginners never managed to separate itself from #haskell - there was no real difference in content - so it just created fragmentation. The concept seems good but I think to succeed it would need a clear scope different from #haskell's and some strong leadership/curation.
11:43:49	<sm>	(I haven't been hanging out there, so if things have changed let us know)
11:44:30	×	acidjnk quits (~acidjnk@p200300d0c7049f825551b1368b4030e6.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
11:45:17	→	ProfSimm joins (~ProfSimm@87.227.196.109)
11:45:36	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
11:46:23	<DigitalKiwi>	that's the great part about #haskell is you never know if it's a beginner or advanced phd thesis level question you're going to get sniped by
11:47:06	AlexNoo__	is now known as AlexNoo
11:47:18	<hpc>	yeah, i like having everything in one place
11:47:30	<hpc>	you're getting the whole community that way too
11:47:56	<DigitalKiwi>	and then you never have to be like "is this a beginner question or not"
11:48:10	<DigitalKiwi>	and you don't have to move lol
11:48:23	<hpc>	and more people answer questions
11:48:42	<hpc>	sometimes the best answers come from the people who don't normally answer "beginner questions"
11:49:03	<hpc>	because the question might accidentally touch on some really neat more advanced concept
11:49:35	<sm>	I often wished for a channel more... focussed on my needs as a haskell learner/new practitioner. Trouble is there's a wide variety of haskellers and typs of "beginner"
11:49:59	<DigitalKiwi>	and a lot of times something's out of left field or something like the answerer might have some knowledge about the topic but be beginner in haskell
11:50:50	<sm>	is someone wanting to chat about category theory a beginner ? in a sense, yes
11:52:02	<DigitalKiwi>	sm: you have to make #haskell the channel you want! what i mean is you have to ask questions. learning by osmosis isn't so good here. i've tried lol. i think that's probably partly because of the wide variety of topics that everyone asks. if you try to learn from their questions you will get lost
11:52:45	<sm>	maybe several beginner channels could work
11:52:58	<sm>	but, that requires organisation
11:54:02	<sm>	and really it would require chasing beginners out of here, which won't happen
11:54:25	<DigitalKiwi>	don't the scary phd questions do that enough ;D
11:55:17	<sm>	apparently not :)
11:57:18	sm	thinks a better next step would be a clearer overview/roadmap to existing channels
11:57:51	→	zer0bitz joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
11:58:44	<sm>	that would help folks wanting a more focussed chat find the right place
12:00:41	×	zer0bitz__ quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 272 seconds)
12:02:10	<sm>	in matrix, the #haskell-space:matrix.org helps. In IRC I expect there's a wiki page, but out of date
12:10:38	<sm>	some current matrix "members" counts, for what they're worth: #haskell:libera.chat 2487, #haskell:matrix.org 1791, #haskell-space:matrix.org 255
12:15:02	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
12:16:04	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
12:23:37	×	zer0bitz quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 240 seconds)
12:23:58	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
12:24:15	rustacean	is now known as razetime
12:25:07	×	razetime quits (~quassel@117.254.34.170) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
12:25:22	→	razetime joins (~quassel@117.254.34.170)
12:26:30	→	zer0bitz joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
12:30:08	→	zer0bitz_ joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
12:32:56	×	zer0bitz quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 260 seconds)
12:33:01	→	zer0bitz__ joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
12:34:11	×	Digit quits (~user@user/digit) (Ping timeout: 256 seconds)
12:36:46	×	zer0bitz_ quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 272 seconds)
12:36:48	×	geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
12:37:10	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
12:37:42	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
12:38:39	→	geekosaur joins (~geekosaur@xmonad/geekosaur)
12:40:04	×	cdman quits (~dcm@user/dmc/x-4369397) (Quit: Leaving)
12:42:27	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
12:49:59	×	razetime quits (~quassel@117.254.34.170) (Read error: Connection reset by peer)
12:50:33	→	zer0bitz joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
12:52:16	→	Digit joins (~user@user/digit)
12:52:36	×	zer0bitz__ quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 272 seconds)
12:52:38	→	CiaoSen joins (~Jura@p200300c95735b0002a3a4dfffe84dbd5.dip0.t-ipconnect.de)
12:52:39	×	joo-_ quits (~joo-_@fsf/member/joo--) (Ping timeout: 252 seconds)
12:53:23	→	CATS joins (apic@brezn3.muc.ccc.de)
12:54:25	→	joo-_ joins (~joo-_@87-49-146-72-mobile.dk.customer.tdc.net)
12:54:25	×	joo-_ quits (~joo-_@87-49-146-72-mobile.dk.customer.tdc.net) (Changing host)
12:54:25	→	joo-_ joins (~joo-_@fsf/member/joo--)
12:58:09	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
13:05:55	→	razetime joins (~quassel@117.254.34.170)
13:09:48	→	jonathanx joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se)
13:11:26	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
13:13:22	→	bahamas joins (~lucian@84.232.140.158)
13:16:10	×	Everything quits (~Everythin@37.115.210.35) (Quit: leaving)
13:19:00	×	joo-_ quits (~joo-_@fsf/member/joo--) (Ping timeout: 240 seconds)
13:20:56	→	joo-_ joins (~joo-_@87-49-146-56-mobile.dk.customer.tdc.net)
13:20:56	×	joo-_ quits (~joo-_@87-49-146-56-mobile.dk.customer.tdc.net) (Changing host)
13:20:56	→	joo-_ joins (~joo-_@fsf/member/joo--)
13:21:46	×	hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection)
13:23:14	→	hololeap joins (~hololeap@user/hololeap)
13:34:22	→	zer0bitz_ joins (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi)
13:35:55	×	zer0bitz quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 260 seconds)
13:43:08	→	cdman joins (~dcm@user/dmc/x-4369397)
13:54:47	→	DNH joins (~DNH@8.43.122.72)
14:01:06	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
14:11:05	×	bahamas quits (~lucian@84.232.140.158) (Ping timeout: 256 seconds)
14:16:03	→	[itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
14:16:14	×	CiaoSen quits (~Jura@p200300c95735b0002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
14:18:57	→	justsomeguy joins (~justsomeg@user/justsomeguy)
14:23:50	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
14:38:43	<janus>	sm: i think lower volume channels like #haskell-in-depth may be better for beginners, since you'd only get one answer
14:39:33	<[exa]>	b...b...but
14:39:38	<[exa]>	answer polymorphism!
14:47:49	<abastro[m]>	Ad-hoc polymorphic answers?
14:50:34	→	bahamas joins (~lucian@84.232.140.158)
14:53:25	×	DNH quits (~DNH@8.43.122.72) (Ping timeout: 240 seconds)
14:54:17	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
14:57:00	×	bahamas quits (~lucian@84.232.140.158) (Ping timeout: 240 seconds)
15:04:57	→	AlexZenon_2 joins (~alzenon@94.233.240.35)
15:06:37	×	AlexZenon quits (~alzenon@94.233.240.35) (Ping timeout: 256 seconds)
15:10:15	×	DigitalKiwi quits (~kiwi@2604:a880:400:d0::12fc:5001) (Quit: quite.)
15:12:55	<dsal>	ProfSimm: it's odd that you think it was overlooked and not a conscious decision.
15:13:39	×	cdman quits (~dcm@user/dmc/x-4369397) (Quit: Leaving)
15:18:18	×	img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
15:20:28	<ProfSimm>	dsal: I'm writing a language which has very similar application chain to haskell's, so I have the same problem with unary minus
15:20:41	<ProfSimm>	dsal: and frankly it's making me rethink my entire life.
15:20:54	<ProfSimm>	dsal: but that's just me being perfectionist.
15:20:59	<geekosaur>	unary minus has always been a problem
15:21:09	<ProfSimm>	dsal: but this is why I wonder about Haskell
15:21:17	<geekosaur>	different languages have different solutions, and they all have weird pain points
15:21:19	<abastro[m]>	Whh
15:21:33	<dsal>	It depends on what you consider perfect. Special cases are blemishes.
15:21:48	<ProfSimm>	geekosaur: unary minus is not a problem when you have no application chain like Haskell I think.
15:21:49	<geekosaur>	makes me wish everyone had gone with the solutionof just choosing a different operator character (at least one uses ~ instead of -)
15:21:57	<ProfSimm>	geekosaur: for example in most language you need () around params, so
15:22:02	<ProfSimm>	foo (-5) is not an issue
15:22:14	<ProfSimm>	In haskell though foo -5 vs foo - 5 is a problem
15:22:42	<geekosaur>	it makesit more obvious, but there are still weird corner cases, they're just less common in many languages
15:22:43	<ProfSimm>	geekosaur: math notation sucks
15:22:47	→	img joins (~img@user/img)
15:23:25	<ProfSimm>	dsal: I'm thinking of maybe only allowing bare identifiers outside parens in the chain
15:23:38	<dsal>	Adding lots of punctuation all the time just so you don't have to add punctuation that one rare time doesn't seem like a good trade-off.
15:23:44	<ProfSimm>	dsal: so you need to write: foo bar (12) baz ("text") something somethin qux
15:24:17	<ProfSimm>	dsal: well
15:25:14	<ProfSimm>	dsal: I implemented the 'no space' trick from the plugin you linked me to, try this (no quotes): foo - 5, foo -5 here: https://www.coltram.com/proto/
15:25:21	<ProfSimm>	dsal: it seems too subtle doesn't it
15:26:35	<ProfSimm>	dsal: I can also cover the case of foo-5 being binary minus (currently parsed as unary)
15:26:44	<ProfSimm>	But I don't like 'blemishes'
15:27:05	<dsal>	I've never used it because it's never mattered to me. I don't have enough negative literals in my code to justify such a special case.
15:27:21	<ProfSimm>	dsal curious
15:27:40	<dsal>	I'm a somewhat positive person.
15:27:42	<ProfSimm>	dsal: you don't recall sometimes writing "something -1" and then cursing why it doesn't work like you expected?
15:27:51	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
15:28:19	<dsal>	Sure. Part of every day I write code the compiler tells me something stupid I did.
15:28:31	<hpc>	i am more of the "i don't care if it works, don't write 'something -1'" kind of person
15:28:59	<ProfSimm>	hpc: I'm curious why. Isn't it a pretty common think to pass a number to a function
15:29:02	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds)
15:29:04	<ProfSimm>	thing*
15:29:20	<ProfSimm>	hpc: how do you write it
15:30:36	<hpc>	with parens, or i try to dodge the use of negative literals
15:30:56	→	eddiemundo joins (~eddiemund@2001:470:69fc:105::a80)
15:31:05	<hpc>	this isn't a problem unique to haskell, haskell is just one of the few languages that doesn't try to guess what you mean
15:31:10	<ProfSimm>	hpc: it makes it sound like it's consciously on your mind to avoid the situation
15:31:17	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4)
15:31:18	<hpc>	C also has this issue with *
15:31:27	<hpc>	C++ has this issue with all sorts of operators
15:31:32	<hpc>	it's a pretty common thing
15:31:34	<ProfSimm>	hpc: oh what's the issue with C
15:31:48	<hpc>	are you multiplying, or are you dereferencing
15:32:10	<hpc>	the ambiguity happens when you're also doing a type cast at the same time
15:32:15	<hpc>	(abc) *def
15:32:32	<ProfSimm>	hpc: I was thinking about introducing the concept of left/right "bias" on the operator, depending on surrounding whitespace: foo-5 (no bias) foo - 5 (no bias) foo- 5 (left bias) foo -5 (right bias), and using the bias to resolve conflicts. What do you think?
15:32:35	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
15:33:24	<ProfSimm>	hpc: it plays with whitespace which feels dangerous, but it's very intuitive to a human being
15:33:29	<hpc>	it's reasonable, i think
15:33:42	<hpc>	or for extra fun, what if you always needed spaces
15:33:53	<hpc>	foo-5 isn't subtraction, it's a single name
15:34:12	<ProfSimm>	hpc: I've considered it, especially since I wanted dash in names. But I suspect it'll be annoying to people
15:34:12	<hpc>	now you can be like powershell :P
15:35:20	<ProfSimm>	hpc: my decision against it was consistency. I require space around - and +, fine, but what about / and * ? What about exponentiation ^? And finally, what about operators like comma, semicolon, colon and so on
15:35:41	<abastro[m]>	`let n = -1 in f n`
15:35:43	<ProfSimm>	hpc: if there'll be rule I prefer it be one rule for all operators
15:36:53	<ProfSimm>	hpc: interestingly, whitespace "bias" would resolve the C example you gave me: foo* bar vs foo *bar
15:37:05	<ProfSimm>	hpc: thanks for the feedback I might actually do it
15:37:13	×	zyklotomic quits (~ethan@r4-128-61-94-5.res.gatech.edu) (Ping timeout: 256 seconds)
15:37:43	<abastro[m]>	I wonder what happens in C if you do `i---j`
15:37:44	<geekosaur>	whitespace bias is already a thing in ghc9.x
15:38:03	<ProfSimm>	geekosaur: oh is it. Where can I read about it/
15:38:13	<geekosaur>	C uses LTM so it should be i-- - j
15:38:39	<abastro[m]>	Confuusssing
15:38:58	<ProfSimm>	My parser would resolve this to subtract(i, neg(neg(j)))
15:39:06	→	zyklotomic joins (~ethan@res380d-128-61-83-1.res.gatech.edu)
15:39:15	<geekosaur>	GHC is now more sensitive to whitespace between infix operators and their arguments, requiring it in some cases where it was not previously necessary as the result of the whitespace-sensitive operator parsing proposal. It also affects the usage of !,``~`` and @ as BangPatterns, irrefutable patterns and type applications respectively. This means that expressions that were parsed as visible type applications in previous versions when the @ was
15:39:15	<geekosaur>	surrounded by whitespace will now be parsed as an operator application. For more details see the migration guide on the wiki.
15:39:22	<geekosaur>	per the release notes
15:39:45	<geekosaur>	this subsumes a bunch of ad hoc rules used by various other extensions
15:40:04	<ProfSimm>	geekosaur: niccccee, this kinda supports me going in this direction myself
15:40:26	→	bahamas joins (~lucian@84.232.140.158)
15:42:01	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
15:42:25	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
15:44:42	<ProfSimm>	Long live significant whitespace i guess
15:46:03	×	eldritch quits (~eldritch@user/eldritch) (Quit: bye)
15:46:03	×	glider quits (~glider@user/glider) (Quit: ZNC - https://znc.in)
15:46:03	×	anderson quits (~ande@user/anderson) (Quit: bye)
15:47:25	→	alp joins (~alp@user/alp)
15:49:52	<maerwald>	yeah, I love it when a whitespaces changes the meaning of my program :D
15:50:10	<maerwald>	it's the dark matter of programming
15:50:34	→	lagash joins (lagash@lagash.shelltalk.net)
15:50:57	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Ping timeout: 240 seconds)
15:51:25	×	gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving)
15:55:55	×	boxscape_ quits (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
15:56:24	→	anderson joins (~ande@user/anderson)
15:56:46	<ProfSimm>	maerwald: butletsfaceiteverylanguagereliesonwhitespaceinsomeway
15:57:40	<dsal>	This is not a perl channel.
15:58:23	<hpc>	hey, even perl has acme::bleach
15:58:34	<geekosaur>	that's an empty program in Whitespace }:>
15:58:42	<dsal>	haha. all comments
15:59:06	<dsal>	The best thing about programming is that any statement about programming is false.
16:00:22	<ProfSimm>	dsal: why
16:00:30	<ProfSimm>	dsal: all my statements are true :P
16:01:15	<dsal>	My language only supports unary logic.
16:01:30	→	eldritch_ joins (~eldritch@user/eldritch)
16:01:53	<ProfSimm>	dsal: in my language every single value can be true or false independently of its contents
16:02:10	<ProfSimm>	you can have true 0 false 0, true "true", false "true" and so on
16:02:21	<ProfSimm>	lots of fun
16:02:48	<geekosaur>	snobol
16:03:00	<geekosaur>	where it's success/failure instead of true/false
16:03:07	→	glider joins (~glider@user/glider)
16:03:43	<ProfSimm>	geekosaur: oh it does that what i described?
16:04:20	<dsal>	But for the most part, when someone says "programming languages do X", there's a counterexample of a programming language that does not do X.
16:04:59	<dsal>	I like languages that go all-in on boolean blindness by making it so that you can treat everything as a boolean.
16:05:38	<ProfSimm>	dsal: that;s what I did, but maybe not as typically done
16:05:51	<ProfSimm>	dsal: everything is a boolean.
16:06:13	<ProfSimm>	dsal: but it's more of a replacement for returning result or throwing exception.
16:06:18	<ProfSimm>	It calls one of two continuations
16:06:22	<ProfSimm>	then or else
16:08:05	<dsal>	So, Either?
16:08:13	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
16:08:49	<ProfSimm>	dsal: in a way yes, but the integration with the syntax and every value makes it take on a different flavor
16:08:55	<dsal>	Either is much less of a problem for boolean blindness
16:08:57	<monochrom>	Haha that reminds me. Robert Harper critiqued boolean blindness, right? And then in his textbook, he went on to explain parametricity in System F by adding only one type: boolean. >:)
16:09:23	<ProfSimm>	dsal: for example this is if/then/else and ternary, no need for dedicated operators: if & then \| else
16:09:49	<ProfSimm>	dsal: this is also chaining actions and handling errors: do1 & do2 & do3 & do4 \| handleError
16:10:21	<ProfSimm>	dsal: basicaly an entire method is a single expression, like Haskell, but booleans do the flow control
16:11:02	<ProfSimm>	It gets very interesting honestly
16:11:17	<ProfSimm>	I like when things fit together and 5 things end up being 1 thing
16:11:21	<ProfSimm>	simplification
16:14:00	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
16:14:24	<ProfSimm>	I think having booleans as distinct values may be an error
16:14:54	<ProfSimm>	in machine code you almost never use such values. Sometimes you "jump if zero" or "not zero"
16:15:04	<ProfSimm>	But way more often you directly jump from a comparison operation etc.
16:15:07	<ProfSimm>	No boolean values
16:15:26	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
16:16:28	→	`2jt joins (~jtomas@210.red-88-24-179.staticip.rima-tde.net)
16:16:32	<ProfSimm>	if (x > 0 && x < 10) print("x in range"); else print("x not in range"); ----> x > 0 & x < 10 & print("x in range") \| print ("x not in range")
16:16:47	<geekosaur>	looks like bash scripting
16:16:54	<ProfSimm>	Probably
16:17:17	<geekosaur>	[ x > 0 && x < 10] && echo x in range \|\| echo x not in range
16:17:36	<ProfSimm>	geekosaur: yeah. In Lua they also use && and \|\| as ternary
16:18:00	<ProfSimm>	geekosaur: there's a gotcha though, if "echo x in range" returns falsy value, your "else" will run
16:18:09	<geekosaur>	that's not ternary, it's just how && and \|\| associate
16:18:14	<ProfSimm>	geekosaur: in my case there's no such danger because all values are true by default
16:18:47	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 250 seconds)
16:18:50	<ProfSimm>	geekosaur: I knot it's not ternary, but my point is it's used as such
16:19:03	<ProfSimm>	geekosaur: but consider: 1 && 0 \|\| 2
16:19:14	<ProfSimm>	Here you may hope to see 0 as a result, but you'll see 2
16:19:41	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
16:19:43	<ProfSimm>	In my lang, 1 & 0 \| 2 will produce 0
16:19:49	<ProfSimm>	Because 0 is not "falsey"
16:20:09	<ProfSimm>	You have to explicitly write "x != 0"
16:21:11	<ProfSimm>	You can turn any value at all into false with not: !"something" ---> becomes a falsey string "something"
16:21:35	<hpc>	so every value has a completely independent truthiness attached to it?
16:21:48	<ProfSimm>	hpc: yes, and it's true for all by default
16:21:50	<hpc>	neat
16:21:52	<geekosaur>	again this sounds like snobol/icon
16:21:59	×	infinity0 quits (~infinity0@occupy.ecodis.net) (Ping timeout: 256 seconds)
16:22:03	<ProfSimm>	geekosaur: where can I see examples of snobo
16:22:06	<ProfSimm>	Sounds curious
16:22:10	<geekosaur>	success/failure is distinct from boolean false/true
16:22:17	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
16:22:41	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 250 seconds)
16:22:43	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
16:22:43	<geekosaur>	you might find icon more approachable as snobol was from the punched card days
16:23:03	→	tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net)
16:23:04	<geekosaur>	https://en.wikipedia.org/wiki/Icon_(programming_language)
16:24:21	×	vysn quits (~vysn@user/vysn) (Remote host closed the connection)
16:24:37	×	Teacup quits (~teacup@user/teacup) (Quit: Teacup)
16:24:37	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
16:24:49	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
16:25:27	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
16:25:30	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 252 seconds)
16:25:50	<ProfSimm>	hpc: technically !something wraps something in not(something). What not does is swap then -> else and else -> then for the value. Every other interface is proxied transparently through not to something.
16:26:16	<ProfSimm>	But it works as if there's a boolean attached to every value.
16:26:26	<ProfSimm>	Internally every value is true, unless wrapped in odd number of "nots"
16:28:11	<ProfSimm>	geekosaur: I don't understand icon, says a < b will return b, if b is bigger. what does if (a<b) mean then
16:30:31	<ProfSimm>	I think i get it
16:30:48	<geekosaur>	a < b fails if b is not bigger. if looks only at success/failure
16:30:48	×	geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
16:30:48	→	Vajb joins (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813)
16:31:13	→	Teacup joins (~teacup@user/teacup)
16:32:19	×	ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
16:32:29	→	geekosaur joins (~geekosaur@xmonad/geekosaur)
16:32:42	→	ChaiTRex joins (~ChaiTRex@user/chaitrex)
16:32:45	<geekosaur>	this allows a < b to produce b if it'sbigger, which allows chaining comparisons (e.g. if 3 < x < 10)
16:33:23	<geekosaur>	(sorry, network around here sucks)
16:35:44	<ProfSimm>	geekosaur: got it
16:36:06	<ProfSimm>	geekosaur: seems similar indeed. But FAIL can't carry information it seems
16:36:13	<geekosaur>	no, it can't
16:36:28	<geekosaur>	internally failing is the same as producing &fail
16:36:35	<ProfSimm>	In my case I use "falsey" values to carry error information (or other information for the else case as needed)
16:36:35	→	vglfr joins (~vglfr@88.155.46.233)
16:37:11	<geekosaur>	hm, actually I'm not certain of that, it may be possible toextract information from a fail. I'm not an icon wizard
16:37:19	<ProfSimm>	:)
16:37:33	<ProfSimm>	geekosaur: it's full of languages in the 80s that do things I do
16:37:49	<ProfSimm>	geekosaur: either I'm about to learn why they failed... or we branched onto a dark timeline since
16:38:17	<geekosaur>	I still think if the current version of icon (unicon) had been around earlier, it might have prevented the rise of perl
16:38:42	<ProfSimm>	geekosaur: for a new language to rise now it needs a killer app
16:38:53	<geekosaur>	that said, icon uses snobol-like patterns insteadof regexes so perl might still have won solely because of that
16:39:36	<geekosaur>	the world needed something better than shell scripting. unicon andperl both offered that… but unicon came too late and earlier versions of icon didn't really fill the need
16:39:56	<maerwald>	what's wrong with shell
16:40:32	<geekosaur>	generally once you reach around 10 lines of shell you're either beating your head against a wall or making a major mistake :)
16:41:05	<geekosaur>	everything being a string with (back then) limited manipulation ability didn't help
16:41:27	<geekosaur>	these days bash and zsh both offer advenced programming features, but they didn't back then
16:42:08	<geekosaur>	no arrays (well, zsh had simple ones on a par with (t)csh), limited number handling,etc.
16:42:25	<geekosaur>	you could fake arrays even in bourne shell with some evil eval tricks, but still
16:42:41	<hpc>	the current bash arrays are not much better :P
16:42:56	<ProfSimm>	What did "bash" mean
16:42:58	<ProfSimm>	Batch shell?
16:43:05	<maerwald>	who needs arrays, just pick some delimiter and hope it works
16:43:05	<geekosaur>	"bourne-again shell"
16:43:10	<ProfSimm>	oh
16:43:22	<geekosaur>	reference to unix shell history
16:44:24	<hpc>	you get a similar sort of history with vim
16:44:31	<hpc>	vi improved
16:44:50	×	aliosablack quits (~chomwitt@2a02:587:dc18:da00:e2ec:eb52:4039:9bfe) (Quit: Leaving)
16:45:04	<hpc>	vi is visual editor, because its predecessor was ed
16:45:20	<hpc>	or maybe sed?
16:45:47	<hpc>	you would print out your program on paper, and then use ed/sed to make individual line edits without being able to actually see the file on the computer
16:46:12	<geekosaur>	vi was visual ex, ex was enhanced ed
16:46:22	<hpc>	ah, right
16:46:50	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
16:46:51	<hpc>	back in those days, just catting out a file was enough to make your network connection chug
16:47:03	<hpc>	and that's assuming your teletype wasn't an actual typewriter
16:49:03	→	boxscape_ joins (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de)
16:51:36	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 245 seconds)
16:52:45	<monochrom>	Quite remarkable that coding style guides of those days were obsessed with using magic numbers to express "we mean to say that each function should fit on one page".
16:52:46	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
16:54:08	→	DigitalKiwi joins (~kiwi@159.223.106.6)
16:57:05	→	ss- joins (~ss-@187.83.249.216.dyn.smithville.net)
16:58:01	<ProfSimm>	monochrom: they should gzipped the code and printed it in base64
16:58:31	<monochrom>	Wait, the irony of the person who changed ghcup from written-in-bash to written-in-Haskell asking "what's wrong with shell?" hahaha
16:58:58	×	bahamas quits (~lucian@84.232.140.158) (Ping timeout: 272 seconds)
17:00:29	<hpc>	monochrom: that's the beauty of those old spooled printers, a page was as long as you wanted it to be :P
17:01:30	<ss->	I've got a stack project where some files have a preprocessor run over them with {-# OPTIONS_GHC -F -pgmF=myPreprocessor #-}. everything works as expected, except that when I get a compile error with stack build, it points to a randomly-numbered temporary file e.g. ghc_42.hspp rather than the original module. I don't mind the line numbers being off
17:01:30	<ss->	(though the preprocessor does preserve line numbers), but is there an easy way to get the original file name to show up in error messages?
17:02:19	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 250 seconds)
17:03:31	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
17:04:34	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
17:05:35	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
17:07:14	<geekosaur>	ss-, the preprocessor would need to add LINE pragmas specifying the original file name and ideally line number
17:07:21	<geekosaur>	otherwise ghc has no idea
17:07:49	<geekosaur>	ProfSimm, you've never had to debug from a memory image printout
17:08:31	<geekosaur>	my first year of college, I did. (only once. after that I got myself a COBOL compiler I could use at home with a more sensible debugging environment)
17:10:05	<ss->	geekosaur oh, got it! thanks!
17:10:29	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
17:14:06	→	mc47 joins (~mc47@xmonad/TheMC47)
17:15:23	×	ss- quits (~ss-@187.83.249.216.dyn.smithville.net) (Quit: Client closed)
17:16:21	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Quit: WeeChat 3.4.1)
17:16:32	×	razetime quits (~quassel@117.254.34.170) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
17:17:17	×	vglfr quits (~vglfr@88.155.46.233) (Ping timeout: 256 seconds)
17:18:23	→	gehmehgeh joins (~user@user/gehmehgeh)
17:24:12	×	dextaa_ quits (~dextaa@user/dextaa) (Remote host closed the connection)
17:24:24	→	jbox joins (~jbox@user/jbox)
17:24:33	×	Teacup quits (~teacup@user/teacup) (Remote host closed the connection)
17:24:48	→	Teacup joins (~teacup@user/teacup)
17:25:08	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
17:26:05	×	nautical quits (~nautical@2601:602:900:1630::7cbb) (Quit: WeeChat 3.4)
17:26:39	×	jbox quits (~jbox@user/jbox) (Read error: Connection reset by peer)
17:27:12	×	kosmikus quits (~kosmikus@nullzig.kosmikus.org) (Quit: Lost terminal)
17:29:50	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
17:30:11	×	eotdlt^ quits (~eotdlt@96-91-136-49-static.hfc.comcastbusiness.net) (Remote host closed the connection)
17:31:09	×	mrmonday quits (~robert@what.i.hope.is.not.a.tabernaevagant.es) (Quit: .)
17:31:15	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
17:33:04	→	mrmonday joins (~robert@what.i.hope.is.not.a.tabernaevagant.es)
17:33:30	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
17:35:52	×	pavonia quits (~user@user/siracusa) (Quit: Bye!)
17:37:16	→	Unicorn_Princess joins (~Unicorn_P@93-103-228-248.dynamic.t-2.net)
17:42:22	→	nattiestnate joins (~nate@202.138.250.62)
17:44:01	→	infinity0 joins (~infinity0@occupy.ecodis.net)
17:47:01	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds)
17:49:06	→	chomwitt joins (~chomwitt@2a02:587:dc18:da00:e2ec:eb52:4039:9bfe)
17:49:22	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
17:52:15	×	Vajb quits (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) (Read error: Connection reset by peer)
17:52:49	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
17:55:44	→	Guest98 joins (~Guest98@82.212.116.123)
17:57:57	→	vglfr joins (~vglfr@88.155.46.233)
17:59:27	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
17:59:31	→	dextaa_ joins (~dextaa@user/dextaa)
17:59:48	→	Sgeo joins (~Sgeo@user/sgeo)
18:00:07	×	ddb quits (~ddb@2607:5300:203:9993::196) (Quit: WeeChat 3.4)
18:05:11	×	deadmarshal_ quits (~deadmarsh@95.38.230.121) (Ping timeout: 260 seconds)
18:25:30	×	Teacup quits (~teacup@user/teacup) (Remote host closed the connection)
18:27:21	<maerwald>	monochrom: xD
18:29:51	×	boxscape_ quits (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de) (Ping timeout: 250 seconds)
18:32:46	→	Teacup joins (~teacup@user/teacup)
18:33:04	×	dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection)
18:34:58	→	simendsjo joins (~user@84.211.91.241)
18:36:40	→	bahamas joins (~lucian@84.232.140.158)
18:42:03	×	kaph quits (~kaph@net-109-116-124-149.cust.vodafonedsl.it) (Ping timeout: 260 seconds)
18:44:12	×	`2jt quits (~jtomas@210.red-88-24-179.staticip.rima-tde.net) (Remote host closed the connection)
18:44:35	→	`2jt joins (~jtomas@210.red-88-24-179.staticip.rima-tde.net)
18:48:29	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 250 seconds)
18:50:22	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
18:50:27	→	econo joins (uid147250@user/econo)
18:53:27	×	justOkay quits (~justache@user/justache) (Read error: Connection reset by peer)
18:54:24	→	justOkay joins (~justache@user/justache)
18:55:20	→	pera joins (~pera@user/pera)
18:56:11	→	CodeKiwi joins (~kiwi@137.184.156.191)
18:57:16	→	danso joins (~danso@danso.ca)
18:58:24	→	rond_ joins (~rond_@90.254.208.190)
18:59:15	×	simendsjo quits (~user@84.211.91.241) (Ping timeout: 268 seconds)
18:59:48	<danso>	is there a standard way of running an action only for a Left value, as in `\ f act -> \case { Left l -> f l >> act ; Right _ -> act }`
18:59:52	←	jakalx parts (~jakalx@base.jakalx.net) (Error from remote client)
19:00:07	→	boxscape_ joins (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de)
19:00:29	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
19:01:14	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
19:02:11	×	gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection)
19:02:32	<Rembane>	danso: There's left from Control.Arrow and first from Data.Bifunctor.
19:02:56	→	gehmehgeh joins (~user@user/gehmehgeh)
19:06:02	×	tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Ping timeout: 268 seconds)
19:08:31	×	dextaa_ quits (~dextaa@user/dextaa) (Remote host closed the connection)
19:10:00	<danso>	thanks, will investigate.
19:10:48	→	pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
19:12:55	→	solrize joins (~solrize@user/solrize)
19:13:49	<danso>	Rembane, i'm not sure that is what i mean. left/first returns an Either l r
19:14:04	<danso>	my function does something with the Left value, then discards it
19:15:04	×	hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection)
19:16:26	→	hololeap joins (~hololeap@user/hololeap)
19:16:46	<geekosaur>	either (\l -> f l) (const ()) >> act
19:16:50	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
19:17:38	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
19:17:39	<Rembane>	danso: Oh, then use geekosaur's solution.
19:17:58	<geekosaur>	uh rught, I rearranged that after. either f (const ()) >> act
19:19:00	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
19:19:05	<Rembane>	I wonder if void . left act would do the same thing.
19:19:12	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
19:20:35	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
19:20:50	→	acidjnk joins (~acidjnk@p200300d0c7049f8284fff18517a389b2.dip0.t-ipconnect.de)
19:22:53	<danso>	there might not be an idiomatic way of doing it. the type i want is (l -> IO ()) -> IO () -> Either l () -> IO ()
19:23:39	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
19:24:02	<Rembane>	danso: EitherT might help you there.
19:25:02	→	dextaa_ joins (~dextaa@user/dextaa)
19:33:47	×	bahamas quits (~lucian@84.232.140.158) (Ping timeout: 268 seconds)
19:34:27	×	wolfshappen quits (~waff@irc.furworks.de) (Read error: Connection reset by peer)
19:35:15	×	alp quits (~alp@user/alp) (Ping timeout: 252 seconds)
19:36:38	<[exa]>	"acting on Left value" sounds a tiny bit like `catch` to me
19:37:55	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds)
19:39:06	<[exa]>	(from Control.Monad.Catch, with `e~SomeException => Left e a` not the IO one)
19:39:16	<[exa]>	(s/Left/Either/ whoops)
19:40:00	→	jgeerds joins (~jgeerds@55d4548e.access.ecotel.net)
19:40:59	→	boxscape_12 joins (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de)
19:41:02	×	boxscape_12 quits (~boxscape_@p4ff0b60b.dip0.t-ipconnect.de) (Client Quit)
19:42:05	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
19:42:37	×	CodeKiwi quits (~kiwi@137.184.156.191) (Ping timeout: 240 seconds)
19:44:36	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Ping timeout: 252 seconds)
19:47:48	→	michalz joins (~michalz@185.246.204.119)
19:47:54	→	justsomeguy joins (~justsomeg@user/justsomeguy)
19:48:01	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
19:48:04	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
19:48:16	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
19:49:32	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
19:50:08	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
19:53:52	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
19:56:07	→	CodeKiwi joins (~kiwi@137.184.156.191)
19:59:55	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds)
20:00:05	<maerwald>	danso: either f (\_ -> pure ())?
20:00:07	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
20:00:29	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
20:02:35	→	jakalx joins (~jakalx@base.jakalx.net)
20:03:49	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
20:04:24	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
20:09:24	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
20:09:33	×	rond_ quits (~rond_@90.254.208.190) (Quit: Client closed)
20:09:36	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
20:11:03	→	Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
20:11:33	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
20:12:01	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
20:12:07	×	Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
20:12:39	×	vglfr quits (~vglfr@88.155.46.233) (Ping timeout: 252 seconds)
20:13:14	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
20:13:47	Lord_of_Life_	is now known as Lord_of_Life
20:15:37	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 240 seconds)
20:17:09	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
20:18:28	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
20:18:41	→	pavonia joins (~user@user/siracusa)
20:18:44	→	unit73e joins (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291)
20:19:58	<unit73e>	hey. finally got xp3 extract working with the dumbest method. just use drop and take in a bytearray many times... not very efficient but apparently xp3 segments can be any range, including intersect with other ranges.
20:20:27	<unit73e>	hopefully it doesn't exaust memory in large files
20:21:54	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
20:24:10	×	DigitalKiwi quits (~kiwi@159.223.106.6) (Quit: quite.)
20:24:46	→	wolfshappen joins (~waff@irc.furworks.de)
20:25:14	CodeKiwi	is now known as DigitalKiwi
20:27:55	×	zer0bitz_ quits (~zer0bitz@dsl-hkibng32-54fbf8-224.dhcp.inet.fi) (Ping timeout: 256 seconds)
20:28:24	×	takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
20:29:24	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
20:30:02	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
20:33:52	→	Pickchea joins (~private@user/pickchea)
20:35:55	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
20:36:25	×	_ht quits (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection)
20:38:15	→	deadmarshal_ joins (~deadmarsh@95.38.230.121)
20:40:00	×	jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 272 seconds)
20:43:10	×	deadmarshal_ quits (~deadmarsh@95.38.230.121) (Ping timeout: 272 seconds)
20:43:21	<hololeap>	lets say you build a library with -O2 and install it globally, then build an executable which uses dynamic linking. would the -O2 potentially affect the executable's performance?
20:45:41	<hololeap>	I would think it would, but I just wanted to double check
20:47:31	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
20:48:21	<geekosaur>	the shared object includes an abi hash which includes among other things optimization level, so (a) when you build the executable you have to specify you want the -O2 version of the library or it'll build it again with -O1 (cabal / stack default) (2) it'll only use that shared library, not one with a different optimization level
20:48:50	<sm>	if building with cabal or stack, I had the impression they would always build deps optimised, and only your project's local packages, or the packages you requested on the command line, would be affected
20:49:05	<geekosaur>	this is one of the reasons we don't usually build shared; it doesn't gain you anything with ghc, since abi hashes have to match or bad things happen
20:50:12	<hololeap>	right, but the optimization level of the library will affect performance when you eventually use it
20:50:21	<geekosaur>	with cabal you can stick a stanza like "package *\n optimization: 2" in your cabal.project
20:51:02	<hololeap>	it's probably such an obvious question that it's difficult to answer
20:51:19	<geekosaur>	and if you don't do that or the equivalent, it'll go for -O1, look and see no cached build at -O1,and build it all over again
20:51:27	<sm>	this is haskell tooling, nothing is obvious :)
20:51:56	<hpc>	sufficiently researched nuance is indistinguishable from obvious
20:52:06	AlexZenon_2	is now known as AlexZenon
20:52:28	<hololeap>	hypothetically, this isn't using cabal-v2, so there is no chance that it will rebuild the library
20:53:05	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
20:53:38	<napping>	hololeap: I think the sticky point is that ghc can't actually produce an single executable that would be capable of using either the O1 or O2 version of the library, so it's not exactly a change. But yes, executable and library built with -O2 ought to be faster than executable and library built from the same source with -O1
20:53:42	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
20:54:50	<hololeap>	oh, sorry, I didn't mean to imply that the executable could be linked to both -O1 and -O2. I just wanted to confirm that -O2 on the library will affect performance on the executable
20:54:58	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
20:55:00	<hololeap>	ok
20:55:35	<hpc>	is testing it infeasible?
20:56:00	<hololeap>	no, I just wanted a general response, because like sm said, haskell is full of surprises
20:56:17	<geekosaur>	-O2 will affect it but may do so oddly because of laziness
20:56:49	<geekosaur>	like, of an optimized portion forces a thunk that was generated by lower optimization code, it'll confuse your timings
20:57:43	<geekosaur>	which is another reason to build everything at the same optimization level: it can be really hard to tell. (plus -O2 doesn't often make much of a runtime difference over -O1)
20:57:57	×	DigitalKiwi quits (~kiwi@137.184.156.191) (Quit: quite.)
20:58:17	<hololeap>	without any flags, does it default to -O0?
20:58:36	→	DigitalKiwi joins (~kiwi@137.184.156.191)
20:58:42	<hololeap>	I would like to use -O2 on everything, but I've got limited ram on this system
20:58:51	<hololeap>	so I was just curious
21:02:40	<sclv>	without any flags we default to O1 and that's what's recommended.
21:02:56	<hololeap>	ok, good
21:03:16	<sclv>	only certain very specific packages will benefit significantly from O2, and often at an undesired cost not only in compilation time but generated binary size
21:03:32	<sclv>	and it may even be that the blowup in binary size hurts caches in a way that undercuts the optimization
21:05:24	<hololeap>	I noticed that aeson has a 'fast' flag
21:06:46	<hololeap>	if flag(fast); ghc-options: -O0; else; ghc-options: -O2
21:07:25	<hololeap>	I guess they took that out in v2
21:08:15	<hololeap>	but I take that to mean that they decided -O2 was worth it most of the time for that lib
21:08:35	<sclv>	i imagine fast was for development, but they decided they could just pass it manually
21:08:41	×	mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection)
21:09:00	<hololeap>	I'm more curious about the -O2 by default
21:09:19	<sclv>	well something like aeson it really matters for because it really relies on pervasive inlining
21:09:42	<sclv>	O2 is basically about how much you try to expand and inline, so it especially especially matters when there's fusion stuff happening
21:10:12	<hololeap>	I see
21:11:02	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
21:11:35	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
21:16:44	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
21:20:36	→	tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net)
21:22:09	→	tremon joins (~tremon@83-84-18-241.cable.dynamic.v4.ziggo.nl)
21:23:15	×	michalz quits (~michalz@185.246.204.119) (Remote host closed the connection)
21:23:56	×	Axman6 quits (~Axman6@user/axman6) (Ping timeout: 260 seconds)
21:26:19	→	cosimone joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20)
21:30:40	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Remote host closed the connection)
21:30:53	×	cosimone quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Read error: Connection reset by peer)
21:30:57	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
21:35:58	×	gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving)
21:38:55	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
21:40:33	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
21:41:06	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
21:42:19	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
21:42:32	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
21:42:39	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
21:42:55	×	wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 240 seconds)
21:43:20	×	perrierjouet quits (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Ping timeout: 272 seconds)
21:43:33	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
21:44:45	<sm>	possible addition for https://www.extrema.is/articles/haskell-books, tcard: https://www.reddit.com/r/haskell/comments/tpsbti/new_early_access_book_functional_programming_for
21:48:35	<tcard>	sm: Thank you! With the current policy, however, I only put books that are complete in the index. Early access books are not in the index.
21:49:00	<sm>	oops, gotcha
21:49:25	→	alp joins (~alp@user/alp)
21:49:52	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
21:49:54	→	wyrd joins (~wyrd@gateway/tor-sasl/wyrd)
21:50:02	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
21:50:07	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
21:50:14	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
21:50:22	<sm>	slightly unfortunate for discovery of WIP books
21:51:55	<tcard>	Indeed. I agree. There are drawbacks to including WIP books as well, and it was a difficult decision to make.
21:52:10	<sm>	oh, this one's not freely readable, I didn't notice. That makes it a bit less important to discover early
21:52:27	<tcard>	It looks really good, though! :)
21:52:54	<sm>	yup it looks fun
21:58:46	→	yauhsien_ joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
21:58:46	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Read error: Connection reset by peer)
21:59:45	→	cosimone joins (~user@93-44-187-176.ip98.fastwebnet.it)
22:05:15	×	yauhsien_ quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
22:08:30	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
22:09:12	×	Tuplanolla quits (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) (Quit: Leaving.)
22:17:16	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
22:18:37	→	Axman6 joins (~Axman6@user/axman6)
22:23:34	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
22:23:49	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
22:23:56	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
22:24:10	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
22:24:17	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
22:25:37	×	Midjak quits (~Midjak@82.66.147.146) (Quit: Leaving)
22:26:14	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
22:26:47	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
22:28:33	×	sagax quits (~sagax_nb@user/sagax) (Quit: Konversation terminated!)
22:34:58	→	dsrt^ joins (~dsrt@96-91-136-49-static.hfc.comcastbusiness.net)
22:37:44	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
22:38:17	s4msung	is now known as EldenJohn
22:38:58	EldenJohn	is now known as s4msung
22:39:04	×	Pickchea quits (~private@user/pickchea) (Ping timeout: 272 seconds)
22:39:48	×	alp quits (~alp@user/alp) (Ping timeout: 240 seconds)
22:41:05	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
22:42:02	×	Axman6 quits (~Axman6@user/axman6) (Ping timeout: 240 seconds)
22:43:21	×	tremon quits (~tremon@83-84-18-241.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
22:43:47	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
22:46:40	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
22:50:49	→	perrierjouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca)
22:51:44	×	machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 272 seconds)
22:52:16	×	pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5)
22:53:17	×	geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
22:54:04	×	ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
22:54:19	→	ChaiTRex joins (~ChaiTRex@user/chaitrex)
22:54:58	→	geekosaur joins (~geekosaur@xmonad/geekosaur)
22:56:50	→	lumberjack123 joins (~alMalsamo@gateway/tor-sasl/almalsamo)
22:56:56	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
23:00:17	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
23:08:03	×	acidjnk quits (~acidjnk@p200300d0c7049f8284fff18517a389b2.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
23:08:04	×	`2jt quits (~jtomas@210.red-88-24-179.staticip.rima-tde.net) (Remote host closed the connection)
23:10:52	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 260 seconds)
23:12:04	×	Guest98 quits (~Guest98@82.212.116.123) (Quit: Client closed)
23:14:37	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
23:15:16	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
23:15:35	×	stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds)
23:18:04	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:193d:75d8:745d:e91e)
23:19:23	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
23:19:35	×	shailangsa quits (~shailangs@host86-162-150-212.range86-162.btcentralplus.com) ()
23:20:13	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
23:21:12	→	szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
23:23:27	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Ping timeout: 260 seconds)
23:24:37	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
23:25:46	→	Axman6 joins (~Axman6@user/axman6)
23:28:51	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
23:32:02	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
23:35:38	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
23:36:02	→	stiell joins (~stiell@gateway/tor-sasl/stiell)
23:41:57	×	pera quits (~pera@user/pera) (Quit: leaving)
23:47:58	→	stiell_ joins (~stiell@gateway/tor-sasl/stiell)
23:48:15	×	stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds)
23:52:16	→	machinedgod joins (~machinedg@24.105.81.50)
23:52:18	→	Topsi joins (~Tobias@dyndsl-095-033-020-104.ewe-ip-backbone.de)
23:53:43	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Remote host closed the connection)
23:55:01	→	yauhsien joins (~yauhsien@61-231-25-68.dynamic-ip.hinet.net)
23:57:10	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4)
23:59:24	×	yauhsien quits (~yauhsien@61-231-25-68.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)

All times are in UTC on 2022-03-27.