Logs on 2021-06-01 (liberachat/#haskell)

00:04:09	→	ddellacosta joins (~ddellacos@86.106.143.157)
00:06:00	×	abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Read error: Connection reset by peer)
00:06:56	×	tremon quits (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
00:07:28	→	Heffalump joins (~ganesh@urchin.earth.li)
00:07:34	→	shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net)
00:08:31	→	jsilver joins (~jonathan@2601:282:300:aa0:e0bc:bc4e:7821:4001)
00:08:35	×	ddellacosta quits (~ddellacos@86.106.143.157) (Ping timeout: 252 seconds)
00:08:42	←	Heffalump parts (~ganesh@urchin.earth.li) ()
00:09:37	×	waleee quits (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 272 seconds)
00:12:24	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
00:13:03	×	jsilver quits (~jonathan@2601:282:300:aa0:e0bc:bc4e:7821:4001) (Quit: Leaving)
00:16:58	×	Cubic quits (~hannesste@ip5f5be453.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
00:17:37	→	abhixec joins (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net)
00:17:37	×	Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
00:18:12	→	Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net)
00:24:05	→	steeps joins (~steeps@cpc121168-oxfd27-2-0-cust161.4-3.cable.virginm.net)
00:24:32	×	cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds)
00:24:53	→	cheater joins (~Username@user/cheater)
00:30:03	→	hmmmas joins (~chenqisu1@183.217.202.217)
00:31:41	×	argento quits (~argent0@168.227.96.53) (Ping timeout: 252 seconds)
00:34:47	→	o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com)
00:34:55	→	Erutuon joins (~Erutuon@user/erutuon)
00:39:18	×	o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 264 seconds)
00:40:45	×	hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.)
00:41:17	×	sm2n quits (~sm2n@user/sm2n) (Ping timeout: 272 seconds)
00:41:30	→	ddellacosta joins (~ddellacos@89.45.224.40)
00:41:43	→	hmmmas joins (~chenqisu1@183.217.202.217)
00:42:10	×	steeps quits (~steeps@cpc121168-oxfd27-2-0-cust161.4-3.cable.virginm.net) (Quit: Leaving)
00:42:15	→	Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-133-166.cust.tzulo.com)
00:44:05	×	boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Ping timeout: 264 seconds)
00:45:21	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
00:46:25	×	ddellacosta quits (~ddellacos@89.45.224.40) (Ping timeout: 265 seconds)
00:46:32	×	bfrk quits (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) (Ping timeout: 252 seconds)
00:46:59	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds)
00:49:00	→	argento joins (~argent0@168.227.96.53)
00:49:50	×	raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds)
00:50:56	×	oxide quits (~lambda@user/oxide) (Ping timeout: 268 seconds)
00:51:33	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds)
00:51:41	→	oxide joins (~lambda@user/oxide)
00:52:20	→	pe200012 joins (~pe200012@120.236.162.14)
00:52:29	×	pe200012_ quits (~pe200012@119.131.208.84) (Ping timeout: 272 seconds)
00:53:42	×	cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds)
00:53:49	→	cheater joins (~Username@user/cheater)
00:53:50	→	notzmv joins (~zmv@user/notzmv)
00:54:16	×	Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 244 seconds)
00:54:16	×	hylisper2 quits (~yaaic@111.119.208.67) (Ping timeout: 244 seconds)
00:56:06	→	Erutuon joins (~Erutuon@user/erutuon)
00:59:22	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
01:01:30	→	tonyday joins (~user@202-65-93-249.ip4.superloop.com)
01:02:57	→	chisui joins (~chisui@200116b86662dd0045dcdbf42fb73e43.dip.versatel-1u1.de)
01:03:29	<tonyday>	I was wondering if anyone would be interested in a project I'm calling docperf, like doctest except for performance benchmarking?
01:03:33	×	wenzel quits (~wenzel@user/wenzel) (Read error: Connection reset by peer)
01:03:57	→	wenzel joins (~wenzel@user/wenzel)
01:04:24	<tonyday>	Covering the basics, like checking the Order claim of a function, and documenting the expected factor.
01:04:34	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
01:05:24	<tonyday>	The design ethic would be that performance, like tests, are very useful when they're right next to the code.
01:05:32	→	boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com)
01:05:57	<cdsmith>	It sounds intriguing. Off-hand, my thoughts are (a) I care about performance claims for only a tiny number of packages, but for that tiny package set, it's very important. Not sure if that argues for or against. And (b) complexity claims in Haskell can be complex, since they depend on how much of the result is evaluated.
01:06:53	<cdsmith>	Err, I should have said "can be complicated". That's probably clearer than mixing meanings of "complex"
01:08:16	<tonyday>	Yes, I'm forever adding and subtracting -XStrictData or is it -XDataStrict, measuring that empirically. Help with that etc.
01:12:35	×	siraben quits (~siraben@user/siraben) (Quit: node-irc says goodbye)
01:12:53	→	siraben joins (~siraben@user/siraben)
01:16:07	→	ddellacosta joins (~ddellacos@89.45.224.131)
01:16:51	<tonyday>	If someone has designed some "strict in the spline" style, say, then performance usage should be part of the documentation, showing the implications of miss-use.
01:17:34	→	wei2912 joins (~wei2912@112.199.250.21)
01:20:34	→	renzhi joins (~xp@2607:fa49:6500:bc00::e7b)
01:20:38	×	ddellacosta quits (~ddellacos@89.45.224.131) (Ping timeout: 252 seconds)
01:20:44	×	argento quits (~argent0@168.227.96.53) (Ping timeout: 265 seconds)
01:20:44	×	ixlun quits (~user@109.249.184.235) (Read error: Connection reset by peer)
01:21:51	→	ixlun joins (~user@109.249.184.235)
01:22:52	<tonyday>	It would be great to direct core to the comments as well. It would be alert to core changes then.
01:24:26	→	Guest86 joins (~Guest86@189.197.116.11)
01:24:49	→	hylisper joins (~yaaic@111.119.208.67)
01:24:51	→	argento joins (~argent0@168.227.96.53)
01:26:53	×	ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 272 seconds)
01:27:08	→	ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net)
01:28:46	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
01:28:47	×	shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 272 seconds)
01:30:20	Guest86	is now known as ram535
01:32:09	→	xff0x_ joins (~xff0x@2001:1a81:52ca:4f00:908c:1e58:afd0:4053)
01:34:18	→	lavaman joins (~lavaman@98.38.249.169)
01:35:45	×	xff0x quits (~xff0x@port-92-195-46-148.dynamic.as20676.net) (Ping timeout: 272 seconds)
01:38:55	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 272 seconds)
01:45:23	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 265 seconds)
01:48:03	×	zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!)
01:48:15	<sm[m]>	hi tonyday, it sounds very interesting. Would it be mostly useful for "small" code (tight loops..) ? Or also describing application/system performance ?
01:51:23	<tonyday>	small certainly. But my Vector chains break at a certain level of compositional complexity, and it's difficult to spot where. I'd like to see fusion in the lab with some form of benchmark or standard so to speak.
01:51:38	<tonyday>	just an example
01:55:42	→	shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net)
01:55:53	→	ddellacosta joins (~ddellacos@89.45.224.131)
01:59:29	<tonyday>	I do use the same mechanisms to measure latencies in a tcp connection, though, so its pretty flexible.
01:59:48	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
02:00:14	×	ddellacosta quits (~ddellacos@89.45.224.131) (Ping timeout: 252 seconds)
02:03:45	→	o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com)
02:04:53	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 272 seconds)
02:07:12	×	argento quits (~argent0@168.227.96.53) (Quit: leaving)
02:07:23	×	machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 252 seconds)
02:07:32	→	argento joins (~argent0@168.227.96.53)
02:07:39	×	hubvu quits (uid495858@id-495858.tinside.irccloud.com) (Quit: Connection closed for inactivity)
02:10:26	×	Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-133-166.cust.tzulo.com) (Quit: Leaving)
02:10:29	×	alex3 quits (~Chel@BSN-77-82-41.static.siol.net) (Ping timeout: 268 seconds)
02:12:54	→	finn_elija joins (~finn_elij@user/finn-elija/x-0085643)
02:12:54	FinnElija	is now known as Guest2152
02:12:54	finn_elija	is now known as FinnElija
02:16:02	×	Guest2152 quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 268 seconds)
02:21:33	→	ikex joins (~ash@user/ikex)
02:23:02	×	chisui quits (~chisui@200116b86662dd0045dcdbf42fb73e43.dip.versatel-1u1.de) (Ping timeout: 250 seconds)
02:27:47	→	ddellacosta joins (~ddellacos@86.106.121.196)
02:29:04	×	lawt quits (~lawt@2601:200:8101:f140:dea6:32ff:fea1:adfa) (Quit: WeeChat 2.8)
02:31:29	×	td_ quits (~td@muedsl-82-207-238-238.citykom.de) (Ping timeout: 264 seconds)
02:32:45	×	ddellacosta quits (~ddellacos@86.106.121.196) (Ping timeout: 272 seconds)
02:33:18	→	td_ joins (~td@94.134.91.112)
02:34:08	→	falafel_ joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net)
02:34:14	→	beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net)
02:37:59	→	myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net)
02:39:53	×	Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 264 seconds)
02:41:23	→	Erutuon joins (~Erutuon@user/erutuon)
02:42:02	×	shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
02:42:59	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
02:44:23	→	alex3 joins (~Chel@BSN-77-82-41.static.siol.net)
02:46:36	→	cheater1__ joins (~Username@user/cheater)
02:46:41	×	cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds)
02:46:48	cheater1__	is now known as cheater
02:50:15	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
02:50:34	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 268 seconds)
02:57:57	×	boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Remote host closed the connection)
03:00:37	×	xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Ping timeout: 272 seconds)
03:03:31	×	boxscape quits (~boxscape@user/boxscape) (Ping timeout: 268 seconds)
03:04:25	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
03:05:22	×	oxide quits (~lambda@user/oxide) (Ping timeout: 268 seconds)
03:06:01	×	ikex quits (~ash@user/ikex) (Ping timeout: 244 seconds)
03:06:53	→	ddellacosta joins (~ddellacos@89.46.62.196)
03:07:02	→	oxide joins (~lambda@user/oxide)
03:07:16	→	eddiemundo[m] joins (~eddiemun_@2001:470:69fc:105::a9c)
03:07:46	eddiemundo[m]	is now known as eddiemundo
03:08:52	×	eddiemundo quits (~eddiemun_@2001:470:69fc:105::a9c) (Client Quit)
03:09:08	→	eddiemundo joins (~eddiemund@2001:470:69fc:105::a9c)
03:11:54	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds)
03:12:01	×	ddellacosta quits (~ddellacos@89.46.62.196) (Ping timeout: 272 seconds)
03:16:18	<arahael>	What's the difference between 'set' and 'assign' with haskelll's lenses?
03:16:22	×	jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 264 seconds)
03:16:48	→	otto_s_ joins (~user@p5de2ffe1.dip0.t-ipconnect.de)
03:18:17	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
03:19:45	×	willbush quits (~user@47.183.200.14) (Remote host closed the connection)
03:20:11	×	otto_s quits (~user@p5de2fbac.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
03:20:13	<glguy>	arahael, assign uses MonadState
03:21:46	<arahael>	glguy: Oooh? I've not covered MonadState as such when it comes to lenses.
03:22:08	×	o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Remote host closed the connection)
03:23:23	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
03:23:53	→	o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com)
03:24:37	<sm[m]>	tonyday: are these effectively performance tests ? Can't you express those with ordinary doctest ?
03:24:50	→	mustafa joins (~mustafa@rockylinux/releng/mstg)
03:26:35	×	Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds)
03:26:50	→	Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
03:27:14	→	berberman_ joins (~berberman@user/berberman)
03:27:41	×	berberman quits (~berberman@user/berberman) (Ping timeout: 252 seconds)
03:27:59	→	AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net)
03:28:14	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds)
03:28:14	aighearach_	is now known as Aighearach
03:28:48	→	Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com)
03:28:48	×	o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 268 seconds)
03:32:50	×	kiweun quits (~sheepduck@2607:fea8:2a60:b700::5d55) (Remote host closed the connection)
03:35:05	→	sheepduck joins (~sheepduck@2607:fea8:2a60:b700::8a94)
03:35:36	→	lavaman joins (~lavaman@98.38.249.169)
03:36:17	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 264 seconds)
03:36:54	×	nerdypepper quits (znc@152.67.162.71) (Changing host)
03:36:54	→	nerdypepper joins (znc@user/nerdypepper)
03:37:02	×	shiraeeshi quits (~shiraeesh@109.166.59.30) (Ping timeout: 265 seconds)
03:39:03	×	Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt)
03:40:07	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 244 seconds)
03:40:37	→	evolve75` joins (~user@c-76-20-160-130.hsd1.mi.comcast.net)
03:40:42	×	monochrom quits (trebla@216.138.220.146) (Quit: NO CARRIER)
03:40:59	→	monochrom joins (trebla@216.138.220.146)
03:44:16	→	shiraeeshi joins (~shiraeesh@109.166.59.30)
03:45:28	×	smitop quits (uid328768@user/smitop) (Quit: Connection closed for inactivity)
03:53:29	×	argento quits (~argent0@168.227.96.53) (Remote host closed the connection)
03:54:19	→	leeb joins (~leeb@KD111239155018.au-net.ne.jp)
03:54:28	×	alx741 quits (~alx741@186.178.108.160) (Quit: alx741)
03:54:55	→	justsomeguy joins (~justsomeg@user/justsomeguy)
04:00:22	×	pe200012 quits (~pe200012@120.236.162.14) (Read error: Connection reset by peer)
04:00:48	→	pe200012 joins (~pe200012@119.131.208.84)
04:02:31	→	mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be)
04:03:08	→	mustafa joins (~mustafa@rockylinux/releng/mstg)
04:04:51	→	lavaman joins (~lavaman@98.38.249.169)
04:05:10	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
04:05:25	→	lavaman joins (~lavaman@98.38.249.169)
04:05:31	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
04:05:47	→	lavaman joins (~lavaman@98.38.249.169)
04:05:55	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
04:06:10	→	lavaman joins (~lavaman@98.38.249.169)
04:06:17	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
04:06:32	→	lavaman joins (~lavaman@98.38.249.169)
04:06:39	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
04:08:16	×	renzhi quits (~xp@2607:fa49:6500:bc00::e7b) (Ping timeout: 268 seconds)
04:10:29	×	cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds)
04:10:30	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 264 seconds)
04:10:48	→	cheater joins (~Username@user/cheater)
04:12:35	×	evolve75` quits (~user@c-76-20-160-130.hsd1.mi.comcast.net) (Ping timeout: 268 seconds)
04:18:18	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
04:18:18	×	ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Read error: Connection reset by peer)
04:18:37	→	ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net)
04:22:10	×	slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving)
04:29:54	→	lbseale_ joins (~lbseale@ip72-194-54-201.sb.sd.cox.net)
04:33:17	×	lbseale quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 264 seconds)
04:35:22	→	wonko joins (~wjc@62.115.229.50)
04:38:22	<tonyday>	sm: yes, you just have a few differences; compile not ghci, an ability to record a "performance" in the comments (eg "O(N^2): 12"), and an ability to trigger an error/warning if there is a regression.
04:38:27	→	dhu1337 joins (~dhu1337@user/dhu1337)
04:38:34	×	ram535 quits (~Guest86@189.197.116.11) (Quit: Client closed)
04:39:43	×	danso quits (~danso@23-233-111-52.cpe.pppoe.ca) (Ping timeout: 268 seconds)
04:40:27	<tonyday>	I think cabal-extras can help with all of that
04:43:43	<tonyday>	And we would be able to check for regressions in CI and all that
04:45:10	→	mustafa joins (~mustafa@rockylinux/releng/mstg)
04:46:55	→	v01d4lph4 joins (~v01d4lph4@122.160.65.250)
04:46:55	×	v01d4lph4 quits (~v01d4lph4@122.160.65.250) (Changing host)
04:46:55	→	v01d4lph4 joins (~v01d4lph4@user/v01d4lph4)
04:48:09	×	dhu1337 quits (~dhu1337@user/dhu1337) (Quit: dhu1337)
04:48:41	o	is now known as niko
04:49:52	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 244 seconds)
04:49:55	→	lbseale__ joins (~lbseale@ip72-194-54-201.sb.sd.cox.net)
04:53:24	×	lbseale_ quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 265 seconds)
04:54:01	→	o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com)
04:56:11	×	gambpang quits (~ian@207.181.230.156) (Remote host closed the connection)
04:56:39	×	hylisper quits (~yaaic@111.119.208.67) (Quit: Yaaic - Yet another Android IRC client - http://www.yaaic.org)
04:57:20	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds)
04:58:29	×	o1lo01ol1o quits (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) (Ping timeout: 264 seconds)
05:02:16	×	img quits (~img@2405:6580:b1c0:2500:43d1:94bf:adb9:8dcf) (Quit: ZNC 1.8.1 - https://znc.in)
05:04:07	lep	is now known as test
05:04:07	test	is now known as lep
05:04:49	×	AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.)
05:10:53	→	img joins (~img@2405:6580:b1c0:2500:1e68:3732:5209:e4c0)
05:13:55	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
05:17:00	→	hololeap joins (hololeap@user/hololeap)
05:17:16	<hololeap>	hi, I'm looking for some help with this: http://sprunge.us/rOOfCr
05:17:57	<hololeap>	I set up a GADT rose tree that carries a couple types for each node in a type-level rose tree
05:18:41	<hololeap>	at some point I want to forget this extra type-level info and convert it to a regular Tree, but I'm not sure how to do this
05:19:26	<dy>	I think that's a forgetful functor... but I can't remember :^)
05:19:38	→	wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com)
05:21:08	<hololeap>	I thought I would need to do something like: fromFoo :: (forall t. FooItem t -> x) -> (forall ts. Foo ts) -> x
05:22:38	×	Athas quits (athas@2a01:7c8:aaac:1cf:885f:6d75:b55f:82a8) (Quit: ZNC 1.8.2 - https://znc.in)
05:22:54	→	Athas joins (athas@2a01:7c8:aaac:1cf:7de4:bc5c:7241:d6d9)
05:24:55	→	vicfred_ joins (~vicfred@static-198-54-131-72.cust.tzulo.com)
05:25:30	×	falafel_ quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 264 seconds)
05:27:53	×	schuelermine quits (~schuelerm@user/schuelermine) (Ping timeout: 264 seconds)
05:27:53	→	chisui joins (~chisui@200116b866065d0037bb6f0935c2f6da.dip.versatel-1u1.de)
05:28:22	×	vicfred quits (~vicfred@user/vicfred) (Ping timeout: 264 seconds)
05:30:11	<hololeap>	I did just find a typo, but it seems like no matter what I do here I end up with errors like this: Could not deduce: ts2 ~ ts from the context: ts1 ~ 'Node '(r, a) ts
05:30:18	×	myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 264 seconds)
05:30:50	×	vicfred_ quits (~vicfred@static-198-54-131-72.cust.tzulo.com) (Quit: Leaving)
05:34:15	→	pe200012_ joins (~pe200012@120.236.162.14)
05:34:30	×	pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 264 seconds)
05:34:36	×	shiraeeshi quits (~shiraeesh@109.166.59.30) (Ping timeout: 268 seconds)
05:35:17	×	chisui quits (~chisui@200116b866065d0037bb6f0935c2f6da.dip.versatel-1u1.de) (Quit: Client closed)
05:36:22	×	xff0x_ quits (~xff0x@2001:1a81:52ca:4f00:908c:1e58:afd0:4053) (Ping timeout: 244 seconds)
05:36:55	×	pavonia quits (~user@user/siracusa) (Quit: Bye!)
05:37:18	→	xff0x_ joins (~xff0x@2001:1a81:52ca:4f00:5ed9:a747:2841:c1b7)
05:39:27	→	mustafa joins (~mustafa@rockylinux/releng/mstg)
05:40:48	→	michalz joins (~user@185.246.204.45)
05:41:51	→	chomwitt joins (~Pitsikoko@2a02:587:dc02:b00:b16c:5166:feb8:97d5)
05:43:37	→	Bartosz joins (~textual@24.35.90.211)
05:43:37	×	Bartosz quits (~textual@24.35.90.211) (Client Quit)
05:44:41	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 264 seconds)
05:45:19	<hololeap>	ok, here's a question that should get to the crux of the issue: if I have a heterogeneous list of types with a Show instance, how can I convert it to a regular list of type [String] ?
05:45:46	<hololeap>	*each type in the heterogeneous list has a Show instance
05:47:47	<hololeap>	data HList (ts :: [Type]) where ; HNil :: HList '[] ; (:-:) :: Show t => t -> HList ts -> HList (t ': ts)
05:48:01	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds)
05:51:33	→	Bartosz joins (~textual@24.35.90.211)
05:55:05	→	nschoe joins (~quassel@91-162-58-134.subs.proxad.net)
05:57:02	×	beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Ping timeout: 244 seconds)
05:57:14	<int-e>	hololeap: https://paste.debian.net/1199557/ ...that doesn't seem to raise any difficulties
05:58:20	<int-e>	(well, the function is terribly named)
05:59:51	×	nschoe quits (~quassel@91-162-58-134.subs.proxad.net) (Ping timeout: 272 seconds)
06:00:34	<Bartosz>	dy: I thought about it and I think real world is not a perfect model for functors. A functor can contain an arbitrary type inside, so as a container it has to be enormous. It must be able to hold an aircraft carrier, the sun, the galaxy, etc.
06:00:41	→	Guest6538 joins (~Guest65@2400:8902::f03c:92ff:fe60:98d8)
06:01:10	<Guest6538>	I have a simple Parsec question, how to filter comment on this code https://paste.ubuntu.com/p/tSbwNBNxhw/
06:02:03	<int-e>	hololeap: fromHListWith :: (forall a. Show a => a -> b) -> HList ts -> [b] <--this type may be more to the point.
06:02:03	<Guest6538>	it parses something like "a=b" is ok, but I'd like to ignore like "--comment"
06:03:02	→	vicentius joins (~vicentius@user/vicentius)
06:04:49	<dy>	Bartosz: so functors are hammerspace :p
06:04:59	×	amk quits (~amk@176.61.106.150) (Ping timeout: 252 seconds)
06:05:53	→	amk joins (~amk@176.61.106.150)
06:08:46	<hololeap>	hm, actually my original idea seems to work without the (forall ts. ...) surrounding the tree and forest data types
06:09:49	×	vicentius quits (~vicentius@user/vicentius) (Quit: Leaving)
06:11:28	→	manicennui joins (uid349235@id-349235.tinside.irccloud.com)
06:15:34	→	_ht joins (~quassel@82-169-194-8.biz.kpn.net)
06:15:42	<hololeap>	dy: I think comonads are hammerspace. those are things you can always pull something out of
06:16:24	<dminuoso>	Guest6538: https://hackage.haskell.org/package/parsec-3.1.14.0/docs/Text-Parsec-Token.html
06:18:19	<dminuoso>	Guest6538: Alternatively you can just reimplement the `space` combinator from megaparsec, it's really trivial
06:18:43	<dminuoso>	And adopt the rule that you always use `space` before or after (pick one!) each lexeme
06:20:54	<dy>	More concretely (hah) you can also just parse a CST (concrete syntax tree) first and then map it to the AST you want.
06:21:26	<dy>	The distinction with a CST is that there exists a bijection from it to/from the original source.
06:21:38	→	danso joins (~danso@23-233-111-52.cpe.pppoe.ca)
06:21:40	→	dyeplexer joins (~dyeplexer@user/dyeplexer)
06:22:10	→	nschoe joins (~quassel@91-162-58-134.subs.proxad.net)
06:22:24	<dminuoso>	Mmm, usually a CST does not contain whitespace or comments.
06:24:09	<Guest6538>	dminuoso, can I just use parsec to implement that? I don't install megaparsec yet
06:24:13	<dminuoso>	Guest6538: Yes.
06:24:20	<dy>	They don't contain whitespace but they do contain token positions you could recreate the whitespace from
06:24:26	<dminuoso>	https://hackage.haskell.org/package/megaparsec-9.0.1/docs/src/Text.Megaparsec.Lexer.html#space
06:24:31	<dy>	Comments otoh are usually in CSTs, at least in my e Irwin en
06:24:31	×	Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…)
06:24:35	<dy>	My experience*
06:26:13	<hololeap>	hm, here's an interesting one: a class function where instances occasionally need extra arguments passed in, in order to produce the desired output.
06:26:41	<dy>	hololeap: as an example of...?
06:27:01	×	nschoe quits (~quassel@91-162-58-134.subs.proxad.net) (Ping timeout: 268 seconds)
06:27:14	<hololeap>	I'm just thinking of ways to implement this
06:27:26	<dy>	I missed the context/not in my backlog
06:27:34	<hololeap>	no context :p
06:27:45	<dy>	What are you trying to implement?
06:27:55	<hololeap>	what I just described
06:28:14	<dy>	Do you mean class as in typeclass?
06:28:18	<dy>	Or like more traditional class?
06:28:23	<hololeap>	no, a typeclass
06:28:32	<dy>	I'm reminded of how printf works in Haskell
06:28:51	<hololeap>	hm, yeah that should be a good example to look at
06:29:23	→	nschoe joins (~quassel@91-162-58-134.subs.proxad.net)
06:29:57	<dy>	The trick there is recursion at the instance definition level I believe
06:30:34	<dy>	But I don't think Printf is actually properly type safe.
06:30:55	→	leeb_ joins (~leeb@KD111239153130.au-net.ne.jp)
06:30:59	<dy>	Would require dependent types to be properly type safe I think.
06:31:16	→	cheater1__ joins (~Username@user/cheater)
06:31:20	→	lortabac joins (~lortabac@2a01:e0a:541:b8f0:bdf8:f228:7df7:147f)
06:31:31	×	cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds)
06:31:34	<hololeap>	I have 23 language extensions enabled in my module right now :p
06:31:37	cheater1__	is now known as cheater
06:31:59	<dy>	I think I heard something about dependent typing coming to mainline GHC?
06:32:03	<dy>	I feel like that's... probably going to be messy.
06:32:12	<dy>	Refinement types seem a better Pareto optimal choice.
06:32:25	<hololeap>	nah
06:32:30	→	Toast52 joins (~Toast52@151.192.167.120)
06:32:48	<Guest6538>	why there's char in parsec, but not string? use satisfy to match a string?
06:32:54	<dy>	Refinement types are a bit more intuitive and map nicely to more traditional notions of code contracts.
06:32:55	<hololeap>	most of them are quite safe, except maybe AllowAmbiguousTypes and NoMonomorphismRestriction
06:33:29	<dy>	There comes a day in every Haskell programmer's life when they just have to give up and enable NoMonomorphismRestricfion :p
06:33:35	×	leeb quits (~leeb@KD111239155018.au-net.ne.jp) (Ping timeout: 252 seconds)
06:33:35	<dy>	Perhaps for reasons they do not understand.
06:33:44	→	mustafa joins (~mustafa@rockylinux/releng/mstg)
06:33:47	<dminuoso>	Uh. No?
06:34:01	<dy>	It's a joke.
06:34:12	<[exa]>	Guest6538: https://hackage.haskell.org/package/megaparsec-9.0.1/docs/Text-Megaparsec-Char.html#v:string ?
06:34:19	<dy>	Just one of those extensions I've seen people enable blindly after seeing error messages mentioning it a lot.
06:34:26	<Guest6538>	[exa] I mean in parsec
06:34:30	<dminuoso>	Curious, I have not seen this behavior.
06:34:42	<[exa]>	Guest6538: uh sorry I'm aliasing the names automatically now :D
06:34:43	→	ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net)
06:34:45	<dminuoso>	Guest6538: https://hackage.haskell.org/package/parsec-3.1.14.0/docs/Text-Parsec-Char.html#v:string
06:35:05	<Guest6538>	ok, my mistake
06:35:06	×	nschoe quits (~quassel@91-162-58-134.subs.proxad.net) (Ping timeout: 264 seconds)
06:35:22	<[exa]>	yap there it is :]
06:36:24	<[exa]>	even if not, you could easily construct it, roughly as `traverse char`
06:37:20	→	neceve joins (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130)
06:37:58	<dminuoso>	string s = tokens show updatePosString s
06:38:29	×	mustafa quits (~mustafa@rockylinux/releng/mstg) (Ping timeout: 272 seconds)
06:38:32	<dminuoso>	If you naively just parse each character, you'll get horrid error messages.
06:38:41	→	sondre joins (~sondrelun@cm-84.212.100.140.getinternet.no)
06:39:11	→	azeem joins (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it)
06:39:26	<dminuoso>	Rather than `expected "foobar"`, it would tell you `expected 'b'`, which for more complex strings is not going to be very helpful
06:39:56	<dminuoso>	And if there's any <\|>, you might not even know what's going on if the character could come from any of the choices.
06:40:22	<[exa]>	yeah that's the "roughly" warning. :]
06:40:37	×	ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Quit: leaving)
06:41:39	<[exa]>	kinda thinking, why'd they have the "show" in the definition? doesn't it totally obliterate any unicode in the error messages?
06:42:46	×	pe200012_ quits (~pe200012@120.236.162.14) (Ping timeout: 264 seconds)
06:45:14	×	rubin55 quits (sid175221@id-175221.stonehaven.irccloud.com) ()
06:45:35	→	rubin55 joins (sid175221@id-175221.stonehaven.irccloud.com)
06:45:56	×	rubin55 quits (sid175221@id-175221.stonehaven.irccloud.com) (Client Quit)
06:46:24	→	rubin55 joins (sid175221@id-175221.stonehaven.irccloud.com)
06:46:32	→	holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665)
06:47:24	→	Cubic joins (~hannesste@ip5f5be453.dynamic.kabel-deutschland.de)
06:50:41	<Guest6538>	comment = string "--" *> (manyTill anyChar newline)
06:50:47	<Guest6538>	newSpaces = spaces <\|> comment
06:51:27	→	mc47 joins (~yecinem@89.246.239.190)
06:52:08	<hololeap>	dy, is this what you were referring to by refinement types? https://hackage.haskell.org/package/refined
06:52:16	<dy>	No, think Liquid Haskell
06:52:19	<int-e>	> let x --> y = y in 2 --> 4
06:52:20	<lambdabot>	4
06:52:23	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
06:52:24	<Guest6538>	Expected type: ParsecT String u Data.Functor.Identity.Identity () ; Actual type: ParsecT String u Data.Functor.Identity.Identity [Char]; In the second argument of ‘(<\|>)’,
06:52:28	<hololeap>	I've never used it
06:52:42	<Guest6538>	where is wrong?
06:52:59	<Axman6>	what is the type of: comment, spaces and <\|>
06:53:24	<int-e>	:t void
06:53:24	<dy>	It looks like that refined package is a similar idea? Not entirely clear. Haven't seen it befofez
06:53:25	<lambdabot>	Functor f => f a -> f ()
06:53:32	→	beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net)
06:53:37	<Axman6>	int-e: we'll get to that ;)
06:53:38	<Guest6538>	oh, <\|> ask the same type
06:53:42	<int-e>	Axman6: I know
06:54:17	<dy>	Untyped comments? In my Haskell?
06:54:26	<dy>	"It's more likely than you think!"
06:55:03	<int-e>	dy: "untyped", hmmmm. Sometimes it's better to not type a comment and let the code speak for itself.
06:55:28	<int-e>	@where semantics
06:55:28	<lambdabot>	I know nothing about semantics.
06:55:40	<dminuoso>	That should be a quote.
06:55:52	→	chele joins (~chele@user/chele)
06:56:42	×	azeem quits (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Quit: Quit)
06:56:51	→	azeem joins (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it)
06:58:02	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
06:58:23	→	dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be)
06:59:29	<hololeap>	I also haven't seen it befofez
07:02:34	<Guest6538>	comment = string "--" *> (manyTill anyChar newline) $> ()
07:02:40	<Guest6538>	newSpaces = spaces <\|> comment
07:02:55	<Guest6538>	dminuoso use this newSpaces intead of spaces is ok?
07:05:22	<dminuoso>	Guest6538: Its not needed, `spaces` already covers this need.
07:06:04	<dminuoso>	Guest6538: The idea is that `space` takes three lexers/consumers. One that consumes regular whitespace, one that consumes line comments and one that consumes block comments.
07:06:12	<dminuoso>	So if we look at the implementation
07:06:41	<dminuoso>	space sp line block = skipMany (choice [sp, line, block])
07:07:00	<dminuoso>	You can see this just munches all contiguous whitespace, line and block comments
07:07:29	<dminuoso>	Ah naming confusion
07:08:05	→	raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
07:08:18	<dminuoso>	Guest6538: Its not enough
07:08:39	<Guest6538>	dminuoso, but this `spaces` is from megaparsec?
07:08:55	<dminuoso>	Guest6538: So lets avoid confusion now:
07:09:00	<dminuoso>	I propose a simple combinator called:
07:09:13	<Guest6538>	dminuoso what if the comment character is not '--' but '#' or '//'?
07:09:21	<dminuoso>	munch sp line block = skipMany (choice [sp, line, block])
07:09:41	<dminuoso>	The implementation of `munch` mimics the implementation of `space` from megaparsec, it's unlike `space` from parsec.
07:09:47	→	gehmehgeh joins (~user@user/gehmehgeh)
07:10:01	<dminuoso>	Guest6538: This combinator is almost like your `newSpaces` but differs chiefly in 3 aspects.
07:10:13	<dminuoso>	1) Your combinator wont work if there's any further whitespace after the comment
07:10:23	<dminuoso>	2) Your combinator wont accept block comments (might be important to you or not)
07:10:34	<dminuoso>	3) Your combinator is fixed rather than parametrized
07:11:02	×	tonyday quits (~user@202-65-93-249.ip4.superloop.com) (Remote host closed the connection)
07:12:13	<dminuoso>	The idea is that you'd write something like `sc = munch spaces lineComment blockComment where lineComment = string "--" > manyTill anyChar newline; blockComment = string "{-" > manyTill anyChar (string "-}")`
07:12:25	→	jakzale joins (uid499518@id-499518.charlton.irccloud.com)
07:12:28	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
07:13:21	×	albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
07:14:20	→	thiross joins (~user@173.242.113.143.16clouds.com)
07:14:28	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
07:14:43	×	albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
07:17:43	×	gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving)
07:17:54	→	gehmehgeh joins (~user@user/gehmehgeh)
07:17:57	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
07:18:53	×	abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds)
07:20:37	→	xprlgjf joins (~gavin@60.27.93.209.dyn.plus.net)
07:22:41	<Guest6538>	dminuoso, I should copy `spaces` and `lexeme` from https://hackage.haskell.org/package/megaparsec-9.0.1/docs/src/Text.Megaparsec.Lexer.html#space ?
07:25:51	→	dpl_ joins (~dpl@77-121-78-163.chn.volia.net)
07:26:25	×	albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
07:26:39	×	ixlun quits (~user@109.249.184.235) (Remote host closed the connection)
07:26:49	→	Shaeto joins (~Shaeto@94.25.234.213)
07:28:33	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds)
07:35:04	→	riatre joins (~quassel@2001:310:6000:f::5198:1)
07:36:07	×	riatre_ quits (~quassel@2001:310:6000:f::5198:1) (Ping timeout: 272 seconds)
07:36:23	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
07:36:32	×	albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
07:36:35	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
07:36:53	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
07:38:33	×	holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 268 seconds)
07:38:35	×	river quits (~river@tilde.team/user/river) (Quit: Leaving)
07:41:06	×	thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 264 seconds)
07:41:14	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 252 seconds)
07:44:32	→	thiross joins (~user@173.242.113.143.16clouds.com)
07:45:28	<albet70>	is there bot here?
07:45:32	<dminuoso>	Yes.
07:45:58	<albet70>	:t id
07:45:59	<lambdabot>	a -> a
07:46:14	<dminuoso>	We also have yahb, which can be triggered by %
07:46:16	<dminuoso>	% :t id
07:46:16	<yahb>	dminuoso: a -> a
07:46:36	<albet70>	what it short for?
07:46:41	<dminuoso>	Yet another haskell bot
07:46:55	<albet70>	:)
07:47:04	<dminuoso>	yahb exposes ghci directly, while lambdabot is way more special and multi purpose
07:47:21	<dminuoso>	lambdabot has stuff like @pl
07:47:40	<albet70>	and hoogle bot?
07:47:52	<dminuoso>	Mmm, I think lambdabot can hoogle
07:47:56	<dminuoso>	@hoogle a -> a
07:47:56	<lambdabot>	Prelude id :: a -> a
07:47:56	<lambdabot>	Data.Function id :: a -> a
07:47:56	<lambdabot>	GHC.Base breakpoint :: a -> a
07:48:03	<albet70>	ok
07:48:19	→	schuelermine joins (~anselmsch@user/schuelermine)
07:48:46	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
07:49:07	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
07:52:04	×	Athas quits (athas@2a01:7c8:aaac:1cf:7de4:bc5c:7241:d6d9) (Quit: ZNC 1.8.2 - https://znc.in)
07:52:14	→	Athas joins (athas@sigkill.dk)
07:52:40	×	Flonk quits (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com) (Quit: Ping timeout (120 seconds))
07:53:06	→	Flonk joins (~Flonk@ec2-52-40-29-25.us-west-2.compute.amazonaws.com)
07:54:32	→	shryke joins (~shryke@190.43.6.93.rev.sfr.net)
07:56:02	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
07:56:21	→	shryke_ joins (~shryke@91.103.43.254)
07:56:39	→	bfrk joins (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de)
07:58:01	→	nschoe joins (~quassel@178.251.84.79)
07:58:05	×	raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
07:58:45	→	brandonh joins (~brandonh@151.44.69.241)
07:59:06	×	shryke quits (~shryke@190.43.6.93.rev.sfr.net) (Ping timeout: 264 seconds)
07:59:35	→	raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
08:03:27	→	Bartosz joins (~textual@24.35.90.211)
08:05:04	→	dhil joins (~dhil@195.213.192.85)
08:07:28	→	hendursa1 joins (~weechat@user/hendursaga)
08:07:36	×	Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
08:08:11	×	beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Ping timeout: 252 seconds)
08:08:35	×	Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Read error: Connection reset by peer)
08:08:42	→	Kaipi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net)
08:08:58	×	hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity)
08:10:07	×	hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 252 seconds)
08:12:30	→	ikex joins (~ash@user/ikex)
08:13:56	→	pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
08:16:54	×	azeem quits (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Remote host closed the connection)
08:17:03	→	azeem joins (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it)
08:19:49	×	guest0123 quits (~aaron@2601:602:a080:fa0:21da:7ddc:2cc6:a10c) (Ping timeout: 272 seconds)
08:21:23	×	thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 252 seconds)
08:21:37	→	thiross joins (~user@173.242.113.143.16clouds.com)
08:23:51	→	fendor_ joins (~fendor@178.165.178.245.wireless.dyn.drei.com)
08:25:23	×	tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz)
08:26:42	×	fendor quits (~fendor@178.115.56.93.wireless.dyn.drei.com) (Ping timeout: 264 seconds)
08:27:54	×	Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…)
08:33:22	→	holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665)
08:35:05	×	Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 264 seconds)
08:36:23	fendor_	is now known as fendor
08:36:46	×	xff0x_ quits (~xff0x@2001:1a81:52ca:4f00:5ed9:a747:2841:c1b7) (Ping timeout: 264 seconds)
08:37:30	→	xff0x_ joins (~xff0x@2001:1a81:52ca:4f00:158d:7c0b:fd80:1302)
08:37:37	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
08:39:51	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
08:40:41	×	schuelermine quits (~anselmsch@user/schuelermine) (Quit: WeeChat 3.1)
08:43:14	<Taneb>	I dislike Yesod-style pervasive quasiquotes :(
08:45:02	<Hecate>	Taneb: I managed to avoid persistent, working with Yesod
08:45:11	<Hecate>	but uh, the route declaration still resists :<
08:46:24	×	Guest6538 quits (~Guest65@2400:8902::f03c:92ff:fe60:98d8) (Quit: Client closed)
08:47:08	<albet70>	I use scotty
08:47:14	<albet70>	it's more easy to ise
08:47:16	<albet70>	ise
08:50:05	×	azeem quits (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Read error: Connection reset by peer)
08:52:14	×	dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection)
08:53:49	×	holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 272 seconds)
08:56:06	→	wanagnuj joins (~wanagnuj@101.95.97.158)
08:56:26	→	ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233)
08:57:25	→	kuribas joins (~user@ptr-25vy0i96apm5u45pamz.18120a2.ip6.access.telenet.be)
08:58:38	<merijn>	Friends don't let friends use persistent >.>
08:59:29	<kuribas>	merijn: why not?
09:00:57	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
09:00:59	<merijn>	The API is incredibly hard to use safely/correctly, it makes it incredibly tedious to do non-trivial operations and in general (in the long run) just seems to produce more work than it saves
09:01:33	<merijn>	Oh, also easy to leak resources
09:01:38	→	matsurago joins (~matsurago@nttkyo1723091.tkyo.nt.ngn.ppp.infoweb.ne.jp)
09:01:59	<merijn>	Because it was designed for an older version of conduit (that guaranteed prompt finalisation), but conduit no longer does that
09:02:17	→	azeem joins (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it)
09:02:41	×	ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Ping timeout: 264 seconds)
09:03:10	→	boxscape joins (~boxscape@user/boxscape)
09:03:31	→	ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net)
09:03:53	×	dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 264 seconds)
09:04:14	<Taneb>	Sadly I am stuck with persistent
09:04:37	<boxscape>	% type A :: forall a -> (Allowed a ~ True) => Type; data A a = A a deriving Show
09:04:37	<yahb>	boxscape: ; <interactive>:14:45: error:; Ambiguous occurrence `Type'; It could refer to; either `Language.Haskell.TH.Type', imported from `Language.Haskell.TH' (and originally defined in `Language.Haskell.TH.Syntax'); or `Data.Kind.Type', imported from `Data.Kind' (and originally defined in `GHC.Types')
09:04:42	<Taneb>	My objection is quasiquotes mean I have to learn another, poorly documented, language, to do anythiing
09:04:43	<boxscape>	err
09:04:57	<boxscape>	% type family Allowed a where Allowed Int = True; Allowed _ = False
09:04:57	<yahb>	boxscape:
09:04:58	<boxscape>	% type A :: forall a -> (Allowed a ~ True) => *; data A a = A a deriving Show
09:04:58	<yahb>	boxscape:
09:05:02	<boxscape>	% A "not allowed"
09:05:02	<yahb>	boxscape: A "not allowed"
09:05:09	<boxscape>	this does not seem like it should work?
09:05:09	→	dunj3 joins (~dunj3@2001:16b8:3059:9800:5856:7ab4:1dd8:26ae)
09:06:27	<merijn>	Taneb: Same
09:07:02	<merijn>	Taneb: But the fact that I have a considerable amount of commits in persistent to keep my own stuff working is why I can't recommend others get started with it :p
09:07:31	<merijn>	My advice would be: Just use SQL >.>
09:09:18	<tdammers>	SQL is a pretty reasonable DSL for SQL
09:09:28	→	lavaman joins (~lavaman@98.38.249.169)
09:10:33	<merijn>	SQL also really scratches my "purely functional language with a basis in math" itch :p
09:10:51	<nshepperd>	boxscape: i don't think class constraints in kinds work, or mean anything
09:11:05	×	cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds)
09:11:11	→	cheater1__ joins (~Username@user/cheater)
09:11:11	cheater1__	is now known as cheater
09:11:21	<boxscape>	nshepperd I was under the impression that that implies to class constraints but not equality constraints, but I might be wrong
09:11:36	→	Torro joins (Torro@gateway/vpn/protonvpn/torro)
09:12:12	×	matsurago quits (~matsurago@nttkyo1723091.tkyo.nt.ngn.ppp.infoweb.ne.jp) (Quit: Leaving)
09:12:16	<boxscape>	% type B :: forall a -> Eq a => *; data B a = B a deriving Show
09:12:16	<yahb>	boxscape: ; <interactive>:20:11: error:; * Illegal constraint in a kind: forall a -> Eq a => ; In a standalone kind signature for `B': forall a -> Eq a => *
09:12:26	<boxscape>	nshepperd for what it's worth it doesn't say that the equality constraint is illegal
09:12:30	<nshepperd>	hm
09:14:05	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 264 seconds)
09:14:05	×	azeem quits (~azeem@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 264 seconds)
09:14:38	<boxscape>	% type C :: forall a -> (a ~ Int) => *; data C a = C a deriving Show -- (there's actually no need to bring type families into this)
09:14:38	<yahb>	boxscape:
09:15:00	×	wei2912 quits (~wei2912@112.199.250.21) (Quit: Lost terminal)
09:15:32	<nshepperd>	% :t A
09:15:32	<yahb>	nshepperd: forall {a} {ev :: Allowed a ~ 'True}. a -> A a
09:15:48	<boxscape>	hm that doesn't look like a constraint
09:16:20	<maerwald>	merijn: my suspicion is that it's laziness to learn SQL... which, I agree, is tedious if you don't use raw SQL a lot. It's easy to forget the details, because none of it is intuitive.
09:17:54	<dminuoso>	maerwald: But with persistent you have to learn SQL and some poorly documented DSL ontop.
09:18:19	<maerwald>	Yeah, which is why I usually re-learn SQL
09:18:28	<kuribas>	learning a DSL or language in order not to have to understand SQL is a terrible idea.
09:18:33	<dminuoso>	It's my experience, that any reasonable use of an "sql abstraction layer" eventually leads to you thinking of queris in terms of SQL, and then figuring out how to write the DSL that produces the expected SQL
09:18:51	<nshepperd>	% :t A "not allowed"
09:18:51	<yahb>	nshepperd: A String
09:19:00	<dminuoso>	nshepperd: cute!
09:19:05	<maerwald>	But if I don't use SQL for 1-2 years, most of it is gone from my brain
09:19:11	<dminuoso>	So is persistent. :P
09:19:17	<kuribas>	dminuoso: which is why my DSL is pretty much 1-1 with SQL.
09:19:24	<nshepperd>	not sure that what that is but i guess it can't be a real constraint since A isn't a GADT
09:19:43	<boxscape>	I wonder if GHC just instantiates that argument with `Any` and that's that
09:20:01	<kuribas>	dminuoso: except that I disallow right joins in the typed layer because it makes null checking very hard.
09:20:37	×	brandonh quits (~brandonh@151.44.69.241) (Quit: brandonh)
09:20:43	→	jumper149 joins (~jumper149@80.240.31.34)
09:21:00	<boxscape>	% data D where D :: forall {a} {ev :: a ~ Int}. a -> C a
09:21:00	<yahb>	boxscape: ; <interactive>:34:37: error:; * Expected a type, but `a ~ Int' has kind `Constraint'; * In the kind `a ~ Int'; In the definition of data constructor `D'; In the data declaration for `D'
09:21:03	<boxscape>	:(
09:21:03	×	xff0x_ quits (~xff0x@2001:1a81:52ca:4f00:158d:7c0b:fd80:1302) (Ping timeout: 272 seconds)
09:21:41	<nshepperd>	seems possible. a type can't carry evidence anyway so Any is as good as... anything there
09:21:41	→	xff0x_ joins (~xff0x@2001:1a81:52ca:4f00:8a7f:8182:f670:e586)
09:21:42	<jumper149>	Hi, What are currently the best tools for dead code detection regarding Haskell.
09:21:53	→	azeem joins (~azeem@dynamic-adsl-78-13-240-225.clienti.tiscali.it)
09:21:57	<maerwald>	the new weeder
09:22:15	<maerwald>	https://github.com/ocharles/weeder
09:22:19	<jumper149>	https://hackage.haskell.org/package/weeder ?
09:22:43	<maerwald>	yep, since version 2
09:25:01	<jumper149>	maerwald: Ok this is looking perfect, let's hope it works well :)
09:25:45	×	shryke_ quits (~shryke@91.103.43.254) (Quit: WeeChat 3.1)
09:25:52	<maerwald>	dminuoso: yeah... there are only two ways to learn: 1. build an intuition and keep that (and be able to deconstruct the intuition into its components if needed), 2. mess up really hard and learn through PTSD. Frameworks try to avoid both.
09:27:17	×	ikex quits (~ash@user/ikex) (Ping timeout: 264 seconds)
09:28:07	→	shryke joins (~shryke@91.103.43.254)
09:30:13	<dy>	maerwald: bash, the only language named after how you learn it!
09:30:19	<dy>	Bashing your head against hard surfaces.
09:30:20	xff0x_	is now known as xff0x
09:30:32	<maerwald>	dy: yeat, confusingly, I remember a lot of bash pitfalls
09:30:42	<maerwald>	because they delete your files and break your environment :)
09:31:00	<dy>	Amen to the SQL thing though
09:31:18	<dy>	While I do like some ORMs and such, "just write raw SQL" is honestly usually the better approach in the long run
09:31:24	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
09:31:39	<dy>	Not to mention many ORMs make even basic n+1 type query optimization a pain
09:32:05	<maerwald>	It's also embarrassing to have done backend dev for several years and not be able to write a correct SQL statement without google... but yeah, can you blame us?
09:32:14	<boxscape>	nshepperd dumping core reveals it actually passes UnsafeRefl, at least in HEAD, and unsafely coerces a representational equality in 8.10
09:32:23	<dy>	Even more infuriating is how frameworks seem to just be completely blind to (materialized) views, triggers, etc
09:32:32	<dy>	Or provide no means to handle them in migrations.
09:32:32	<kuribas>	maerwald: erm yes? Just grab a book on SQL? Read the mysql (or postgresql) manual?
09:32:40	→	qbt joins (~edun@user/edun)
09:32:55	<dy>	So you have to basically give up your framework's migrations or substantial features if you want to use views, triggers, in-DB constraints etc
09:32:57	<kuribas>	maerwald: also, goole to look up some details is fine IMO.
09:33:00	<maerwald>	kuribas: when? During saturdays when I'm drunk?
09:33:23	<kuribas>	maerwald: for example :)
09:33:26	<dy>	Even though that's way better in general as it means you don't have to worry reproducing the same sanity checks and cleaning everywhere
09:34:36	<dy>	But yeah stuff that should be easy because of SQL being the way it is are made hard by an ORM layer.
09:34:52	<dy>	Like using indices, views, etc to optimize common queries.
09:34:55	→	cheater1__ joins (~Username@user/cheater)
09:35:05	<dy>	Even Django's ORM which is generally pretty good just throws up its hands at views.
09:35:05	×	cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds)
09:35:06	cheater1__	is now known as cheater
09:35:23	<kuribas>	dy: what's the problem with views?
09:35:37	<dy>	There's no real first class support for them.
09:35:38	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 252 seconds)
09:35:49	<dy>	You have to basically trick Django into thinking they're normal models.
09:36:13	<dy>	And you get no support with migrations and end up with parallel setup code.
09:36:24	<maerwald>	I've done django too and ended up doing raw sql pretty quickly
09:36:41	<dy>	You have to fake the migrations and then manually write the raw SQL into them
09:36:44	<maerwald>	There it was because of abyssmal performance
09:37:07	<dy>	prefetch_related + Q
09:37:10	<dy>	It's essential.
09:37:24	<dy>	Otherwise you'll get 1+N queries everywhere.
09:37:28	<maerwald>	People end up loading huge sets into memory and do stuff there, because they don't understand what the ORM does
09:37:33	<dy>	Django-debug-toolbar thankfully has a nice query inspector panel.
09:37:42	dminuoso	finds that for the majority of problems, handwritten SQL is faster to write and you dont have a bunch of magic semantics in your ORM layer with automatic query twisting, caching, etc.
09:37:50	<dminuoso>	And you get predictable performance
09:37:52	<dy>	Yeah I tend to agree
09:37:55	<boxscape>	% :t C "test" :: C String -- is there any way to actually write the type of `C "test"`?
09:37:55	<yahb>	boxscape: ; <interactive>:1:13: error:; * Couldn't match kind `[Char]' with `Int'; Expected: Int; Actual: String; * In an expression type signature: C String; In the expression: C "test" :: C String
09:38:11	<sshine>	I remember doing a database join in LINQ some years ago where the predicate was '<' rather than '='... it was possible, but hacky.
09:38:12	<boxscape>	% C "test"
09:38:12	<yahb>	boxscape: C "test"
09:38:29	<dy>	LINQ is just janky monads :p
09:38:35	<dy>	Oh I'm sorry "computation expressions"
09:38:38	<sshine>	mernerds
09:39:14	<kuribas>	dminuoso: this. Orm's solve an imaginary problem
09:39:16	<dminuoso>	Is there a way to ruthlessly exit from a Haskell program? exitWith relies on exceptions which are caught on their way up in my program.
09:39:23	<dminuoso>	This is just for debugging purposes. :)
09:39:48	→	Feuermagier joins (~Feuermagi@user/feuermagier)
09:39:55	<boxscape>	cause a ghc panic?
09:40:00	×	Kaipi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
09:40:24	→	Kaipi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net)
09:40:27	<boxscape>	or a segfault
09:40:29	<dminuoso>	Mmm. oh well, I guess I could use unsafeCoerce ..
09:40:48	<dminuoso>	Is exit(2) not exposed to Haskell-land?
09:40:57	×	mc47 quits (~yecinem@89.246.239.190) (Remote host closed the connection)
09:41:17	<maerwald>	https://hackage.haskell.org/package/unix-2.7.2.2/docs/System-Posix-Process.html#v:exitImmediately
09:41:35	<maerwald>	foreign import ccall unsafe "exit" -- looks good
09:41:51	<dminuoso>	maerwald: Ah that looks right, thanks.
09:43:00	<kuribas>	merijn: I don't think my library has those problems.
09:43:47	→	xwx joins (~george@user/george)
09:43:55	<kuribas>	merijn: if conduit doesn't finalize, then how do you finalize?
09:43:58	<dminuoso>	Nobody thinks their library has problems.
09:44:00	<dminuoso>	:-)
09:44:06	→	dpl_ joins (~dpl@77-121-78-163.chn.volia.net)
09:44:26	<maerwald>	kuribas: wait for streamly to get SQL support :p
09:44:27	<kuribas>	dminuoso: not until proven otherwise :)
09:44:43	<Taneb>	kuribas: sometimes even then ;)
09:44:43	<xwx>	does anyone know if you can use a preprocessor (specifically lhs2tex) with the haskell language server?
09:44:59	→	japh joins (~scp1@user/japh)
09:45:52	<kuribas>	dminuoso: also, I haven't made the library official since I still make changes as I use it :)
09:46:22	<boxscape>	nshepperd erm I take my last statement about UnsafeRefl back, that's in the Core of any expression in ghci
09:48:10	→	_xft0 joins (~root@185.234.208.208.r.toneticgroup.pl)
09:48:46	×	chomwitt quits (~Pitsikoko@2a02:587:dc02:b00:b16c:5166:feb8:97d5) (Ping timeout: 264 seconds)
09:52:34	→	Katarushisu joins (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net)
09:54:06	<boxscape>	% f :: forall a . (a ~ Int) => C a -> Bool; f = undefined -- this error message surprises me as well tbh
09:54:06	<yahb>	boxscape: ; <interactive>:41:30: error:; * Couldn't match expected kind `Int' with actual kind `a'; `a' is a rigid type variable bound by; `forall a. (a ~ Int) => C a -> Bool'; at <interactive>:41:13; * In the type signature: f :: forall a. (a ~ Int) => C a -> Bool
09:56:48	→	haskman joins (~haskman@171.48.41.1)
10:01:19	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
10:04:29	×	raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds)
10:04:56	→	raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
10:05:53	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 252 seconds)
10:06:22	→	Guest31 joins (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net)
10:06:53	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
10:08:18	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:08:33	×	shryke quits (~shryke@91.103.43.254) (Ping timeout: 272 seconds)
10:08:46	→	satai joins (~satai@static-84-42-172-253.net.upcbroadband.cz)
10:10:32	→	Nahra joins (~user@static.161.95.99.88.clients.your-server.de)
10:11:47	×	bgamari quits (~bgamari@2001:470:e438::1) (Quit: ZNC 1.8.1 - https://znc.in)
10:12:05	→	bgamari joins (~bgamari@72.65.101.148)
10:13:30	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
10:13:51	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:17:17	×	Nahra quits (~user@static.161.95.99.88.clients.your-server.de) (Remote host closed the connection)
10:17:25	→	shryke joins (~shryke@91.103.43.254)
10:18:34	→	prite joins (~pritam@user/pritambaral)
10:19:02	→	Nahra joins (~user@static.161.95.99.88.clients.your-server.de)
10:23:57	×	thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 272 seconds)
10:24:26	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds)
10:25:06	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:26:46	<boxscape>	hah
10:26:47	<boxscape>	% type C :: forall a -> (a ~ Int) => *; data C a = C a deriving Show
10:26:47	<yahb>	boxscape:
10:26:54	<boxscape>	as far as I can tell, this Show instance is impossible to write by hand
10:27:34	<boxscape>	(barring, perhaps, unsafeCoerce)
10:28:16	<boxscape>	though I'm not even sure that helps
10:30:10	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
10:30:14	<boxscape>	you can write one for `C Int`, but not for `Show a => C a`, which the derived one is
10:30:17	×	cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds)
10:30:24	→	cheater1__ joins (~Username@user/cheater)
10:30:25	cheater1__	is now known as cheater
10:30:46	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
10:31:09	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:31:34	→	chomwitt joins (~Pitsikoko@athedsl-20549.home.otenet.gr)
10:31:41	→	zeenk joins (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41)
10:34:10	→	pera joins (~pera@user/pera)
10:35:14	<boxscape>	% :t show @(C _) -- well, this claims that it only works for C Int, however...
10:35:14	<yahb>	boxscape: C Int -> String
10:35:15	<boxscape>	% show (C "foo") -- this works just fine
10:35:15	<yahb>	boxscape: "C \"foo\""
10:35:25	×	hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.)
10:35:47	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds)
10:35:59	×	Toast52 quits (~Toast52@151.192.167.120) (Ping timeout: 272 seconds)
10:36:25	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds)
10:36:43	×	haskman quits (~haskman@171.48.41.1) (Quit: Going to sleep. ZZZzzz…)
10:37:07	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:37:19	<dminuoso>	boxscape What is this `type C :: ` annotation?
10:37:37	<boxscape>	dminuoso -XStandaloneKindSignatures, or do you mean this specific one?
10:37:41	×	chomwitt quits (~Pitsikoko@athedsl-20549.home.otenet.gr) (Ping timeout: 272 seconds)
10:37:43	<dminuoso>	I guess that's what I mean
10:37:45	<boxscape>	ok
10:38:28	<dminuoso>	boxscape: Is there a linkage between the choice of the type variable `a` in the standalone kind signature and the following declaration?
10:38:35	<dminuoso>	% type C :: forall b -> (b ~ Int) => *; data C a = C a deriving Show
10:38:35	<yahb>	dminuoso:
10:38:39	<boxscape>	nope
10:38:49	<boxscape>	I don't think ScopedTypeVariables interacts with this, either
10:39:01	<dminuoso>	What is => ?
10:39:09	×	Feuermagier quits (~Feuermagi@user/feuermagier) (Ping timeout: 272 seconds)
10:39:13	<dminuoso>	Dark magic here
10:39:14	<boxscape>	same as ever, constraint quantifier
10:39:19	<dminuoso>	Oh
10:39:34	<dminuoso>	Ah hold on, this `forall b -> ` is a visible something something
10:39:38	<boxscape>	yup
10:39:44	<boxscape>	visible dependent quantification
10:39:48	<dminuoso>	Yes.
10:40:03	<dminuoso>	I recall the ghc proposal
10:40:23	<nshepperd>	% :t C
10:40:23	<yahb>	nshepperd: forall {b} {ev :: b ~ Int}. b -> C b
10:40:48	<dminuoso>	% :t C String
10:40:48	<yahb>	dminuoso: ; <interactive>:1:3: error:; * Data constructor not in scope: String; * Perhaps you meant one of these: `StringL' (imported from Language.Haskell.TH), variable `string' (imported from Text.Parsec), `Strict' (imported from Control.Lens)
10:40:51	<dminuoso>	% :t C "foo"
10:40:51	<yahb>	dminuoso: C String
10:40:58	<nshepperd>	???
10:41:17	<boxscape>	% :k C String
10:41:17	<yahb>	boxscape: (String ~ Int) => *
10:41:32	<dminuoso>	{ev :: b ~ Int}
10:41:34	<dminuoso>	What is that even saying?
10:41:41	<boxscape>	err
10:42:01	<boxscape>	pass a dictionary with an equality constraint?
10:42:11	<boxscape>	(I'm kind of wondering where the ev name comes from)
10:42:22	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds)
10:42:24	<dminuoso>	boxscape: wouldn't that rather be written as `b ~ Int =>`?
10:42:35	<boxscape>	yeah but I guess that's sort of the same thing in core
10:42:40	<dminuoso>	this thing is quantified over ev, whose type is (!) b ~ Int
10:42:44	<dminuoso>	I have no clue what that means
10:43:09	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:43:09	<boxscape>	I mean you can't write it, so it's questionable whether it means anything
10:43:16	<nshepperd>	pass a promoted constraint evidence as a type variable, lol
10:43:24	→	haskman joins (~haskman@171.48.41.1)
10:43:24	<dminuoso>	lol
10:44:12	<dminuoso>	Well, but wouldnt I be able to write
10:44:19	<nshepperd>	also how does it even refer to b when the type variables in the declaration didn't even match up
10:44:45	<dminuoso>	nshepperd: that's not a problem
10:44:52	<boxscape>	okay "ev" means "evidence"
10:45:10	<dminuoso>	boxscape: So I guess your assumption about "pass a dictionary with an equality cosntraint" is right
10:45:15	→	thiross joins (~user@173.242.113.143.16clouds.com)
10:45:17	<dminuoso>	Or it seems reasonable
10:45:21	<dminuoso>	but the type signature still looks off
10:45:27	<boxscape>	oh yeah absolutely
10:45:36	<nshepperd>	except it's a promoted dictionary, which is nonsense
10:45:39	<dminuoso>	as that should rahter read `forall b. b ~ Int => b -> C b`
10:46:06	→	hmmmas joins (~chenqisu1@183.217.202.217)
10:46:06	<dminuoso>	Is this some subtle bug?
10:47:08	<boxscape>	probably
10:47:12	<nshepperd>	dminuoso: isn't it a problem? where is it getting that the type variable which has to be ~ Int, is the same type variable as the first parameter of C? that's not written anywhere
10:47:25	<dminuoso>	nshepperd: its from the standalone signature
10:47:34	<dminuoso>	% type C :: forall b -> (b ~ Int) => *; data C a = C a deriving Show
10:47:34	<yahb>	dminuoso:
10:47:51	<nshepperd>	right, b is not a
10:47:54	<dminuoso>	boxscape: curious, is the visible dependent qualifier necessary? why cant we use `forall b.`?
10:47:58	<dminuoso>	nshepperd: that's irrelevant
10:48:07	<dminuoso>	nshepperd: its not in the same scope
10:48:14	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
10:48:18	<nshepperd>	that doesn't help
10:48:25	<boxscape>	nshepperd it's the same because it's the first parameter to C, in the standalone kind signature and in its definition
10:48:32	<dminuoso>	similar to how you could write: `id :: forall a. a -> a; id @b c = c`
10:48:46	<boxscape>	% type D :: forall b . (b ~ Int) => *; data D a = MkD a deriving Show
10:48:46	<yahb>	boxscape: ; <interactive>:57:38: error:; * Not a function kind: ; but extra binders found: a; In the data type declaration for `D'
10:48:53	<nshepperd>	hmm
10:48:59	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:49:08	<dminuoso>	boxscape: this diagnostic reads really weird too
10:49:12	<dminuoso>	"not a function kind: *"
10:49:29	<boxscape>	% type D :: forall b . (b ~ Int) => *; data D @a = MkD a deriving Show -- I would almost expect this to work
10:49:29	<yahb>	boxscape: ; <interactive>:59:46: error:; Unexpected type application @a; In the data declaration for `D'
10:49:32	<dminuoso>	I think I understand why GHC says this.
10:49:45	<dminuoso>	Presumably with the chance, data declarations are necessarily visible dependent
10:49:48	<dminuoso>	*change
10:49:53	×	thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 252 seconds)
10:51:24	<boxscape>	hmm, not quite
10:51:27	<boxscape>	% :k Proxy
10:51:27	<yahb>	boxscape: k -> *
10:51:36	×	xff0x quits (~xff0x@2001:1a81:52ca:4f00:8a7f:8182:f670:e586) (Remote host closed the connection)
10:51:43	<boxscape>	this has both non-dependent visible and dependent invisible quantification
10:51:52	→	xff0x joins (~xff0x@2001:1a81:52ca:4f00:a77b:5731:d9ca:93c9)
10:52:01	<boxscape>	I think
10:52:32	<boxscape>	full kind is `forall k . k -> *`
10:54:01	<dminuoso>	% :set -fexplicit-forall
10:54:01	<yahb>	dminuoso: Some flags have not been recognized: -fexplicit-forall
10:54:03	<dminuoso>	uh
10:54:17	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
10:54:27	<dminuoso>	% :set -fprint-explicit-foralls
10:54:28	<yahb>	dminuoso:
10:54:30	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
10:54:31	<dminuoso>	% :k Proxy
10:54:31	<yahb>	dminuoso: forall {k}. k -> *
10:54:49	<dminuoso>	boxscape: this looks very invisible to me
10:55:02	<boxscape>	yes, the k is inferred, invisible, and dependent
10:55:05	<boxscape>	the forall {k}
10:55:12	<boxscape>	but the `k ->` is visible and independent
10:55:24	<dminuoso>	uh
10:55:26	<boxscape>	or.. non-dependent, not sure
10:55:43	×	wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
10:55:52	<nshepperd>	% :t Proxy
10:56:13	<boxscape>	I accidentally redefined the data constructor Proxy in a private yahb session I think fwiw :)
10:56:22	<boxscape>	but not sure why yahb isn't showing anything
10:56:29	→	aman joins (~aman@user/aman)
10:56:54	<boxscape>	% "yahb?"
10:57:25	<nshepperd>	RIP
10:58:28	<dminuoso>	12:55:12 boxscape \| but the `k ->` is visible and independent
10:58:36	<dminuoso>	boxscape: Are you sure here?>
10:58:46	<boxscape>	yep, 98%
10:58:58	×	yahb quits (xsbot@user/mniip/bot/yahb) (Ping timeout: 264 seconds)
10:59:54	<boxscape>	dminuoso from richard eisenberg's thesis: https://i.imgur.com/2XEl2Ls.png
11:00:03	×	favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat)
11:01:19	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
11:01:22	<boxscape>	(though he has since said calling it "relevant" is a mistake, and it should be "erasable" and "non-erasable" instead of "irrelevant" and "relevant", but that's one of the dimensions we weren't talking about here, anyway)
11:01:24	<dminuoso>	boxscape: Ah I see where my confusion comes from.
11:01:45	→	thiross joins (~user@173.242.113.143.16clouds.com)
11:02:49	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
11:03:45	→	yahb joins (xsbot@user/mniip/bot/yahb)
11:04:50	<boxscape>	% :t Proxy
11:04:51	<yahb>	boxscape: forall {k} {a :: k}. Proxy' a
11:04:58	×	pera quits (~pera@user/pera) (Ping timeout: 264 seconds)
11:05:05	→	pera joins (~pera@137.221.132.196)
11:05:19	<boxscape>	% :q
11:05:19	<yahb>	boxscape:
11:05:22	<boxscape>	% :t Proxy
11:05:22	<yahb>	boxscape: forall {k} {t :: k}. Proxy t
11:05:28	pera	is now known as Guest5645
11:05:39	×	haskman quits (~haskman@171.48.41.1) (Quit: Going to sleep. ZZZzzz…)
11:05:46	×	megaTherion quits (~therion@unix.io) (.net .split)
11:05:47	×	farn quits (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) (.net .split)
11:06:22	×	shryke quits (~shryke@91.103.43.254) (Ping timeout: 268 seconds)
11:06:39	→	haskman joins (~haskman@171.48.41.1)
11:07:36	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 268 seconds)
11:09:17	→	waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd)
11:11:23	→	megaTherion joins (~therion@unix.io)
11:11:23	→	farn joins (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505)
11:11:29	→	Feuermagier joins (~Feuermagi@user/feuermagier)
11:11:45	×	waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Client Quit)
11:11:52	<boxscape>	% toDyn (MkC 53 :: C Int)
11:11:52	<yahb>	boxscape: ; <interactive>:5:1: error:; * No instance for (Typeable <>) arising from a use of `toDyn'; * In the expression: toDyn (MkC 53 :: C Int); In an equation for `it': it = toDyn (MkC 53 :: C Int)
11:11:54	<boxscape>	what?
11:11:55	×	Guest5645 quits (~pera@137.221.132.196) (Ping timeout: 268 seconds)
11:11:57	<boxscape>	what is <>
11:12:07	→	waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd)
11:12:18	<dminuoso>	% :t toDyn
11:12:18	<yahb>	dminuoso: Typeable a => a -> Dynamic
11:13:40	<dminuoso>	% :t MkC
11:13:40	<yahb>	dminuoso: forall {a} {ev :: a ~ Int}. a -> C a
11:14:11	<lortabac>	is there a way to get the list of all the dependencies of a project (including the transitive ones)?
11:14:22	<dminuoso>	lortabac: cabal-plan
11:14:44	<lortabac>	is it a separate executable that I need to install?
11:14:57	<dminuoso>	Yeah, you can install it with `cabal install cabal-plan` if you like
11:15:14	×	raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 265 seconds)
11:15:17	<lortabac>	ok thanks
11:17:02	×	econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity)
11:17:02	<dminuoso>	lortabac: Alternatively you can jq into dist-newstyle/cache/plan.json (cabal-plan is also just an interface for that file)
11:17:28	<lortabac>	apparently cabal-plan can generate dot files, it seems worth installing
11:17:40	<dminuoso>	Indeed, it can also do transitive reduction, which might be useful to you
11:18:43	×	farn quits (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) (Ping timeout: 268 seconds)
11:19:04	→	farn joins (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505)
11:19:06	→	bhrgunatha joins (~bhrgunath@2001-b011-8011-18ad-e68c-7ce2-e7ef-f120.dynamic-ip6.hinet.net)
11:19:20	×	megaTherion quits (~therion@unix.io) (Ping timeout: 268 seconds)
11:19:29	→	megaTherion joins (~therion@unix.io)
11:21:14	→	raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
11:22:59	×	bhrgunatha quits (~bhrgunath@2001-b011-8011-18ad-e68c-7ce2-e7ef-f120.dynamic-ip6.hinet.net) (Client Quit)
11:25:09	→	shryke joins (~shryke@91.103.43.254)
11:25:18	←	lieuwex parts (~lieuwelie@2001:470:69fc:105::4e6) ()
11:30:42	→	machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca)
11:32:27	×	Guest31 quits (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com)
11:34:26	×	slep quits (~slep@cpc150002-brnt4-2-0-cust437.4-2.cable.virginm.net) (Ping timeout: 252 seconds)
11:34:35	×	raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 3.1)
11:34:56	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
11:36:29	→	keutoi joins (~keutoi@157.48.91.62)
11:36:41	→	slep joins (~slep@cpc150002-brnt4-2-0-cust437.4-2.cable.virginm.net)
11:37:52	→	Toast52 joins (~Toast52@151.192.167.120)
11:42:30	×	xsperry quits (~as@user/xsperry) (Read error: Connection reset by peer)
11:42:59	→	lavaman joins (~lavaman@98.38.249.169)
11:44:36	×	aman quits (~aman@user/aman) (Quit: aman)
11:44:46	×	wanagnuj quits (~wanagnuj@101.95.97.158) (Quit: wanagnuj)
11:46:21	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:46:31	→	mc47 joins (~yecinem@89.246.239.190)
11:46:59	<thiross>	% :t flip
11:46:59	<yahb>	thiross: (a -> b -> c) -> b -> a -> c
11:48:18	×	shailangsa quits (~shailangs@host165-120-169-73.range165-120.btcentralplus.com) (Ping timeout: 268 seconds)
11:50:38	→	mattil joins (~mattil@airio.portalify.com)
11:51:07	×	eightball quits (~eight@86.106.121.164) (Quit: Leaving)
11:51:16	→	smitop joins (uid328768@user/smitop)
11:51:23	×	v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 268 seconds)
11:52:11	→	Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi)
11:52:56	×	ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Ping timeout: 265 seconds)
11:55:23	→	shiraeeshi joins (~shiraeesh@109.166.57.115)
11:58:32	→	ubert joins (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233)
12:00:37	←	japh parts (~scp1@user/japh) ()
12:03:40	→	v01d4lph4 joins (~v01d4lph4@122.160.65.250)
12:03:40	×	v01d4lph4 quits (~v01d4lph4@122.160.65.250) (Changing host)
12:03:40	→	v01d4lph4 joins (~v01d4lph4@user/v01d4lph4)
12:04:04	→	Toast52_ joins (~Toast52@151.192.167.120)
12:04:23	×	sondre quits (~sondrelun@cm-84.212.100.140.getinternet.no) (Ping timeout: 244 seconds)
12:04:29	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds)
12:06:35	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
12:07:45	×	hmmmas quits (~chenqisu1@183.217.202.217) (Quit: Leaving.)
12:08:15	×	Toast52 quits (~Toast52@151.192.167.120) (Ping timeout: 272 seconds)
12:09:20	→	holy_ joins (~h01y_b4z0@103.244.176.36)
12:13:10	→	zebrag joins (~chris@user/zebrag)
12:18:54	×	waleee quits (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) (Ping timeout: 264 seconds)
12:18:55	×	azeem quits (~azeem@dynamic-adsl-78-13-240-225.clienti.tiscali.it) (Read error: Connection reset by peer)
12:18:59	×	holy_ quits (~h01y_b4z0@103.244.176.36) (Remote host closed the connection)
12:20:37	→	waleee joins (~waleee@h-98-128-228-119.NA.cust.bahnhof.se)
12:20:46	→	shailangsa joins (~shailangs@host165-120-169-73.range165-120.btcentralplus.com)
12:20:48	→	azeem joins (~azeem@dynamic-adsl-78-13-240-225.clienti.tiscali.it)
12:27:37	→	river joins (~river@tilde.team/user/river)
12:33:40	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
12:43:47	→	bor0 joins (~boro@user/bor0)
12:44:25	×	xff0x quits (~xff0x@2001:1a81:52ca:4f00:a77b:5731:d9ca:93c9) (Ping timeout: 268 seconds)
12:44:57	<bor0>	Hey, ski :wave: I just did https://github.com/bor0/hoare-imp/commit/d7b154b8d9b68fcf6466b22ff1f40591db3dcdb4 per your suggestions. Now I find myself doing this a lot: https://github.com/bor0/hoare-imp/blob/master/examples/ExampleHoare.hs#L47. Is there a neater way? :)
12:45:05	→	xff0x joins (~xff0x@2001:1a81:52ca:4f00:7b0a:bab9:5836:8b3b)
12:45:23	←	otoburb parts (~otoburb@user/otoburb) ()
12:45:29	<bor0>	Specifically, the `x >>= \x -> ...` part. `hlint` reported `>=>` but it only slightly helps
12:45:39	×	xwx quits (~george@user/george) (Ping timeout: 268 seconds)
12:48:29	<boxscape>	:t \pre post step5 hoareConsequence -> pre >>= \pre -> post >>= \post -> step5 >>= \step5 -> hoareConsequence pre step5 post
12:48:30	<lambdabot>	Monad m => m t1 -> m t2 -> m t3 -> (t1 -> t3 -> t2 -> m b) -> m b
12:48:32	<boxscape>	:t \pre post step5 hoareConsequence -> hoareConsequence <$> pre <> step5 <> post
12:48:32	<lambdabot>	Applicative f => f a1 -> f a2 -> f a3 -> (a1 -> a3 -> a2 -> b) -> f b
12:48:39	<boxscape>	^ does that work for you bor0?
12:49:12	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
12:49:13	<bor0>	Whoa. Let me try that. Looks like it should do it
12:49:30	→	lavaman joins (~lavaman@98.38.249.169)
12:49:36	<boxscape>	:t \pre post step5 hoareConsequence -> liftA3 hoareConsequence pre step5 post -- bor0 alternatively
12:49:37	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
12:49:37	<lambdabot>	Applicative f => f a -> f c -> f b -> (a -> b -> c -> d) -> f d
12:51:17	<bor0>	It works! Magical. Looks awesome. Thanks!
12:51:21	<boxscape>	np
12:51:42	<boxscape>	(you'll see this "applicative style" quite often)
12:51:53	×	brian_da_mage quits (~Neuromanc@user/briandamag) (Ping timeout: 264 seconds)
12:52:17	<bor0>	An interesting ride. From pure functions to monads to applicative. But the end result is totally worth it
12:53:16	<boxscape>	that's pretty much the timeline in terms of how people applied the concepts to functional programming, as well :)
12:53:38	→	berberman joins (~berberman@user/berberman)
12:53:42	×	berberman_ quits (~berberman@user/berberman) (Ping timeout: 264 seconds)
12:53:46	→	pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net)
12:53:46	<bor0>	History repeats itself! :D
12:56:50	<bor0>	Any clue why `ruleJoin <$> ruleSepR pq <> ruleSepL pq ` doesn't work but `ruleJoin <$> ruleSepR pq <> ruleSepL pq >>= id` does? `>>= id` seems hacky
12:57:30	<boxscape>	(>>= id) is called join
12:57:31	<boxscape>	:t join
12:57:32	<lambdabot>	Monad m => m (m a) -> m a
12:57:59	<tomsmeding>	bor0: if this is your first meeting with those applicative operators, I encourage you to look closely at the types of (<$>) (which is just fmap, by the way), (<>) and (>>=). Then look at them again the next time you use them. At some point it will become clear how this 'f <$> a <> b <> c' style actually works. A bit later you'll realise how Applicative, which is defined by pure and <>, is
12:57:59	<tomsmeding>	actually a bit weaker than Monad, and them you might understand how things like applicative parsing are different from monadic parsing. For me it took a while to get familiar with these type classes, but it's worth spending a bit of time looking at type signatures now and then :)
12:58:07	<boxscape>	I imagine you're ending up with a nested Monad in the first expression, and join lets you flatten that to one level of Monad
13:00:22	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
13:00:44	<bor0>	tomsmeding, thanks. I did meet Applicative/Monad and vaguely know their definition. I'm at the level where it isn't obvious what makes a monad and what makes an applicative so my approach is usually to write it "manually" and only then to abstract when it becomes obvious (usually becomes obvious when I join and ping this channel :))
13:01:00	→	xwx joins (~george@user/george)
13:01:16	→	alx741 joins (~alx741@186.178.108.160)
13:04:05	→	geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com)
13:04:08	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
13:05:30	×	hydroxonium quits (uid500654@id-500654.stonehaven.irccloud.com) (Quit: Connection closed for inactivity)
13:05:49	<dminuoso>	bor0: Yup, keep on doing this. At some point, Applicative/Monad will kick in completely automatically, without you forcing the issue.
13:06:04	<bor0>	Thanks. Right, just like driving. I hope. :)
13:06:07	<dminuoso>	Im going to argue, until then its not even important to understand what they abstract over.
13:06:35	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Remote host closed the connection)
13:06:48	×	xprlgjf quits (~gavin@60.27.93.209.dyn.plus.net) (Read error: Connection reset by peer)
13:07:32	×	v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
13:08:01	<dminuoso>	Applicative is probably a bit harder to grasp, because most Applicative things happen to be Monad too (which subsumes Applicative), so you're less likely to encounter "just Applicative" things.
13:08:05	→	v01d4lph4 joins (~v01d4lph4@user/v01d4lph4)
13:08:21	<dminuoso>	(Though both interfaces are easy enough to learn, obviously)
13:08:41	→	wei2912 joins (~wei2912@112.199.250.21)
13:08:54	<bor0>	Another thing that smells is the too many `Right`'s here: https://github.com/bor0/hoare-imp/blob/master/src/Gentzen.hs#L31-L42. Any way it can be improved?
13:09:13	<bor0>	(Just throwing random code lines, but happy to elaborate further on the code/ideas behind it)
13:09:15	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 272 seconds)
13:10:33	→	dunkeln joins (~dunkeln@94.129.65.28)
13:11:06	<boxscape>	make a helper function `foo arg = go xs f x >>= \prfx -> Right $ Proof $ arg`, though choose a better name than `foo` :)
13:11:14	<boxscape>	and then replace each of those lines with a call to that function
13:11:24	<bor0>	I thought of that, but note `go _ f x = f (Proof x)`
13:11:43	<boxscape>	right, just keep that line as is
13:11:53	<boxscape>	and use the helper function in the other lines
13:12:16	<dminuoso>	I can see some elaborate tricks to make the Right go away, but nothing worth your while
13:12:52	×	thiross quits (~user@173.242.113.143.16clouds.com) (Remote host closed the connection)
13:12:53	×	azeem quits (~azeem@dynamic-adsl-78-13-240-225.clienti.tiscali.it) (Ping timeout: 252 seconds)
13:12:53	×	v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 264 seconds)
13:13:00	→	thiross joins (~user@173.242.113.143.16clouds.com)
13:13:11	<boxscape>	ah I suppose it has to be slightly different
13:13:18	<boxscape>	because arg may depend on prfx/prfy
13:13:43	<boxscape>	err, also on x/y
13:13:50	<dminuoso>	bor0: though, just use fmap, rather than >>=
13:14:00	<dminuoso>	That lets you avoid the Right
13:14:03	<bor0>	Yeah. OK, just felt a little bit odd and wanted to double-check if it can be abstracted even further
13:14:13	<dminuoso>	Yeah, that's the key thing. Just use fmap, the Right disappears :)
13:14:20	→	flowz joins (~flowz@2a01:aea0:dd4:1573:a8:24ac:7db2:5b39)
13:14:26	<dminuoso>	<&> fits comfortably there
13:14:33	<dminuoso>	Looks ergonomically nicer than <$> or fmap
13:14:46	<dminuoso>	I'd write it like this:
13:15:01	<dminuoso>	go xs f <&> \(Proof f) -> Proof (Not f)
13:15:53	→	azeem joins (~azeem@dynamic-adsl-94-34-16-203.clienti.tiscali.it)
13:16:05	<bor0>	OK, I'll need some time to unpack that. Otherwise I won't be able to update my code when I go back to it in a few days :D
13:16:12	<bor0>	Read-only!
13:16:20	<dminuoso>	bor0: So let me make it easy to see for you
13:16:34	<dminuoso>	First realize that `Right = return` or `Right = pure`
13:17:15	<dminuoso>	Then realize you have: fmap f x = pure f <*> x
13:17:39	<dminuoso>	Do a bit of juggling
13:17:42	×	thiross quits (~user@173.242.113.143.16clouds.com) (Ping timeout: 264 seconds)
13:18:48	→	thiross joins (~user@173.242.113.143.16clouds.com)
13:20:22	→	lavaman joins (~lavaman@98.38.249.169)
13:20:44	<boxscape>	you could also derive Functor for Proof and then replace `\(Proof f) -> Proof (Not f)` with `fmap Not`, I think
13:20:54	<dminuoso>	Yup!
13:21:01	<dminuoso>	Or, with <&> that would look even nicer
13:21:17	<dminuoso>	go xs f <&> fmap Not
13:21:27	←	thiross parts (~user@173.242.113.143.16clouds.com) ()
13:21:37	→	xsperry joins (~as@user/xsperry)
13:21:40	<dminuoso>	Or maybe you write g <&&> f = fmap (fmap f) g
13:21:43	<dminuoso>	And then you have
13:21:45	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
13:21:47	<dminuoso>	go xs f <&&> Not
13:22:10	<bor0>	Reading it makes sense, thanks. Just still need some practice for it to sink in.
13:24:10	→	geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com)
13:24:34	×	Toast52_ quits (~Toast52@151.192.167.120) (Quit: Leaving)
13:24:54	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 264 seconds)
13:25:04	×	mjs2600 quits (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in)
13:25:18	→	mjs2600 joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net)
13:27:06	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
13:27:15	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
13:28:04	×	mjs2600 quits (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Client Quit)
13:28:19	→	mjs2600 joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net)
13:29:13	→	AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net)
13:29:23	×	hendursa1 quits (~weechat@user/hendursaga) (Quit: hendursa1)
13:29:49	→	hendursaga joins (~weechat@user/hendursaga)
13:32:02	→	arrowd joins (~arr@2.94.203.147)
13:32:04	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
13:33:40	→	chomwitt joins (~Pitsikoko@athedsl-20549.home.otenet.gr)
13:33:47	→	niflce joins (~IceChat95@user/niflce)
13:35:34	<boxscape>	Has anyone tried to make STG run on a GPU?
13:36:32	→	fm joins (~fm@user/fm)
13:36:45	<[exa]>	boxscape: but why
13:36:58	<boxscape>	idle curiosity, mostly :)
13:37:08	<[exa]>	GPUs are _terribly bad_ at that precise kind of computation
13:37:13	<merijn>	boxscape: tbh, that sounds like a bad idea
13:37:23	×	wonko quits (~wjc@62.115.229.50) (Quit: See You Space Cowboy..)
13:37:34	<boxscape>	what is the part of STG that they are bad at?
13:37:37	<[exa]>	pointers
13:37:41	<boxscape>	Ah, I see
13:37:44	<merijn>	Lots of pointers, lots of branches
13:37:55	<[exa]>	"control flow" too
13:38:16	<merijn>	Poor cache locality, no easy way to do latency hiding due to irregular control flow
13:38:33	<boxscape>	okay
13:38:50	<[exa]>	technically, it would be extremely interesting to do an experiment of STG vs. nursery in the shared memory
13:38:56	<merijn>	boxscape: Basically, GPU memory is rather high latency (high bandwidth, but also high latency)
13:39:08	×	shiraeeshi quits (~shiraeesh@109.166.57.115) (Quit: Leaving)
13:39:15	<merijn>	boxscape: Which is not a problem if you can do latency hiding due to high levels of parallelism
13:39:17	→	slowButPresent joins (~slowButPr@user/slowbutpresent)
13:39:30	<[exa]>	but likely that's the same esoterism level of "interesting" as "you can do programming with drawing an interpretable bitmap"
13:39:37	<merijn>	But the parallelism in current GPUs really wants regular access patterns/control flow, which STG doesn't really have
13:39:49	<boxscape>	I see, that makes sense
13:41:05	×	keutoi quits (~keutoi@157.48.91.62) (Ping timeout: 264 seconds)
13:41:08	<bor0>	`(axiom1 (Var A) >>= \ax1 -> ruleSpec ax1 (Var A))` So I thought something like `ruleSpec <$> axiom1 (Var A) <*> Var A` would work, but not. I need to "lift"(?) the last Var A somehow?
13:41:50	<boxscape>	it's more like you're lifting it when it shouldn't be lifted IIUC
13:42:00	<bor0>	Or that :)
13:42:11	<boxscape>	flip ruleSpec (Var A) <$> axiom1 (Var A)
13:42:12	<boxscape>	does that work?
13:42:34	→	jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
13:42:43	→	keutoi joins (~keutoi@157.48.91.62)
13:43:15	<bor0>	With a join prepended, yeah. ghci evals True == (join $ flip ruleSpec (Var A) <$> axiom1 (Var A)) == (axiom1 (Var A) >>= \ax1 -> ruleSpec ax1 (Var A))
13:43:49	<bor0>	There's no unlift or something? `flip` seems to be specific,.. what if the argument was 3rd
13:44:10	<boxscape>	right, I guess we're not really gaining anywhere here, it's just (axiom1 (Var A) >>= flip ruleSpec)
13:44:49	<bor0>	I am happy with it as it is, unless it can look better :)
13:45:21	<boxscape>	bor0 I don't think there's a nice way to unlift something at the moment, at least in base
13:45:21	×	unyu quits (~pyon@user/pyon) (Quit: WeeChat 3.1)
13:45:43	<boxscape>	flip is pretty specific , sometimes there isn't a better way than writing a lambda
13:45:45	<boxscape>	e.g.
13:45:49	<boxscape>	@pl f a b = f b a
13:45:49	<lambdabot>	f = fix flip
13:45:55	<boxscape>	eh wait I don't want fix
13:46:01	<boxscape>	@pl f a b = g b a
13:46:01	<lambdabot>	f = flip g
13:46:04	<boxscape>	that's fine
13:46:20	<boxscape>	@pl f a d e = g a b c d e f
13:46:20	<lambdabot>	f = fix (flip (flip . (flip .) . flip (flip g b) c))
13:46:27	<boxscape>	that's definitely not fine, and a lambda is better
13:46:33	<bor0>	Haha!
13:47:29	<bor0>	That seems like a nice way to make a friendly coworker, if I ever get to write Haskell in production
13:47:41	<boxscape>	true
13:47:47	<flowz>	hi, haskell newbie with a quick question here. I need to create a tree structure with some special handling of the root node. I tried to encode my idea like the following "MWE": https://pastebin.com/bHdtkJvy . But it doesn't allow me to match the "inner" sum type that way. I haven't been able to figure out how to do so. Would need and appreciate a
13:47:47	<flowz>	bit of help :)
13:49:13	→	ystael joins (~ystael@user/ystael)
13:50:46	→	pe200012 joins (~pe200012@119.131.208.84)
13:51:54	<[exa]>	flowz: you either need to setup overloading, or have a second function for the "inner" tree
13:52:35	<[exa]>	flowz: this kind of ad-hoc overloading a function for multiple types (as known from c++ and others) does not combine well with type inference, so haskell doesn't really support it
13:53:41	→	jneira joins (~jneira@166.red-81-39-172.dynamicip.rima-tde.net)
13:53:42	<flowz>	@[exa] thanks for the help, will go for secondary functions then. Though it may be possible someway like that and I just couldn't find the right syntax.
13:53:57	<ski>	flowz : `data Tree = Root \| Node' looks confused
13:54:22	→	myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net)
13:54:46	<[exa]>	flowz: you might not even need the whole second data structure, I'd go with one Tree structure for everything, and have 2 functions for root and non-root cases (and let the user call the root one always)
13:54:57	<ski>	(hint, that declaration is entirely unrelated to the two earlier `data' declarations)
13:55:03	→	lavaman joins (~lavaman@98.38.249.169)
13:55:59	<flowz>	@ski oh, good to know. @[exa] thanks for the tip, I'll probably have to rethink my approach
13:55:59	<lambdabot>	Maybe you meant: wiki src ask
13:56:11	<ski>	flowz : what are you trying to do ?
13:56:32	<[exa]>	flowz: btw @ doesn't work for highlighting on IRC, the convention is to just write `nick:` :]
13:57:30	×	haskman quits (~haskman@171.48.41.1) (Quit: Going to sleep. ZZZzzz…)
13:57:51	<arrowd>	Speaking of STG, there are many posts on this matter in the Internet, but I haven't found any information on how STG gets mapped to machine instructions.
13:57:54	→	chddr joins (~Thunderbi@31.148.23.125)
13:57:55	<ski>	(from what you've said, i'd go with [exa]'s suggestion)
13:58:00	<arrowd>	It isn't being interpreted, right?
13:58:07	<flowz>	ski: basically I have to build a balanced tree from some input data and then output the tree in a given format. Choice of language is left to us, so I thought I might use haskell as an exercise (as the task seemed simple enough, and I recently started learning it)
13:58:21	×	mattil quits (~mattil@airio.portalify.com) (Remote host closed the connection)
13:58:27	×	pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2-dev)
13:59:06	×	Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection)
13:59:36	<boxscape>	arrowd https://www.microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf Chapter 9 is "Compiling the STG language to C"
13:59:40	<boxscape>	page 52
13:59:41	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 264 seconds)
13:59:43	<ski>	flowz : and in what way is that related to handling the root differently ?
14:00:58	<flowz>	the definition of the btree we are given the root only has 1 value and 2 childs, while all other nodes have /k/ values and /k+1/ childs. It's a weird definition of the balanced tree, haven't been able to find any other resources that define it like that
14:01:08	<arrowd>	boxscape: The current GHC does not compile to C. AFAIK, that "registerization" thing is exactly what I'm looking for.
14:01:47	<geekosaur>	in ghc, STG is compiled to Cmm which is compiled to assembly language or LLVM IR depending on backend
14:04:40	<arrowd>	So, "registerization" is related to Cmm, not STG?
14:05:00	<int-e>	flowz: that's restrictive (each node should allow up to 2k-1 children)... but the root is indeed a bit special in b-trees
14:05:20	→	pe200012_ joins (~pe200012@218.107.17.245)
14:05:41	×	pe200012 quits (~pe200012@119.131.208.84) (Ping timeout: 264 seconds)
14:06:54	<geekosaur>	I think so, yes. the unregisterized backend still exists (but isn't included in ghc releases) and is another post-Cmm target
14:07:37	<ski>	flowz : hm, ok. anyway, the issue with `data Tree = Root \| Node' is that this is declaring an (unparameterized) data type, named `Tree', having two possible shapes (data constructors), `Root' and `Node'. these two are entirely unrelated to your (parameterized) types `Root' and `Node'
14:08:27	<ski>	flowz : basically, `data Tree = Root \| Node' is comparable to `data Pet = Cat \| Dog' or `data Bool = False \| True' .. it's just a data type, having two values
14:10:01	<arrowd>	Ok, then I'm interested in STG -> Cmm part.
14:10:48	<ski>	flowz : in any case, it seems misguided to want to check whether you're given a root node, or another node. afaiui, you should already know which one you're passed, in every point of the program
14:11:59	×	ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Ping timeout: 268 seconds)
14:12:10	<flowz>	I'm starting to think I should go through some tutorials some more before doing even this (comparatively simple) task. There're still some more basic things I haven't grasped enough. I'll do it in some other language as the deadline is approaching rapidly, but still thanks for all the help and pointers :)
14:13:34	→	hexfive joins (~eric@50.35.83.177)
14:13:38	<ski>	flowz : possibly you could use something like `data Node a = EmptyNode \| InternalNode (Node a) [(a,Node a)]', for the internal nodes
14:16:25	<ski>	(hm, or maybe you intended `k' to be the same for all internal nodes ?)
14:21:53	×	azeem quits (~azeem@dynamic-adsl-94-34-16-203.clienti.tiscali.it) (Read error: Connection reset by peer)
14:22:50	→	ikex joins (~ash@user/ikex)
14:23:51	<flowz>	ski: yep, k should be the same, and I've also got that included in my actual code. But I'm going to do it in some other language for now, as I've only got a couple of hours left, and there's still some other more time-consuming stuff left to do as well.. Though I'll have a look at doing something with haskell at the next good opportunity, as I find
14:23:52	<flowz>	the language quite interesting. Again, thanks for all the help, gtg now
14:24:10	×	flowz quits (~flowz@2a01:aea0:dd4:1573:a8:24ac:7db2:5b39) (Quit: Client closed)
14:26:24	→	azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it)
14:27:08	→	adziahel[m] joins (~adziahelm@2001:470:69fc:105::b4d)
14:28:25	×	niflce quits (~IceChat95@user/niflce) (Ping timeout: 272 seconds)
14:30:20	→	lavaman joins (~lavaman@98.38.249.169)
14:31:39	→	niflce joins (~IceChat95@user/niflce)
14:41:09	→	koishi_ joins (~koishi_@67.209.186.120.16clouds.com)
14:43:13	×	koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection)
14:44:15	→	Sgeo joins (~Sgeo@user/sgeo)
14:47:46	→	haskman joins (~haskman@171.48.41.1)
14:48:04	→	LukeHoersten joins (~LukeHoers@user/lukehoersten)
14:50:30	<[exa]>	arrowd: Cmm is a VERY rough lookalike of C, assignment of instructions and registers happens when compiling Cmm
14:51:04	<arrowd>	[exa]: So, "registerizing" is basically adding a new backend to Cmm?
14:51:06	×	LukeHoersten quits (~LukeHoers@user/lukehoersten) (Client Quit)
14:51:38	<[exa]>	I'm not sure if I translated "registerizing" correctly
14:52:04	<[exa]>	to start, afaik STG has is own notion of registers that is more or less independent of the actual CPU registers
14:52:24	<[exa]>	I guess you are interested in how the decision "what data to put into which CPU register" happens right?
14:53:19	<dminuoso>	bor0: By the way, this is a bit of a subtle thing but I decided to let you know anyhow. Depending on how deep your Proof is nested, this could perform not so nicely.
14:53:24	<arrowd>	I guess so. I imagined it to be more like a direct mapping between STG registers and real CPU registers.
14:53:43	<arrowd>	I took the "registerizing" term from here: https://downloads.haskell.org/~ghc/6.4/docs/html/building/sec-porting-ghc.html
14:53:55	<dminuoso>	bor0: This is because while there is a Functor law that states `fmap f . fmap g = fmap (f . g)`, GHC will not use this knowledge and fuse these functions `f` and `g` together.
14:54:34	<dminuoso>	bor0: There is however a standard trick to ensure fusion occurs. It's something we can talk about in a later point in time if the need arises.
14:54:41	<geekosaur>	arrowd, just to let you know, that's fairly old documentation
14:55:05	<arrowd>	I know, but I believe this part is still more or less relevant.
14:56:40	<[exa]>	arrowd: no, STG is a virtual machine with virtual registers... there will be some correspondence, but mostly accidental
14:58:29	×	dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 264 seconds)
14:58:33	<arrowd>	I'm confused about this.
14:58:51	×	haskman quits (~haskman@171.48.41.1) (Ping timeout: 268 seconds)
14:59:08	<arrowd>	LLVM is also a VM in a sense, but only architecturally. There are no traces of "VM-ness" in the final compiled executable.
14:59:17	×	dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1)
14:59:28	×	bfrk quits (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) (Ping timeout: 268 seconds)
14:59:43	<arrowd>	Unlike Java, where the compiled binary is a bytecode, which get interpreted/JITed during execution.
14:59:58	<arrowd>	STG is like LLVM in this sense, right?
15:00:14	<merijn>	Not really
15:00:23	→	fart joins (~fart@user/actor)
15:00:24	<merijn>	STG is much higher level still
15:00:35	<[exa]>	well, in this very rough sense, yes -- it's not interpreted nor JITed, just compiled into next layer
15:00:55	<arrowd>	Ok, and the next layer is Cmm?
15:00:58	<[exa]>	yes
15:01:03	<merijn>	arrowd: FYI, those docs you linked are ancient
15:01:04	<[exa]>	(I hope)
15:01:19	<merijn>	GHC 6.4 is like over a decade old?
15:01:58	→	amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi)
15:02:18	<arrowd>	Good. Now if I try to port GHC to a new ISA, at what level would I need to work? Cmm, right?
15:02:35	<merijn>	Correction, over 16 years old :p
15:03:20	<merijn>	arrowd: There's two backends in GHC: the native backend that goes from Cmm to assembly directly and an LLVM backend that converts Cmm to LLVM IR, then uses LLVM for that
15:03:34	<arrowd>	I'm talking about NCG right now.
15:03:48	<merijn>	arrowd: NCG goes from Cmm to a specific ISA, yes
15:04:14	<arrowd>	All right, now I get it. Thanks everyone for explanations.
15:04:37	<merijn>	arrowd: See also #ghc for questions about GHC specifics
15:04:49	→	dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be)
15:05:43	→	Bartosz joins (~textual@24.35.90.211)
15:06:01	<merijn>	arrowd: angerman has been working on a NCG backend for Apple's M1 (iirc?), so he probably knows where to get the most up-to-date info
15:08:11	→	shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net)
15:08:36	×	Kaipi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
15:10:51	×	oxide quits (~lambda@user/oxide) (Ping timeout: 272 seconds)
15:11:07	→	Kaipi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net)
15:14:46	→	hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com)
15:16:48	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
15:17:00	<bor0>	dminuoso, I guess this is related to `join`? If I don't `join`, I end up with `Proof (Proof ...)`
15:18:10	<ski>	bor0 : you have a `Monad Proof' instance ?
15:18:16	→	oxide joins (~lambda@user/oxide)
15:18:45	<bor0>	Nope. Not sure what that would look like, yet. https://github.com/bor0/hoare-imp/blob/master/src/Common.hs#L16-L19
15:19:14	<ski>	imho, it'd probably not be usefuö
15:19:53	<boxscape>	bor0 note btw that `x >>= f` is the same as `join (f <$> x)`, which is why it came up in some of those translations
15:19:56	<ski>	(i was just wondering, since you mentioned `join' and `Proof (Proof (..))' at the same time ..)
15:20:53	→	renzhi joins (~xp@2607:fa49:6500:bc00::e7b)
15:21:24	<boxscape>	hm, seems like it would have been Either String (Either String (Proof (..)))
15:21:25	→	Guest9 joins (~Guest9@43.241.144.2)
15:21:26	<bor0>	Actually, sorry, I meant `Right (Right (Proof ... ))`
15:21:33	<boxscape>	or that
15:21:38	<ski>	yea, that's another thing
15:22:27	<bor0>	But that's probably related to what dminuoso said, "depending how deep your Proof is nested". My expectation is it's only 1 level, right after `Right` - all should be of form `Right (Proof ...)`
15:23:23	×	fart quits (~fart@user/actor) (Quit: Connection closed)
15:23:47	×	curiousgay quits (~quassel@178.217.208.8) (Ping timeout: 252 seconds)
15:23:52	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
15:25:15	<boxscape>	bor0 I don't think that's what dminuoso meant - to get into Right (Right (Proof (..))) you would have to use (fmap . fmap) f, rather than (fmap f . fmap g). Rather, since `go` is a recursive function, it fmaps again and again, and these fmaps are not automatically optimized into a single fmap
15:26:09	×	shailangsa quits (~shailangs@host165-120-169-73.range165-120.btcentralplus.com) ()
15:26:24	<boxscape>	(and how often it recurs depends on how deep the data structure of the proof is)
15:26:42	<bor0>	Ah, was he talking specifically about `go`? My bad then. I thought it was in general, e.g.:https://paste.tomsmeding.com/aCf3hYea
15:27:06	×	lortabac quits (~lortabac@2a01:e0a:541:b8f0:bdf8:f228:7df7:147f) (Quit: WeeChat 2.8)
15:27:25	<bor0>	https://paste.tomsmeding.com/H3e0gBbu shows what c1 and c2 are specifically
15:28:02	←	ubh parts (~ubh@2001:470:69fc:105::852) ()
15:28:55	→	blizzard joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com)
15:29:05	blizzard	is now known as derelict
15:29:29	<ski>	bor0> :t hoareSequence
15:29:51	<boxscape>	ski https://github.com/bor0/hoare-imp/blob/d7b154b8d9b68fcf6466b22ff1f40591db3dcdb4/src/Hoare.hs#L35
15:29:53	<bor0>	https://github.com/bor0/hoare-imp/blob/master/src/Hoare.hs#L35
15:33:27	×	qbt quits (~edun@user/edun) (Ping timeout: 272 seconds)
15:34:42	<ski>	bor0 : you know you could use `do'-notation, for the `Either' stuff, yes ?
15:35:40	×	wei2912 quits (~wei2912@112.199.250.21) (Quit: Lost terminal)
15:35:49	<bor0>	I totally forgot about that one! Are you saying these can look better? :D https://github.com/bor0/hoare-imp/blob/master/examples/ExampleTNT.hs
15:36:08	<bor0>	(Don't look at the other examples, I still haven't updated all of them to use monadic Either instead of hacky `fromRight`)
15:36:46	<ski>	lemma1 = do
15:36:49	<boxscape>	that code almost looks like you took something that was written in do-notation and translated it to non-do-notation :)
15:36:58	<bor0>	Hahahah.
15:37:03	<ski>	step1 <- axiom3 (Var A) (Var B)
15:37:10	<ski>	step2 <- ruleSpec step1 (Var D)
15:37:12	<ski>	...
15:37:17	<bor0>	Oh man...
15:37:24	<bor0>	Time for another rewrite!
15:38:59	<ski>	(flipping the order of the `ruleFantasy' parameters might also look nicer)
15:39:04	<bor0>	Wow, it just looks amazing this way!
15:39:17	×	ikex quits (~ash@user/ikex) (Ping timeout: 264 seconds)
15:39:17	ski	smiles
15:39:35	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
15:40:25	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds)
15:40:26	<bor0>	Can you expand on the `ruleFantasy` parameters?
15:41:41	×	dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 264 seconds)
15:42:09	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
15:42:25	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
15:43:50	<ski>	let premise = PropVar (ForAll D (PropVar (Eq (..) (..))))
15:44:12	<ski>	step7 <- ruleFantasy premise $ \premise -> do
15:44:30	×	boxscape quits (~boxscape@user/boxscape) (Quit: Connection closed)
15:44:33	<bor0>	Ah!
15:44:35	<ski>	step8 <- ruleSpec premise (Var D)
15:44:39	<APic>	☺
15:44:39	<ski>	...
15:45:00	<bor0>	I'll definitely miss those redundant `let f premise`
15:45:01	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
15:45:09	<ski>	ruleGeneralize step10 D (Just premise)
15:45:26	<ski>	ruleGeneralize step7 C Nothing
15:46:37	<ski>	"miss", as in you'll regret removing them, or as in you'll prefer to drop them ?
15:46:40	×	Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…)
15:46:43	→	boxscape joins (~boxscape@user/boxscape)
15:46:44	×	ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection)
15:47:30	<ski>	(it's not clear to me what the relation between these two different `premise's are, but i kept your variable naming ..)
15:48:03	<bor0>	I think it's safe to assume just another redundancy
15:48:46	×	dunj3 quits (~dunj3@2001:16b8:3059:9800:5856:7ab4:1dd8:26ae) (Remote host closed the connection)
15:50:07	<bor0>	These proofs suddenly became readable! This is fun
15:50:49	<boxscape>	Haskell does have a reputation for being a good host language for EDSLs
15:51:03	<ski>	readability is a good thing, yea :)
15:51:22	<bor0>	boxscape, I thought it had a good reputation for being a good host language without readability, but now with this readability... ++
15:51:35	<boxscape>	hehe
15:51:35	→	dunkeln joins (~dunkeln@94.129.65.28)
15:51:44	×	chele quits (~chele@user/chele) (Remote host closed the connection)
15:52:07	<bor0>	One thing I really like about doing this in Haskell, vs e.g. in Racket is refactoring. It's a breeze. Almost like random work until ghci is happy
15:52:56	<boxscape>	yep static types are pretty cool
15:53:05	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
15:53:10	<boxscape>	(though I think racket has an optional static type system? I've never used racket)
15:53:16	→	Deide joins (~Deide@wire.desu.ga)
15:53:16	×	Deide quits (~Deide@wire.desu.ga) (Changing host)
15:53:16	→	Deide joins (~Deide@user/deide)
15:53:26	ski	. o O ( "Follow the types where they lead -- follow the types where they lead. Follow, follow, follow, follow -- follow the types where they lead." )
15:53:44	→	hseg joins (~gesh@185.120.126.41)
15:54:03	→	shailangsa joins (~shailangs@host165-120-169-73.range165-120.btcentralplus.com)
15:54:09	<ski>	there's Typed Racket, yea
15:54:40	<boxscape>	ok
15:54:43	<hseg>	stack isn't picking up the new commonmark version (from last friday) on hackage
15:54:58	<hseg>	even though I ran stack update
15:55:04	<ski>	(one interesting thing is the higher-order blame tracking system, for contracts)
15:55:52	<kosmikus>	xwx: lhs2tex-1.24 should work ok with HLS (within certain limits).
15:57:27	×	zeenk quits (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) (Quit: Konversation terminated!)
15:58:43	→	haltux joins (~lbigas@a89-154-181-47.cpe.netcabo.pt)
16:00:25	→	guest61 joins (~xxx@47.245.54.240)
16:00:37	×	haltux quits (~lbigas@a89-154-181-47.cpe.netcabo.pt) (Quit: Leaving)
16:01:43	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
16:02:05	×	shryke quits (~shryke@91.103.43.254) (Ping timeout: 264 seconds)
16:02:18	→	haltux joins (~lbigas@a89-154-181-47.cpe.netcabo.pt)
16:02:29	→	wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com)
16:03:01	<hseg>	nuked $XDG_DATA_HOME/stack, hopefully that helps things
16:05:18	→	pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
16:07:11	×	pe200012_ quits (~pe200012@218.107.17.245) (Read error: Connection reset by peer)
16:08:17	→	shryke joins (~shryke@91.103.43.254)
16:08:46	→	softinio joins (~softinio@c-73-70-215-171.hsd1.ca.comcast.net)
16:10:17	<kuribas>	"cabal haddock --executables" gives an error: cabal: unrecognized 'haddock' option `--executables'
16:10:55	→	v01d4lph4 joins (~v01d4lph4@122.160.65.250)
16:10:55	×	v01d4lph4 quits (~v01d4lph4@122.160.65.250) (Changing host)
16:10:55	→	v01d4lph4 joins (~v01d4lph4@user/v01d4lph4)
16:11:25	<bor0>	ski, boxscape https://github.com/bor0/hoare-imp/blob/master/examples/ExampleTNT.hs 😎
16:11:41	<kuribas>	hmm cabal haddock myproject:executables does work...
16:11:50	<boxscape>	bor0 nice
16:11:55	<kuribas>	the cabal haddock --help text is wrong however.
16:11:56	<geekosaur>	looks like it's --haddock-executables ?
16:12:20	→	favonia joins (~favonia@user/favonia)
16:12:25	×	Guest9 quits (~Guest9@43.241.144.2) (Quit: Connection closed)
16:13:08	×	favonia quits (~favonia@user/favonia) (Client Quit)
16:13:28	<geekosaur>	the text at the top is wrong but the actual option descriptions later are correct
16:14:07	×	softinio quits (~softinio@c-73-70-215-171.hsd1.ca.comcast.net) ()
16:15:27	<boxscape>	bor0 do step0, step1, step2 etc all have the same type or different types?
16:15:31	<kuribas>	geekosaur: right
16:16:32	<boxscape>	(whoops step0 doesn't actually exist)
16:16:36	<bor0>	All same I believe - either string (error) or proof
16:16:42	<boxscape>	ok
16:17:31	<boxscape>	bor0 I was thinking about whether it would make sense to use the State monad which is why I asked that, but the answer is no
16:18:11	<boxscape>	(the State monad would make sense if you only used step1 for step2, only used step2 for step3, etc.)
16:22:08	×	jakzale quits (uid499518@id-499518.charlton.irccloud.com) (Quit: Connection closed for inactivity)
16:22:28	→	Bartosz joins (~textual@24.35.90.211)
16:23:29	×	niflce quits (~IceChat95@user/niflce) (Ping timeout: 272 seconds)
16:23:31	×	Bartosz quits (~textual@24.35.90.211) (Client Quit)
16:24:48	→	niflce joins (~IceChat95@user/niflce)
16:26:10	<gentauro>	I find this hilariously funny: https://twitter.com/vamchale/status/1399390668754198532 (it's funny cos it's true)
16:26:35	<gentauro>	as a "freelance clownsultant" you see some of the most horrible things created by humans
16:27:05	<boxscape>	oh wow I thought that was automatically minified javascript or something but no
16:27:17	×	nschoe quits (~quassel@178.251.84.79) (Ping timeout: 264 seconds)
16:27:19	<gentauro>	for example, 5000 lines methods, with if statements as wide as a 1000 characters
16:27:48	<gentauro>	all kind of logic (and side-effects) hidden everywhere
16:27:53	lbseale__	is now known as lbseale
16:28:11	<gentauro>	we must be doing something wrong in this field, since Haskell is not the norm :(
16:28:24	<boxscape>	and column 876 of the if statement accidentally has a `=` instead of a `==` ;)
16:28:45	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
16:29:16	<gentauro>	boxscape: I see you also have these nightmares
16:31:16	→	lavaman joins (~lavaman@98.38.249.169)
16:31:45	<gentauro>	as well
16:32:10	<boxscape>	mhm
16:33:17	×	azeem quits (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) (Ping timeout: 264 seconds)
16:33:49	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds)
16:35:56	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
16:37:30	×	chddr quits (~Thunderbi@31.148.23.125) (Ping timeout: 264 seconds)
16:43:08	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
16:43:31	×	v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
16:43:54	×	neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 244 seconds)
16:44:46	→	sm2n joins (~sm2n@user/sm2n)
16:47:21	<ski>	gentauro : how about an `if' condition that's some 77 lines ?
16:47:49	<yin>	libera
16:48:01	<yin>	ignore this pls
16:48:22	ski	glances around nervously
16:48:52	→	Bartosz joins (~textual@67.135.32.118)
16:49:19	→	motherfsck joins (~motherfsc@68.235.43.102)
16:49:24	→	dpl_ joins (~dpl@77-121-78-163.chn.volia.net)
16:49:38	×	motherfsck quits (~motherfsc@68.235.43.102) (Quit: quit)
16:50:38	→	motherfsck joins (~motherfsc@68.235.43.102)
16:50:56	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
16:51:15	→	beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net)
16:51:35	×	leeb_ quits (~leeb@KD111239153130.au-net.ne.jp) (Quit: WeeChat 3.1)
16:52:03	×	motherfsck quits (~motherfsc@68.235.43.102) (Client Quit)
16:53:19	<gentauro>	ski: "some 77 lines"?
16:53:32	×	haltux quits (~lbigas@a89-154-181-47.cpe.netcabo.pt) (Quit: Leaving)
16:53:32	<ski>	yes
16:53:42	<gentauro>	:\|
16:53:44	<gentauro>	jaiks
16:53:45	×	keutoi quits (~keutoi@157.48.91.62) (Quit: leaving)
16:54:05	<ski>	it was a fun experiment of writing Prolog in C, i suppose you could say
16:54:58	→	motherfsck joins (~motherfsc@68.235.43.102)
16:55:23	→	vjoki joins (~vjoki@2a00:d880:3:1::fea1:9ae)
16:55:37	<ski>	bor0 : anyway .. i'm a bit suspicious about `ruleGeneralize'
16:55:52	→	haskman joins (~haskman@106.201.8.96)
16:56:10	×	motherfsck quits (~motherfsc@68.235.43.102) (Changing host)
16:56:10	→	motherfsck joins (~motherfsc@user/motherfsck)
16:57:00	→	haltux joins (~haltux@a89-154-181-47.cpe.netcabo.pt)
16:57:27	<ski>	(also, personally, i'm continually confused by each intermediate conclusion comment preceding the step that effects it, rather than succeding it)
16:57:48	←	novasenco parts (novasenco@user/nova) (♥☺)
16:59:21	→	pavonia joins (~user@user/siracusa)
17:00:52	<monochrom>	Once again "what I'm going to do next" vs "what I just did".
17:02:26	→	tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net)
17:02:34	<monochrom>	This can run deep as the fundamental philosophical divide between "this is what's happening, oh btw here is computer code" vs "this is computer code, oh btw here is what's happening"
17:04:09	→	benin joins (~benin@183.82.205.186)
17:04:47	→	Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com)
17:04:51	→	qbt joins (~edun@user/edun)
17:06:40	→	Ariakenom joins (~Ariakenom@2001:9b1:efb:fc00:d9c3:69a3:f97b:be95)
17:06:40	×	kmein quits (~weechat@user/kmein) (Quit: ciao kakao)
17:07:05	→	kmein joins (~weechat@user/kmein)
17:08:31	×	Bartosz quits (~textual@67.135.32.118) (Quit: My MacBook has gone to sleep. ZZZzzz…)
17:09:06	<ski>	bor0 : part of the point of `ruleFantasy' is that you should be able to nest it. iow, there may be more than one hypothetical assumption, in force, at the same time, and so it seems inappropriate for `ruleGeneralize' to only `Maybe' take a hypothesis
17:09:53	→	azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it)
17:10:11	→	ec joins (~ec@gateway/tor-sasl/ec)
17:10:16	<ski>	(and, it's possible that you've already nested it like this, without realizing it, if you've, from inside a `ruleFantasy', used a lemma that used `ruleFantasy' in its proof
17:10:19	<ski>	)
17:12:06	×	ec quits (~ec@gateway/tor-sasl/ec) (Client Quit)
17:12:17	→	ec joins (~ec@gateway/tor-sasl/ec)
17:12:42	→	bfrk joins (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de)
17:12:54	<monochrom>	I don't know whether ruleFantasy is a cute name or a horrible name :)
17:14:38	×	motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit)
17:17:16	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:18:28	→	novasenco joins (novasenco@user/nova)
17:18:48	ski	. o O ( maybe both ? )
17:18:56	×	hseg quits (~gesh@185.120.126.41) (Quit: WeeChat 3.1)
17:19:17	×	myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 252 seconds)
17:19:22	<novasenco>	cabal install alsa-mixer -> http://ix.io/3ov9/
17:19:32	<monochrom>	i/sqrt(2) \|cute> - i/sqrt(2) \|horrible>
17:19:36	×	jumper149 quits (~jumper149@80.240.31.34) (Quit: WeeChat 3.1)
17:19:45	→	bitmapper joins (uid464869@id-464869.tooting.irccloud.com)
17:20:26	<novasenco>	07dist/build/Sound/ALSA/Mixer/Internal.i:1: (column 1) [ERROR] >>> Lexical error ! The character '#' does not fit here.
17:20:56	<monochrom>	probably gcc vs clang in terms of CPP things
17:21:33	<novasenco>	I have both installed. I have no idea how to tell it to prefer one or the other
17:22:19	→	motherfsck joins (~motherfsc@user/motherfsck)
17:24:17	×	sm2n quits (~sm2n@user/sm2n) (.net .split)
17:24:17	×	oxide quits (~lambda@user/oxide) (.net .split)
17:24:17	×	jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (.net .split)
17:24:17	×	pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (.net .split)
17:24:17	×	berberman quits (~berberman@user/berberman) (.net .split)
17:24:17	×	bor0 quits (~boro@user/bor0) (.net .split)
17:24:17	×	cheater quits (~Username@user/cheater) (.net .split)
17:24:17	×	leif quits (uid501722@id-501722.stonehaven.irccloud.com) (.net .split)
17:24:17	×	joel135 quits (sid136450@id-136450.stonehaven.irccloud.com) (.net .split)
17:24:17	×	Firedancer quits (sid336191@id-336191.stonehaven.irccloud.com) (.net .split)
17:24:17	×	mthvedt quits (uid501949@id-501949.stonehaven.irccloud.com) (.net .split)
17:24:17	×	amir quits (sid22336@user/amir) (.net .split)
17:24:17	×	peteretep quits (sid143467@id-143467.stonehaven.irccloud.com) (.net .split)
17:24:17	×	acertain quits (sid470584@id-470584.stonehaven.irccloud.com) (.net .split)
17:24:17	×	sqrt2 quits (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net) (.net .split)
17:24:17	×	Megant quits (megant@user/megant) (.net .split)
17:24:17	×	Aighearach quits (~paris@c-71-63-160-210.hsd1.or.comcast.net) (.net .split)
17:24:17	×	the-coot[m] quits (~the-cootm@2001:470:69fc:105::95f) (.net .split)
17:24:17	×	hexology quits (~hexology@user/hexology) (.net .split)
17:24:17	×	jiribenes quits (~jiribenes@rosa.jiribenes.com) (.net .split)
17:24:17	×	dexterfoo quits (dexter@2a01:7e00::f03c:91ff:fe86:59ec) (.net .split)
17:24:17	×	dmwit quits (~dmwit@pool-173-66-86-32.washdc.fios.verizon.net) (.net .split)
17:24:17	×	vjoki quits (~vjoki@2a00:d880:3:1::fea1:9ae) (.net .split)
17:24:17	×	thonkpod quits (~thonkpod@2001:19f0:ac01:b46:5400:1ff:fec7:d73d) (.net .split)
17:24:17	×	NemesisD quits (sid24071@tooting.irccloud.com) (.net .split)
17:24:17	×	parseval quits (sid239098@brockwell.irccloud.com) (.net .split)
17:24:17	×	edwtjo quits (~edwtjo@user/edwtjo) (.net .split)
17:24:17	×	fabfianda[m] quits (~fabfianda@2001:470:69fc:105::6db) (.net .split)
17:24:17	×	bmsk quits (~user@2001:19f0:5001:2f3b:5400:3ff:fe53:2d96) (.net .split)
17:24:17	×	dy quits (~dy@user/dy) (.net .split)
17:24:17	×	Teacup quits (~teacup@user/teacup) (.net .split)
17:24:17	×	fjmorazan quits (~quassel@user/fjmorazan) (.net .split)
17:24:17	×	ajb quits (~ajb@cupid.whatbox.ca) (.net .split)
17:24:17	×	mstruebing quits (~maex@2001:41d0:8:93c7::1) (.net .split)
17:24:17	×	teehemkay quits (sid14792@id-14792.tooting.irccloud.com) (.net .split)
17:24:17	×	dixie quits (~dixie@real.wilbury.sk) (.net .split)
17:24:17	×	funsafe quits (~funsafe@2601:1c1:4200:938f:389d:16a4:ae2d:65aa) (.net .split)
17:24:17	×	statusbot quits (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (.net .split)
17:24:17	×	plateno quits (~plateno@user/plateno) (.net .split)
17:24:17	×	edwardk quits (sid47016@haskell/developer/edwardk) (.net .split)
17:24:17	×	iphy quits (sid67735@tooting.irccloud.com) (.net .split)
17:24:17	×	immae quits (~immae@2a01:4f8:141:53e7::) (.net .split)
17:24:17	×	Hecate quits (~mariposa@user/hecate) (.net .split)
17:24:17	×	ham quits (~ham4@user/ham) (.net .split)
17:24:17	×	bcoppens quits (~bartcopp@vpn2.bartcoppens.be) (.net .split)
17:24:17	×	pie_bnc quits (~pie_bnc@user/pie/x-2818909) (.net .split)
17:24:17	×	df quits (~ben@51.15.198.140) (.net .split)
17:24:17	×	liskin quits (~liskin@ackle.nomi.cz) (.net .split)
17:24:17	×	samebchase quits (~samebchas@51.15.68.182) (.net .split)
17:24:17	×	bjfs quits (bart@kobayashi.com.pl) (.net .split)
17:24:17	×	supersven quits (uid501114@charlton.irccloud.com) (.net .split)
17:24:17	×	mikolaj_ quits (~mikolaj@purple.well-typed.com) (.net .split)
17:24:17	×	keltono quits (~kelton@x-160-94-179-178.acm.umn.edu) (.net .split)
17:24:17	×	nitrix quits (~nitrix@user/nitrix) (.net .split)
17:24:17	×	bsima quits (~bsima@simatime.com) (.net .split)
17:24:17	×	mikolaj quits (~mikon@duch.mimuw.edu.pl) (.net .split)
17:24:17	×	bcmiller quits (~bm3719@66.42.95.185) (.net .split)
17:24:17	×	Aardwolf quits (~lode@77-56-208-202.dclient.hispeed.ch) (.net .split)
17:24:17	×	alp quits (~alp@user/alp) (.net .split)
17:24:17	×	Pent quits (sid313808@tooting.irccloud.com) (.net .split)
17:24:17	×	yushyin quits (0mbcixlPGk@karif.server-speed.net) (.net .split)
17:24:17	×	seeg quits (~thelounge@static.89.161.217.95.clients.your-server.de) (.net .split)
17:24:17	×	ivan quits (~ivan@user/ivan) (.net .split)
17:24:17	×	fryguybob quits (~fryguybob@cpe-74-65-31-113.rochester.res.rr.com) (.net .split)
17:24:17	×	haasn quits (~nand@haasn.dev) (.net .split)
17:24:17	×	dragestil quits (~quassel@user/dragestil) (.net .split)
17:24:17	×	Adran quits (~adran@botters/adran) (.net .split)
17:24:17	×	agander_m quits (sid407952@id-407952.tinside.irccloud.com) (.net .split)
17:24:21	<maralorn[m]>	monochrom: You’re in a weird phase.
17:24:21	×	lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection)
17:24:24	→	Hecate joins (~mariposa@163.172.211.189)
17:24:24	→	parseval joins (sid239098@id-239098.brockwell.irccloud.com)
17:24:24	→	mikolaj joins (~mikolaj@purple.well-typed.com)
17:24:25	→	mikolaj_ joins (~mikon@duch.mimuw.edu.pl)
17:24:25	→	supersven joins (uid501114@id-501114.charlton.irccloud.com)
17:24:25	→	dmwit joins (~dmwit@pool-173-66-86-32.washdc.fios.verizon.net)
17:24:28	→	bcoppens joins (~bartcopp@vpn2.bartcoppens.be)
17:24:28	→	dixie joins (~dixie@real.wilbury.sk)
17:24:30	→	edwtjo joins (~edwtjo@h-79-136-7-145.A213.priv.bahnhof.se)
17:24:30	→	dexterfoo joins (dexter@2a01:7e00::f03c:91ff:fe86:59ec)
17:24:30	→	ajb joins (~ajb@cupid.whatbox.ca)
17:24:30	→	mthvedt joins (uid501949@id-501949.stonehaven.irccloud.com)
17:24:30	→	teehemkay joins (sid14792@id-14792.tooting.irccloud.com)
17:24:32	→	keltono joins (~kelton@x-160-94-179-178.acm.umn.edu)
17:24:32	→	sqrt2 joins (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net)
17:24:32	→	alp joins (~alp@163.172.83.213)
17:24:32	→	mstruebing joins (~maex@2001:41d0:8:93c7::1)
17:24:33	→	Pent joins (sid313808@id-313808.tooting.irccloud.com)
17:24:33	→	samebchase joins (~samebchas@51.15.68.182)
17:24:35	→	dragestil joins (~quassel@180-150-39-25.b49627.bne.nbn.aussiebb.net)
17:24:36	→	Aardwolf joins (~lode@77-56-208-202.dclient.hispeed.ch)
17:24:37	→	fjmorazan joins (~quassel@user/fjmorazan)
17:24:37	→	fryguybob joins (~fryguybob@cpe-74-65-31-113.rochester.res.rr.com)
17:24:37	→	Aighearach joins (~paris@c-71-63-160-210.hsd1.or.comcast.net)
17:24:43	→	guest0123 joins (~aaron@2601:602:a080:fa0:21da:7ddc:2cc6:a10c)
17:24:45	→	bjfs joins (bart@kobayashi.com.pl)
17:24:45	→	yushyin joins (exGFiU2tsp@karif.server-speed.net)
17:24:47	→	liskin joins (~liskin@ackle.nomi.cz)
17:24:49	→	amir joins (sid22336@id-22336.stonehaven.irccloud.com)
17:24:49	→	agander_m joins (sid407952@id-407952.tinside.irccloud.com)
17:24:50	→	pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net)
17:24:51	→	oxide joins (~lambda@61.0.149.238)
17:24:52	→	thonkpod joins (~thonkpod@2001:19f0:ac01:b46:5400:1ff:fec7:d73d)
17:24:52	→	joel135 joins (sid136450@id-136450.stonehaven.irccloud.com)
17:24:52	→	acertain joins (sid470584@id-470584.stonehaven.irccloud.com)
17:24:52	→	Firedancer joins (sid336191@id-336191.stonehaven.irccloud.com)
17:24:52	→	Teacup joins (~teacup@user/teacup)
17:24:52	→	leif joins (uid501722@id-501722.stonehaven.irccloud.com)
17:24:52	→	peteretep joins (sid143467@id-143467.stonehaven.irccloud.com)
17:24:52	→	bmsk joins (~user@2001:19f0:5001:2f3b:5400:3ff:fe53:2d96)
17:24:53	→	funsafe joins (~funsafe@2601:1c1:4200:938f:389d:16a4:ae2d:65aa)
17:24:54	→	bor0 joins (~boro@46.217.54.116)
17:24:56	→	jiribenes joins (~jiribenes@rosa.jiribenes.com)
17:25:00	→	iphy joins (sid67735@2001:67c:2f08:4::1:897)
17:25:00	→	NemesisD joins (sid24071@2001:67c:2f08:4::5e07)
17:25:01	→	nitrix joins (~nitrix@ns569831.ip-51-79-81.net)
17:25:04	→	immae joins (~immae@2a01:4f8:141:53e7::)
17:25:04	→	edwardk joins (sid47016@2001:67c:2f08:3::b7a8)
17:25:10	×	edwtjo quits (~edwtjo@h-79-136-7-145.A213.priv.bahnhof.se) (Changing host)
17:25:10	→	edwtjo joins (~edwtjo@user/edwtjo)
17:25:14	→	ivan joins (~ivan@static.38.6.217.95.clients.your-server.de)
17:25:36	×	amir quits (sid22336@id-22336.stonehaven.irccloud.com) (Changing host)
17:25:36	→	amir joins (sid22336@user/amir)
17:25:46	×	edwardk quits (sid47016@2001:67c:2f08:3::b7a8) (Changing host)
17:25:46	→	edwardk joins (sid47016@haskell/developer/edwardk)
17:25:52	×	yushyin quits (exGFiU2tsp@karif.server-speed.net) (Client Quit)
17:25:53	×	ivan quits (~ivan@static.38.6.217.95.clients.your-server.de) (Changing host)
17:25:53	→	ivan joins (~ivan@user/ivan)
17:25:59	bjfs	is now known as Guest6937
17:26:02	×	nitrix quits (~nitrix@ns569831.ip-51-79-81.net) (Changing host)
17:26:02	→	nitrix joins (~nitrix@user/nitrix)
17:26:07	bmsk	is now known as Guest7513
17:26:11	bor0	is now known as Guest929
17:26:14	→	yushyin joins (iqIKChYq4t@karif.server-speed.net)
17:26:32	→	sm2n joins (~sm2n@user/sm2n)
17:26:39	→	jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
17:26:40	→	statusbot joins (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com)
17:26:42	→	pie_bnc joins (~pie_bnc@user/pie/x-2818909)
17:26:44	→	abhixec joins (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net)
17:26:45	→	bsima joins (~bsima@simatime.com)
17:26:49	→	ham joins (~ham4@user/ham)
17:26:56	→	hexology joins (~hexology@user/hexology)
17:27:09	×	yushyin quits (iqIKChYq4t@karif.server-speed.net) (Client Quit)
17:27:11	→	haasn joins (~nand@haasn.dev)
17:27:17	→	Adran joins (~adran@botters/adran)
17:27:19	→	vjoki joins (~vjoki@2a00:d880:3:1::fea1:9ae)
17:27:23	→	berberman joins (~berberman@user/berberman)
17:27:23	→	yushyin joins (nrX1Axr00h@karif.server-speed.net)
17:27:54	→	cheater joins (~Username@user/cheater)
17:28:04	→	Guest31 joins (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net)
17:28:47	×	liskin quits (~liskin@ackle.nomi.cz) (Client Quit)
17:28:56	→	liskin joins (~liskin@ackle.nomi.cz)
17:29:20	→	bcmiller joins (~bm3719@66.42.95.185)
17:29:24	→	Megant joins (megant@user/megant)
17:29:47	→	ku joins (~ku@2601:280:c780:7ea0:d1c6:52a:4bf2:1ff2)
17:30:55	×	dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 244 seconds)
17:31:55	→	sbmsr joins (~pi@2600:1700:63d0:4830:7dbf:92d8:fd42:235d)
17:32:48	→	fabfianda[m] joins (~fabfianda@2001:470:69fc:105::6db)
17:34:22	×	Pent quits (sid313808@id-313808.tooting.irccloud.com) ()
17:34:34	→	Pent joins (sid313808@id-313808.tooting.irccloud.com)
17:34:41	→	Bartosz joins (~textual@24.35.90.211)
17:39:00	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 265 seconds)
17:40:29	×	azeem quits (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) (Ping timeout: 264 seconds)
17:40:43	→	myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net)
17:42:17	×	shryke quits (~shryke@91.103.43.254) (Ping timeout: 264 seconds)
17:42:57	→	geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com)
17:43:29	×	xff0x quits (~xff0x@2001:1a81:52ca:4f00:7b0a:bab9:5836:8b3b) (Ping timeout: 252 seconds)
17:44:17	→	xff0x joins (~xff0x@2001:1a81:52ca:4f00:7e41:f92f:ed4d:a7b5)
17:45:20	→	learner-monad joins (~ehanneken@cpe-174-105-47-100.columbus.res.rr.com)
17:47:42	<dminuoso>	Im using context to implement simple basic authentication in Servant. Im pondering whether there is a way to short circuit this process for local unix domain sockets.
17:47:59	<dminuoso>	A way to have a cli tool talk to the local management socket skipping authentication
17:48:45	→	mccoyb joins (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632)
17:48:49	<monochrom>	ski: (A tangent from the conversation in freenode #haskell) I once had a student who used "show x == show y" for their (==) too. Except that their handwritten Show instance was wrong. And not just "disapproved by Haskell community" wrong. It downright bottomed out on some values.
17:48:52	<Lycurgus>	only answer localhost?
17:49:12	<Lycurgus>	(or whitelisted ip)
17:50:27	<mccoyb>	Hi -- I'm looking for some FFI help with Haskell. In particular, I'm trying to link a `dylib` in for a wrapper package I'm writing to `MLIR`: https://github.com/femtomc/mlir-hs. I'm having trouble getting linking to work correctly. Does anyone have expertise with this?
17:50:33	→	the-coot[m] joins (~the-cootm@2001:470:69fc:105::95f)
17:50:54	→	a6a45081-2b83 joins (~aditya@106.212.79.20)
17:51:18	×	a6a45081-2b83 quits (~aditya@106.212.79.20) (Remote host closed the connection)
17:51:46	<dminuoso>	Lycurgus: I dont have access to that information when popping a context
17:52:26	<dminuoso>	Or maybe I do.. let me dive into this
17:53:32	<ski>	monochrom : ouch :/
17:53:35	<Lycurgus>	if its unix socket ... also unclear if local carried that already and exactly what context means if it was meant exactly
17:53:45	<edwardk>	monochrom: FREX uses unsafePerformIO to show the result of `Q (TExp a)` as an Exp, so comparatively that is a minor sin ;)
17:54:30	→	y04nn joins (~y04nn@193.32.127.220)
17:54:40	<monochrom>	Yeah I wouldn't mind if their show implementation were total and injective. But it failed both.
17:54:42	→	azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it)
17:54:48	→	neceve joins (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130)
17:54:57	<dminuoso>	Lycurgus: Im talking servant context. But it seems, that all the magic is in HasServer, and I can implement that for a custom context.
17:55:09	<Lycurgus>	mccoyb, looks like you've stepped into llvm which is not mere linking
17:55:09	<dminuoso>	So I guess I need to handroll the basic authentication hook for HasServer
17:55:20	<monochrom>	If a person fails at recursion, they don't just fail at recursive (==), they fail at recursive show too.
17:55:43	→	lavaman joins (~lavaman@98.38.249.169)
17:56:16	<mccoyb>	Lycurgus, interesting. But I have headers and a dylib, shouldn't I be able to link?
17:56:30	<Lycurgus>	dminuoso, ah, well that pkgs comes with a number of auth suggestions
17:56:32	→	ddellacosta joins (~ddellacos@89.45.224.79)
17:56:39	<Lycurgus>	(fully implemented)
17:56:45	<monochrom>	btw I saw accursedUnutterablePerformIO in Data.ByteString source code :)
17:56:45	<Lycurgus>	*pkg
17:57:23	<mccoyb>	This is a pure C API, I don't have to handle name mangling, etc. I'm just wrapping a C API (for more info).
17:57:38	<monochrom>	Basically 50% of the functions there utter it. It's very utterable.
17:58:09	<Lycurgus>	well linking with that should be straightforward, at least from the c side
17:58:41	×	oxide quits (~lambda@61.0.149.238) (Changing host)
17:58:41	→	oxide joins (~lambda@user/oxide)
17:58:52	<Lycurgus>	i didn look at ur link but inferred llvm from the IR in MLIR
17:58:58	→	vicfred joins (~vicfred@user/vicfred)
17:59:51	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 244 seconds)
18:00:22	×	mccoyb quits (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632) (Quit: My MacBook Air has gone to sleep. ZZZzzz…)
18:00:35	<Lycurgus>	confirmed, fortunately since that was an outrageous stretch
18:00:44	→	mccoyb joins (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632)
18:00:53	×	ddellacosta quits (~ddellacos@89.45.224.79) (Ping timeout: 244 seconds)
18:01:00	<mccoyb>	Lycurgus -- sorry, I should have been more clear. Yes, no need for difficulties, just linking with C.
18:01:38	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds)
18:01:44	<mccoyb>	In general, I'm looking for a Haskell package which I can use as a template, is anyone aware of a package which links with a `dylib`?
18:01:45	<Lycurgus>	lemme put it this way, once upon a time linking was straightforward
18:02:03	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
18:02:20	<Lycurgus>	and fundamentally it still is
18:02:49	→	igghibu joins (~igghibu@91.193.5.46)
18:03:45	×	dmwit quits (~dmwit@pool-173-66-86-32.washdc.fios.verizon.net) (Ping timeout: 272 seconds)
18:07:21	×	Guest31 quits (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com)
18:08:05	<mccoyb>	My main issue has been getting this stuff working with `stack` and/or `cabal`. I studied `llvm-hs` relatively deeply -- but thought there could be a simpler way to prototype linking without having a custom `Setup.hs`.
18:08:51	<Lycurgus>	is llvm the only backend now?
18:09:19	<Lycurgus>	it was optional for a long time
18:09:59	<Lycurgus>	after link it's all the same object code
18:10:30	×	qbt quits (~edun@user/edun) (Quit: WeeChat 3.1)
18:11:14	<Lycurgus>	llvm conceptually is like user microprogamming but just, at least on regular cpus
18:14:46	Guest929	is now known as bor0
18:14:48	×	bor0 quits (~boro@46.217.54.116) (Changing host)
18:14:48	→	bor0 joins (~boro@user/bor0)
18:15:23	<mccoyb>	Lycurgus -- when you say backend, do you mean final lower target for MLIR? Or are you referring to usage in a different context?
18:15:57	<Lycurgus>	compiler backend, the code generation stage, in this case ghc
18:15:59	<bor0>	ski, sorry, I was afk. It's true that `ruleGeneralize` can have multiple premises, but I believe we only care about the inner most premise?
18:16:10	<bor0>	ski, I might have, as well, misunderstood its description from GEB :)
18:16:16	×	ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Read error: Connection reset by peer)
18:16:24	<dminuoso>	monochrom: One does wonder, if the usage frequency is so high, whether that doesn't that desensetizes the authors. I mean if you fling it around at every chance, do you really even pay attention to that danger name?
18:16:31	→	ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net)
18:16:45	<dminuoso>	Might at as well call it "mostlySafePerformIO"
18:16:59	<dminuoso>	On the basis that all uses of it are considered safe.
18:17:00	×	Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…)
18:17:07	→	jorjor joins (~jorgemene@85.251.190.6.dyn.user.ono.com)
18:17:31	→	Bartosz joins (~textual@24.35.90.211)
18:18:09	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
18:18:15	→	Erutuon joins (~Erutuon@user/erutuon)
18:18:27	×	prite quits (~pritam@user/pritambaral) (Quit: Konversation terminated!)
18:18:32	<boxscape>	maybe they should have chosen a name that's very difficult to type
18:18:52	×	Bartosz quits (~textual@24.35.90.211) (Client Quit)
18:19:01	×	Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt)
18:19:09	×	ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Client Quit)
18:19:13	<dminuoso>	accursdeUntturabelPerfformIO
18:19:20	<dminuoso>	I guarantee, you will mispell it every time.
18:19:25	<boxscape>	haha
18:19:40	<monochrom>	Unpopular opinion: Every long caml case name is difficult to type anyway.
18:20:04	<monochrom>	haha that's nice
18:22:14	→	curiousgay joins (~quassel@178.217.208.8)
18:22:48	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
18:24:25	→	df joins (~ben@51.15.198.140)
18:24:26	×	sqrt2 quits (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net) (Ping timeout: 265 seconds)
18:24:46	→	allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com)
18:24:54	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 264 seconds)
18:27:15	→	sqrt2 joins (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net)
18:28:45	<maerwald>	snake case > camel case
18:28:49	<maerwald>	there's research
18:29:00	<maerwald>	https://ieeexplore.ieee.org/document/5521745
18:29:19	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
18:30:58	→	ddellacosta joins (~ddellacos@89.45.224.170)
18:31:36	×	dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1)
18:33:49	←	jorjor parts (~jorgemene@85.251.190.6.dyn.user.ono.com) (Konversation terminated!)
18:33:54	<tdammers>	kebab case is best
18:33:57	×	neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 272 seconds)
18:34:10	<maerwald>	only chicken
18:34:55	→	dunkeln joins (~dunkeln@94.129.65.28)
18:35:17	<maerwald>	which language does kebab?
18:35:37	<tdammers>	lisps
18:36:02	<tdammers>	they can pull it off because prefix-everything notation
18:38:41	<nf>	> subjects were trained mainly in the underscore style [...] subjects recognize identifiers in the underscore style more quickly
18:38:42	<lambdabot>	<hint>:1:30: error: parse error on input ‘in’
18:38:53	<nf>	interesting methodology o_Ô
18:39:49	<tdammers>	or maybe just randomizing casing conventions entirely is the best way forward, that way everyone has something to complain
18:41:28	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
18:42:31	<maerwald>	haskell is a dense language... I read haskell different than C
18:42:37	<maerwald>	I wouldn't want camel case in C
18:43:18	→	__monty__ joins (~toonn@user/toonn)
18:43:51	<nf>	i think it's a matter of habit, probably?
18:43:53	×	mcglk quits (~mcglk@131.191.49.120) (Read error: Connection reset by peer)
18:44:05	×	beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Ping timeout: 264 seconds)
18:44:13	<maerwald>	of course, but how strong the effects are is the question
18:44:34	→	mcglk joins (~mcglk@131.191.49.120)
18:45:32	→	dss joins (~dss@144.202.106.125)
18:46:18	←	dss parts (~dss@144.202.106.125) ()
18:50:28	×	benin quits (~benin@183.82.205.186) (Quit: The Lounge - https://thelounge.chat)
18:51:25	×	wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
18:53:35	×	bor0 quits (~boro@user/bor0) (Quit: This computer has gone to sleep)
18:54:44	→	lavaman joins (~lavaman@98.38.249.169)
18:55:28	→	wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com)
18:56:10	×	Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 244 seconds)
18:57:00	<monochrom>	https://0paste.com/251395 shows the problem with camel case.
18:57:29	<monochrom>	Error message: non-exhaustive pattern. Can you catch it?
18:57:49	<xsperry>	yes, i not capitalized
18:57:58	<nf>	not any more than foo_bar/foo-bar shows the problem with snake case :shrug:
18:58:06	<monochrom>	Took both the asker and me 10 minutes.
18:58:22	<ski>	@tell bor0 "It's true that `ruleGeneralize` can have multiple premises, but I believe we only care about the inner most premise?" -- no, all of them should be taken into account, for the side condition of generalization (`forall'-intro) (as well as for `exists'-elim)
18:58:22	<lambdabot>	Consider it noted.
18:58:58	<xsperry>	monochrom, to be honest, if you didn't talk about the problem with camel case first, it would probably take me longer
18:59:08	<monochrom>	No, would you spot it when you make this kind of mistakes?
18:59:23	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds)
18:59:27	<monochrom>	In fact, even, would you even make this kind of mistakes with snake case for example?
18:59:32	<maerwald>	there should be an error AND a warning
18:59:40	<maerwald>	the warning should tell you what's wrong
18:59:48	<ski>	error for ?
18:59:49	<maerwald>	missing type sig
19:00:01	<xsperry>	I don't know. I never actually encountered something similar, I'd use editor's auto completion to type most of that function name for me
19:00:08	<monochrom>	The problem exists because you attempt to type I in the first place but then fail.
19:00:25	<monochrom>	With snake case you won't even attempt.
19:00:38	<ski>	iirc, John Hughes generally doesn't put type signatures on his definitions
19:01:32	←	guest0123 parts (~aaron@2601:602:a080:fa0:21da:7ddc:2cc6:a10c) ()
19:01:33	×	azeem quits (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) (Read error: Connection reset by peer)
19:02:22	×	dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 244 seconds)
19:03:55	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 244 seconds)
19:06:35	×	wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
19:08:32	<Torro>	.discon
19:08:45	<monochrom>	It's /discon or /quit
19:08:45	×	Torro quits (Torro@gateway/vpn/protonvpn/torro) (Quit: bye)
19:11:05	→	azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it)
19:13:14	×	mc47 quits (~yecinem@89.246.239.190) (Remote host closed the connection)
19:13:32	×	ku quits (~ku@2601:280:c780:7ea0:d1c6:52a:4bf2:1ff2) (Ping timeout: 268 seconds)
19:15:01	→	dunkeln joins (~dunkeln@94.129.65.28)
19:15:46	→	Erutuon joins (~Erutuon@user/erutuon)
19:17:36	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 265 seconds)
19:18:17	×	sbmsr quits (~pi@2600:1700:63d0:4830:7dbf:92d8:fd42:235d) (Quit: WeeChat 2.3)
19:18:52	→	tremon joins (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl)
19:23:35	×	dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 252 seconds)
19:23:35	<dminuoso>	nf: sample size of 15 too
19:23:43	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
19:25:37	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
19:26:41	→	ppieters joins (~ppieters@105-213-89-241.access.mtnbusiness.co.za)
19:27:13	→	ku joins (~ku@2601:280:c780:7ea0:a829:e2b3:d453:ddc1)
19:27:30	<dminuoso>	And they were volunteers without any selection methodology
19:29:15	<monochrom>	Gosh I suck at C because of Haskell.
19:29:24	→	beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net)
19:29:34	<monochrom>	I wrote "int fac(int n) { n == 0 ? 1 : n * fac(n-1); }"
19:30:03	<dminuoso>	Ontop, they used just 8 phrases for this study, with no explanation how these phrases were selected either.
19:30:08	<monochrom>	Since I didn't say "return" I got machine-dependent answers, in my case it always returns 0.
19:31:11	<dminuoso>	monochrom: What surprises me is, your compiler doesn't flat out error out?
19:31:22	<monochrom>	No :)
19:31:54	<ski>	successful compilation is a wonderful thing
19:32:03	×	ppieters quits (~ppieters@105-213-89-241.access.mtnbusiness.co.za) (Remote host closed the connection)
19:34:45	×	ddellacosta quits (~ddellacos@89.45.224.170) (Ping timeout: 272 seconds)
19:36:56	<mccoyb>	Lycurgus -- I'm not sure if what backend GHC uses is relevant here. This problem is just basically "take a generic .dylib + some C header files and get stack to use them in some foreign calls".
19:37:41	→	mc47 joins (~yecinem@89.246.239.190)
19:38:05	→	hiptobecubic joins (~john@c-73-55-99-95.hsd1.fl.comcast.net)
19:43:02	→	brian_da_mage joins (~Neuromanc@adsl-187.46.190.47.tellas.gr)
19:43:02	×	brian_da_mage quits (~Neuromanc@adsl-187.46.190.47.tellas.gr) (Changing host)
19:43:02	→	brian_da_mage joins (~Neuromanc@user/briandamag)
19:44:04	×	Shaeto quits (~Shaeto@94.25.234.213) (Quit: WeeChat 3.1)
19:44:29	×	sqrt2 quits (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net) (Ping timeout: 252 seconds)
19:44:41	→	bor0 joins (~boro@46.217.54.116)
19:44:41	×	bor0 quits (~boro@46.217.54.116) (Changing host)
19:44:41	→	bor0 joins (~boro@user/bor0)
19:44:53	×	Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 272 seconds)
19:44:53	→	justsomeguy joins (~justsomeg@user/justsomeguy)
19:45:05	×	notzmv quits (~zmv@user/notzmv) (Ping timeout: 272 seconds)
19:45:32	×	igghibu quits (~igghibu@91.193.5.46) (Quit: Textual IRC Client: www.textualapp.com)
19:46:31	→	Erutuon joins (~Erutuon@user/erutuon)
19:46:36	×	Hecate quits (~mariposa@163.172.211.189) (Changing host)
19:46:36	→	Hecate joins (~mariposa@user/hecate)
19:46:44	<mccoyb>	Asking again in case any active chatters have exp -- has anyone linked (dylib + headers) with stack/cabal before and wouldn't mind chatting about it?
19:47:16	×	vicfred quits (~vicfred@user/vicfred) (Quit: Leaving)
19:49:42	<bor0>	Thanks ski. I didn't get the `@tell` message, though found your reply on ircbrowse
19:50:04	<bor0>	Ah! Right after I post a message here lambdabot messages me.
19:52:24	<dminuoso>	bor0: Right. Im specifically talking about the usage of `go`.
19:52:29	×	chomwitt quits (~Pitsikoko@athedsl-20549.home.otenet.gr) (Ping timeout: 272 seconds)
19:53:33	<dminuoso>	bor0: It's not a major deficit necessarily, but since you're writing non-trivial code I thought I'd point it out. The lack of guaranteed fusion is easily addressed by wrapping it with a particular newtype before doing all the fmapping.
19:55:04	<novasenco>	people of #haskell. I am still unable to install alsa-mixer with cabal. https://asciinema.org/a/byZnjGK2NOeaIz7xYne3f8A1I
19:55:21	<dminuoso>	Wrap with this https://hackage.haskell.org/package/kan-extensions-5.2.2/docs/Data-Functor-Yoneda.html#v:liftYoneda - do your recursive fmapping, and then lowerYoneda out. Done!
19:55:30	<bor0>	Thank you. This is a toy implementation, mainly for learning purposes. But I am now curious, could you show a minimal example of achieving this? In my case, `Proof` is already a newtype - or is the trick to do another wrap?
19:55:33	<dminuoso>	And completely ignore the scary sounding names.
19:55:53	<bor0>	Ah, Yoneda. Seen that many times, but never learned more about it
19:56:19	<dminuoso>	bor0: The gist of Yoneda is: if you have repeated fmap applications, with Yoneda GHC has a chance to fuse the function together.
19:56:21	<dminuoso>	That's all
19:56:31	<dminuoso>	Without it, you will most likely not get any fusion
19:57:10	<bor0>	By fusion you mean the composition law, right?
19:57:42	→	arson joins (~arson@pool-100-36-47-118.washdc.fios.verizon.net)
19:58:03	<dminuoso>	The fmap composition law `fmap f . fmap g`, yes.
19:58:28	<davean>	novasenco: too new a GCC
19:58:33	<dminuoso>	Turning it into `fmap (f . g)` gives better performance, since the cost of fmap is taken only once
19:58:39	<bor0>	OK, I think it makes sense. Thanks. Yeah, one `fmap` (application) on the LHS, and two of them on the RHS so I can see how optimization can be affected
19:59:09	<bor0>	(Using fmap (f . g) == fmap f . fmap g)
19:59:11	<novasenco>	wat
19:59:47	<dminuoso>	bor0: Right. Except while the law holds in our minds, GHC cant know whether all instances actually abide, so we need some trickery to force the issue.
20:00:04	<davean>	novasenco: your GCC version is too new
20:00:10	×	ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 252 seconds)
20:00:23	<dminuoso>	bor0: Internally, Yoneda is really simple. It's just partially applied fmap, with the Functor instance defined as: fmap f m = Yoneda (\k -> runYoneda m (k . f))
20:01:09	<dminuoso>	bor0: And since Yoneda is a newtype, it disappears at runtime entirely. So you can see how repeated fmap application `lowerYoneda . fmap f . fmag g . liftYoneda` gets turned into `fmap (f . g)`
20:01:43	<bor0>	I see. I knew newtypes were faster, but not because they disappeared at runtime. That's helpful to know!
20:02:15	<davean>	bor0: thats what makes newtype not data
20:03:13	→	ddellacosta joins (~ddellacos@89.45.224.170)
20:03:57	<dminuoso>	bor0: And as a teaser, we have a similar trick for repeated applications of >>=, using Codensity/liftCodensity/lowerDensity! :)
20:04:06	×	oxide quits (~lambda@user/oxide) (Ping timeout: 268 seconds)
20:04:21	<dminuoso>	If you can look over these scary looking names, they're useful primitives to allow GHC to optimize better
20:04:51	<dminuoso>	s/lowerDensity/lowerCodensity/
20:04:52	<bor0>	Does `do` notation automatically use *density?
20:04:56	<dminuoso>	No.
20:04:59	<novasenco>	davean, hmm. okay. anything I can do about that?
20:05:29	<davean>	novasenco: well you could set an older gcc, oyu're already setting CC manually
20:05:37	→	oxide joins (~lambda@user/oxide)
20:05:59	<novasenco>	(I don't even know if setting CC does anything; I was grasping at straws)
20:06:31	<davean>	anything not gcc11 should work
20:06:52	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
20:07:06	<davean>	https://github.com/haskell/c2hs/issues/268
20:07:51	→	sqrt2 joins (~ben@tunnel330957-pt.tunnel.tserv6.fra1.ipv6.he.net)
20:08:05	×	ddellacosta quits (~ddellacos@89.45.224.170) (Ping timeout: 264 seconds)
20:08:44	×	_ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection)
20:09:24	<dminuoso>	bor0: As far as I can tell, you will need Compose too to make this work.
20:09:32	×	arrowd quits (~arr@2.94.203.147) ()
20:11:01	<novasenco>	hm. oki. thanks
20:11:29	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 272 seconds)
20:11:31	<dminuoso>	Ah no, it wouldn't even work with a nested functor.
20:13:04	<bor0>	Thanks, this is all useful, although probably way beyond me at this point. If at least one more person gets to use this, I'll be happy to get deeper into optimization :D
20:13:13	<dminuoso>	bor0: Let me show you, it's really simple! :)
20:13:30	→	ddellacosta joins (~ddellacos@89.46.62.170)
20:13:39	<bor0>	Sure! Let's talk specifically about `go`. I think that'll help :D
20:15:53	×	_xft0 quits (~root@185.234.208.208.r.toneticgroup.pl) (Ping timeout: 264 seconds)
20:16:01	<davean>	novasenco: you might get around it by installing c2hs with a newer language-c, but who knows
20:16:06	×	AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.)
20:17:24	<dminuoso>	bor0: There might be the odd typo here, but roughly this: https://gist.github.com/dminuoso/fef54010b5d7dd475245d6f9b6546737
20:18:17	<dminuoso>	Typo fixed, reload! :)
20:18:52	<dminuoso>	Ah there's some small impedance mismatching with the argument `x` here
20:19:52	×	Cubic quits (~hannesste@ip5f5be453.dynamic.kabel-deutschland.de) (Quit: leaving)
20:20:55	<dminuoso>	Ah I see what's wrong. We need to massage the function `f` first
20:21:30	<bor0>	Yeah, YESP x vs Either String (Proof x)
20:21:53	<bor0>	I noticed that but thought that'd be handled by some of the magic between L5-L9 :D
20:22:09	<dminuoso>	bor0: Reload, it should be fine now
20:22:58	→	dunkeln joins (~dunkeln@94.129.65.28)
20:23:20	ski	would use `<$>'
20:23:26	→	ec joins (~ec@gateway/tor-sasl/ec)
20:24:09	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
20:24:28	<bor0>	Small typo on line 13, just a nit.
20:24:36	<bor0>	Ahhh Yoneda isn't in base.
20:24:41	<ski>	bor0 : oh, another thing i thought about (but forgot to say), is that `applyPropRule' could generalize from `Either String' to any functor
20:24:42	<dminuoso>	Yeah, its from kan-extensions
20:24:43	→	econo joins (uid147250@user/econo)
20:25:04	×	kuribas quits (~user@ptr-25vy0i96apm5u45pamz.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
20:25:11	<dminuoso>	But, if that's too heavy for you, you can just reimplement Yoneda yourself. It's just a few lines of code.
20:27:13	→	ixlun joins (~matthew@109.249.184.235)
20:27:52	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
20:27:53	×	michalz quits (~user@185.246.204.45) (Remote host closed the connection)
20:28:09	<dminuoso>	The Compose/getCompose could be dropped if you used `x <&&> f = fmap (fmap f) x` probably. Fusion should still happen (because the inner fmap would disappear since its just a newtype)
20:28:30	×	dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 264 seconds)
20:29:13	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Ping timeout: 272 seconds)
20:37:01	×	mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 272 seconds)
20:37:13	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
20:41:14	→	dpl_ joins (~dpl@77-121-78-163.chn.volia.net)
20:41:18	maralorn[m]	is now known as maralorn
20:44:34	×	maralorn quits (~maralorn@2001:470:69fc:105::251) (Quit: node-irc says goodbye)
20:44:50	→	maralorn joins (~maralorn@2001:470:69fc:105::251)
20:46:19	←	arson parts (~arson@pool-100-36-47-118.washdc.fios.verizon.net) ()
20:46:21	×	mc47 quits (~yecinem@89.246.239.190) (Quit: Leaving)
20:48:28	×	mccoyb quits (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632) (Quit: Textual IRC Client: www.textualapp.com)
20:48:50	→	Guest60 joins (~Guest60@90.242.128.21)
20:50:19	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
20:50:36	→	Digit joins (~user@user/digit)
20:51:54	×	amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 244 seconds)
20:55:10	×	ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 252 seconds)
20:57:19	×	orzo quits (joe@lasker.childrenofmay.org) (.net .split)
20:57:32	→	orzo joins (joe@lasker.childrenofmay.org)
20:57:39	Guest60	is now known as Abedegno
20:58:04	×	ddellacosta quits (~ddellacos@89.46.62.170) (Remote host closed the connection)
20:58:15	→	ddellacosta joins (~ddellacos@89.46.62.170)
20:59:57	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
21:01:13	→	unyu joins (~pyon@user/pyon)
21:01:37	→	dy joins (~dy@user/dy)
21:06:14	×	Abedegno quits (~Guest60@90.242.128.21) (Ping timeout: 250 seconds)
21:06:17	×	beka quits (~beka@104.193.170-254.PUBLIC.monkeybrains.net) (Ping timeout: 264 seconds)
21:06:26	×	derelict quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 252 seconds)
21:07:23	×	Ariakenom quits (~Ariakenom@2001:9b1:efb:fc00:d9c3:69a3:f97b:be95) (Read error: Connection reset by peer)
21:08:37	×	ddellacosta quits (~ddellacos@89.46.62.170) (Remote host closed the connection)
21:09:52	×	funsafe quits (~funsafe@2601:1c1:4200:938f:389d:16a4:ae2d:65aa) (Quit: funsafe)
21:10:12	→	funsafe joins (~funsafe@2601:1c1:4200:938f:389d:16a4:ae2d:65aa)
21:11:43	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
21:14:08	×	myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 252 seconds)
21:15:16	→	lavaman joins (~lavaman@98.38.249.169)
21:15:24	×	dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 272 seconds)
21:15:29	→	sondre joins (~sondrelun@cm-84.212.100.140.getinternet.no)
21:18:33	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:20:06	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds)
21:20:49	×	ixlun quits (~matthew@109.249.184.235) (Read error: Connection reset by peer)
21:22:09	→	dustinm joins (~dustinm@static.38.6.217.95.clients.your-server.de)
21:26:48	→	egoist joins (~egoist@186.235.82.52)
21:26:57	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
21:27:55	→	tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
21:30:23	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
21:32:34	→	mccoyb joins (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632)
21:32:37	×	mccoyb quits (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632) (Client Quit)
21:33:15	→	wenzel_ joins (~wenzel@user/wenzel)
21:33:36	allbery_b	is now known as geekosaur
21:34:24	×	merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds)
21:35:40	×	wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
21:36:18	×	wenzel quits (~wenzel@user/wenzel) (Ping timeout: 264 seconds)
21:37:18	×	learner-monad quits (~ehanneken@cpe-174-105-47-100.columbus.res.rr.com) (Quit: WeeChat 3.1)
21:37:25	×	wenzel_ quits (~wenzel@user/wenzel) (Client Quit)
21:39:25	×	xsperry quits (~as@user/xsperry) (Read error: Connection reset by peer)
21:39:52	→	myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net)
21:39:55	→	mccoyb joins (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632)
21:41:47	×	pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2-dev)
21:43:47	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
21:44:16	→	imdoor joins (~imdoor@balticom-142-78-50.balticom.lv)
21:44:20	×	pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (Quit: WeeChat 3.1)
21:44:33	→	pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net)
21:45:25	×	tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:45:30	→	ddellacosta joins (~ddellacos@89.45.224.40)
21:45:51	×	bfrk quits (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) (Ping timeout: 268 seconds)
21:46:26	→	notzmv joins (~zmv@user/notzmv)
21:47:15	×	werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Quit: Lost terminal)
21:50:06	×	ddellacosta quits (~ddellacos@89.45.224.40) (Ping timeout: 264 seconds)
21:51:24	×	sheepduck quits (~sheepduck@2607:fea8:2a60:b700::8a94) (Remote host closed the connection)
21:52:27	→	vdukhovni joins (~vdukhovni@100.2.39.101)
21:53:14	×	Digit quits (~user@user/digit) (Ping timeout: 265 seconds)
21:54:14	→	beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net)
21:54:18	×	mccoyb quits (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632) (Quit: My MacBook Air has gone to sleep. ZZZzzz…)
21:56:06	→	sheepduck joins (~sheepduck@2607:fea8:2a60:b700::8a94)
21:56:56	→	werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net)
22:00:30	<novasenco>	davean, well, I did ghcup tui and then installed latest ghc and set it. Then, for some reason, it also updated c2hs, though I don't know how or why. And it looks like alsa-mixer is installing ^u^
22:00:41	→	dutchgriffon joins (~laurens@2604:3d08:4383:6200:14a:dacb:8b69:ead6)
22:00:43	×	__monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:01:22	<novasenco>	(ie, I installed prereleast,base-4.16.0.0)
22:01:28	<novasenco>	s/st/se
22:01:52	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
22:02:56	×	haskman quits (~haskman@106.201.8.96) (Quit: Going to sleep. ZZZzzz…)
22:03:19	→	blankhart joins (~blankhart@pool-72-88-174-206.nwrknj.fios.verizon.net)
22:03:23	×	gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving)
22:03:58	<novasenco>	sike. It failed with the same error; it just took longer.
22:04:05	→	ddellacosta joins (~ddellacos@86.106.143.209)
22:04:48	×	bor0 quits (~boro@user/bor0) (Quit: Leaving)
22:06:42	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds)
22:08:01	<blankhart>	is there a canonical discussion of how to implement higher kinded types? (as a compiler writer not as a language user)
22:10:03	×	eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9) (Remote host closed the connection)
22:10:23	<geekosaur>	novasenko, either downgrade gcc (if possible) or wait for https://github.com/haskell/c2hs/issues/268 to be fixed
22:12:24	<ski>	blankhart : allow type variables to have arbitrary kind ?
22:12:25	×	sondre quits (~sondrelun@cm-84.212.100.140.getinternet.no) (Ping timeout: 245 seconds)
22:12:50	<blankhart>	looks like i may have been looking for TAPL ch 29
22:13:24	×	xwx quits (~george@user/george) (Quit: WeeChat 3.1)
22:15:12	<novasenco>	geekosaur, I be waiting -_- In the meantime, at least I have my handy dandy script bound to xmonad key bindings https://gist.github.com/novasenco/a048f34753cc3eb76eef7da5e8b59ee4
22:15:17	×	myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 264 seconds)
22:16:15	<novasenco>	(eg, vol -i, vol -d, and vol to (resp) increase vol to nearest mult of 5, decrease vol to nearest multiple of 5, or show volume - all of them use notify-send to show volume. works for now. thanks for your help.)
22:18:13	×	hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 252 seconds)
22:18:53	×	lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 264 seconds)
22:19:03	→	janus joins (janus@anubis.0x90.dk)
22:19:23	<janus>	i am trying to build with profiling, so i put "profiling: true" in cabal.project
22:19:43	<janus>	but a transitive dependency called convertible (from hdbc) is failing
22:19:56	<janus>	the error message is https://paste.tomsmeding.com/KDHTbbaa
22:20:06	→	hendursaga joins (~weechat@user/hendursaga)
22:20:26	<janus>	how can the profiling libraries for that package be missing? wouldn't cabal know whether it needs rebuilding?
22:26:41	×	dpl_ quits (~dpl@77-121-78-163.chn.volia.net) (Ping timeout: 264 seconds)
22:26:44	<janus>	is this even the right channel for that question? guess it isn't really specific to haskell the language
22:26:49	<janus>	but i don't know of a cabal channel
22:27:22	<monochrom>	This is the right channel, but I haven't run into that kind of problem so I have no answer.
22:28:46	<janus>	i have ghc from ghcup so it should support profiling (i say that because previously i was using OS packages where you'd have to get that in a separate package)
22:29:51	→	eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:5878:fcfd:e07b:ffd9)
22:31:39	×	tremon quits (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
22:31:53	<janus>	i suspect it may be somewith with convertible being so old, seems like it wasn't updated for years: https://github.com/hdbc/convertible
22:32:18	<janus>	but on the other hand, it has "Build-Type: Simple", so that shouldn't cause problems...
22:32:24	×	dragestil quits (~quassel@180-150-39-25.b49627.bne.nbn.aussiebb.net) (Changing host)
22:32:24	→	dragestil joins (~quassel@user/dragestil)
22:32:24	<dminuoso>	Lets say I really wanted to override an existing Show instance, I dont care whether its dirty. Do I have any options?
22:33:05	<dminuoso>	I have just 2 types, that occur deeply nested in my data types that have a very unsuitable Show instance. And Im really fine with Show otherwise for this output.
22:33:28	<dminuoso>	Or is forking my best bet here?
22:33:39	<dminuoso>	(that is, forking the library that introduces the undesirable Show instance)
22:34:31	<geekosaur>	I don't think overlapping will work if the instance heads are identical (I may be wrong) so forking may be your only alternative
22:35:18	×	vdukhovni quits (~vdukhovni@100.2.39.101) (Quit: Client closed)
22:35:26	<dminuoso>	mmm, perhaps I should just try overlapping instances then
22:35:29	→	is7s joins (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e)
22:36:02	<janus>	now i wonder what happens if you have two instances, where one requires a 'trivial' constraint like HasCallStack ... hmm
22:36:11	×	hrnz quits (~ulli@cherry.hrnz.li) (Quit: das ist mir zu bld hier; bb)
22:36:23	→	hrnz joins (~ulli@cherry.hrnz.li)
22:38:16	×	GIANTWORLDKEEPER quits (~pjetcetal@2.95.204.25) (Ping timeout: 268 seconds)
22:38:33	→	zeenk joins (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41)
22:38:37	<hpc>	constraints don't count for instance resolution
22:39:26	<hpc>	so like, "instance Applicative f => Monad f" resolves the same as "instance Monad f"
22:39:43	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
22:39:44	→	bfrk joins (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de)
22:40:05	→	geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com)
22:40:45	<monochrom>	To get dirty, the "reflection" package, or the idea within, may help, I forgot whether it does help. But the idea is you can supply a record value and convert it to a class dictionary and sneak it in by a backdoor, so now without newtyping you can change the dictionary at will.
22:40:55	←	is7s parts (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e) ()
22:41:03	→	is7s joins (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e)
22:41:09	→	GIANTWORLDKEEPER joins (~pjetcetal@2.95.204.25)
22:41:11	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
22:41:37	←	is7s parts (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e) ()
22:42:30	→	wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
22:43:54	<dminuoso>	Mmm, I dont understand the phrasing in https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/instances.html
22:44:12	→	is7s joins (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e)
22:44:13	<dminuoso>	Naively I'd expect `instance {-# OVERLAPPING #-} Show T` to just work
22:44:34	<dminuoso>	% instance {-# OVERLAPPING #-} Show Int where show _ = "foo"
22:44:34	<yahb>	dminuoso: ; <interactive>:15:30: error:; Duplicate instance declarations:; instance [overlapping] Show Int -- Defined at <interactive>:15:30; instance Show Int -- Defined in `GHC.Show'
22:45:15	<monochrom>	overlapping still wants to see at most one match. It is incoherentinstances that is happy with multiple matches just randomly pick one.
22:45:24	<janus>	hpc: aaaah right, makes sense! and i see it in the ghc user guide link that dminuoso provided
22:45:33	<dminuoso>	monochrom: Oh that might be acceptable!
22:45:53	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 264 seconds)
22:45:55	<monochrom>	If it picks the one you hate, please don't cry. :)
22:46:54	<dminuoso>	Well Ill debug GHC and see how I can massage it into picking the right one :>
22:47:22	<dminuoso>	Mmm
22:47:26	<dminuoso>	% instance {-# INCOHERENT #-} Show Int where show _ = "foo"
22:47:26	<yahb>	dminuoso: ; <interactive>:16:29: error:; Duplicate instance declarations:; instance [incoherent] Show Int -- Defined at <interactive>:16:29; instance Show Int -- Defined in `GHC.Show'
22:48:01	<monochrom>	I guess I worded wrong. s/at most one match/a single match that is more specific than all other matches/
22:48:19	<dminuoso>	Yeah. I guess IncoherentInstances only works if the matches are not most specific
22:48:45	×	niflce quits (~IceChat95@user/niflce) (Ping timeout: 268 seconds)
22:48:57	<monochrom>	If you have two incomparable matches, then it's incoherentinstances.
22:50:03	→	boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com)
22:50:48	<dminuoso>	Why wont GHC let me just specify "discard this dictionary from a package" :(
22:57:48	→	derelict joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com)
22:57:53	→	ec_ joins (~ec@gateway/tor-sasl/ec)
22:59:37	→	mccoyb joins (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632)
23:02:01	→	neceve joins (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130)
23:02:41	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
23:03:17	×	alx741 quits (~alx741@186.178.108.160) (Ping timeout: 264 seconds)
23:06:52	×	ddellacosta quits (~ddellacos@86.106.143.209) (Remote host closed the connection)
23:06:52	×	derelict quits (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com) (Ping timeout: 272 seconds)
23:11:32	→	vdukhovni joins (~vdukhovni@100.2.39.101)
23:12:41	×	Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.)
23:13:21	→	ddellacosta joins (~ddellacos@89.45.224.118)
23:15:48	→	myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net)
23:15:51	→	alx741 joins (~alx741@181.196.69.176)
23:16:46	→	spatchkaa joins (~spatchkaa@S010600fc8da47b63.gv.shawcable.net)
23:17:06	×	vdukhovni quits (~vdukhovni@100.2.39.101) (Quit: Client closed)
23:17:21	×	is7s quits (~is7s@2a01:4b00:895f:3d00:a806:e7e7:5179:550e) (Quit: Client closed)
23:18:53	→	benin joins (~benin@183.82.205.186)
23:21:34	→	bfrk1 joins (~Thunderbi@200116b845fca000f97ff890167a6943.dip.versatel-1u1.de)
23:21:44	×	bfrk quits (~Thunderbi@200116b84593d400e083e41adfb91d63.dip.versatel-1u1.de) (Ping timeout: 244 seconds)
23:21:44	bfrk1	is now known as bfrk
23:24:07	×	tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: nvkjsb)
23:25:28	→	yav joins (~username@2001:428:6002:405:c8cd:63fb:2af4:b319)
23:27:09	×	boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Remote host closed the connection)
23:29:00	×	yav quits (~username@2001:428:6002:405:c8cd:63fb:2af4:b319) (Remote host closed the connection)
23:30:15	→	yav joins (~username@2001:428:6002:405:c8cd:63fb:2af4:b319)
23:30:32	→	merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
23:37:11	×	ec_ quits (~ec@gateway/tor-sasl/ec) (Quit: ec_)
23:37:27	→	pavonia_ joins (~user@user/siracusa)
23:39:37	→	sayola1 joins (~vekto@88.78.152.150)
23:39:54	×	pavonia quits (~user@user/siracusa) (Ping timeout: 264 seconds)
23:39:54	×	sayola quits (~vekto@dslb-088-078-152-150.088.078.pools.vodafone-ip.de) (Ping timeout: 264 seconds)
23:40:35	×	tv quits (~tv@user/tv) (Ping timeout: 272 seconds)
23:41:35	×	pavonia_ quits (~user@user/siracusa) (Ping timeout: 245 seconds)
23:41:38	→	allbery_b joins (~geekosaur@069-135-003-034.biz.spectrum.com)
23:42:00	×	yav quits (~username@2001:428:6002:405:c8cd:63fb:2af4:b319) (Remote host closed the connection)
23:42:08	×	abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Quit: leaving)
23:42:23	×	geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Killed (NickServ (GHOST command used by allbery_b)))
23:42:28	allbery_b	is now known as geekosaur
23:44:14	×	sayola1 quits (~vekto@88.78.152.150) (Ping timeout: 272 seconds)
23:44:14	→	tv joins (~tv@user/tv)
23:46:56	→	pavonia joins (~user@user/siracusa)
23:47:24	→	WhyNot joins (~Thunderbi@2a02:aa12:540:e480:d738:2660:2e:8993)
23:48:13	→	hiruji` joins (~hiruji@72.74.190.75)
23:49:54	×	hiruji` quits (~hiruji@72.74.190.75) (Client Quit)
23:49:59	×	hiruji quits (~hiruji@user/hiruji) (Ping timeout: 272 seconds)
23:50:18	→	hiruji joins (~hiruji@user/hiruji)
23:50:41	×	mnrmnaugh quits (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net) (Ping timeout: 264 seconds)
23:51:05	→	mnrmnaugh joins (~mnrmnaugh@pool-96-252-87-182.bstnma.fios.verizon.net)
23:52:36	×	mccoyb quits (~textual@2601:182:d000:3b50:74fc:67c:ef8b:8632) (Quit: My MacBook Air has gone to sleep. ZZZzzz…)
23:53:26	×	WhyNot quits (~Thunderbi@2a02:aa12:540:e480:d738:2660:2e:8993) (Quit: WhyNot)
23:55:37	→	derelict joins (~winter@2603-6011-f901-9e5b-0000-0000-0000-08cf.res6.spectrum.com)
23:57:47	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
23:59:11	→	pavonia_ joins (~user@user/siracusa)

All times are in UTC on 2021-06-01.