Home liberachat/#haskell: Logs Calendar

Logs on 2024-05-17 (liberachat/#haskell)

00:05:08 × bollu quits (~bollu@159.65.151.13) (Quit: Ping timeout (120 seconds))
00:05:35 → bollu joins (~bollu@159.65.151.13)
00:06:49 × philopsos1 quits (~caecilius@user/philopsos) (Quit: Lost terminal)
00:10:34 → philopsos1 joins (~caecilius@user/philopsos)
00:19:22 → random-jellyfish joins (~developer@user/random-jellyfish)
00:20:07 × philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 246 seconds)
00:21:05 × mei quits (~mei@user/mei) (Remote host closed the connection)
00:23:26 × FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 260 seconds)
00:27:27 → zzz joins (~yin@user/zero)
00:27:31 → mei joins (~mei@user/mei)
00:47:03 → rekahsoft joins (~rekahsoft@bras-base-orllon1103w-grc-13-184-148-6-204.dsl.bell.ca)
00:47:27 × rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-13-184-148-6-204.dsl.bell.ca) (Remote host closed the connection)
00:50:26 → bilegeek joins (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf)
00:51:53 × m257 quits (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 256 seconds)
01:03:31 × zzz quits (~yin@user/zero) (Ping timeout: 268 seconds)
01:07:52 × otto_s quits (~user@p4ff27827.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
01:09:41 → otto_s joins (~user@p5b0448c7.dip0.t-ipconnect.de)
01:12:48 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
01:13:19 × ystael quits (~ystael@user/ystael) (Ping timeout: 246 seconds)
01:15:36 × xff0x quits (~xff0x@2405:6580:b080:900:25be:f228:ec64:b69c) (Ping timeout: 255 seconds)
01:15:41 → Guest85 joins (~Guest85@c-76-115-231-219.hsd1.or.comcast.net)
01:16:14 × Guest85 quits (~Guest85@c-76-115-231-219.hsd1.or.comcast.net) (Client Quit)
01:17:26 → philopsos joins (~caecilius@user/philopsos)
01:21:11 → m257 joins (~maaz@174.92.92.146)
01:49:20 × causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1)
01:51:49 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 272 seconds)
01:54:05 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds)
02:01:23 → xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
02:04:01 × Athas quits (athas@2a01:7c8:aaac:1cf:a4c:e787:a74:d356) (Quit: ZNC 1.8.2 - https://znc.in)
02:04:11 → Athas joins (athas@sigkill.dk)
02:10:44 × td_ quits (~td@i53870936.versanet.de) (Ping timeout: 252 seconds)
02:12:45 → td_ joins (~td@i53870915.versanet.de)
02:15:16 × m257 quits (~maaz@174.92.92.146) (Ping timeout: 246 seconds)
02:30:54 → FinnElija joins (~finn_elij@user/finn-elija/x-0085643)
02:31:43 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
02:47:39 × mei quits (~mei@user/mei) (Remote host closed the connection)
02:54:06 → mei joins (~mei@user/mei)
02:54:31 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
03:01:52 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Quit: WeeChat 4.2.2)
03:03:35 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
03:09:52 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds)
03:17:25 → philopsos1 joins (~caecilius@user/philopsos)
03:29:49 × philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 246 seconds)
03:39:53 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
03:44:40 → m257 joins (~maaz@174.92.92.146)
03:52:32 → aforemny_ joins (~aforemny@2001:9e8:6cfa:400:979c:514d:c315:798d)
03:53:47 × aforemny quits (~aforemny@2001:9e8:6cd4:e700:d233:e5e6:582d:855) (Ping timeout: 256 seconds)
03:58:13 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:02:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
04:04:40 × philopsos quits (~caecilius@user/philopsos) (Quit: leaving)
04:05:01 → philopsos joins (~caecilius@user/philopsos)
04:06:31 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:09:11 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
04:09:57 → oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl)
04:10:21 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:15:09 × doyougnu quits (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Ping timeout: 255 seconds)
04:17:04 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
04:21:38 → doyougnu joins (~doyougnu@syn-045-046-170-068.res.spectrum.com)
04:21:41 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:24:23 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
04:27:02 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:32:03 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
04:33:35 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
04:43:58 × EvanR quits (~EvanR@user/evanr) (Ping timeout: 268 seconds)
04:45:31 × m257 quits (~maaz@174.92.92.146) (Ping timeout: 268 seconds)
04:48:10 × dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection)
05:06:16 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
05:09:22 × tinjamin quits (~tinjamin@banshee.h4x0r.space) (Quit: Ping timeout (120 seconds))
05:09:39 → tinjamin joins (~tinjamin@banshee.h4x0r.space)
05:22:04 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
05:22:41 × ft quits (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving)
05:28:11 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
05:28:39 → euphores joins (~SASL_euph@user/euphores)
05:30:04 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
05:34:42 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
05:37:06 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
05:40:26 → acidjnk_new joins (~acidjnk@p200300d6e714dc64113083a2457f0359.dip0.t-ipconnect.de)
05:51:51 → madeleine-sydney joins (~madeleine@c-71-229-185-228.hsd1.co.comcast.net)
05:54:10 × xal quits (~xal@mx1.xal.systems) ()
05:55:07 → xal joins (~xal@mx1.xal.systems)
05:55:58 → Square joins (~Square@user/square)
05:57:39 × xal quits (~xal@mx1.xal.systems) (Client Quit)
05:58:06 → xal joins (~xal@mx1.xal.systems)
05:58:19 × xal quits (~xal@mx1.xal.systems) (Client Quit)
05:58:57 → xal joins (~xal@mx1.xal.systems)
06:08:24 × mikko quits (~mikko@user/mikko) (Ping timeout: 260 seconds)
06:13:38 × bilegeek quits (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf) (Quit: Leaving)
06:27:58 → kuribas joins (~user@2a02:1808:3:6cf7:b1e9:2b2e:cd0:dec5)
06:30:26 × kuribas quits (~user@2a02:1808:3:6cf7:b1e9:2b2e:cd0:dec5) (Remote host closed the connection)
06:30:28 → philopsos1 joins (~caecilius@user/philopsos)
06:30:39 → kuribas joins (~user@2a02:1808:3:6cf7:1525:c8e2:6d38:988c)
06:31:47 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
06:34:57 × kuribas quits (~user@2a02:1808:3:6cf7:1525:c8e2:6d38:988c) (Read error: Connection reset by peer)
06:35:15 → kuribas joins (~user@2a02:1808:3:6cf7:1525:c8e2:6d38:988c)
06:50:22 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
07:01:13 × kuribas quits (~user@2a02:1808:3:6cf7:1525:c8e2:6d38:988c) (Ping timeout: 255 seconds)
07:18:36 → danza joins (~francesco@fi-19-216-22.service.infuturo.it)
07:18:47 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
07:28:31 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 246 seconds)
07:38:18 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
07:40:59 → mikko joins (~mikko@dsl-trebng22-58c1a8-185.dhcp.inet.fi)
07:40:59 × mikko quits (~mikko@dsl-trebng22-58c1a8-185.dhcp.inet.fi) (Changing host)
07:40:59 → mikko joins (~mikko@user/mikko)
07:42:11 <Hecate> Rembane: yoooo
07:42:15 <Hecate> what's up?
07:45:18 × danza quits (~francesco@fi-19-216-22.service.infuturo.it) (Ping timeout: 255 seconds)
07:45:43 <[exa]> hey guys, is there a way to paste clipboard to the play.haskell.org code textarea on cellphones? This might be me becoming obsolete but I can't find a way to do that, the editor blocks the usual "hold select & paste" way
07:46:06 <[exa]> "on cellphones" I mean android in this case
07:46:15 <[exa]> cc tomsmeding ^
07:46:46 → sawilagar joins (~sawilagar@user/sawilagar)
07:46:53 <tomsmeding> [exa]: yeah the mobile experience on the playground is a bit broken because the editor is too clever
07:46:59 <tomsmeding> I'm open to suggestions
07:47:26 <tomsmeding> I'm not unwilling to just make it a plain <textarea>, but then how to detect whether to do so?
07:47:29 → chele joins (~chele@user/chele)
07:48:05 <tomsmeding> the horizontal vs vertical layout is based on window width, but that makes some kind of sense for layout but is certainly too indirect for something like "has a proper external keyboard"
07:48:45 <[exa]> yeah maybe a completely stupid switch like "plain textarea/cool colorcodearea" could do
07:49:15 <tomsmeding> there's actually some kind of context menu thing that this fancy editor does where it does offer clipboard actions
07:49:16 <[exa]> otoh there us no reason why the editor would block pastes right? so maybe better if I go scream at upstream :)
07:49:23 <tomsmeding> but I think I disabled that because it was terribly annoying
07:50:18 <[exa]> yeah
07:51:41 <[exa]> as a stupid workaround, a button to open a local file would probably do as well
07:52:11 <[exa]> what's the editor btw? (quite annoyingly I'm on a cellphone now :D )
07:52:44 → fendor joins (~fendor@2a02:8388:1605:ce00:24e2:c141:1f86:a346)
07:53:36 <tomsmeding> Ace
07:53:40 <tomsmeding> https://ace.c9.io/
07:57:18 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 268 seconds)
07:58:04 <[exa]> ah I see
07:58:24 <[exa]> yeah really, I cannot paste to the official ace demo
07:58:43 <[exa]> but e.g. CodeMirror6 seems to work
07:58:43 <tomsmeding> [exa]: do you get the (...) button the right-hand side of the line
07:59:00 <tomsmeding> I was using codemirror before because maerwald put that in but I could not make heads or tails of its configuration
07:59:18 <tomsmeding> documentation was incomplete, the typescript typing seemed incorrect in places, and there was way too much abstraction
07:59:31 <tomsmeding> ace just worked (tm)
07:59:36 <tomsmeding> except now this
08:00:09 <[exa]> yeah not saying CM would be better :D
08:00:37 <[exa]> the ldots button I dont see on play.h.o bot it seems to work on the official site
08:00:44 <[exa]> *but
08:01:06 <tomsmeding> yeah you don't see it on play.h.o because https://github.com/haskell/play-haskell/blob/master/play-haskell-server/play.mustache#L332-L334 lol
08:01:16 <[exa]> what are folks like gitlabs and giteas using?
08:01:34 <[exa]> lol
08:01:36 <[exa]> ok
08:01:58 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
08:01:58 <tomsmeding> [exa]: removed that css now, reload play.haskell.org
08:02:23 <tomsmeding> should I just keep that button?
08:02:48 <[exa]> ooh yes it works now
08:02:51 <[exa]> thanks!
08:03:07 <tomsmeding> the full menu doesn't even fit on my phone's screen
08:03:13 <[exa]> lemme check a thing tho
08:03:16 <[exa]> yep
08:03:25 <tomsmeding> and the menu is weird because there's no visual separator between the buttons etc
08:03:50 <tomsmeding> but the mobile experience is bound to be awkward anyway so I'm willing to just keep this as a hack :
08:03:52 <tomsmeding> * :p
08:05:37 × barak quits (~barak@2a0d:6fc2:68c1:7200:e61a:851b:d7b:27e8) (Ping timeout: 268 seconds)
08:06:43 <[exa]> yeah apparently that is the same on the official site too
08:06:49 <tomsmeding> yeah
08:07:04 <[exa]> javascripts. *exhales*
08:07:21 <tomsmeding> not sure this is js's fault :)
08:07:37 <[exa]> anyway this kinda works and does not seem as annoying as I thought it would be
08:08:18 <[exa]> so I guess lets wait if anyone comes here to complain about this stupid 3dot button appearing again :D
08:11:48 → cfricke joins (~cfricke@user/cfricke)
08:11:53 <tomsmeding> [exa]: thanks for complaining :)
08:13:07 <[exa]> ah np :) thanks for fixing this
08:24:29 → danse-nr3 joins (~danse-nr3@ge-19-102-90.service.infuturo.it)
08:26:26 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:35:54 × remedan quits (~remedan@ip-78-102-118-253.bb.vodafone.cz) (Quit: Bye!)
08:36:04 → gmg joins (~user@user/gehmehgeh)
08:36:20 × zer0bitz quits (~zer0bitz@user/zer0bitz) (Ping timeout: 260 seconds)
08:42:08 → rosco joins (~rosco@173.150.68.85.rev.sfr.net)
08:42:32 → __monty__ joins (~toonn@user/toonn)
08:44:47 × danse-nr3 quits (~danse-nr3@ge-19-102-90.service.infuturo.it) (Ping timeout: 268 seconds)
08:50:45 → danse-nr3 joins (~danse-nr3@151.46.212.14)
08:53:36 × philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 260 seconds)
08:54:06 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
09:00:15 → euphores joins (~SASL_euph@user/euphores)
09:09:27 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 272 seconds)
09:09:40 → ubert joins (~Thunderbi@p200300ecdf1a44248c362e018d65ba14.dip0.t-ipconnect.de)
09:25:10 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
09:26:41 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
09:30:30 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
09:31:16 × driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
09:31:54 → driib3 joins (~driib@vmi931078.contaboserver.net)
09:33:00 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
09:44:02 × Square quits (~Square@user/square) (Ping timeout: 256 seconds)
10:01:15 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds)
10:05:40 × xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds)
10:08:38 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds)
10:10:45 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
10:14:31 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
10:19:36 → Guest13 joins (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net)
10:28:11 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 256 seconds)
10:36:27 ← L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
10:47:36 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
10:49:43 × talismanick quits (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection)
10:50:42 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
10:56:04 × madeleine-sydney quits (~madeleine@c-71-229-185-228.hsd1.co.comcast.net) (Ping timeout: 246 seconds)
10:59:11 <Guest13> ski I got my memoized recursive function working!
11:02:53 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds)
11:03:57 → Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
11:14:05 × random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 256 seconds)
11:24:11 × danse-nr3 quits (~danse-nr3@151.46.212.14) (Ping timeout: 268 seconds)
11:34:07 → ubert1 joins (~Thunderbi@p200300ecdf1a442d1be818c703728472.dip0.t-ipconnect.de)
11:34:22 × ubert quits (~Thunderbi@p200300ecdf1a44248c362e018d65ba14.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
11:34:22 ubert1 is now known as ubert
11:55:01 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:55:03 <Rembane> \o/
11:55:49 → libertyprime joins (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz)
11:56:36 → rvalue- joins (~rvalue@user/rvalue)
11:57:17 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 240 seconds)
12:00:38 rvalue- is now known as rvalue
12:03:43 × cfricke quits (~cfricke@user/cfricke) (Remote host closed the connection)
12:04:03 → cfricke joins (~cfricke@user/cfricke)
12:09:53 × libertyprime quits (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Remote host closed the connection)
12:10:07 → ft joins (~ft@p508db8fc.dip0.t-ipconnect.de)
12:13:58 → xff0x joins (~xff0x@2405:6580:b080:900:4704:a3e5:3fba:c1dc)
12:29:47 → qqq joins (~qqq@92.43.167.61)
12:30:05 <[Leary]> Guest13: Speaking of, I got nerdsniped and figured out the dirty version: https://play-haskell.tomsmeding.com/saved/ukgOdGqj
12:30:40 <Guest13> ?
12:31:03 → danse-nr3 joins (~danse-nr3@151.46.212.14)
12:31:24 × Nixkernal quits (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
12:31:54 <[Leary]> (the dirty way to memoise a recursive function with a Map)
12:32:07 <Guest13> ah what's that?
12:32:20 <[Leary]> Check the link?
12:37:49 <ski> nice, Guest13 !
12:38:50 <Guest13> [Leary] I have no clue what is going on there XD
12:39:30 <Guest13> mine looks like:
12:39:30 <Guest13> permutationsMemo :: Problem -> (Int, Int, Int) -> Int
12:39:31 <Guest13> permutationsMemo problem@(springs, grps) ix@(i, grp, count)
12:39:31 <Guest13>   | i < 0 || i > length springs = undefined
12:39:32 <Guest13>   | grp < 0 || grp > length grps = undefined
12:39:32 <Guest13>   | count < 0 || count > length springs = undefined
12:39:33 <Guest13>   | otherwise = memo ! ix
12:39:33 <Guest13>   where bounds = ((0,0,0), (length springs, length grps, length springs))
12:39:34 <Guest13>         memo = tabulate bounds get
12:39:34 <Guest13>         get ixx@(i, grp, count)
12:39:35 <Guest13>           | i == length springs = if (count == 0 && grp == length grps) then 1 else endOnHash -- end of springs
12:39:35 <Guest13>           | grp == length grps = if ((springs !! i) == Damaged) then 0 else dotCase -- matched all groups
12:39:36 <Guest13>           | cur == Operational = dotCase
12:39:36 <Guest13>           | cur == Damaged = hashCase
12:39:37 <Guest13>           | cur == Unknown = dotCase + hashCase
12:39:37 <Guest13>           | otherwise = undefined
12:39:38 <Guest13>           where cur = springs !! I
12:39:38 <Guest13>                 groupTarget = grps !! grp
12:39:39 <yushyin> pls ...
12:40:28 <Guest13> sorry ill send a link
12:43:20 <Guest13> https://play.haskell.org/saved/WOB84oaz
12:44:25 → joeyadams joins (~joeyadams@2603:6010:5100:2ed:e620:4fb2:2e9f:c7fe)
12:45:17 <Guest13> I have a function "get" which is meant to be the recursive part which refers to the memoized array inside it
12:45:53 <Guest13> and my answer is contained within (0,0,0)
12:46:12 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
12:46:39 <Guest13> it is basically same code as the unmemorised function
12:47:20 <Guest13> maybe it would be best to lazily pass the memo to the "get" function and define it somewhere else?
12:47:49 <Guest13> so memo = tabulate bounds (get memo)
12:53:41 × danse-nr3 quits (~danse-nr3@151.46.212.14) (Ping timeout: 252 seconds)
12:54:19 → danse-nr3 joins (~danse-nr3@151.44.168.106)
13:09:05 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:13:35 × Guest13 quits (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) (Quit: Client closed)
13:14:26 → ystael joins (~ystael@user/ystael)
13:17:24 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
13:22:41 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
13:23:42 × igemnace quits (~igemnace@user/igemnace) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in)
13:25:05 → igemnace joins (~igemnace@user/igemnace)
13:31:07 → ph88 joins (~ph88@2a02:8109:9e26:c800:8347:c769:dd97:86a2)
13:31:53 × joeyadams quits (~joeyadams@2603:6010:5100:2ed:e620:4fb2:2e9f:c7fe) (Quit: Leaving)
13:32:30 <ph88> i took this as a starting point https://play.haskell.org/saved/A0jyJ40g ok works. Then i wanted to add another typeclass but ran into trouble https://play.haskell.org/saved/nsO7Fn41 Managed to typecheck it like this https://play.haskell.org/saved/fYRQ1REb but the latter is coupled. Is there a way i can write this code decoupled? (see second snippet)
13:35:55 → ubert1 joins (~Thunderbi@p200300ecdf1a442dbe8e8c8f9360db77.dip0.t-ipconnect.de)
13:40:13 <[Leary]> ph88: I don't really know what you're trying to do, but `class (c1 a, c2 a) => (c1 & c2) a; instance (c1 a, c2 a) => (c1 & c2) a` will allow you to write `Entity (HasDataID & GetMessage)`.
13:40:17 × ubert quits (~Thunderbi@p200300ecdf1a442d1be818c703728472.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
13:40:17 ubert1 is now known as ubert
13:41:04 → zer0bitz joins (~zer0bitz@user/zer0bitz)
13:46:04 <[Leary]> You may also want to generalise some functions or instances with QuantifiedConstraints; something like `(forall x. cs x => c x, c a) => a -> Entity cs -> ...` will allow you to handle any `Entity (... & c & ...)` uniformly.
13:47:48 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
13:48:06 → causal joins (~eric@50.35.88.207)
13:49:25 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:49:40 <ph88> [Leary], what is that type operator & ?
13:50:31 <[Leary]> It's the name of the typeclass I declared.
13:52:17 × talukara quits (~talukara@user/talukara) (Quit: I closed IRC (probably gonna sleep))
13:52:36 <tomsmeding> -XTypeOperators
13:52:46 → addfb3 joins (~dante@2804:431:cff7:525d:eaa8:811b:a49b:6191)
13:52:46 × addfb3 quits (~dante@2804:431:cff7:525d:eaa8:811b:a49b:6191) (Changing host)
13:52:46 → addfb3 joins (~dante@user/addfb3)
13:53:24 → patrl joins (~patrl@user/patrl)
13:54:05 <ph88> thanks i'll have a look how that works
14:00:26 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1)
14:13:13 <ncf> my divination skills are failing me, i still have no idea what the actual problem is here
14:18:57 × FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Read error: Connection reset by peer)
14:18:57 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
14:18:57 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
14:19:39 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
14:20:06 → FinnElija joins (~finn_elij@user/finn-elija/x-0085643)
14:22:23 → gmg joins (~user@user/gehmehgeh)
14:24:28 → Sgeo joins (~Sgeo@user/sgeo)
14:26:39 × danse-nr3 quits (~danse-nr3@151.44.168.106) (Remote host closed the connection)
14:27:05 → danse-nr3 joins (~danse-nr3@151.44.168.106)
14:28:46 → zzz joins (~yin@user/zero)
14:32:30 × califax quits (~califax@user/califx) (Remote host closed the connection)
14:34:15 → califax joins (~califax@user/califx)
14:38:26 × danse-nr3 quits (~danse-nr3@151.44.168.106) (Remote host closed the connection)
14:38:51 → danse-nr3 joins (~danse-nr3@151.44.168.106)
14:50:10 × fendor quits (~fendor@2a02:8388:1605:ce00:24e2:c141:1f86:a346) (Remote host closed the connection)
15:00:53 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds)
15:06:40 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds)
15:11:23 × fun-safe-math quits (~fun-safe-@24.21.106.247) (Ping timeout: 260 seconds)
15:12:57 × mei quits (~mei@user/mei) (Remote host closed the connection)
15:19:24 → mei joins (~mei@user/mei)
15:21:12 → billchenchina joins (~billchenc@103.152.35.21)
15:23:31 → EvanR joins (~EvanR@user/evanr)
15:23:44 × billchenchina quits (~billchenc@103.152.35.21) (Remote host closed the connection)
15:24:02 → billchenchina joins (~billchenc@103.152.35.21)
15:33:45 × rosco quits (~rosco@173.150.68.85.rev.sfr.net) (Remote host closed the connection)
15:42:22 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
15:44:40 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
15:47:59 × cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
15:55:12 × danse-nr3 quits (~danse-nr3@151.44.168.106) (Ping timeout: 256 seconds)
16:03:20 × zzz quits (~yin@user/zero) (Quit: leaving)
16:07:32 × sp1ff quits (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Read error: Connection reset by peer)
16:10:06 → yin joins (~yin@user/zero)
16:13:24 → sp1ff joins (~user@c-24-21-45-157.hsd1.wa.comcast.net)
16:19:51 × billchenchina quits (~billchenc@103.152.35.21) (Quit: Leaving)
16:20:25 → billchenchina joins (~billchenc@103.152.35.21)
16:27:46 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds)
16:39:45 × petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
16:41:03 → _xor8 joins (~xor@ip-208-102-243-175.dynamic.fuse.net)
16:42:35 × _xor quits (~xor@ip-208-102-243-175.dynamic.fuse.net) (Ping timeout: 264 seconds)
16:42:35 _xor8 is now known as _xor
16:45:40 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
16:56:05 → petrichor joins (~znc-user@user/petrichor)
16:57:32 <ph88> [Leary], something is not quite right https://play.haskell.org/saved/R4jW1YVV
16:59:34 <[Leary]> "Use UndecidableSuperClasses to accept this"
16:59:42 <monochrom> Again, "instance ... => Foo a" means that every type is a Foo instance. (Oh, the ... conditions are checked later and cause hard errors, not as preconditions.)
17:00:47 <monochrom> You should simply enable ConstraintKinds and write "type (&) c1 c2 a = (c1 a, c2 a)"
17:01:01 <[Leary]> No, that doesn't suffice for their use-case.
17:05:32 → tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
17:08:56 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:10:04 × nullie quits (~nullie@2a01:4f8:c2c:6177::1) (Quit: WeeChat 4.1.1)
17:10:28 → nullie joins (~nullie@nuremberg.nullie.name)
17:10:53 <ph88> [Leary], will allow you to write `Entity (HasDataID & GetMessage)`. Do you mean data Entity ?
17:15:55 → target_i joins (~target_i@user/target-i/x-6023099)
17:16:34 × mei quits (~mei@user/mei) (Remote host closed the connection)
17:19:31 <[Leary]> ph88: Yes? I mean the type constructor defined by the `data Entity ...` declaration in your first paste.
17:20:31 <glguy> Maybe you want to bake the idea of multiple constraints into your entity type? https://play.haskell.org/saved/cMgRB0yD
17:21:27 <glguy> I did an example of this style a while back https://github.com/glguy/operations/blob/master/src/Example.hs
17:22:44 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
17:23:00 → mei joins (~mei@user/mei)
17:23:03 <ph88> [Leary], from my second paste https://play.haskell.org/saved/nsO7Fn41 when i move stuff from GetMessage (user part) into data Entity (library part) it defeats the goal. A creative idea nonetheless i will keep it in mind for other situations
17:24:47 <ph88> glguy, cool i'll play around with that see how it goes
17:24:48 × nullie quits (~nullie@nuremberg.nullie.name) (Quit: WeeChat 4.1.1)
17:25:11 → nullie joins (~nullie@nuremberg.nullie.name)
17:25:53 × chele quits (~chele@user/chele) (Remote host closed the connection)
17:27:31 → kimiamania joins (~76637481@user/kimiamania)
17:30:49 × nullie quits (~nullie@nuremberg.nullie.name) (Quit: WeeChat 4.1.1)
17:31:07 → nullie joins (~nullie@nuremberg.nullie.name)
17:41:13 <ph88> glguy, what are the symbols on line 14 and 20 in the gists ?
17:42:11 <glguy> ∈ is pronounced "element of" and ⊆ is pronounced "subset of or equal to"
17:42:39 <ph88> by the way, this reminds me of the effectful library, looks similar to how to compose effects
17:43:06 <glguy> so on line 14 it's a constraint that Show is an element of the list (cs), 20 is that the list [Show] is a subset of the list cs . They're two ways to do write the same idea
17:44:20 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
17:45:05 × ubert quits (~Thunderbi@p200300ecdf1a442dbe8e8c8f9360db77.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
17:50:55 <[Leary]> ph88: I think you've misunderstood. The `data` declaration in the library part doesn't need to change, the /user/ just uses the type at `Entity (c & GetMessage)` instead of `Entity c`.
17:54:46 <[Leary]> glguy: Just BTW, the bare constraint is already powerful enough without the list. `class Null` ~ []; `class (c1 & c2) a` ~ c1 ++ c2; `type c <: cs = (forall x. cs x => c x) :: Constraint` ~ c subset cs.
17:58:01 <[Leary]> Ah, though I guess that subset is actually just elem, due to QuantifiedConstraints limitations.
17:58:13 <glguy> that repository predates quantified constraints
18:02:18 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:08:38 <ph88> [Leary], maybe i misunderstood. When i try to use your suggestion i'm not sure how it would work https://play.haskell.org/saved/KPj9Vxob
18:16:44 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
18:30:06 <ph88> glguy, i adapted your code. It works with 2 constraints. Why does it fail with one? https://play.haskell.org/saved/EAupqGhV
18:31:29 × califax quits (~califax@user/califx) (Remote host closed the connection)
18:31:32 <ph88> glguy, this type checks https://play.haskell.org/saved/EAupqGhV but it carries Op2 into class of Op1 .. they need to be separate
18:31:51 × petrichor quits (~znc-user@user/petrichor) (Ping timeout: 268 seconds)
18:33:35 → califax joins (~califax@user/califx)
18:34:31 <glguy> ph88: you need '[Op1]
18:34:39 <[Leary]> ph88: I can't help much when I don't know just what it is you're struggling to achieve---the line where you've commented ?? was already, err, /mysterious/ to me from the start. That said, you probably want `type c <: cs = (forall x. cs x => c x) :: Constraint` (library-side) and `instance GetMessage <: cs => GetMessage (Entity cs)` (user-side).
18:34:52 → petrichor joins (~znc-user@user/petrichor)
18:38:38 <ph88> glguy, thanks
18:39:40 × califax quits (~califax@user/califx) (Remote host closed the connection)
18:40:53 → califax joins (~califax@user/califx)
18:42:12 <glguy> [Leary]: adapted https://github.com/glguy/operations/blob/quantifiedconstraints/src/Example.hs
18:43:39 × JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
18:43:57 → JimL joins (~quassel@89.162.16.26)
18:46:00 <[Leary]> glguy: Nice, looks a bit prettier at least.
18:46:50 <glguy> Fwiw I don't recommend using either this or the previous version. It's just exploring the possible
18:48:36 <ncf> your ⊆ is backwards
18:49:07 × raym quits (~ray@user/raym) (Ping timeout: 268 seconds)
18:49:34 <ncf> oh no i see it's a projection
18:51:21 <ncf> like, instead of saying "the cs objects are a subset of the Show objects" (cs ⊆ Show) you're saying "Show is a member of the list of constraints represented by cs, so that you can project it out" (Show ⊆ cs)
18:55:35 × JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
18:55:55 → JimL joins (~quassel@89.162.16.26)
18:57:02 → suvid joins (~suvid@103.144.93.164)
18:57:09 × suvid quits (~suvid@103.144.93.164) (Remote host closed the connection)
18:57:46 × califax quits (~califax@user/califx) (Remote host closed the connection)
18:58:43 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
18:59:26 → califax joins (~califax@user/califx)
18:59:56 <glguy> ncf: yeah, maybe the other way around makes more sense; I was still in the list of constraints mindset
19:00:47 → raym joins (~ray@user/raym)
19:07:37 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds)
19:08:53 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
19:10:13 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
19:10:58 → fliife joins (~fliife@user/fliife)
19:14:40 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
19:20:12 → euphores joins (~SASL_euph@user/euphores)
19:28:41 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
19:33:23 → emmanuelux joins (~emmanuelu@user/emmanuelux)
19:40:52 <[Leary]> I suppose the most direct unicode name would be: cs ⊢ c := forall x. cs x => c x
19:41:57 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds)
19:45:50 <ncf> looks like a natural transformation to me, but => is already taken
19:48:28 <EvanR> there's like 50 different unicode =>'s xD
19:48:42 <EvanR> an embarrassment of riches
19:49:55 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
19:49:55 ChanServ sets mode +v haskellbridge
19:52:28 × califax quits (~califax@user/califx) (Remote host closed the connection)
19:54:23 → califax joins (~califax@user/califx)
19:56:43 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
19:56:52 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
19:57:31 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
19:57:31 ChanServ sets mode +v haskellbridge
20:00:19 × califax quits (~califax@user/califx) (Remote host closed the connection)
20:02:00 → califax joins (~califax@user/califx)
20:02:38 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:03:28 <Rembane> \o/
20:03:41 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:04:32 → jmdaemon joins (~jmdaemon@user/jmdaemon)
20:05:38 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
20:06:50 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:06:52 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:07:02 <geekosaur> uh
20:08:16 <EvanR> bifrost has returned
20:11:31 → kadir joins (~kadir@88.251.51.100)
20:11:32 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:11:33 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:12:02 × TonyStone quits (~TonyStone@user/TonyStone) (Ping timeout: 252 seconds)
20:12:08 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
20:12:54 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
20:12:54 ChanServ sets mode +v haskellbridge
20:14:34 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:14:34 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:15:23 × notzmv quits (~daniel@user/notzmv) (Ping timeout: 256 seconds)
20:16:00 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
20:17:44 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:17:45 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:19:23 <geekosaur> ble. matterbridge is seriously messed up
20:19:24 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:19:25 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:19:32 <geekosaur> guess it's time to look into heisenbridge
20:21:14 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:21:15 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:21:56 <haskellbridge> <s​m> welcome back geekosaur !
20:23:28 × addfb3 quits (~dante@user/addfb3) (Remote host closed the connection)
20:23:32 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
20:23:53 → addfb3 joins (~dante@user/addfb3)
20:24:05 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
20:24:05 ChanServ sets mode +v haskellbridge
20:26:56 <haskellbridge> <g​eekosaur> okay, bridge should finally be back up. may be a bit slow as it processes two weeks' worth of messages in other rooms
20:26:57 <haskellbridge> <g​eekosaur> there will be another outage sometime tomorrow when they switch my network over
20:26:59 <haskellbridge> <s​m> welcome back geekosaur !
20:27:10 <geekosaur> argh
20:27:13 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
20:29:41 → matt3 joins (~matt@24-111-26-254-static.midco.net)
20:30:07 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds)
20:30:13 × hueso quits (~root@user/hueso) (Read error: Connection reset by peer)
20:30:22 × matt3 quits (~matt@24-111-26-254-static.midco.net) (Client Quit)
20:30:42 × petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
20:31:17 → hueso joins (~root@user/hueso)
20:31:55 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
20:37:25 → pavonia joins (~user@user/siracusa)
20:39:54 → sawilagar joins (~sawilagar@user/sawilagar)
20:44:51 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
20:47:30 × ph88 quits (~ph88@2a02:8109:9e26:c800:8347:c769:dd97:86a2) (Remote host closed the connection)
20:59:21 → jmdaemon joins (~jmdaemon@user/jmdaemon)
20:59:30 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
20:59:30 ChanServ sets mode +v haskellbridge
21:05:42 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
21:06:01 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds)
21:07:02 → visilii_ joins (~visilii@188.254.126.77)
21:08:13 → gmg joins (~user@user/gehmehgeh)
21:10:11 × visilii quits (~visilii@217.107.125.158) (Ping timeout: 264 seconds)
21:10:23 → jmdaemon joins (~jmdaemon@user/jmdaemon)
21:10:48 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds)
21:14:34 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
21:15:04 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
21:15:04 ChanServ sets mode +v haskellbridge
21:15:04 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Read error: Connection reset by peer)
21:15:12 × califax quits (~califax@user/califx) (Remote host closed the connection)
21:15:26 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
21:15:26 ChanServ sets mode +v haskellbridge
21:15:38 → califax joins (~califax@user/califx)
21:21:38 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
21:21:43 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
21:23:30 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
21:23:30 ChanServ sets mode +v haskellbridge
21:27:30 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
21:29:53 → haskellbridge joins (~haskellbr@syn-069-135-003-034.biz.spectrum.com)
21:29:53 ChanServ sets mode +v haskellbridge
21:34:45 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
21:47:08 × haskellbridge quits (~haskellbr@syn-069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
21:53:14 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
21:58:58 → joeyadams joins (~joeyadams@2603:6010:5100:2ed:cfe3:13e2:96f6:9d2c)
22:11:08 → AlexNoo_ joins (~AlexNoo@5.139.232.131)
22:13:08 × kadir quits (~kadir@88.251.51.100) (Quit: WeeChat 4.2.2)
22:14:28 × AlexZenon quits (~alzenon@178.34.162.221) (Ping timeout: 268 seconds)
22:14:49 × AlexNoo quits (~AlexNoo@178.34.162.221) (Ping timeout: 256 seconds)
22:15:19 → zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
22:21:11 × ystael quits (~ystael@user/ystael) (Ping timeout: 256 seconds)
22:22:47 → AlexZenon joins (~alzenon@5.139.232.131)
22:26:10 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:26:25 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds)
22:31:07 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds)
22:46:03 → talismanick joins (~user@2601:644:937c:ed10::ae5)
22:47:23 → m257 joins (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca)
22:48:29 <talismanick> typeclass laws let us make intuitive assumptions about the behavior of any instance satisfying them, but you do have to prove it
22:48:31 <talismanick> but, in math, figuring out how to prove something is a big part of understanding it
22:49:03 <talismanick> just writing out the proofs for Reader, Writer, and State, I don't feel like I understand anything more for doing so
22:58:08 × yin quits (~yin@user/zero) (Remote host closed the connection)
23:01:01 <monochrom> I would not take "prove implies understanding" religiously. When it works, it works. When it doesn't, it doesn't, or at most maybe look for another proof approach that brings understanding.
23:02:36 <monochrom> Hell, in fact, we know in math of a lot of elementary proofs that only achieve being elementary, not furthering understanding, precisely because they avoid "advanced" structures that bring understanding.
23:07:07 <talismanick> what are some instances with nontrivial proofs?
23:08:04 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:09:52 ski . o O ( "Mathematics, morally" by Eugenia Cheng in 2004-01 at <https://eugeniacheng.com/wp-content/uploads/2017/02/cheng-morality.pdf> )
23:15:58 × acidjnk_new quits (~acidjnk@p200300d6e714dc64113083a2457f0359.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
23:17:08 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Remote host closed the connection)
23:17:58 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
23:18:54 <dolio> I've been reading a book with some people, and it seems like most of the proofs are less believable than the facts they state.
23:21:31 → Lycurgus joins (~georg@user/Lycurgus)
23:21:47 <Lycurgus> 'understanding' - that's a feel innit?
23:22:41 <Lycurgus> a feel of cognition
23:24:24 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer)
23:24:37 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
23:25:08 <Lycurgus> feel, qualia, obscure thing
23:26:05 <Lycurgus> without qualification that is; demonstrated understanding brings you back
23:27:00 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
23:40:05 <Hecate> tomsmeding: eyo, do you want a PR to enable linear-base for GHC 9.10 on the playground?
23:40:31 × Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
23:42:17 <ski> presumably understanding is objective insofar as it allows someone to better predict, diagnose, design
23:54:55 × internatetional quits (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) (Quit: WeeChat 4.2.2)
23:55:43 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)

All times are in UTC on 2024-05-17.