Logs on 2022-04-01 (liberachat/#haskell)

00:01:51	→	chenqisu1 joins (~chenqisu1@183.217.200.168)
00:02:26	×	pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5)
00:07:15	×	littlebobeep quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
00:09:09	×	Topsi quits (~Tobias@dyndsl-095-033-092-148.ewe-ip-backbone.de) (Read error: Connection reset by peer)
00:09:36	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
00:14:55	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 246 seconds)
00:17:15	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
00:20:53	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
00:20:54	×	immae quits (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 3.3)
00:21:16	×	geranim0 quits (~geranim0@modemcable242.171-178-173.mc.videotron.ca) (Remote host closed the connection)
00:21:19	→	immae joins (~immae@2a01:4f8:141:53e7::)
00:21:28	×	xff0x quits (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp) (Ping timeout: 260 seconds)
00:24:39	×	immae quits (~immae@2a01:4f8:141:53e7::) (Client Quit)
00:25:09	→	immae joins (~immae@2a01:4f8:141:53e7::)
00:25:35	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Ping timeout: 260 seconds)
00:26:44	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
00:31:01	×	mixfix41 quits (~homefame@user/mixfix41) (Ping timeout: 246 seconds)
00:31:20	×	immae quits (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 3.3)
00:31:23	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
00:32:01	→	immae joins (~immae@2a01:4f8:141:53e7::)
00:38:28	<zebrag>	"λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", "Name k is bound to the continuation which adds 8". I've never seen anything like that before. I'm wondering how you manage to give it the argument "x". But otherwise, it is awesome. ("Minimal classical logic and control operators")
00:39:49	<Axman6>	I can't parse that
00:40:12	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
00:42:00	<abastro[m]>	What is K in `\x. K(..)`
00:42:37	<ProfSimm>	Is there a very precise guide to how HAskell parses whitespace
00:42:38	<Axman6>	yeah, and what's k2?
00:43:17	<zebrag>	abastro[m]: apparently it's an operator that will catch the context, so here it would be the adding of 8
00:43:26	<abastro[m]>	Perhaps `k 2`, because `k` is sth you could apply an argument
00:43:47	<abastro[m]>	Oh, operator catching contexr
00:44:58	<abastro[m]>	Idk why it adds 8 tho, like, this looks like delimited continuation on the surface
00:45:14	<abastro[m]>	Where `k 2` replace the K(..) term with 2 when called
00:45:23	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
00:45:54	<zebrag>	well they say it's delimited continuation, but I'm not crystal with delimited continuations, so I couldn't say
00:46:43	<abastro[m]>	Me too, tbh
00:49:55	→	[itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
00:51:08	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
00:51:13	→	littlebobeep joins (~alMalsamo@gateway/tor-sasl/almalsamo)
01:00:09	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 250 seconds)
01:00:26	→	xff0x joins (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp)
01:01:33	×	nosewings quits (~ngpc@2603-8081-3e05-e2d0-96c1-0fad-58de-6f58.res6.spectrum.com) (Remote host closed the connection)
01:09:24	→	vysn joins (~vysn@user/vysn)
01:10:33	×	albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
01:10:58	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
01:15:14	×	anon61924576 quits (~anon61924@85.210.203.240) (Remote host closed the connection)
01:15:31	→	anon61924576 joins (~anon61924@85.210.203.240)
01:16:39	→	albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
01:16:56	→	Akiva joins (~Akiva@user/Akiva)
01:19:24	→	neurocyte8614 joins (~neurocyte@IP-094016090045.dynamic.medianet-world.de)
01:19:24	×	neurocyte8614 quits (~neurocyte@IP-094016090045.dynamic.medianet-world.de) (Changing host)
01:19:24	→	neurocyte8614 joins (~neurocyte@user/neurocyte)
01:21:32	×	neurocyte861 quits (~neurocyte@user/neurocyte) (Ping timeout: 260 seconds)
01:21:33	neurocyte8614	is now known as neurocyte861
01:24:17	<zebrag>	I've read a couple of lines of https://en.wikipedia.org/wiki/Delimited_continuation, so I think, I almost know everything there is to know.
01:24:51	→	lainon joins (~lainon@2601:7c0:c500:4d20::6dc6)
01:26:00	<zebrag>	I've read that line to be specific: `(* 2 (reset (+ 1 (shift k (k 5)))))`
01:31:39	←	jakalx parts (~jakalx@base.jakalx.net) (Error from remote client)
01:36:02	×	anon61924576 quits (~anon61924@85.210.203.240) (Remote host closed the connection)
01:36:39	→	jakalx joins (~jakalx@base.jakalx.net)
01:43:14	<zebrag>	"Partial continuations are control operators in functional programming such that a function-like object is abstracted from a part of the rest of computation, rather than the whole rest of computation." (https://doi.org/10.1007/3-540-44929-9_34 A Type-Theoretic Study on Partial Continuations)
01:44:05	→	abastro joins (~abab9579@220.75.216.63)
01:46:44	<abastro[m]>	So the behavior differs in interesting way when continuation is called multiple times
01:46:57	<abastro[m]>	Otherwise, effectively just replacing the shifting code with 5
01:47:27	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
01:48:12	<dolio>	They differ in multiple ways, unless you use pretty specific examples.
01:49:23	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 252 seconds)
01:49:42	<dolio>	Doing nothing but calling the continuation once immediately is one such example, though.
01:51:02	<abastro>	I mean by calling continuation at most once, it is equivalent with replacing the code in `shift` with the value supplied
01:51:07	<janus>	can ghc for the m1 automatically compile for x86_64 such that it is backwards compatible?
01:51:17	<janus>	does stack support this?
01:51:34	<janus>	asking because of this comment: https://stackoverflow.com/questions/69143043/how-to-create-native-arm-executables-on-macos-using-ghc-stack/71670541?noredirect=1#comment126696956_71670541
01:52:27	<dolio>	abastro: No, it's not that simple. For instance, you don't need to call the continuation inside the lexical scope of `shift`, and then the behavior is going to be very different.
01:53:04	<abastro>	Wait, no need to call continuation inside `shift`?
01:54:16	<dolio>	Although in the case of the undelimited analogue of shift, it's unclear how that would even happen, because you'd basically just be ending the computation.
01:56:06	<abastro>	Wait, soo
01:56:44	<abastro>	How do you even refer to the continuation out of the lexical scope of shift
01:56:54	<dolio>	You can return it from shift.
01:57:01	<dolio>	(shift k k)
01:57:16	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
01:57:29	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
01:57:38	<dolio>	That yields the continuation to whichever reset is enclosing it.
01:58:57	<abastro>	Oh. Tho tbh that is not 'calling' it
01:59:15	×	Benzi-Junior quits (~BenziJuni@88-149-64-179.du.xdsl.is) (Remote host closed the connection)
01:59:39	<dolio>	That doesn't mean it's never called, just that it isn't called inside the lexical scope of shift.
02:00:34	×	califax quits (~califax@user/califx) (Remote host closed the connection)
02:00:46	→	califax joins (~califax@user/califx)
02:00:53	<dolio>	let k = reset (8 + shift (\k -> k)) in 3 + k 5
02:01:13	<zebrag>	I don't know how the "λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", can be simulated by shift and reset: the `lambda x.K(...)` is really something.
02:01:20	<zebrag>	hum
02:01:51	<dolio>	That is 16, because `k` is the function that adds 8 in both cases.
02:01:54	×	jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 272 seconds)
02:02:35	<zebrag>	okay, I get it
02:02:41	<abastro>	Yep, I should have said like, called at most once inside the lexical scope and never escapes
02:04:10	<abastro>	Uhm isn't `2 + 8 = 10`?
02:05:32	<zebrag>	k is adding 8
02:05:47	<zebrag>	3 + 8 + 5
02:05:56	<monochrom>	I don't use (or trust) wordy verbal "intuitive" descriptions. I use algebra-like operational rules. Here:
02:06:05	<monochrom>	outerstuff reset (innerstuff (shift k body) innerstuff) outerstuff
02:06:12	<monochrom>	-> let k = \x -> reset (innerstuff x innerstuff) in outerstuff body outerstuff
02:07:01	<abastro>	Meh I was looking at `λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8`
02:07:23	<zebrag>	hum, this one
02:07:45	<abastro>	2 'outerstuff's
02:07:48	<abastro>	I am confused
02:07:51	×	euandreh quits (~euandreh@191.181.59.160) (Ping timeout: 256 seconds)
02:07:59	<monochrom>	The word "delimited continuation" refers to "reset (innerstuff [.] interstuff)" which is the scoped continuation (context) of the shift command there.
02:08:31	<monochrom>	What would you like me to call them? dot dot dot? Then I would have four "dot dot dot"s.
02:08:47	<abastro>	Btw I thought binding k cannot escape the scope of `body`, while its body could
02:09:07	<monochrom>	Ah OK, my bad for this one.
02:09:22	<monochrom>	outerstuff (let k = \x -> ... in body) outerstuff
02:10:26	<dolio>	The 'replacing the code in shift' is also mistaken, and responsible for this example.
02:10:47	<dolio>	reset (8 + shift (\k -> 1 + k 5)) = 1 + (8 + 5)
02:11:07	<dolio>	k acts like a function.
02:11:40	<abastro>	(reset (i1 (shift k body) i2) = (let_in k (\ x (i1 x i2)) body)
02:11:45	<dolio>	With undelimited continuations, the example acts differently.
02:12:09	<abastro>	Okay I just confused undelimited continuation with delimited continuation. Meh
02:12:51	<monochrom>	shift becomes undelimited if you don't have reset :)
02:13:10	<monochrom>	call/cc becomes delimited if you recall that there is a global RTS reset.
02:13:32	<zebrag>	what about `reset (8 + shift (\k -> 1 + k 5)) = 8 + 5` only?
02:13:33	<monochrom>	At least that's how Racket thinks of it.
02:15:02	<abastro>	I hate continuation now
02:16:14	<monochrom>	My http://www.vex.net/~trebla/haskell/cont.xhtml uses "Cont (\k -> ...)" for "shift k ...", "runCont p id" for "reset p". This is my favourite way of using the Cont monad now. I no longer care about callCC.
02:16:58	<monochrom>	Indeed a lot of Scheme/Racket people ditch call/cc as well.
02:17:07	×	Codaraxis__ quits (~Codaraxis@user/codaraxis) (Ping timeout: 272 seconds)
02:17:32	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:18:10	<abastro>	I did not know that `Cont (\k -> ...) was shift`
02:18:12	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
02:18:22	<abastro>	Now I can somewhat use mtl style continuation then
02:18:36	<abastro>	Uhm wait, ContT tho
02:18:52	<sm>	Hecate: flora: not only postgres, I even installed nix again (on mac). FYI I was stopped by https://discourse.nixos.org/t/derivations-failing-on-macos-due-to-libattr/5703 (of which a 2020 person said "I don’t think the attr library will ever build on mac, so the correct solution would be modifying the package to remove the attr library on mac")
02:18:53	<monochrom>	The observation is that the way people use call/cc is that they store continuations in mutable variables to emulate delimited continuations. When that happens, you know it's the end of an era and the dawn of a new one.
02:20:18	<zebrag>	Is there an equivalent of `reset` with `Cont (\k -> ...)`? or is it undelimited only?
02:20:35	<dolio>	reset is runCont.
02:20:42	<zebrag>	tx
02:20:57	×	lainon quits (~lainon@2601:7c0:c500:4d20::6dc6) (Quit: lainon)
02:21:01	<dolio>	With id.
02:21:24	<abastro>	Continuation is too hard, and so monad is somewhat hard as well :(
02:22:22	<zebrag>	monads are quite straightforward, no?
02:22:41	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
02:22:46	<zebrag>	applicatives are straightforward
02:22:47	<monochrom>	s/continuation/callback/ and suddenly it's easy :)
02:22:49	<abastro>	Well my understanding of monads go through continuation, soo..
02:23:04	<abastro>	I don't find callbacks that easy tho
02:23:13	<abastro>	Like, when it is used like continuation
02:23:48	<monochrom>	getLine >>= \s -> putStrLn ("hello " ++ s) --- That lambda is the continuation^W callback.
02:24:12	<abastro>	Yep, and that makes monad quite hard for many ppl I think
02:25:05	<monochrom>	Callback-based programming has been around for 20 years.
02:25:11	<zebrag>	callbacks can't drop a part of the code; callbacks are always easy to type
02:25:52	<zebrag>	in "λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8", k does not behave like a function
02:26:00	<monochrom>	No one dare to say it's hard. It's best practice in many sectors.
02:26:12	<abastro>	`k` does behave like function, no?
02:26:18	<zebrag>	no
02:26:21	<zebrag>	not there
02:26:32	<abastro>	I thought `k` is just captured continuation there
02:27:12	<zebrag>	because if x=0, the result is supposed to be 10, not 11
02:27:13	<abastro>	Wait now I am confused
02:27:16	<monochrom>	If the framework decides to not call your callback, that's observationally equivalent to dropping code.
02:27:35	<abastro>	Yep, this one is not delimited continuation I guess
02:27:44	<zebrag>	but it would be the other way around here
02:28:02	<zebrag>	if you call the k, then it drops the `+ 1`
02:28:15	<abastro>	Yep, inner code decides what to do
02:28:50	<abastro>	Tho this looks like not-delimited continuation
02:29:02	<monochrom>	That's just known as "goto" to 60yos. :)
02:29:08	<zebrag>	it doesn't return like a function and then obediently add the 1
02:30:05	<monochrom>	or setjmp/longjmp.
02:31:06	<abastro>	& ppl dislike `goto` with passion :$
02:31:23	<monochrom>	Dislike, shame, but not "it's hard".
02:32:46	<abastro>	Because it is hard to follow the control-flow
02:33:37	<abastro>	+ look at me, I am extremely confused btwn delimited continuation and normal continuation
02:34:13	<abastro>	Finally I see that the two are extremely different
02:36:15	×	zyklotomic quits (~ethan@res388d-128-61-91-237.res.gatech.edu) (Ping timeout: 260 seconds)
02:37:48	×	xkuru quits (~xkuru@user/xkuru) (Read error: Connection reset by peer)
02:38:14	→	zyklotomic joins (~ethan@res380d-128-61-86-82.res.gatech.edu)
02:39:34	→	c209e6dc-4d76-47 joins (~aditya@2601:249:4300:1296:195:dac6:592c:a55a)
02:40:25	→	euandreh joins (~euandreh@2804:14c:33:9fe5:ac31:7ac1:bab2:710d)
02:43:23	×	terrorjack quits (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat)
02:44:38	→	terrorjack joins (~terrorjac@2a01:4f8:1c1e:509a::1)
02:46:33	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
02:48:14	×	waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
02:50:49	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
02:52:10	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
02:54:24	×	c209e6dc-4d76-47 quits (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!)
02:57:12	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
02:59:14	<zebrag>	yes, like: no application should be without its continuation, never `(lambda x.u)v` but always `(lambda k x.u)kv`, and no function call ever return.
03:00:00	<zebrag>	so you need some side effects otherwise you'll be unaware of what is possibly happening, because it never returns
03:00:16	×	Macbethwin quits (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection)
03:00:37	→	Macbethwin joins (~chargen@D964062A.static.ziggozakelijk.nl)
03:01:22	<zebrag>	`1 + 2` is okay because 1 and 2 are constant and `+` is a function symbol
03:01:51	<zebrag>	for every thing else you would need an additional continuation
03:02:16	→	frost joins (~frost@user/frost)
03:04:25	<sm>	Hecate, FYI got a bit further by commenting out ghcid and iputils in shell.nix, and running make soufflé build -> https://termbin.com/0yuk
03:05:09	→	mixfix41 joins (~homefame@user/mixfix41)
03:05:56	<sm>	(cc is https://termbin.com/92vk)
03:15:36	×	lbseale quits (~ep1ctetus@user/ep1ctetus) (Read error: Connection reset by peer)
03:15:51	×	zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!)
03:16:55	×	jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
03:18:03	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
03:18:58	→	jpds joins (~jpds@gateway/tor-sasl/jpds)
03:21:03	×	abastro quits (~abab9579@220.75.216.63) (Ping timeout: 260 seconds)
03:24:04	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
03:24:18	→	mbuf joins (~Shakthi@122.162.64.255)
03:26:36	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
03:31:38	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
03:34:07	×	rawley quits (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca) (Remote host closed the connection)
03:51:19	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
03:58:42	→	cdman joins (~dcm@user/dmc/x-4369397)
04:06:55	<albet70>	if I git clone a haskell project which used cabal, how I can use cabal install that and expose its module to ghc?
04:07:59	<albet70>	for example, xlsx project on github, cabal v2-build, cabal v2-install --lib, now only cabal repl can use this module xlsx, ghci still not found
04:08:24	<abastro[m]>	Or just `cabal build` and always use cabal repl
04:12:21	×	jinsun__ quits (~jinsun@user/jinsun) ()
04:14:29	→	Codaraxis joins (~Codaraxis@user/codaraxis)
04:15:48	→	c209e6dc-4d76-47 joins (~aditya@2601:249:4300:1296:195:dac6:592c:a55a)
04:23:56	×	c209e6dc-4d76-47 quits (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!)
04:26:44	×	Unicorn_Princess quits (~Unicorn_P@93-103-228-248.dynamic.t-2.net) (Quit: Leaving)
04:27:03	→	wardrunal joins (~goose@167.179.114.36)
04:36:49	→	abastro joins (~abab9579@220.75.216.63)
04:37:43	→	Codaraxis_ joins (~Codaraxis@user/codaraxis)
04:37:49	×	mvk quits (~mvk@2607:fea8:5ce3:8500::3800) (Ping timeout: 240 seconds)
04:41:10	×	shriekingnoise quits (~shrieking@201.231.16.156) (Quit: Quit)
04:41:37	×	Codaraxis quits (~Codaraxis@user/codaraxis) (Ping timeout: 246 seconds)
04:50:14	→	bahamas joins (~lucian@86.121.135.166)
04:52:05	<sclv>	add it to your cabal.project file as an extra package
04:54:24	→	jinsun joins (~jinsun@user/jinsun)
04:55:08	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
04:59:02	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
04:59:15	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
04:59:31	×	zyklotomic quits (~ethan@res380d-128-61-86-82.res.gatech.edu) (Ping timeout: 260 seconds)
04:59:59	×	bahamas quits (~lucian@86.121.135.166) (Ping timeout: 260 seconds)
05:00:18	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
05:01:34	→	zyklotomic joins (~ethan@r4-128-61-95-82.res.gatech.edu)
05:07:08	→	takuan joins (~takuan@178-116-218-225.access.telenet.be)
05:17:23	<jneira[m]>	hmm but `cabal install --lib` should make it available to ghci 🤔
05:18:42	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
05:20:46	×	mjrosenb quits (~mjrosenb@pool-108-54-97-96.nycmny.fios.verizon.net) (Ping timeout: 272 seconds)
05:20:53	→	mjrosenb joins (~mjrosenb@pool-108-54-97-96.nycmny.fios.verizon.net)
05:21:18	×	sayola quits (~vekto@dslb-002-201-085-116.002.201.pools.vodafone-ip.de) (Ping timeout: 260 seconds)
05:23:16	×	InstX1 quits (~Liam@2601:6c4:4080:3f80:85fa:fa6d:a3c9:394a) (Ping timeout: 245 seconds)
05:28:36	→	Inst joins (~Liam@2601:6c4:4080:3f80:8562:905a:59dc:27e9)
05:28:54	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
05:30:21	→	dschrempf joins (~dominik@mobiledyn-62-240-134-186.mrsn.at)
05:52:35	→	chomwitt joins (~chomwitt@2a02:587:dc0e:a100:8d19:188:687f:a348)
05:53:54	→	jinsun__ joins (~jinsun@user/jinsun)
05:55:22	→	jinsun___ joins (~jinsun@user/jinsun)
05:57:24	×	jinsun quits (~jinsun@user/jinsun) (Ping timeout: 240 seconds)
05:58:03	jinsun___	is now known as jinsun
05:58:12	→	coot joins (~coot@213.134.190.95)
05:58:43	×	jinsun__ quits (~jinsun@user/jinsun) (Ping timeout: 256 seconds)
06:03:20	<albet70>	"jneira[m] :hmm but `cabal install --lib` should make it available to ghci 🤔", still no
06:03:50	<Axman6>	this kind of global install of packages is generally not how we do things any more as far as I understand it
06:03:58	<albet70>	but I'd like to use runghc
06:04:22	×	MasseR46 quits (~MasseR@51.15.143.128) (Quit: The Lounge - https://thelounge.chat)
06:04:23	<albet70>	load Main.hs in cabal repl to run seems not good...
06:05:04	→	MasseR46 joins (~MasseR@51.15.143.128)
06:05:38	<Axman6>	is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful?
06:10:14	×	[itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
06:10:36	<abastro>	Oh, runghc..
06:10:40	<albet70>	"Axman6 :is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful?", but v2-run script.hs which is not a normal a.hs
06:10:54	<abastro>	So you want to use it for script?
06:11:10	<Axman6>	it is, everything that makes it scriptable is in comments
06:11:19	<albet70>	I'd like to run it easy like runghc a.hs
06:11:20	<Axman6>	IIRC including the shebang at the top
06:11:37	<abastro>	Yep, tho I guess it is not as easy with cabal
06:11:54	×	azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection)
06:12:10	→	azimut joins (~azimut@gateway/tor-sasl/azimut)
06:12:33	<albet70>	but v2-run script.hs need build-depends?
06:12:59	<Axman6>	isn't that what you'rte trying to do? depend on another library?
06:13:07	<albet70>	why cabal can't not like pip to install package and expose its all module
06:13:35	<albet70>	in python, pip could install package, and you can in python repl to it
06:13:44	<Axman6>	We've literally spent the last 15 years trying to get away from all the problems that doing that introduces
06:14:19	×	jinsun quits (~jinsun@user/jinsun) ()
06:15:40	→	jinsun joins (~jinsun@user/jinsun)
06:18:41	×	slim quits (uid300876@id-300876.lymington.irccloud.com) (Quit: Connection closed for inactivity)
06:18:46	<abastro>	I mean, for scripting you don't want to have .cabal file
06:19:17	<abastro>	`cabal v1-install` was basically what pip was doing, but it ended up being problematic
06:19:22	<Axman6>	exactly, which is why cabal v2-run specifically lets you embed the necessary parts of one into your .hs file
06:19:33	<abastro>	Oh, so you can embed in .hs?
06:19:42	<Axman6>	yes, that's why I linked to it
06:19:46	<abastro>	Well tell us how
06:19:48	<abastro>	Oh?
06:19:56	×	Macbethwin quits (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection)
06:20:18	→	Macbethwin joins (~chargen@D964062A.static.ziggozakelijk.nl)
06:20:20	<Axman6>	"is https://cabal.readthedocs.io/en/3.6/cabal-commands.html?highlight=run#cabal-v2-run helpful?" 15 minutes ago
06:20:41	<abastro>	`#!/usr/bin/env cabal
06:20:43	<abastro>	{- cabal:
06:20:44	<abastro>	build-depends: base ^>= 4.11
06:20:44	<abastro>	, shelly ^>= 1.8.1
06:20:45	<abastro>	-}
06:20:45	<abastro>	main :: IO ()
06:20:46	<abastro>	main = do
06:20:47	<abastro>	...`
06:20:50	<abastro>	So that is it
06:21:21	×	Macbethwin quits (~chargen@D964062A.static.ziggozakelijk.nl) (Remote host closed the connection)
06:23:42	×	xff0x quits (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds)
06:24:04	→	odnes joins (~odnes@5-203-245-187.pat.nym.cosmote.net)
06:24:58	×	dschrempf quits (~dominik@mobiledyn-62-240-134-186.mrsn.at) (Quit: WeeChat 3.4.1)
06:25:46	→	xff0x joins (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp)
06:29:31	<albet70>	I found the way, just cabal v2-install --lib xlsx, now ghci can directly use it...
06:30:42	→	mattil joins (~mattil@d5z9ccdfmyl1jmjj16z-4.rev.dnainternet.fi)
06:30:47	→	gehmehgeh joins (~user@user/gehmehgeh)
06:32:18	<albet70>	cabal v2-install --lib lens, now runghc can use it directly
06:32:49	→	michalz joins (~michalz@185.246.204.61)
06:33:11	→	jgeerds joins (~jgeerds@d5364b87.access.ecotel.net)
06:33:42	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
06:34:15	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
06:38:16	→	mncheck joins (~mncheck@193.224.205.254)
06:38:33	→	acidjnk joins (~acidjnk@p200300d0c7049f94683de86d14f3245b.dip0.t-ipconnect.de)
06:39:14	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
06:40:16	×	phma quits (~phma@host-67-44-208-132.hnremote.net) (Read error: Connection reset by peer)
06:41:29	→	phma joins (phma@2001:5b0:211c:8dc8:4016:a5c0:9e05:5df9)
06:41:45	<abastro>	Wait, that's def strange
06:41:53	<abastro>	Didn't you use `cabal install --lib` before?
06:45:48	<albet70>	"abastro :Didn't you use `cabal install --lib` before?", no, so I can just use cabal install --lib to do the same?
06:48:21	×	mattil quits (~mattil@d5z9ccdfmyl1jmjj16z-4.rev.dnainternet.fi) (Remote host closed the connection)
06:49:23	→	machinedgod joins (~machinedg@24.105.81.50)
06:50:45	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
06:52:00	<abastro>	Yep, it's the same
06:52:08	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
06:52:13	<abastro>	`v2-install == install` for newest versions of cabal
06:52:43	<albet70>	ok
06:52:53	<abastro>	I heard that `cabal install --lib` is supposed to be only used for experienced ppl though.
06:53:19	<albet70>	cabal v1-install is available?
06:53:36	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
06:54:45	<tomsmeding>	yes, but use is discouraged -- if there is something you really can only do through the v1- commands, you should open an issue on the cabal repo and describe your use case
06:58:43	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
07:00:36	→	lortabac joins (~lortabac@2a01:e0a:541:b8f0:3685:42fa:d9de:143d)
07:00:54	→	ph88 joins (~ph88@2a02:8109:9e00:71d0:8958:bc94:e84c:ec28)
07:02:14	→	cfricke joins (~cfricke@user/cfricke)
07:02:19	→	alp joins (~alp@user/alp)
07:03:17	→	briandaed joins (~root@109.95.142.93.r.toneticgroup.pl)
07:03:18	<abastro>	I recall massively being confused by `v1-build` `v1-install` etc. tbh
07:04:38	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
07:09:32	→	mc47 joins (~mc47@xmonad/TheMC47)
07:11:03	→	ProfSimm joins (~ProfSimm@87.227.196.109)
07:11:26	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds)
07:12:43	×	Akiva quits (~Akiva@user/Akiva) (Ping timeout: 256 seconds)
07:15:28	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
07:15:29	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
07:15:45	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
07:15:54	×	mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection)
07:19:39	×	Inst quits (~Liam@2601:6c4:4080:3f80:8562:905a:59dc:27e9) (Quit: Leaving)
07:28:10	×	mcglk quits (~mcglk@131.191.49.120) (Read error: Connection reset by peer)
07:29:09	→	mcglk joins (~mcglk@131.191.49.120)
07:30:13	×	xff0x quits (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds)
07:31:50	→	mikoto-c1 joins (~mikoto-ch@213.177.151.239)
07:31:52	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 272 seconds)
07:34:12	→	vpan joins (~0@212.117.1.172)
07:34:16	→	merijn joins (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl)
07:34:33	→	xff0x joins (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp)
07:34:39	<jackdk>	Question: Given a finite type `t` (easy mode: Bounded and Enum instances; hard mode: Finite instance), is there a library which maps it to a representable functor `f` such that `Rep f ~ t`?
07:39:07	×	merijn quits (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
07:42:23	×	Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
07:42:23	×	mikoto-c1 quits (~mikoto-ch@213.177.151.239) (Read error: Connection reset by peer)
07:45:11	×	acidjnk quits (~acidjnk@p200300d0c7049f94683de86d14f3245b.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
07:45:44	→	merijn joins (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl)
07:48:07	→	mikoto-c1 joins (~mikoto-ch@213.177.151.239)
07:49:01	×	ph88 quits (~ph88@2a02:8109:9e00:71d0:8958:bc94:e84c:ec28) (Ping timeout: 240 seconds)
07:54:32	→	jinsun__ joins (~jinsun@user/jinsun)
07:54:32	jinsun	is now known as Guest3467
07:54:33	jinsun__	is now known as jinsun
07:54:52	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
07:58:28	×	Guest3467 quits (~jinsun@user/jinsun) (Ping timeout: 272 seconds)
08:02:14	→	dsrt^ joins (~dsrt@c-24-99-107-170.hsd1.ga.comcast.net)
08:08:58	→	Digit joins (~user@user/digit)
08:09:09	×	Unhammer quits (~Unhammer@user/unhammer) (Read error: Connection reset by peer)
08:14:06	×	megaTherion quits (~therion@unix.io) (Ping timeout: 245 seconds)
08:14:20	→	ccntrq joins (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b)
08:16:35	×	chenqisu1 quits (~chenqisu1@183.217.200.168) (Quit: Leaving)
08:18:14	×	coot quits (~coot@213.134.190.95) (Quit: coot)
08:19:18	→	ph88 joins (~ph88@213.23.78.154)
08:19:28	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
08:25:37	×	ix quits (~ix@2a02:8010:674f:0:d65d:64ff:fe52:5efe) (Remote host closed the connection)
08:25:46	→	ix joins (~ix@2a02:8010:674f:0:d65d:64ff:fe52:5efe)
08:26:11	→	Unhammer joins (~Unhammer@user/unhammer)
08:27:23	×	mixfix41 quits (~homefame@user/mixfix41) (Ping timeout: 260 seconds)
08:28:46	<tomsmeding>	jackdk: are you talking about adjunctions:Data.Functor.Rep.Representable?
08:29:50	→	ProfSimm joins (~ProfSimm@87.227.196.109)
08:30:50	→	mc47 joins (~mc47@xmonad/TheMC47)
08:31:30	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
08:32:42	→	Pickchea joins (~private@user/pickchea)
08:36:38	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
08:37:01	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
08:38:48	×	belphegor666 quits (~satan@user/belphegor666) (Quit: WeeChat 3.4)
08:39:08	→	belphegor666 joins (~satan@ip-046-223-003-068.um13.pools.vodafone-ip.de)
08:40:09	×	Neuromancer quits (~Neuromanc@user/neuromancer) (Ping timeout: 250 seconds)
08:41:32	×	jinsun quits (~jinsun@user/jinsun) (Ping timeout: 272 seconds)
08:42:07	×	abastro quits (~abab9579@220.75.216.63) (Ping timeout: 260 seconds)
08:45:14	×	kaph quits (~kaph@net-93-67-57-97.cust.vodafonedsl.it) (Read error: Connection reset by peer)
08:45:40	×	belphegor666 quits (~satan@ip-046-223-003-068.um13.pools.vodafone-ip.de) (Changing host)
08:45:40	→	belphegor666 joins (~satan@user/belphegor666)
08:50:59	→	dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be)
08:55:59	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
08:56:46	×	tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz)
08:57:30	×	lispy quits (~lispy@82.212.115.165) (Quit: Client closed)
09:00:05	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:193d:75d8:745d:e91e)
09:00:32	×	Typedfern quits (~Typedfern@73.red-83-57-140.dynamicip.rima-tde.net) (Ping timeout: 272 seconds)
09:00:38	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
09:10:26	→	coot joins (~coot@213.134.190.95)
09:13:33	→	Typedfern joins (~Typedfern@13.red-88-16-189.dynamicip.rima-tde.net)
09:22:45	→	deadmarshal_ joins (~deadmarsh@95.38.118.110)
09:24:30	→	mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
09:28:41	→	megaTherion joins (~therion@unix.io)
09:28:47	×	mikoto-c1 quits (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds)
09:31:05	×	deadmarshal_ quits (~deadmarsh@95.38.118.110) (Ping timeout: 246 seconds)
09:32:02	→	deadmarshal_ joins (~deadmarsh@95.38.119.22)
09:32:56	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
09:36:11	→	mikoto-c1 joins (~mikoto-ch@213.177.151.239)
09:42:33	×	jgeerds quits (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 256 seconds)
09:44:15	×	azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds)
09:47:59	→	azimut joins (~azimut@gateway/tor-sasl/azimut)
09:49:14	→	acidjnk joins (~acidjnk@p200300d0c7049f94699c2b11d21dc0a3.dip0.t-ipconnect.de)
09:52:13	×	econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity)
09:52:19	×	mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection)
09:52:45	<tomsmeding>	jackdk: apparently you can! https://paste.tomsmeding.com/WQYUUcfP
09:52:50	<tomsmeding>	this was actually pretty fun
09:55:29	→	whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com)
09:57:41	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
09:58:50	×	mikoto-c1 quits (~mikoto-ch@213.177.151.239) (Quit: mikoto-c1)
09:59:03	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
10:02:14	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds)
10:06:56	→	madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net)
10:07:50	×	xff0x quits (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds)
10:09:48	→	Unicorn_Princess joins (~Unicorn_P@93-103-228-248.dynamic.t-2.net)
10:09:52	→	xff0x joins (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp)
10:10:09	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
10:11:28	→	kuribas joins (~user@ptr-25vy0i9ukrx95drquaj.18120a2.ip6.access.telenet.be)
10:12:13	→	ProfSimm joins (~ProfSimm@87.227.196.109)
10:13:00	→	cosimone joins (~user@93-47-230-184.ip115.fastwebnet.it)
10:15:54	→	kjak joins (~kjak@pool-108-45-56-21.washdc.fios.verizon.net)
10:16:16	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
10:16:49	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
10:18:13	×	xff0x quits (~xff0x@125x102x200x106.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds)
10:23:23	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
10:28:12	<jackdk>	tomsmeding: yeah Representable. Cool trick. I wish https://hackage.haskell.org/package/universe-1.2.2/docs/Data-Universe.html#t:Finite had a type family so you can get its cardinality at the type level =/
10:32:22	×	Pickchea quits (~private@user/pickchea) (Ping timeout: 272 seconds)
10:34:59	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
10:35:36	<tomsmeding>	jackdk: ah, that Finite. Yeah, my code should be easily adaptable to use Finite instead of Enum+Bounded
10:36:56	<jackdk>	Even using representable would be a bit much for my colleagues, let alone that pastebin. But it's very cool that you can do that.
10:36:59	<tomsmeding>	perhaps Finite doesn't include the cardinality on the type level because that grows super quickly sometimes? I needed to raise type checker reduction limits to get it to typecheck my 256-element type, so what about Set (Set Int) ?
10:37:12	<tomsmeding>	heh
10:38:13	×	rembo10 quits (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in)
10:38:23	<jackdk>	I don't know what back GHC's Nat or whether you could cook something up without needing induction
10:39:06	→	rembo10 joins (~rembo10@main.remulis.com)
10:39:33	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
10:41:31	<tomsmeding>	jackdk: I can't even write the Distributive (NProduct (n + 1)) instance with GHC Nats because that instance head itself doesn't even typecheck
10:41:39	<tomsmeding>	"Illegal type synonym family application ‘n + 1’ in instance:"
10:41:44	<jackdk>	lame
10:42:12	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Read error: No route to host)
10:42:37	<tomsmeding>	I really don't understand why the ghc nats are like this, what are you even supposed to do with type-level naturals if you can't do induction on them
10:42:47	<tomsmeding>	everything you do on the type level is based on induction
10:43:08	<c_wraith>	what GHC's type-level nats have is fast computation. relatively.
10:43:12	<c_wraith>	they lack everything else
10:43:15	<tomsmeding>	right
10:43:22	<tomsmeding>	as in, constant-time computation?
10:43:41	<c_wraith>	I suppose so, as they're fixed size.
10:43:49	<c_wraith>	they're just Int internally
10:43:58	<tomsmeding>	this is fixed size as well https://github.com/AccelerateHS/accelerate/blob/master/src/Data/Array/Accelerate/AST/Idx.hs#L75-L92
10:44:17	<tomsmeding>	though fair, these are not type-level nats
10:44:26	×	MajorBiscuit quits (~MajorBisc@2a02:a461:129d:1:193d:75d8:745d:e91e) (Quit: WeeChat 3.4)
10:44:28	<tomsmeding>	but I wonder whether an analogous trick would be possible
10:44:53	<c_wraith>	but it's worth note that there are ghc plugins that connect up an SMT solver to calculations on Nat
10:45:18	<c_wraith>	and that's a thing that makes sense to not be part of mainline GHC
10:45:38	<tomsmeding>	c_wraith: how would I then write this? instance Distributive (NProduct n) => Distributive (NProduct ('S n)) where
10:45:41	<tomsmeding>	right
10:45:51	<tomsmeding>	use (n - 1) in the context?
10:46:16	<abastro[m]>	Create peano number datatype?
10:46:21	<tomsmeding>	abastro[m]: I did lol
10:46:27	<c_wraith>	that use of 'S looks like a peano number already
10:46:36	<tomsmeding>	c_wraith: it is, it is line 101 of https://paste.tomsmeding.com/WQYUUcfP
10:46:42	<Hecate>	< janus> Hecate: when i search for 'test' on hackage, i get lots of stuff, but on flora i get nothing // yes, it's a dev instance, only ~40 packages are imported
10:46:58	<Hecate>	< Axman6> Hecate: is flora supposed to link to module documentation? I'm not seeing anything? // nope, that's one of the UI elements that's not finished yet
10:46:59	<tomsmeding>	point is that I had to write my own peano numbers and couldn't use ghc nats, because one can't do induction over ghc nats
10:47:07	<Hecate>	< Axman6> Hecate: I find it a bit odd that the search field disappears on some page // yes it is
10:47:53	<tomsmeding>	c_wraith: (um, line 96, but you figured that out already)
10:47:56	<Hecate>	< sm> well I did install postgres just to try out a random FOSS project. // I think some paths are hardcoded in the generated cpp, that's why I stopped vendoring it. Which OS do you use?
10:48:11	<c_wraith>	tomsmeding: no I didn't! I've been awake too many hours in a row. :)
10:48:19	<tomsmeding>	:p
10:49:28	←	jakalx parts (~jakalx@base.jakalx.net) (Error from remote client)
10:50:22	<c_wraith>	yeah, if you had a solver working on it, you'd just say that the instance for (n-1) exists
10:50:34	<tomsmeding>	right
10:51:16	<tomsmeding>	I also do induction over the type-level nats on the value level (using a manual singleton here), e.g. on lines 104--113
10:51:27	×	perrierjouet quits (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 3.4.1)
10:51:41	<c_wraith>	yeah.. I didn't read the code, but that's the only reason to define SNat
10:51:45	<tomsmeding>	I find it hard to see how an SMT-based type checker plugin would provide something like that
10:51:48	<tomsmeding>	yeah
10:51:54	→	perrierjouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca)
10:52:00	<tomsmeding>	but you can't define SNat usefully with ghc nats!!!!
10:52:12	→	jakalx joins (~jakalx@base.jakalx.net)
10:52:17	<tomsmeding>	but maybe I'm missing some of the magic possible with type checker plugins
10:52:22	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
10:53:05	<abastro[m]>	Well you can convert typelevel Nat to your peano type using typefamily :P
10:54:04	<tomsmeding>	right, and the sensibility of that type family would then be checked by the tc plugin presumably (because you currently can't define such a type family)
10:54:13	<c_wraith>	I think the type plugin can just synthesize a KnownNat instance wherever it can calculate one.
10:54:29	<c_wraith>	So you just do your calculations at the type level then reflect down to the value level
10:54:44	<c_wraith>	it all turns into passing Int values around after compilation
10:54:46	<tomsmeding>	type family Conv (n :: TypeNats.Nat) :: Nat where Conv 0 = 'Z ; Conv n = 'S (Conv (n - 1))
10:55:24	<tomsmeding>	maybe I should try playing with ghc nats again with that plugin
10:56:23	→	jgeerds joins (~jgeerds@d5364b87.access.ecotel.net)
10:57:15	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
10:58:52	→	__monty__ joins (~toonn@user/toonn)
11:02:06	→	comerijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
11:03:31	×	merijn quits (~merijn@c-001-002-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
11:04:06	<abastro[m]>	I thought you could indeed define such type family..
11:04:29	→	Benzi-Junior joins (~BenziJuni@dsl-149-64-179.hive.is)
11:04:41	<abastro[m]>	Requires UndecidableInstances but it worked iirc
11:06:20	×	phma quits (phma@2001:5b0:211c:8dc8:4016:a5c0:9e05:5df9) (Read error: Connection reset by peer)
11:06:38	×	comerijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 246 seconds)
11:07:13	→	Guest\|68 joins (~Guest\|68@88.223.202.146)
11:07:29	→	phma joins (phma@2001:5b0:211f:57f8:a451:bb44:e55e:abda)
11:08:06	×	Guest\|68 quits (~Guest\|68@88.223.202.146) (Client Quit)
11:09:25	<tomsmeding>	right, you can define the type family, but you can't use it
11:09:29	<tomsmeding>	or, usefully use it
11:09:42	<tomsmeding>	but perhaps that is indeed solved by some magic KnownNat dicts being generated
11:14:16	<abastro[m]>	You cannot hsefully use it? Hmm
11:17:42	×	ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
11:18:07	→	ChaiTRex joins (~ChaiTRex@user/chaitrex)
11:21:35	<Hecate>	2
11:21:37	<Hecate>	(woops)
11:35:11	→	dcoutts joins (~duncan@host213-122-143-81.range213-122.btcentralplus.com)
11:37:33	×	dcoutts__ quits (~duncan@host109-149-1-229.range109-149.btcentralplus.com) (Ping timeout: 260 seconds)
11:39:14	→	xff0x joins (~xff0x@i121-117-52-147.s41.a013.ap.plala.or.jp)
11:40:03	←	jakalx parts (~jakalx@base.jakalx.net) (Error from remote client)
11:40:35	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds)
11:41:47	×	mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 260 seconds)
11:42:57	×	pavonia quits (~user@user/siracusa) (Quit: Bye!)
11:46:04	→	jakalx joins (~jakalx@base.jakalx.net)
11:49:39	→	ProfSimm joins (~ProfSimm@87.227.196.109)
11:53:32	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
11:53:35	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
11:54:04	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
11:55:07	<tomsmeding>	> join (.) (ap (.)) (const id) (+1) 0
11:55:10	<lambdabot>	2
11:58:19	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
11:58:48	<maerwald[m]>	tomsmeding: did you calculate that in your head?
11:59:13	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
11:59:27	×	alp quits (~alp@user/alp) (Remote host closed the connection)
11:59:38	×	frost quits (~frost@user/frost) (Quit: Client closed)
11:59:48	→	alp joins (~alp@user/alp)
12:00:06	→	frost joins (~frost@user/frost)
12:02:04	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
12:02:42	<tomsmeding>	no lol, made good use of pointfree.io
12:02:47	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
12:03:13	<boxscape>	@unpl join (.) (ap (.)) (const id)
12:03:13	<lambdabot>	(\ b0 x -> b0 (b0 x)) (\ m2 b0 -> (m2 >>= \ x2 -> return (\ x -> b0 (x2 x))) b0) (\ _ x -> x)
12:03:14	<tomsmeding>	'const id' is church encoded zero, 'ap (.)' is church encoded one, 'join (.)' applies twice
12:03:18	<tomsmeding>	useful!
12:03:36	<tomsmeding>	:t ap (.)
12:03:37	<lambdabot>	((b -> c) -> a -> b) -> (b -> c) -> a -> c
12:04:12	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Read error: Connection reset by peer)
12:04:16	<int-e>	W B (S B) (K I) <-- hmm, that doesn't help as much as I thought it would.
12:04:23	<tomsmeding>	@pl \f s z -> s (f s z)
12:04:23	<lambdabot>	ap (.)
12:04:27	×	elkcl quits (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 250 seconds)
12:04:49	<maerwald[m]>	tomsmeding: there should be a "swear jar" for this. Please pay up ;)
12:05:57	<tomsmeding>	what, because fsz sfsz sounds like a slavic swearword?
12:06:45	<maerwald[m]>	tomsmeding: no, for aggressive obfuscation :p
12:07:32	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
12:07:42	<maerwald[m]>	My guess is that's why perl died out. People just went broke
12:08:08	→	abastro joins (~abab9579@220.75.216.63)
12:08:10	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Read error: Connection reset by peer)
12:08:10	<int-e>	:t const id
12:08:11	<lambdabot>	b -> a -> a
12:08:35	<tomsmeding>	:t flip const
12:08:36	<lambdabot>	b -> c -> c
12:08:49	<int-e>	:t ap (.) :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
12:08:50	<lambdabot>	((a -> a) -> a -> a) -> (a -> a) -> a -> a
12:08:53	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
12:09:31	<int-e>	> let zero' = const id; succ' = ap (.) in map (\n -> n succ 0) (iterate succ zero)
12:09:32	<lambdabot>	error:
12:09:32	<lambdabot>	• Variable not in scope: zero :: (a0 -> a0) -> t0 -> b
12:09:32	<lambdabot>	• Perhaps you meant one of these:
12:09:39	<int-e>	> let zero' = const id; succ' = ap (.) in map (\n -> n succ 0) (iterate succ' zero')
12:09:40	<lambdabot>	[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2...
12:10:04	<maerwald[m]>	See what you did...
12:10:27	<int-e>	it's a Church thing
12:10:55	<geekosaur>	did that middle succ want to be succ' ?
12:11:08	→	ProfSimm joins (~ProfSimm@87.227.196.109)
12:11:27	<tomsmeding>	> map (flip uncurry (succ, 0)) (iterate (ap (.)) (const id))
12:11:28	<lambdabot>	[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2...
12:11:47	<int-e>	geekosaur: no, \n -> n succ 0 evaluates a Church numeral to a number
12:11:49	×	tabemann quits (~travisb@2600:1700:7990:24e0:3f89:422:8b05:c533) (Remote host closed the connection)
12:11:55	×	acidjnk quits (~acidjnk@p200300d0c7049f94699c2b11d21dc0a3.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
12:12:08	→	tabemann joins (~travisb@2600:1700:7990:24e0:77bc:a0c0:b3f2:8f7c)
12:13:15	<int-e>	I also went off exploring on myself so I missed tomsmeding's explanation (it's the successor function though, not 1)
12:13:50	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
12:13:53	<tomsmeding>	oh hah yes
12:13:57	<int-e>	*on my own
12:14:12	<tomsmeding>	in my defence, if I didn't know that, I wouldn't have succeeded in writing the obfuscated form
12:14:33	<int-e>	tomsmeding: sure. I'm familiar with errors introduced between brain and keyboard :)
12:18:37	<tomsmeding>	> map (flip uncurry (intersperse 'o', "cl")) (iterate (ap (.)) (const id))
12:18:39	<lambdabot>	["cl","col","coool","coooooool","coooooooooooooool","coooooooooooooooooooooo...
12:21:28	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
12:23:25	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
12:26:03	×	ph88 quits (~ph88@213.23.78.154) (Quit: Leaving)
12:31:07	→	fef joins (~thedawn@user/thedawn)
12:34:31	×	dcoutts quits (~duncan@host213-122-143-81.range213-122.btcentralplus.com) (Ping timeout: 260 seconds)
12:39:22	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
12:43:06	×	mncheck quits (~mncheck@193.224.205.254) (Remote host closed the connection)
12:43:20	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
12:44:13	×	ccntrq quits (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) (Remote host closed the connection)
12:44:31	→	ccntrq joins (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b)
12:48:43	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds)
12:49:38	→	mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
12:51:15	→	ProfSimm joins (~ProfSimm@87.227.196.109)
12:53:00	→	MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net)
12:53:10	→	mncheck joins (~mncheck@193.224.205.254)
12:59:23	→	acidjnk joins (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de)
13:03:23	×	vysn quits (~vysn@user/vysn) (Remote host closed the connection)
13:06:50	×	frost quits (~frost@user/frost) (Ping timeout: 250 seconds)
13:07:35	×	littlebobeep quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
13:08:08	×	Andrew quits (Andrew@user/AndrewYu) (Quit: Leaving)
13:08:39	→	jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
13:09:28	→	Andrew joins (~andrew@user/AndrewYu)
13:10:28	<albet70>	what's Nat?
13:11:02	<albet70>	also Void and Const type
13:11:40	<geekosaur>	Nat is type level natural (that is, non-negative) numbers
13:11:54	<geekosaur>	Void is the empty type (has no values)
13:11:55	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
13:12:27	<geekosaur>	Const is const lifted to type level: the type of (Const Foo Bar) is Bar
13:13:34	→	xkuru joins (~xkuru@user/xkuru)
13:15:09	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
13:16:57	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
13:17:05	<albet70>	no value has Void type, what's its purpose
13:17:30	<tdammers>	the purpose of Void is to indicate that no value of that type can ever exist
13:17:42	<albet70>	Const A B is B, is redundant?
13:17:58	<tdammers>	for example, [Void] implies that it has to be an empty list, because there are no values that you could put into such a list
13:18:12	<tdammers>	well, or a list that remains thunked forever
13:18:47	<maerwald>	that's a tough fate
13:19:00	<tdammers>	poor lits
13:19:02	<tdammers>	list*
13:19:05	×	dsrt^ quits (~dsrt@c-24-99-107-170.hsd1.ga.comcast.net) (Remote host closed the connection)
13:20:03	×	wardrunal quits (~goose@167.179.114.36) (Quit: Leaving)
13:20:50	×	MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 272 seconds)
13:22:51	<albet70>	and Constant type?
13:24:12	<tdammers>	basically "glue" - just like value-level const allows you to ignore an argument, and thus use a function b -> c in a context where a -> b -> c is demanded, Const allows you to ignore a type argument, and use a type of kind * -> * where one of kind * -> * -> * is demanded.
13:26:40	<abastro>	Const is useful for composition and phantom tricks, iirc
13:27:15	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
13:29:16	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
13:30:19	×	briandaed quits (~root@109.95.142.93.r.toneticgroup.pl) (Remote host closed the connection)
13:31:19	→	littlebobeep joins (~alMalsamo@gateway/tor-sasl/almalsamo)
13:31:41	×	odnes quits (~odnes@5-203-245-187.pat.nym.cosmote.net) (Quit: Leaving)
13:32:02	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48)
13:32:28	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 260 seconds)
13:34:07	→	mikoto-chan joins (~mikoto-ch@213.177.151.239)
13:37:56	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
13:39:39	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
13:40:03	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
13:40:17	→	ProfSimm joins (~ProfSimm@87.227.196.109)
13:41:21	→	wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com)
13:41:21	×	wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host)
13:41:21	→	wroathe joins (~wroathe@user/wroathe)
13:41:55	×	hololeap quits (~hololeap@user/hololeap) (Quit: Bye)
13:42:22	→	elkcl joins (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru)
13:43:22	→	shriekingnoise joins (~shrieking@201.231.16.156)
13:47:23	×	MajorBiscuit quits (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 250 seconds)
13:50:32	→	Pickchea joins (~private@user/pickchea)
13:51:21	×	Hash quits (~Hash@hey.howstoned.ru) (Quit: ZNC - https://znc.in)
13:53:28	×	mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 260 seconds)
13:53:51	×	alp quits (~alp@user/alp) (Ping timeout: 260 seconds)
13:55:10	→	Hash joins (~Hash@hey.howstoned.ru)
13:55:15	×	vicfred quits (~vicfred@user/vicfred) (Quit: Leaving)
13:55:39	×	geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving)
13:56:11	×	APic quits (apic@apic.name) (Quit: [TLS] Client upgrade)
13:56:24	→	APic joins (apic@apic.name)
13:56:42	<napping>	If you are using a GADT to define a subset type, like a (Term hasVars) with a constructor Var :: .. -> Term Open and everything else returns a Term hasVars so you know a Term Closed has no Var, is there a way to weaken Term Closed to Term Open without traversing the data, besides unsafeCoerce?
13:56:53	→	geekosaur joins (~geekosaur@xmonad/geekosaur)
13:57:40	×	codedmart quits (~codedmart@li335-49.members.linode.com) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
13:58:13	×	acidjnk quits (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) (Ping timeout: 250 seconds)
13:58:31	<merijn>	:t absurd
13:58:32	<lambdabot>	Void -> a
13:58:39	<merijn>	Some form of fmap + absurd?
13:59:28	→	kaph joins (~kaph@net-93-67-57-97.cust.vodafonedsl.it)
14:00:10	→	codedmart joins (codedmart@2600:3c01::f03c:92ff:fefe:8511)
14:00:25	<napping>	But fmap walks the term, no?
14:00:28	<int-e>	Probably not, because Haskell's type system doesn't track variance of type arguments, so the compiler can't be convinced that coercing is safe.
14:02:49	→	briandaed joins (~root@109.95.142.93.r.toneticgroup.pl)
14:05:29	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds)
14:05:35	×	littlebobeep quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
14:05:49	<int-e>	For this GADT you can easily break it by adding an extra constructor (producing a Term Closed), again something that isn't tracked in the type system.
14:12:54	→	cosimone` joins (~user@93-47-230-184.ip115.fastwebnet.it)
14:14:38	×	lortabac quits (~lortabac@2a01:e0a:541:b8f0:3685:42fa:d9de:143d) (Quit: WeeChat 2.8)
14:14:51	×	cosimone quits (~user@93-47-230-184.ip115.fastwebnet.it) (Ping timeout: 260 seconds)
14:15:28	<napping>	I guess I'll just have to check how much it gets in the way of optimizations
14:17:26	→	Akiva joins (~Akiva@user/Akiva)
14:17:57	×	Hash quits (~Hash@hey.howstoned.ru) (Quit: ZNC - https://znc.in)
14:18:37	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
14:20:44	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
14:21:42	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48)
14:21:50	→	dcoutts joins (~duncan@host213-122-143-81.range213-122.btcentralplus.com)
14:23:19	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
14:29:58	→	tiferrei2000 joins (~tiferrei@user/tiferrei)
14:30:55	×	tiferrei quits (~tiferrei@user/tiferrei) (Ping timeout: 240 seconds)
14:31:58	×	vpan quits (~0@212.117.1.172) (Quit: Leaving.)
14:33:42	→	[itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
14:36:26	→	Hash joins (~Hash@hey.howstoned.ru)
14:36:27	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
14:36:38	×	Pickchea quits (~private@user/pickchea) (Ping timeout: 252 seconds)
14:43:18	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
14:43:47	×	Hash quits (~Hash@hey.howstoned.ru) (Ping timeout: 260 seconds)
14:45:03	→	zebrag joins (~chris@user/zebrag)
14:47:35	<kuribas>	albet70: Void is used for example by the generics-eot library. Since it corresponds to zero, it is the identity element of sum types (Either).
14:47:50	×	cosimone` quits (~user@93-47-230-184.ip115.fastwebnet.it) (Ping timeout: 246 seconds)
14:47:59	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
14:48:48	×	lyxia quits (~lyxia@poisson.chat) (Quit: WeeChat 3.3)
14:49:05	<kuribas>	albet70: x + 0 = x "Either x Void" is isomorphic to x"
14:49:52	×	APic quits (apic@apic.name) (Remote host closed the connection)
14:51:30	×	cdman quits (~dcm@user/dmc/x-4369397) (Quit: Leaving)
14:51:38	×	codedmart quits (codedmart@2600:3c01::f03c:92ff:fefe:8511) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
14:51:38	<kuribas>	likewise, unit () is the identity element of product types, since (x, ()) ~= x
14:51:49	<kuribas>	unit corresponds to 1, 1 * x = x
14:51:59	→	codedmart joins (codedmart@2600:3c01::f03c:92ff:fefe:8511)
14:54:59	×	MajorBiscuit quits (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 260 seconds)
14:56:41	×	ccntrq quits (~Thunderbi@2a01:c22:88e7:1b00:3fae:5eb6:677d:a5b) (Remote host closed the connection)
14:56:46	×	Andrew quits (~andrew@user/AndrewYu) (Quit: identd is broken)
14:57:36	×	cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.4.1)
14:57:38	→	Andrew joins (Andrew@user/AndrewYu)
15:00:18	→	acidjnk joins (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de)
15:00:40	→	Hash joins (~Hash@hey.howstoned.ru)
15:00:45	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
15:01:34	→	cfricke joins (~cfricke@user/cfricke)
15:02:53	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 246 seconds)
15:03:04	×	Hash quits (~Hash@hey.howstoned.ru) (Max SendQ exceeded)
15:03:40	×	zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection)
15:04:29	<kuribas>	albet70: so you can think of sum types as a (type level) fold over a list of types, using Either and Void.
15:04:42	<kuribas>	albet70: and product types over (,) and ()
15:04:54	→	cosimone` joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20)
15:05:08	→	Hash joins (~Hash@hey.howstoned.ru)
15:05:20	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds)
15:05:57	→	lyxia joins (~lyxia@poisson.chat)
15:06:31	<kuribas>	albet70: for example, in idris:
15:06:37	<kuribas>	(foldr Either Void (the (List Type) [Int, String])) => Either Int (Either String Void)
15:07:00	→	Sgeo joins (~Sgeo@user/sgeo)
15:07:06	<kuribas>	(foldr (,) () (the (List Type) [Int, String])) => (Int, (String, ()))
15:07:52	→	justsomeguy joins (~justsomeg@user/justsomeguy)
15:08:33	×	Hash quits (~Hash@hey.howstoned.ru) (Max SendQ exceeded)
15:09:54	→	o-90 joins (~o-90@gateway/tor-sasl/o-90)
15:10:18	<abastro>	Utilizing haskell to memorize manifold analysis: https://paste.tomsmeding.com/NtB6x6VI
15:10:38	<abastro>	(Wait, does this ping tomsmed)
15:11:17	→	Hash joins (~Hash@hey.howstoned.ru)
15:12:28	×	o-90 quits (~o-90@gateway/tor-sasl/o-90) (Remote host closed the connection)
15:12:35	<geekosaur>	his client does regex matching, so I wrote him a custom matching regex that ignores paste urls
15:12:48	×	cosimone` quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Ping timeout: 260 seconds)
15:13:12	×	cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.4.1)
15:14:22	×	Hash quits (~Hash@hey.howstoned.ru) (Max SendQ exceeded)
15:16:28	→	Hash joins (~Hash@hey.howstoned.ru)
15:17:29	×	fryguybob quits (~fryguybob@cpe-74-67-169-145.rochester.res.rr.com) (Quit: leaving)
15:19:09	×	coot quits (~coot@213.134.190.95) (Quit: coot)
15:19:26	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
15:20:34	<abastro>	Oh, that's relieving
15:20:51	→	MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net)
15:21:03	×	MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Client Quit)
15:22:20	<geekosaur>	(and will ignore play when that comes online)
15:23:12	×	Hash quits (~Hash@hey.howstoned.ru) (Max SendQ exceeded)
15:24:31	→	Hash joins (~Hash@hey.howstoned.ru)
15:24:36	→	alp joins (~alp@user/alp)
15:26:14	×	abastro quits (~abab9579@220.75.216.63) (Ping timeout: 272 seconds)
15:28:38	×	Hash quits (~Hash@hey.howstoned.ru) (Remote host closed the connection)
15:29:04	→	fizbin_ joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
15:29:42	→	Hash joins (~Hash@hey.howstoned.ru)
15:30:50	→	APic joins (apic@apic.name)
15:31:03	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
15:31:23	×	deadmarshal_ quits (~deadmarsh@95.38.119.22) (Ping timeout: 260 seconds)
15:32:13	×	jgeerds quits (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 240 seconds)
15:32:38	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 246 seconds)
15:35:10	×	Hash quits (~Hash@hey.howstoned.ru) (Max SendQ exceeded)
15:35:44	→	Hash joins (~Hash@hey.howstoned.ru)
15:37:38	×	doyougnu quits (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 272 seconds)
15:37:51	×	dispater quits (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
15:37:51	×	orcus quits (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in)
15:40:59	×	Hash quits (~Hash@hey.howstoned.ru) (Ping timeout: 252 seconds)
15:41:26	×	lambdabot quits (~lambdabot@haskell/bot/lambdabot) (Ping timeout: 272 seconds)
15:42:33	×	acidjnk quits (~acidjnk@p200300d0c7049f9465be138fb2fd31f4.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
15:42:53	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
15:45:14	×	mniip quits (mniip@libera/staff/mniip) (Ping timeout: 604 seconds)
15:45:15	→	Hash joins (~Hash@hey.howstoned.ru)
15:48:03	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
15:49:39	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
15:50:42	→	lambdabot joins (~lambdabot@silicon.int-e.eu)
15:50:42	×	lambdabot quits (~lambdabot@silicon.int-e.eu) (Changing host)
15:50:42	→	lambdabot joins (~lambdabot@haskell/bot/lambdabot)
15:52:04	→	dispater joins (~dispater@user/brprice)
15:52:36	→	orcus joins (~orcus@user/brprice)
15:54:15	×	dcoutts quits (~duncan@host213-122-143-81.range213-122.btcentralplus.com) (Ping timeout: 260 seconds)
15:54:32	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
15:56:36	→	zeenk joins (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94)
15:57:39	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
15:57:50	→	Vajb joins (~Vajb@85-76-32-79-nat.elisa-mobile.fi)
15:57:56	<sm>	Hecate: mac
15:58:37	→	Pickchea joins (~private@user/pickchea)
15:58:38	×	Vajb quits (~Vajb@85-76-32-79-nat.elisa-mobile.fi) (Read error: Connection reset by peer)
15:58:41	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
16:02:03	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
16:02:44	→	Guest\|66 joins (~Guest\|66@199.27.253.178)
16:02:51	→	lbseale joins (~ep1ctetus@user/ep1ctetus)
16:04:05	→	econo joins (uid147250@user/econo)
16:04:46	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
16:04:52	×	fizbin_ quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
16:04:56	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48)
16:05:39	→	mniip joins (mniip@libera/staff/mniip)
16:05:58	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
16:06:35	→	tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net)
16:07:23	→	Vajb joins (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813)
16:08:35	→	ec joins (~ec@gateway/tor-sasl/ec)
16:09:14	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
16:10:36	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
16:12:54	→	jgeerds joins (~jgeerds@d5364b87.access.ecotel.net)
16:13:06	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
16:14:39	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
16:20:06	→	zaquest joins (~notzaques@5.130.79.72)
16:22:37	→	dextaa_ joins (~dextaa@user/dextaa)
16:23:02	×	zmt00 quits (~zmt00@user/zmt00) (Read error: Connection reset by peer)
16:24:55	→	zmt00 joins (~zmt00@user/zmt00)
16:31:46	×	zeenk quits (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94) (Quit: Konversation terminated!)
16:32:37	→	waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
16:33:50	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
16:35:48	→	lackboardNB joins (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105)
16:36:11	×	lackboardNB quits (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Client Quit)
16:37:01	×	jgeerds quits (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 245 seconds)
16:39:31	→	cosimone joins (~user@93-47-230-184.ip115.fastwebnet.it)
16:41:00	×	Pickchea quits (~private@user/pickchea) (Ping timeout: 240 seconds)
16:41:23	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
16:43:20	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
16:43:34	→	slack1256 joins (~slack1256@186.11.56.117)
16:43:34	→	lackboardNB joins (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105)
16:43:55	×	lackboardNB quits (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Remote host closed the connection)
16:44:32	→	lackboardNB joins (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105)
16:45:52	×	lackboardNB quits (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Remote host closed the connection)
16:46:27	→	arjun joins (~arjun@user/arjun)
16:47:24	→	lackboardNB joins (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105)
16:47:33	<arjun>	hi, can someone tell me whats the deal with the 'forall' stuff goin here -> https://pastebin.com/iNiaTqKt
16:48:00	<arjun>	how does that imply that we cannot do anything with it and just pass it around?
16:50:57	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
16:51:39	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
16:52:22	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 272 seconds)
16:52:34	<geekosaur>	because `x` is under an inner forall, all you can do is something that will work for any type. but the only things that work for any type are passing it around and throwing an exception
16:53:36	→	justsomeguy joins (~justsomeg@user/justsomeguy)
16:54:02	→	deadmarshal_ joins (~deadmarsh@95.38.119.22)
16:54:06	×	lackboardNB quits (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Ping timeout: 245 seconds)
16:55:55	<arjun>	:ded:
16:56:26	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
16:56:35	<arjun>	and removing this inner forall would make a difference? since we have implicit foralls, or are those just for "outer" levels?
16:56:38	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
16:57:13	→	bahamas joins (~lucian@84.232.140.158)
16:57:17	<geekosaur>	just for outer, yes
16:57:37	<arjun>	also, what kind of a signature is f a -> g a ? :x or am i just too used to seeing a -> b
16:58:05	<arjun>	i mean, what would f here even be ?
16:58:07	<geekosaur>	f might be something like Maybe or []
16:58:20	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
16:58:22	<arjun>	a * -> * ? since it's a functor?
16:58:23	×	deadmarshal_ quits (~deadmarsh@95.38.119.22) (Ping timeout: 246 seconds)
16:58:26	<geekosaur>	(and [] Int is the same as [Int])
16:58:34	<geekosaur>	yes
16:58:36	<arjun>	i see
16:58:40	<arjun>	that helped
16:58:42	<arjun>	thanks man
16:59:26	→	benin joins (~benin@183.82.204.110)
16:59:32	×	benin quits (~benin@183.82.204.110) (Client Quit)
16:59:57	<arjun>	so, without the implicit forall a function [a] -> [a] would not see the 'a' on LHS is same as the 'a' on RHS ?
17:00:18	<geekosaur>	no, we know they are the same since they're the type variable
17:00:35	<geekosaur>	the question is whether you (i.e. the function) can know what that type is or not
17:00:38	→	BlackboardN joins (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105)
17:00:49	×	BlackboardN quits (~nathan@2601:602:9e00:365:6c3f:7fdf:c12d:a105) (Changing host)
17:00:49	→	BlackboardN joins (~nathan@user/BlackboardN)
17:00:52	<arjun>	should it even care?
17:01:06	<geekosaur>	in this case, no. that's kinda the point
17:01:32	<arjun>	gotch'a
17:01:48	<geekosaur>	if you knew, you could do something illegal (in this case, changing the structure of the Stream)
17:01:56	→	kor1 joins (~kor1@201.17.127.170)
17:02:11	<arjun>	how trusting
17:03:06	<arjun>	but that's an interesting, could you brief it a little more?
17:03:41	<geekosaur>	well, the whole point of having a strong type system is enforcing rather than trusting :)
17:04:02	×	kor1 quits (~kor1@201.17.127.170) (Client Quit)
17:04:13	→	kor1 joins (~kor1@user/kor1)
17:04:26	<arjun>	like, how does me knowing the type, would allow me to change the structure of the stream?
17:04:35	×	justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4)
17:04:54	<arjun>	an [Int] -> [Int] would not change it much
17:05:12	<arjun>	Maybe Int porbably could because of Nothing
17:05:19	<geekosaur>	if you know the type you can use alternative values. (I admit to being puzzled as to how this changes the structure as opposed to the content, but I don't know anyting about the Stream type beyond your paste)
17:05:40	<kuribas>	arjun: you know haskell is hiding a forall whenever there is a free type variable?
17:05:52	<kuribas>	geekosaur: could be using type families?
17:06:09	<geekosaur>	context: https://pastebin.com/iNiaTqKt
17:06:15	<arjun>	kuribas, i have a vague idea, yes
17:06:26	<kuribas>	arjun: so, "id :: a -> a" is a bit of a lie, it actually means "id :: forall a. a -> a"
17:06:26	×	Vajb quits (~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) (Read error: Connection reset by peer)
17:06:34	<arjun>	sure
17:06:34	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
17:06:52	×	kor1 quits (~kor1@user/kor1) (Client Quit)
17:07:19	→	kor1 joins (~kor1@user/kor1)
17:07:23	<kuribas>	arjun: if you take curry/howard, then the forall is just another argument. But one that takes a type.
17:08:30	<arjun>	i am not familiar with curry/howard but please continue, i'll read up on that later today
17:08:37	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds)
17:08:40	<kuribas>	arjun: each time you call the function with a forall, you are passing a type to it.
17:08:51	<kuribas>	arjun: in haskell, it is done implicitly by the type inference engine.
17:09:26	<kuribas>	with RankN, it means you can use the same function with different types.
17:09:47	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
17:09:54	<kuribas>	like (forall a.a -> a) -> (Int, String) -> (Int, String)
17:10:10	→	benin joins (~benin@183.82.204.110)
17:10:16	<kuribas>	now, the first function can be called on an Int as well as on a String.
17:10:27	<arjun>	sure, thus the type variable
17:10:42	<arjun>	which probably solidifies when we call it
17:10:46	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
17:10:54	<kuribas>	arjun: but if you write (a -> a) -> (Int, String) -> (Int, String), the "a" can be only one thing.
17:11:37	<arjun>	i SEE
17:11:49	×	kor1 quits (~kor1@user/kor1) (Ping timeout: 240 seconds)
17:12:06	<arjun>	not much of a type-variable then is it?
17:12:06	<kuribas>	With RankN, the called function has the choice to use it with another type.
17:12:16	<geekosaur>	and while it might be Int or String, you don't know the type. with the forall, the caller must pass something that will work with any type (as, without the forall, you would have to be ready to deal with any type. both modified by constraints of course)
17:12:34	→	kor1 joins (~kor1@user/kor1)
17:12:41	<kuribas>	yes
17:13:18	<kuribas>	arjun: yes, still a type variable, but the moment when it is "filled" or "passed", is different.
17:14:16	<arjun>	srry, i think i miss-understood, "but if you write (a -> a) -> (Int, String) -> (Int, String), the "a" can be only one thing"
17:14:30	<arjun>	i thought a could only be 1 type
17:14:36	<kuribas>	arjun: it can always only be one thing.
17:15:03	<arjun>	but i think you were saying, since we have a pair, the function can be one, that works on either type
17:15:17	<kuribas>	type variable always have to be applied somewhere.
17:15:30	<kuribas>	hmm gtg.
17:15:39	<kuribas>	I leave it to the other people here :)
17:15:52	<arjun>	alright, thanks for help, i'll read it back again
17:16:52	×	kor1 quits (~kor1@user/kor1) (Client Quit)
17:16:53	<geekosaur>	so the `a` always has to be one type, the question is who knows that type
17:17:05	<geekosaur>	(I admit I'm starting to skate on thin ice here)
17:17:18	→	kor1 joins (~kor1@user/kor1)
17:17:20	×	kuribas quits (~user@ptr-25vy0i9ukrx95drquaj.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3))
17:17:55	<geekosaur>	actually I think I'll withdraw too, I'm confusing myself :(
17:18:05	<arjun>	i think i did too : P
17:18:21	<arjun>	thanks for engaging : )
17:18:23	<geekosaur>	I know in practice what's going on, describing it sanely is another question…
17:18:43	×	slack1256 quits (~slack1256@186.11.56.117) (Ping timeout: 256 seconds)
17:20:30	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
17:23:16	×	kor1 quits (~kor1@user/kor1) (Ping timeout: 245 seconds)
17:23:57	×	mbuf quits (~Shakthi@122.162.64.255) (Quit: Leaving)
17:24:20	→	kor1 joins (~kor1@user/kor1)
17:26:07	→	neverfindme joins (~hayden@158.123.160.43)
17:28:13	×	neverfindme quits (~hayden@158.123.160.43) (Remote host closed the connection)
17:28:21	→	_ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl)
17:28:50	×	kor1 quits (~kor1@user/kor1) (Ping timeout: 246 seconds)
17:30:07	×	stewpot quits (~stewpot@2a02:c7e:34de:4500:c0b2:5560:8807:6081) (Remote host closed the connection)
17:31:14	×	Guest\|66 quits (~Guest\|66@199.27.253.178) (Quit: Connection closed)
17:31:57	→	ProfSimm joins (~ProfSimm@87.227.196.109)
17:34:12	×	MajorBiscuit quits (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Ping timeout: 240 seconds)
17:41:35	→	MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net)
17:41:45	×	cheater quits (~Username@user/cheater) (Quit: (BitchX) Eat, drink and be merry...for tomorrow we die)
17:44:11	×	lagash quits (lagash@lagash.shelltalk.net) (Ping timeout: 252 seconds)
17:46:36	×	ec quits (~ec@gateway/tor-sasl/ec) (Quit: ec)
17:47:04	<maerwald>	arjun: hey
17:47:42	→	doyougnu joins (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com)
17:48:38	→	cheater joins (~Username@user/cheater)
17:48:54	<arjun>	hey maerwald
17:49:02	<maerwald>	we need someone with css knowledge
17:49:20	<arjun>	maerwald has 2 wishes left
17:49:36	<maerwald>	arjun: http://play-haskell.tomsmeding.com:8123/play
17:49:50	×	fef quits (~thedawn@user/thedawn) (Quit: Leaving)
17:49:56	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
17:50:12	→	coot joins (~coot@213.134.190.95)
17:50:22	<arjun>	that doesn't look too bad
17:50:49	<arjun>	whattya need done with it?
17:51:50	<maerwald>	https://github.com/tomsmeding/pastebin-haskell/blob/play/play.mustache
17:51:54	<maerwald>	I dunno, make it better :D
17:52:08	<sm>	my suggestion was add a ui kit such as tailwindcss
17:52:28	<maerwald>	arjun: can't even resize the sections
17:52:43	<maerwald>	like here https://play.rust-lang.org/
17:53:30	<arjun>	sm depends what you want to do with it tbh
17:53:50	<sm>	maerwald just said, he wants to "make it pretty"
17:53:51	×	mniip quits (mniip@libera/staff/mniip) (Ping timeout: 606 seconds)
17:54:01	<sm>	pretty/consistent/more usable
17:54:17	→	mniip joins (mniip@libera/staff/mniip)
17:54:18	<arjun>	maerwald, i'll look into it. i don't suppose we'd have a design or anything at hand?
17:54:32	<arjun>	you don't need it urgent right?
17:54:40	<maerwald>	no, just people who design html pages as if it was the 80s
17:56:07	×	MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Quit: WeeChat 3.4)
17:56:36	×	mncheck quits (~mncheck@193.224.205.254) (Ping timeout: 240 seconds)
18:00:46	→	lagash joins (lagash@lagash.shelltalk.net)
18:05:54	×	coot quits (~coot@213.134.190.95) (Quit: coot)
18:06:01	→	coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba)
18:06:58	→	segfaultfizzbuzz joins (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79)
18:09:12	<segfaultfizzbuzz>	so this might be a lame question: in consideration of laziness versus strictness and performance, laziness presents an advantage when the computation begins thinking that computing something is necessary and then later discovers that it is not. isn't this fairly equivalent to the underlying algorithm simply being bad?
18:09:16	×	califax quits (~califax@user/califx) (Remote host closed the connection)
18:09:40	<geekosaur>	just being different
18:09:42	<segfaultfizzbuzz>	if more than say 50% of computations or more than 90% or some other sensible threshold are cancelled
18:10:15	<geekosaur>	often the most natural description of a computation is wasteful if taken strictly
18:10:19	→	califax joins (~califax@user/califx)
18:10:24	×	gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection)
18:10:41	<segfaultfizzbuzz>	geekosaur: is there a good specific example of this?
18:11:04	→	gehmehgeh joins (~user@user/gehmehgeh)
18:11:54	<geekosaur>	mm, mostof the ones I know off the topof my head are frippery like fibonacci
18:12:27	<maerwald>	segfaultfizzbuzz: if you're just looking at one record of a product types and the others you don't look at are expensive to compute
18:12:51	<geekosaur>	but even little things like using zip (or zipWith) against [0..] are doing something that makes sense in a lazy environment and are obviously suicide in a strict one
18:12:56	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 246 seconds)
18:13:13	<geekosaur>	such as labeling a list with its indices `zip xs [0..]`
18:13:20	<maerwald>	but I don't think that's a particularly useful property
18:13:25	×	BlackboardN quits (~nathan@user/BlackboardN) (Ping timeout: 240 seconds)
18:13:31	<maerwald>	I'd argue if you rely on that, you already have bad architecture
18:13:35	<segfaultfizzbuzz>	fibonacci is a computation for kids who don't know math. you can directly compute the nth fibonacci term
18:13:52	<segfaultfizzbuzz>	in O(1) or whatever if you don't care about the arbitrary precision arithmetic part of the computation
18:13:53	<geekosaur>	thzat's what I meant by frippery
18:14:05	×	Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
18:14:17	→	Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
18:15:01	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
18:15:13	<segfaultfizzbuzz>	zip isn't really an algorithm or computation worth mentioning
18:15:23	<maerwald>	laziness is more interesting for optimization tricks of the compiler than for the end user
18:15:33	<geekosaur>	notealso that marewald has decided that laziness is evil so he's the wrong one to ask about laziness
18:16:08	×	coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot)
18:16:10	<monochrom>	Haha but I have decided that eagerness is evil, so... :)
18:16:15	<monochrom>	I mean >:)
18:17:36	<monochrom>	In an eager language I hand-optimize my algorithm under eagerness. In a lazy language I hand-optimize my algorithm under laziness. The two algorithms will have very different structure. And oh I don't code up unnecessary computations either way.
18:18:11	<monochrom>	But what happens is I like the structure of the designed-for-laziness version.
18:18:40	<monochrom>	It tends to be higher level, for example.
18:19:18	<segfaultfizzbuzz>	monochrom: and a computer will outsmart you eventually at both of your hand optimizations
18:19:48	<segfaultfizzbuzz>	ok. i should probably just shut up and write some code lol
18:19:54	→	jgeerds joins (~jgeerds@d5364b87.access.ecotel.net)
18:20:49	<geekosaur>	a computer already has outsmarted monochrom :)
18:21:02	<monochrom>	And looking at how Python for example goes out of its way to invent yield-generator as a builtin, I don't regret joining the lazy list bandwagon on which the extra invention is unnecessary and the whole thing is user-definable.
18:21:10	<maerwald>	eagerness by default is just more chore at times, laziness is more debugging and "wth is going on" moments
18:21:20	<geekosaur>	[30 23:48:31] <monochrom> hpc: I once compiled in C "int i = 1; while (i > 0) i *= 2;" with gcc -O2. The generated code was "label: jmp label". That is a perfect realization of your preference. >:)
18:21:38	<monochrom>	:)
18:22:07	<monochrom>	My "hand-optimze" means I don't write a quadratic-time algorithm when there is a linear-time algorithm.
18:22:23	×	doyougnu quits (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 260 seconds)
18:22:59	<monochrom>	I'm talking about the big-Theta not "twice as fast because I replace (`mod` 3) by (* magic_number)".
18:23:20	×	mtjm quits (~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection)
18:23:29	<Franciman>	this manichean separation between laziness and eagerness is so old!
18:23:37	<Franciman>	polarisation gentle people
18:23:42	<Franciman>	polarisation and continuations
18:23:46	<Franciman>	duality
18:23:59	<Franciman>	if your language is too weak to express duality, you end up in manichean distinctions
18:24:24	<maerwald>	in that case, probably only Idris can express duality
18:24:39	→	mtjm joins (~mutantmel@2604:a880:2:d0::208b:d001)
18:24:41	<maerwald>	in Haskell it's annotations and hoping it actually is lazy or strict
18:24:51	<segfaultfizzbuzz>	hoping haha
18:25:08	<monochrom>	Then computing is stuck in manichean distinctions by definition. Recall that constructive logics have to lose de Morgan duality.
18:26:09	<Franciman>	ehm
18:26:13	<Franciman>	yes
18:26:21	<Franciman>	but why restrict to constructive logics, when you have continuations?
18:26:34	→	gehmehgeh_ joins (~user@user/gehmehgeh)
18:26:37	<monochrom>	Continuations don't exceed computability.
18:26:49	<monochrom>	Continuations don't solve the halting problem.
18:26:59	<Franciman>	yet allow you to have de morgan duality
18:27:05	<monochrom>	The halting problem itself is also a loss of duality right there.
18:27:15	×	gehmehgeh quits (~user@user/gehmehgeh) (Ping timeout: 240 seconds)
18:27:19	<monochrom>	Emulation doesn't count.
18:27:29	<Franciman>	moving target i reckon
18:27:30	<Franciman>	ok
18:28:16	<segfaultfizzbuzz>	whoa that sounds deep, halting problem is loss of duality
18:28:26	<Franciman>	also, what about having a total language with coinductive types?
18:28:47	×	glguy quits (x@libera/staff/glguy) (Quit: Quit)
18:28:48	<Franciman>	is it more amenable?
18:30:05	→	glguy joins (x@libera/staff/glguy)
18:30:07	→	wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com)
18:30:07	×	wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host)
18:30:07	→	wroathe joins (~wroathe@user/wroathe)
18:30:33	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
18:30:51	<segfaultfizzbuzz>	manichean distinction, coinductive types, lol this went way above my head quickly ;-)
18:31:10	<Franciman>	manichean distinction simply means: it's either black or white
18:31:13	<Franciman>	you're either bad or good
18:31:26	<Franciman>	an all time favourite of the new world
18:31:40	<Franciman>	and of the whole history of humanity really
18:32:03	<segfaultfizzbuzz>	makes reasoning simple, right? ;-)
18:32:25	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
18:32:58	<Franciman>	yes sure
18:33:25	<Franciman>	and thinking you can't mix good and evil because python can't
18:33:30	<Franciman>	in a sensible way
18:37:28	<maerwald>	Franciman: I reject that as a principle. Choice implies expressivity. Expressivity is never for free and can introduce complexity. It depends.
18:37:33	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
18:38:46	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
18:39:23	→	Tuplanolla joins (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi)
18:45:11	×	chomwitt quits (~chomwitt@2a02:587:dc0e:a100:8d19:188:687f:a348) (Ping timeout: 256 seconds)
18:46:18	→	BlackboardN joins (~nathan@user/BlackboardN)
18:46:22	×	wroathe quits (~wroathe@user/wroathe) (Ping timeout: 272 seconds)
18:50:27	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Remote host closed the connection)
18:51:27	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
18:55:14	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
18:56:20	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
18:57:08	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
18:58:04	→	ec joins (~ec@gateway/tor-sasl/ec)
19:02:52	×	alp quits (~alp@user/alp) (Remote host closed the connection)
19:03:16	→	alp joins (~alp@user/alp)
19:05:00	×	segfaultfizzbuzz quits (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) (Ping timeout: 240 seconds)
19:07:01	<monochrom>	System F is a total language. Wadler outlines adding existential types to System F, gaining coinductive types. That is still a total language. https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
19:08:28	→	vicfred joins (~vicfred@user/vicfred)
19:08:38	<monochrom>	Technically, I was lying, System F already allows you to encode exists by higher-rank forall. You don't have to add exists, except for convenience (important too).
19:09:43	<monochrom>	Anyway System F is a total language and you can do both inductive and coinductive types in it.
19:10:38	→	chomwitt joins (~chomwitt@ppp-94-67-69-112.home.otenet.gr)
19:13:09	→	mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
19:16:59	×	bahamas quits (~lucian@84.232.140.158) (Ping timeout: 246 seconds)
19:17:47	×	zer0bitz quits (~zer0bitz@2001:2003:f750:a200:c06:c5f:5435:411f) (Ping timeout: 250 seconds)
19:18:17	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
19:18:45	→	sayola joins (~vekto@dslb-088-078-152-238.088.078.pools.vodafone-ip.de)
19:20:59	→	zer0bitz joins (~zer0bitz@2001:2003:f750:a200:f81b:729b:7ef0:993)
19:22:09	×	califax quits (~califax@user/califx) (Remote host closed the connection)
19:22:31	<maerwald>	is there a way in generics to deep-match `Rec0 type`, so you can match a specific sub-AST, instead of passing onto the next instance resolution?
19:23:09	→	califax joins (~califax@user/califx)
19:23:23	→	kenran joins (~kenran@200116b82bd9b000bb30ac8fe29496f8.dip.versatel-1u1.de)
19:24:43	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
19:26:32	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
19:29:02	<monochrom>	I think no, you can only ask for the next instance resolution on `type`.
19:29:36	<maerwald>	so that means I need a dirty utility function in my class to keep track of the context
19:29:47	→	Guest19 joins (~Guest19@ip-86-49-182-248.zrnko.net)
19:30:09	<monochrom>	But I lied, of course you can always use evil dictionary-reification tricks to institute "local instance declaration".
19:30:57	<c_wraith>	if you're going to do that, use the reflection package though. Rely on someone else to get the fiddly bits right, so all you have to worry about is incoherent logic. :)
19:32:10	<maerwald>	I was kind of expecting someone to have solved this use case... seems rather common if you have a deep ast and want to match on a specific sub-AST?
19:32:28	<maerwald>	or maybe that use case is not that common after all
19:34:44	<monochrom>	I think it is not common. (I have no data though.)
19:35:20	<maerwald>	then you could do something like "for every (int + int), replace it with whatever"
19:37:13	→	segfaultfizzbuzz joins (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79)
19:37:28	<monochrom>	I think it is more common (again no data though, just impressions) to require, for example, every instance of MyClass to have consistent and compatible behaviour. Therefore the fact that some instance uses "deriving Generic" and going through "GMyClass" is an implementation detail that GMyClass itself doesn't care about.
19:38:27	<Guest19>	Hello, I would like to ask about traverse and the Writer monad. I want to create a function `test :: (Traversable t, Real a) => (a -> a) -> t a -> (a, t a)` which goes through a traversable, applies the function (a -> a) to each element (but only if it would increase it, otherwise identity) and returns a tuple (<sum of increases over all elements>,
19:38:28	<Guest19>	<the modified Traversable object>): e.g. test (2) [1, 5, -3] ~> (6, [2, 10, -3]), because only the first 2 elements would increase and 6 = 1 + 5 + 0
19:39:10	<Guest19>	Of course, I can do it using basic Haskell, but I was told, it was possible to do it using Writer monad and traverse. But I am stuck on this for two days and I just can't see what to do.
19:40:28	<maerwald>	monochrom: the idea was that pattern matching on the actual data types is extremely verbose... so with generics I was hoping to skip right to the interesting location and only match there, then let the rest be recursive instance jumping
19:41:03	<c_wraith>	Guest19: the first step is that Writer is required to work over a Monoid. Do you know what Monoid instance would be appropriate for this case?
19:42:49	<Guest19>	I know there is a monoid needed to create the Writer monad, but honestly, I don't know much about it:( I know what a monoid is from theoretical point of view (algebra)
19:43:14	×	mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 246 seconds)
19:44:02	<Guest19>	I guess I need to work on tuples (sum so far, [elements so far])
19:44:31	<c_wraith>	Yes, that's correct. Writer is just a newtype around a tuple with convenient Applicative/Monad instances
19:44:43	<monochrom>	Numbers under addition and 0 form a monoid.
19:46:11	×	zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 250 seconds)
19:46:29	→	mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
19:46:32	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds)
19:46:36	<segfaultfizzbuzz>	okay so i am failing at self-directing my haskell curriculum. i keep reading theory and definitions and they mostly go in one ear and out the other and i don't learn how to write according to whatever the haskell philosophy is, if there is such a thing
19:46:52	<Guest19>	Ok, say Real a => (a, t a) would be the type of my monoid, what can I do with it? sorry for being so stupid :(
19:46:56	<segfaultfizzbuzz>	the best book i have come across is real world haskell
19:47:13	<c_wraith>	Guest19: oh, you don't need to stuff the data structure into the monoid too. Just the sum
19:47:20	<monochrom>	But Real a => (a, t a) will not be the type of your monoid. A number type is.
19:47:24	<c_wraith>	Guest19: traverse takes care of preserving the data structure
19:47:30	<segfaultfizzbuzz>	i started trying to write a chess engine as an exercise but got stuck on the simple problem of representing the game state and representing where a queen can go
19:47:41	<c_wraith>	> runWriter $ tell (Sum 2) >> tell 3 >> return "hello" -- Guest19
19:47:42	<lambdabot>	("hello",Sum {getSum = 5})
19:47:52	<maerwald>	segfaultfizzbuzz: there's a haskell game dev channel I think
19:47:54	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
19:48:21	<segfaultfizzbuzz>	it's not that i want to do gamedev, it's that i am trying to learn the language
19:48:54	<monochrom>	Choose a much simpler game, for example Nim.
19:48:54	<segfaultfizzbuzz>	there are a lot of low quality and/or impractical haskell guides out there... what is the best stuff
19:48:54	<maerwald>	segfaultfizzbuzz: yes and you can ask people in that channel about design ideas wrt game state?
19:49:23	<monochrom>	And don't be perfectionist about "what is the absolutely most optimized way to store three integers".
19:49:27	→	acidjnk joins (~acidjnk@p200300d0c7049f94e8cdd499a79a3878.dip0.t-ipconnect.de)
19:49:32	→	zmt00 joins (~zmt00@user/zmt00)
19:49:47	<monochrom>	Perfectionism is why people never learn.
19:49:49	<Guest19>	ok, so first you specify u use the Sum monoid and then u add into it using tell - this is what traverse would do for me (using good enough function), wight?
19:49:56	<monochrom>	You would think that they have already learned.
19:50:30	<Guest19>	but how do I say in traverse I want it to traverse on `Sum` monoid?
19:51:10	<c_wraith>	Guest19: traverse doesn't care. the only thing traverse cares about is the data structure being traversed and that you have an Applicative instance
19:51:48	<c_wraith>	Guest19: that's what makes traverse so cool. It completely separates the concerns of rewriting a data structure and doing just about anything else at the same time.
19:51:56	×	BlackboardN quits (~nathan@user/BlackboardN) (Remote host closed the connection)
19:53:34	<Guest19>	well, i would like to write something like runWriter $ traverse (2) [1,2,3], wouldn't I? Provided that the given function from Real to Real is 2 of course and ignoring the fact I might sometimes not want to apply it for simplicity
19:53:40	<c_wraith>	Guest19: try starting with a function of type Real a => (a -> a) -> a -> Writer (Sum a) a
19:54:02	<monochrom>	Aim for "t a -> Writer (Sum a) (t a)". This can be done with the help of traverse and a helper function you write. It is trivial to go "Writer (Sum a) (t a) -> (a, t a)".
19:54:06	<c_wraith>	Guest19: forget about traversing over the entire data structure. Just write the pointwise logic
19:54:11	<Guest19>	but this way traverse can never guess what I want to do with the numbers (sum them? multiply them?)
19:54:23	<c_wraith>	Guest19: traverse doesn't care what you do with them.
19:54:33	×	raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds)
19:54:40	<Guest19>	ok, i will try to start with the suggested function
19:54:44	<c_wraith>	its logic is entirely independent of what actual transformation you're doing
19:54:55	<monochrom>	Yes obviously you are supposed to replace (* 2) by something smarter, something you code up.
19:55:41	<monochrom>	Not to mention that (* 2) doesn't type-check there.
19:55:56	<monochrom>	This is not your garden variety map (* 2) xs.
19:58:38	×	zer0bitz quits (~zer0bitz@2001:2003:f750:a200:f81b:729b:7ef0:993) (Ping timeout: 260 seconds)
19:59:30	<Guest19>	`testfun f x = if f x > x then pure (f x) else pure x` would this be the correct implementation you wanted from me?:D i am sorry if it is completely idiotic
19:59:48	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
20:00:19	→	earthy joins (~arthurvl@2001:984:275b:1:ba27:ebff:fea0:40b0)
20:00:37	<c_wraith>	well, I'd share the value instead of calculating (f x) twice. But also, I'd include a tell of the amount of increase in the increase case.
20:01:15	→	raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
20:01:24	<c_wraith>	that tell is the key part of doing what you want
20:01:38	→	dcoutts joins (~duncan@host213-122-143-81.range213-122.btcentralplus.com)
20:02:00	×	_ht quits (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection)
20:02:42	<Guest19>	ok, i am starting to get it a bit more now, I was confused where it would figure it out what I actually want to sum up
20:03:13	<c_wraith>	and you can test your function in ghc, making sure it produces Writer values that look right
20:03:27	×	Kaiepi quits (~Kaiepi@156.34.47.253) (Ping timeout: 260 seconds)
20:03:39	→	ubert joins (~Thunderbi@p200300ecdf15888f6cb689ccf87fbbb5.dip0.t-ipconnect.de)
20:03:41	→	pavonia joins (~user@user/siracusa)
20:03:42	<Guest19>	so I would use pure (f x) >> tell $ (f x) - x? i.e. just put `>> tell` after `pure`
20:04:01	×	cosimone quits (~user@93-47-230-184.ip115.fastwebnet.it) (Remote host closed the connection)
20:04:11	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds)
20:04:33	<Guest19>	well, I am completely lost in the syntax:( ghci won't compile half of my code (for a very good reason obviously), that's why I have to beg you for help
20:04:36	×	segfaultfizzbuzz quits (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79) (Ping timeout: 240 seconds)
20:04:49	<c_wraith>	nah, the type of >> means that the pure should be after it, not before it
20:04:52	<c_wraith>	:t (>>)
20:04:53	<lambdabot>	Monad m => m a -> m b -> m b
20:05:07	<Guest19>	and i am aware of the duplicate f x, I just wanted to keep it simple for now
20:06:17	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
20:06:19	<c_wraith>	You might want to just go full multiline and use do blocks. It's perfectly fine to write that way if it keeps things clearer
20:06:37	×	kenran quits (~kenran@200116b82bd9b000bb30ac8fe29496f8.dip.versatel-1u1.de) (Ping timeout: 240 seconds)
20:06:47	→	segfaultfizzbuzz joins (~segfaultf@2602:306:cd3c:9350:4091:e9b1:bc9f:dc79)
20:07:47	→	kenran joins (~kenran@200116b82bd9b00070509ad7c63ceb6b.dip.versatel-1u1.de)
20:08:40	<Guest19>	:do notation is super confusing to me right now, I am only able to rewrite it once I get the "verbose" notation right
20:09:52	<c_wraith>	In that case, you might find it clearer to use a multiline definition with a where block, so you can parenthesize a lot fewer expressions. Make the structure easier to see
20:09:57	<Guest19>	however, it still has some issues with rewriting it the other way round:( `testfun f x = if f x > x then tell ((f x) - x) >> pure (f x) else tell 0 >> pure x` something about infinite type
20:10:59	<Guest19>	i know what an infinite type is, but I just can't spot it here
20:12:03	→	ProfSimm joins (~ProfSimm@87.227.196.109)
20:12:07	<c_wraith>	You don't need tell 0, fwiw. The whole point of the Monoid requirement is that the neutral element just exists.
20:12:38	→	BlackboardN joins (~nathan@user/BlackboardN)
20:12:52	<c_wraith>	but that's not an infinite type
20:14:40	<c_wraith>	I'd really recommend replacing the if with a guard or something. Reduce the complexity per line
20:15:05	<Guest19>	`testfun f x = if diff > 0 then tell diff >> pure (f x) else pure x
20:15:05	<Guest19>	where diff = f x - x` rewritten for clarity
20:15:46	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
20:15:47	×	Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds)
20:15:47	<Guest19>	still, sadly won't compile:
20:15:47	<Guest19>	```
20:15:48	<Guest19>	Occurs check: cannot construct the infinite type: a ~ Sum a arising from a functional dependency between: constraint ‘MonadWriter
20:15:48	<Guest19>	a (WriterT (Sum a) Data.Functor.Identity.Identity)’ arising from a use of ‘tell’ instance ‘MonadWriter w (WriterT w m)’ at <no location info>
20:15:49	<Guest19>	• In the first argument of ‘(>>)’, namely ‘tell diff’ In the expression: tell diff >> pure (f x) In the expression:
20:15:49	<Guest19>	if diff > 0 then tell diff >> pure (f x) else pure x • Relevant bindings include diff :: a (bound at mini6.hs:6:39)
20:15:50	<Guest19>	x :: a (bound at mini6.hs:5:11) f :: a -> a (bound at mini6.hs:5:9) testfun :: (a -> a) -> a -> Writer (Sum a) a
20:15:50	<Guest19>	```
20:15:58	→	Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
20:16:07	<c_wraith>	probably should pastebin multiline stuff :)
20:16:25	<c_wraith>	Oh, I see.
20:16:46	<c_wraith>	you need to add an explicit Sum constructor to the value you're passing to tell
20:16:59	<c_wraith>	I was able to avoid that when using literals, because literals are polymorphic
20:17:03	<Guest19>	yup, probably can't add screenshots here :(
20:17:13	Lord_of_Life_	is now known as Lord_of_Life
20:18:28	<c_wraith>	But you're passing values of the same type to tell and pure, which only works if both of Writer's type arguments are the same. Since one of them is (Sum a) and the other is a, attempting to unify those gives you an infinite type
20:18:52	×	briandaed quits (~root@109.95.142.93.r.toneticgroup.pl) (Remote host closed the connection)
20:19:17	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
20:19:21	<c_wraith>	So you need to throw in an explicit Sum constructor in the tell
20:21:02	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
20:21:21	<Guest19>	is there a better way that using pure? to me it is confusing, because I never know which pure it is
20:21:48	<Guest19>	like in this case it apparently accepts Sum as well, but for Writer it seems to crash
20:21:56	<c_wraith>	There's a different way, but it's definitely not better
20:22:24	<c_wraith>	pure is really important.
20:22:51	<c_wraith>	It lets you ignore everything except what value you want to produce
20:23:54	×	eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds)
20:24:21	<Guest19>	i understand it is comfortable to just use pure because i need to somehow magically turn this value into another this particular function needs, but i find it very hard to read :D
20:24:33	<Guest19>	but maybe thats just cause im too new at this
20:24:55	<c_wraith>	I think it's a matter of comfort in letting go.
20:26:17	×	mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 246 seconds)
20:26:27	→	alMalsamo joins (~alMalsamo@gateway/tor-sasl/almalsamo)
20:27:06	alMalsamo	is now known as littlebobeep
20:29:08	<Guest19>	anyway, thank you for your help, i think i just needed to finish one exercise of this type (not even by myself) so that i can use it to solve the others and understand it in detail in the process
20:30:03	<c_wraith>	I kind of think the main philosophy of haskell is trusting the compiler to keep track of the fiddly things. The challenge is learning that you can program without focusing on them most of the time.
20:30:15	×	neurocyte861 quits (~neurocyte@user/neurocyte) (Ping timeout: 256 seconds)
20:30:23	→	zer0bitz joins (~zer0bitz@2001:2003:f750:a200:18ec:9063:4133:b132)
20:30:57	→	neurocyte8614 joins (~neurocyte@IP-094016090045.dynamic.medianet-world.de)
20:30:58	×	neurocyte8614 quits (~neurocyte@IP-094016090045.dynamic.medianet-world.de) (Changing host)
20:30:58	→	neurocyte8614 joins (~neurocyte@user/neurocyte)
20:32:26	→	merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl)
20:33:38	×	alp quits (~alp@user/alp) (Ping timeout: 260 seconds)
20:40:32	→	coot joins (~coot@213.134.190.95)
20:44:41	×	motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit)
20:45:25	→	ub joins (~Thunderbi@p548c8d44.dip0.t-ipconnect.de)
20:45:55	×	ubert quits (~Thunderbi@p200300ecdf15888f6cb689ccf87fbbb5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
20:45:56	ub	is now known as ubert
20:45:57	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
20:50:06	→	yauhsien joins (~yauhsien@61-231-60-85.dynamic-ip.hinet.net)
20:51:08	×	mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 272 seconds)
20:54:17	×	yauhsien quits (~yauhsien@61-231-60-85.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
20:54:59	×	BlackboardN quits (~nathan@user/BlackboardN) (Ping timeout: 246 seconds)
20:57:07	×	mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds)
20:57:15	→	bitmapper joins (uid464869@id-464869.lymington.irccloud.com)
20:58:43	×	arjun quits (~arjun@user/arjun) (Ping timeout: 260 seconds)
20:58:53	→	mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475)
20:59:29	×	Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep)
21:03:57	×	madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 260 seconds)
21:06:27	×	merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
21:07:19	×	kenran quits (~kenran@200116b82bd9b00070509ad7c63ceb6b.dip.versatel-1u1.de) (Quit: WeeChat info:version)
21:10:41	→	mvk joins (~mvk@2607:fea8:5ce3:8500::3800)
21:13:56	→	zeenk joins (~zeenk@2a02:2f04:a313:d600:8d26:ec9f:3ff6:fc94)
21:14:52	→	motherfsck joins (~motherfsc@user/motherfsck)
21:15:10	×	gehmehgeh_ quits (~user@user/gehmehgeh) (Remote host closed the connection)
21:15:52	→	gehmehgeh_ joins (~user@user/gehmehgeh)
21:17:21	×	coot quits (~coot@213.134.190.95) (Quit: coot)
21:19:45	→	eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
21:20:51	×	Guest19 quits (~Guest19@ip-86-49-182-248.zrnko.net) (Quit: Client closed)
21:21:15	×	gurkenglas quits (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de) (Read error: Connection reset by peer)
21:23:10	→	gurkenglas joins (~gurkengla@dslb-178-012-018-212.178.012.pools.vodafone-ip.de)
21:33:18	→	Kaiepi joins (~Kaiepi@156.34.47.253)
21:36:14	→	cosimone joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20)
21:38:22	<segfaultfizzbuzz>	so people argue about whether umap is a useful analytic technique. i saw the author of umap say something which i am curious to ask about, which is that he said that for all practical purposes any topology you are interested in can be formed by specifying nodes and edges discretely and then reasoning about that
21:38:44	<segfaultfizzbuzz>	so is there anything useful we can say about the fact that "everything can be discrete"
21:40:04	<geekosaur>	not really. it's more or less how we get away with writing programs that do useful things, since digital computers deal in discrete values
21:40:23	<geekosaur>	(as distinct from analog or quantum computers)
21:40:40	<segfaultfizzbuzz>	like in linear algebra some approaches to it are very careful to not deal with the finite dimensional representation of things
21:41:36	<segfaultfizzbuzz>	but... i've never come across a situation whether the finite or non-finite distinction is meaningful
21:42:02	<segfaultfizzbuzz>	at the end of the day you have to be able to make a graph on paper or draw symbols, and that will always involve some kind of discrete representation,...
21:42:16	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
21:42:28	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
21:42:40	×	cosimone quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Quit: ERC (IRC client for Emacs 27.1))
21:43:09	<geekosaur>	right, but you may only have that at the end.
21:43:35	×	wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 240 seconds)
21:44:07	<monochrom>	Pretty sure it is the niche theoretical physicists working on the fundamentals of quantum physics who are really interested in "topologies that matter can be formed from discrete nodes and edges".
21:44:34	<geekosaur>	analog computers still do many things better than digital computers do, since an operation like integration is fundamental. you may have a discrete value at the end, but getting to that end can involve nasty things like multiple integrals that can only be simulated (and that often only when simplified) on a digital computer
21:45:36	→	wyrd joins (~wyrd@gateway/tor-sasl/wyrd)
21:45:47	<segfaultfizzbuzz>	"nearly all" integrals can be trivially discretized. the only examples i can think of which don't fall into this category are integrals of stochastic functions, which can still be discretized but simply require some more compute
21:46:03	<geekosaur>	"simply"
21:46:10	<hpc>	some people like to call analog computers "experiments" :P
21:46:31	<segfaultfizzbuzz>	put another way, from my perspective discretizing an integral is trivial... i suppose at some point the dimensionality of the integral grows to the point that you are studying light transport and need more of an mcmc kind of approach to integrate,...
21:47:07	<geekosaur>	even figuring water flow can be very difficult to compute… yet the water flows anyway
21:47:46	<geekosaur>	most accurate way to model it? duplicate the flow in question. which is an analog computer although we don't call it that
21:48:02	×	zer0bitz quits (~zer0bitz@2001:2003:f750:a200:18ec:9063:4133:b132) (Read error: Connection reset by peer)
21:48:11	<segfaultfizzbuzz>	well hold on there, you have how the water itself moves and then how to compute a theory of that motion. and that theory can always be discretized and calculated is my view (unless i'm wrong here...)
21:49:39	<geekosaur>	oh, it can always be done. the problem is that that calculation can take much, much longer than just observing the bloody system
21:50:06	<geekosaur>	ot to mention that you have to come up with that theory, which is rarely trivial
21:50:09	<hpc>	and what if you don't know the formulas anyway
21:50:24	<hpc>	you're trying to answer "how accurate is this model?"
21:50:34	<geekosaur>	there are still many open questions in fields that rely on that
21:50:37	<hpc>	and no amount of testing the model against itself at higher resolution is going to help you there
21:50:54	<segfaultfizzbuzz>	so what i am saying is that if i open any math book or any i don't know civil engineering book or what have you
21:51:00	<geekosaur>	and reformulation of relevant theorues
21:51:12	<abastro[m]>	You: I gotta calculate this fluid movement
21:51:12	<abastro[m]>	Chaos: I am going to ruin this person's career
21:51:24	<geekosaur>	civil engineering is filled with known to be inaccurate but "usually good enough" approximations
21:51:53	<segfaultfizzbuzz>	and i look at any question i can ask about whatever is being discussed, even if the topic looks like it is a very non-discrete thing, you can always find a discretization and work towards computing the answer
21:51:59	<hpc>	a lot of civil engineering is arranging things so you never hit where those approximations aren't good enough anymore
21:52:07	<geekosaur>	that too
21:52:12	<hpc>	also usually the approximations break down at the same time the building does
21:52:26	<geekosaur>	see also the tacoma narrows bridge
21:52:52	<geekosaur>	or recent essentially-repeats involving walking bridges
21:53:08	<monochrom>	Chaos, Crash, Burn, and "mess with the best, die like the rest" etc :)
21:53:38	×	gehmehgeh_ quits (~user@user/gehmehgeh) (Quit: Leaving)
21:54:29	<geekosaur>	also just looking at the formulas doesn't show you any of the "I know it says this but this is what we really do because it comes crashing down if we don't"
21:54:39	<monochrom>	But why are we discussing discreteness in #haskell ?
21:54:58	<segfaultfizzbuzz>	i think it ties a bit into thinking about laziness,
21:55:01	<maerwald>	be water, my friend
21:55:14	<monochrom>	May I remind that #haskell-offtopic exists.
21:55:20	<segfaultfizzbuzz>	haha ok :-)
21:56:24	<monochrom>	But my conclusion is maybe we should ban walking on bridges >:)
21:56:44	<shapr>	there's also #haskell-in-depth for long conversations
21:57:03	×	takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 260 seconds)
21:57:15	×	shapr quits (~user@pool-173-73-44-186.washdc.fios.verizon.net) (Quit: rebooting emacs)
21:58:56	×	dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.4.1)
22:01:04	→	shapr joins (~user@pool-173-73-44-186.washdc.fios.verizon.net)
22:10:19	→	mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
22:10:56	×	__monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:17:28	×	mvk quits (~mvk@2607:fea8:5ce3:8500::3800) (Ping timeout: 260 seconds)
22:21:28	×	whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
22:21:35	×	bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds)
22:22:40	<abastro[m]>	Hm how can I access #haskell-in-depth
22:22:45	<abastro[m]>	From matrix
22:23:01	→	fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
22:24:29	→	bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
22:24:53	<geekosaur>	#haskell-in-depth:libera.chat I think
22:26:47	<abastro[m]>	Thank you!!!
22:27:33	×	fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 256 seconds)
22:28:44	→	MajorBiscuit joins (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48)
22:34:54	×	ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection)
22:36:17	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
22:38:13	×	acidjnk quits (~acidjnk@p200300d0c7049f94e8cdd499a79a3878.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
22:40:15	×	ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds)
22:42:08	×	qwedfg quits (~qwedfg@user/qwedfg) (Read error: Connection reset by peer)
22:44:22	×	MajorBiscuit quits (~MajorBisc@2a02:a461:129d:1:6d4c:38a4:18b7:4b48) (Quit: WeeChat 3.4)
22:45:31	→	yauhsien joins (~yauhsien@61-231-37-33.dynamic-ip.hinet.net)
22:46:08	→	qwedfg joins (~qwedfg@user/qwedfg)
22:48:26	→	madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net)
22:50:08	×	yauhsien quits (~yauhsien@61-231-37-33.dynamic-ip.hinet.net) (Ping timeout: 246 seconds)
23:00:03	×	jgeerds quits (~jgeerds@d5364b87.access.ecotel.net) (Ping timeout: 260 seconds)
23:00:40	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
23:01:55	×	lavaman quits (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net) (Remote host closed the connection)
23:04:48	×	Tuplanolla quits (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) (Quit: Leaving.)
23:05:00	→	natechan joins (~nate@98.45.152.91)
23:05:11	×	zyklotomic quits (~ethan@r4-128-61-95-82.res.gatech.edu) (Ping timeout: 246 seconds)
23:07:10	→	zyklotomic joins (~ethan@res380d-128-61-87-11.res.gatech.edu)
23:07:19	×	chomwitt quits (~chomwitt@ppp-94-67-69-112.home.otenet.gr) (Ping timeout: 260 seconds)
23:12:00	→	Guest40 joins (~Guest40@189.101.232.157)
23:12:13	×	Guest40 quits (~Guest40@189.101.232.157) (Client Quit)
23:14:38	×	mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 246 seconds)
23:21:51	→	yauhsien joins (~yauhsien@61-231-37-33.dynamic-ip.hinet.net)
23:26:27	×	yauhsien quits (~yauhsien@61-231-37-33.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
23:32:28	→	lavaman joins (~lavaman@c-174-63-118-52.hsd1.ma.comcast.net)
23:37:19	→	rawley joins (~rawley@216-197-141-102.nbfr.hsdb.sasknet.sk.ca)
23:45:08	×	vicfred quits (~vicfred@user/vicfred) (Quit: Leaving)
23:49:50	→	deadmarshal_ joins (~deadmarsh@95.38.116.113)
23:49:57	→	lainon joins (~lainon@45-18-156-230.lightspeed.knvltn.sbcglobal.net)
23:54:18	×	deadmarshal_ quits (~deadmarsh@95.38.116.113) (Ping timeout: 260 seconds)
23:58:29	→	yauhsien joins (~yauhsien@61-231-37-33.dynamic-ip.hinet.net)
23:59:13	×	geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection)

All times are in UTC on 2022-04-01.