Home liberachat/#haskell: Logs Calendar

Logs on 2024-08-29 (liberachat/#haskell)

00:00:03 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Quit: roll for dice... hmm, no dice)
00:07:11 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:11:33 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
00:22:36 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:27:56 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
00:38:27 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:40:20 athan_ joins (~athan@syn-098-153-145-140.biz.spectrum.com)
00:43:10 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
00:51:45 tt123109783243 joins (~tt1231@syn-075-185-104-199.res.spectrum.com)
00:53:53 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:58:27 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
01:01:37 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
01:01:52 × az181 quits (~az181@bmly-12-b2-v4wan-164596-cust791.vm4.cable.virginm.net) (Ping timeout: 252 seconds)
01:09:18 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:11:13 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds)
01:13:20 justsomeguy joins (~justsomeg@user/justsomeguy)
01:14:05 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
01:14:42 ddellacosta joins (~ddellacos@ool-44c73c8f.dyn.optonline.net)
01:17:53 × jjhoo quits (~jahakala@user/jjhoo) (Ping timeout: 245 seconds)
01:20:07 × ddellacosta quits (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Read error: Connection reset by peer)
01:24:42 × madjestic quits (~madjestic@103-135-99-95.ftth.glasoperator.nl) (Ping timeout: 246 seconds)
01:24:44 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:25:44 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
01:26:25 ddellacosta joins (~ddellacos@ool-44c73c8f.dyn.optonline.net)
01:28:49 × tt123109783243 quits (~tt1231@syn-075-185-104-199.res.spectrum.com) (Ping timeout: 260 seconds)
01:29:22 tt123109783243 joins (~tt1231@syn-075-185-104-199.res.spectrum.com)
01:30:08 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds)
01:30:48 × Typedfern quits (~Typedfern@91.red-83-37-29.dynamicip.rima-tde.net) (Ping timeout: 245 seconds)
01:34:49 jjhoo joins (~jahakala@user/jjhoo)
01:40:46 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:43:25 Typedfern joins (~Typedfern@91.red-83-37-29.dynamicip.rima-tde.net)
01:45:21 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
01:47:06 × krei-se quits (~krei-se@p57af29d2.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
01:48:22 krei-se joins (~krei-se@p57af29f0.dip0.t-ipconnect.de)
01:55:01 × spew quits (~spew@2806:2a0:1522:8662::cebf) (Quit: spew)
01:56:12 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:57:15 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds)
02:00:48 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
02:03:37 machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
02:05:17 <haskellbridge> <Bowuigi> dmj` haven't done much with Lean tbh, but it likely has codata types via suspension, so sort of?
02:08:38 <haskellbridge> <Bowuigi> thirdofmay18081814goya there are a ton of attempts at getting inference for higher rank polymorphism. Apparently the "Complete and easy inference for higher rank types" cites some of the most important ones
02:11:38 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:15:27 benjaminl joins (~benjaminl@user/benjaminl)
02:15:31 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Quit: leaving)
02:15:52 machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
02:16:09 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
02:16:39 × benjaminl_ quits (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) (Ping timeout: 252 seconds)
02:27:03 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:32:04 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
02:38:07 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Quit: leaving)
02:38:22 madhavanmiui joins (~madhavanm@152.58.212.118)
02:38:25 machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
02:38:33 × madhavanmiui quits (~madhavanm@152.58.212.118) (Client Quit)
02:38:57 <haskellbridge> <thirdofmay18081814goya> Bowuigi: nice, thanks for the resource!
02:42:19 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:43:04 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds)
02:46:36 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
02:54:34 × sp1ff` quits (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Remote host closed the connection)
02:54:34 × sp1ff quits (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Remote host closed the connection)
02:57:44 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:01:33 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:01:34 × td_ quits (~td@i53870935.versanet.de) (Ping timeout: 260 seconds)
03:02:08 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
03:03:06 td_ joins (~td@i53870918.versanet.de)
03:08:48 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds)
03:13:09 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:13:30 aforemny joins (~aforemny@i59F516D8.versanet.de)
03:14:25 × aforemny_ quits (~aforemny@2001:9e8:6cc3:6400:e30f:2a23:e5e9:e455) (Ping timeout: 248 seconds)
03:17:41 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds)
03:18:56 × Eoco quits (~ian@128.101.131.218) (Quit: WeeChat 4.1.1)
03:23:59 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds)
03:24:05 Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
03:25:26 Lord_of_Life_ is now known as Lord_of_Life
03:28:35 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:33:54 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
03:34:18 Sgeo_ joins (~Sgeo@user/sgeo)
03:37:48 × Sgeo quits (~Sgeo@user/sgeo) (Ping timeout: 276 seconds)
03:41:34 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:44:00 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:47:02 <dmj`> Bowuigi: Adding lambda sets to Haskell sounds like a really cool idea
03:47:25 <dmj`> you can track the lambdas through the desugaring
03:48:33 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
03:48:34 × sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection)
03:59:25 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:03:38 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
04:06:23 sefidel joins (~sefidel@user/sefidel)
04:13:16 × sroso quits (~sroso@user/SrOso) (Quit: Leaving :))
04:14:51 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:17:22 × sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection)
04:17:51 sefidel joins (~sefidel@user/sefidel)
04:19:21 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
04:30:17 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:31:49 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds)
04:35:39 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
04:43:18 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:44:18 michalz joins (~michalz@185.246.207.197)
04:48:14 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
04:53:26 rosco joins (~rosco@183.171.74.47)
04:58:45 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:03:14 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
05:09:27 × echoreply quits (~echoreply@2001:19f0:9002:1f3b:5400:ff:fe6f:8b8d) (Ping timeout: 276 seconds)
05:11:10 echoreply joins (~echoreply@45.32.163.16)
05:11:18 × carbolymer quits (~carbolyme@dropacid.net) (Remote host closed the connection)
05:12:26 carbolymer joins (~carbolyme@dropacid.net)
05:12:42 Eoco joins (~ian@128.101.131.218)
05:14:10 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:18:45 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
05:22:35 rvalue joins (~rvalue@user/rvalue)
05:29:35 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:33:33 × jle` quits (~jle`@2603:8001:3b02:84d4:2809:1e29:1db7:65cb) (Ping timeout: 246 seconds)
05:33:54 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
05:34:39 jle` joins (~jle`@2603:8001:3b02:84d4:cf52:aad8:ec6d:eddd)
05:44:17 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:46:22 × rosco quits (~rosco@183.171.74.47) (Quit: Lost terminal)
05:48:43 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
05:55:14 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
05:59:42 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:02:15 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
06:03:01 Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
06:03:52 CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-71.web.vodafone.de)
06:04:44 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
06:05:43 bladelizard joins (~bladeliza@213.94.19.138)
06:10:13 × bladelizard quits (~bladeliza@213.94.19.138) (Ping timeout: 252 seconds)
06:15:09 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:19:46 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
06:20:14 gmg joins (~user@user/gehmehgeh)
06:21:48 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
06:22:34 gmg joins (~user@user/gehmehgeh)
06:25:17 acidjnk_new joins (~acidjnk@p200300d6e72cfb18ac0e327209850a07.dip0.t-ipconnect.de)
06:27:11 divya joins (~user@202.170.201.3)
06:30:35 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:34:49 Pixi` joins (~Pixi@user/pixi)
06:35:01 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
06:36:22 neuroevolutus joins (~neuroevol@37.19.200.148)
06:37:12 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
06:37:44 × neuroevolutus quits (~neuroevol@37.19.200.148) (Client Quit)
06:37:56 × Pixi quits (~Pixi@user/pixi) (Ping timeout: 255 seconds)
06:39:55 Pixi__ joins (~Pixi@user/pixi)
06:42:50 Pixi joins (~Pixi@user/pixi)
06:43:33 × Pixi` quits (~Pixi@user/pixi) (Ping timeout: 246 seconds)
06:45:18 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:45:39 × Pixi__ quits (~Pixi@user/pixi) (Ping timeout: 276 seconds)
06:47:38 bladelizard joins (~bladeliza@213.94.19.138)
06:49:06 × bladelizard quits (~bladeliza@213.94.19.138) (Remote host closed the connection)
06:50:51 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
06:51:51 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
06:52:43 × ft quits (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving)
06:53:52 × hueso quits (~root@user/hueso) (Ping timeout: 252 seconds)
06:56:49 × Pixi quits (~Pixi@user/pixi) (Quit: Leaving)
07:01:02 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
07:05:49 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
07:07:43 × aljazmc quits (~aljazmc@user/aljazmc) (Remote host closed the connection)
07:07:50 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
07:09:44 oo_miguel joins (~Thunderbi@78.10.207.45)
07:10:19 ash3en joins (~Thunderbi@p200300e7b71f94fba89838e14b44a860.dip0.t-ipconnect.de)
07:12:07 × ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Read error: Connection reset by peer)
07:12:26 ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com)
07:12:49 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds)
07:16:27 merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
07:16:37 × ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 248 seconds)
07:21:57 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
07:24:56 ash3en1 joins (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0)
07:26:36 × ash3en quits (~Thunderbi@p200300e7b71f94fba89838e14b44a860.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
07:26:37 ash3en1 is now known as ash3en
07:27:34 × aforemny quits (~aforemny@i59F516D8.versanet.de) (Ping timeout: 260 seconds)
07:35:40 aforemny joins (~aforemny@i59F516D8.versanet.de)
07:38:53 madjestic joins (~madjestic@77-63-76-204.mobile.kpn.net)
07:39:45 cfricke joins (~cfricke@user/cfricke)
07:46:04 rosco joins (~rosco@175.136.158.234)
07:50:41 × madjestic quits (~madjestic@77-63-76-204.mobile.kpn.net) (Ping timeout: 252 seconds)
07:53:43 × Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
08:00:04 × Batzy quits (~quassel@user/batzy) (Ping timeout: 260 seconds)
08:00:31 Batzy joins (~quassel@user/batzy)
08:04:16 mreh joins (~matthew@host86-160-168-12.range86-160.btcentralplus.com)
08:06:32 merijn joins (~merijn@77.242.116.146)
08:07:11 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
08:15:54 hueso joins (~root@user/hueso)
08:23:14 <albet70> hi there, is there segmentation library in haskell?
08:26:36 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:26:40 Square2 joins (~Square4@user/square)
08:32:01 × dysthesis quits (~dysthesis@user/dysthesis) (Quit: WeeChat 4.4.1)
08:32:12 simendsjo joins (~user@79.161.5.185)
08:42:47 rvalue- joins (~rvalue@user/rvalue)
08:43:29 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 255 seconds)
08:44:53 madjestic joins (~madjestic@213.208.215.120)
08:47:30 rvalue- is now known as rvalue
09:04:02 × madjestic quits (~madjestic@213.208.215.120) (Ping timeout: 252 seconds)
09:05:59 × tinwood quits (~tinwood@canonical/tinwood) (Changing host)
09:05:59 tinwood joins (~tinwood@user/tinwood)
09:06:02 <int-e> . o O ( https://en.wikipedia.org/wiki/Segmentation#Computing_and_communications )
09:08:52 califax_ joins (~califax@user/califx)
09:09:32 tomsmeding suspects https://en.wikipedia.org/wiki/Speech_segmentation
09:09:53 <tomsmeding> er, https://en.wikipedia.org/wiki/Text_segmentation
09:10:01 × chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds)
09:10:01 × califax quits (~califax@user/califx) (Ping timeout: 260 seconds)
09:10:09 califax_ is now known as califax
09:12:33 chiselfuse joins (~chiselfus@user/chiselfuse)
09:18:20 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:22:33 × califax quits (~califax@user/califx) (Remote host closed the connection)
09:22:56 califax joins (~califax@user/califx)
09:26:17 <Pozyomka> Is it possible to write a *total* function [a] -> [[a]] satisfying the following constraints? (a) The return value is the result of splitting the argument into chunks of length >= 1 but <= 3. (b) A chunk of length 1 is only allowed if the input list has length 1. (c) The recursive cases are either lumped together at the beginning or lumped together at the end, but not in the middle?
09:26:59 <tomsmeding> what do you mean with "the recursive cases"?
09:27:57 <tomsmeding> would it suffice to have the output chunk lengths be this: [1], [2], [3], [2,2], [2,3], [2,2,2], [2,2,3], etc.
09:28:38 az181 joins (~az181@bmly-12-b2-v4wan-164596-cust791.vm4.cable.virginm.net)
09:28:54 × cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
09:30:07 <Pozyomka> Such a function has to be defined using pattern matching and possibly recurring in some cases. Suppose there are 3 cases. If only one case is recursive, then it should be the top or the bottom one, not the middle one. If two cases are recursive, then the middle one should be one of them.
09:30:45 <Pozyomka> And, yes, [], [1], [2], [3], [2,2], [2,3], [2,2,2], [2,2,3], etc. is acceptable.
09:30:47 cfricke joins (~cfricke@user/cfricke)
09:31:12 <Pozyomka> It's annoying how un-googleable @ is.
09:31:23 <Pozyomka> (Not Haskell's fault, though.)
09:36:23 <tomsmeding> Pozyomka: https://paste.tomsmeding.com/1Ys69IVC ?
09:36:55 <tomsmeding> Pozyomka: in case you hadn't found yet, that's called an "as-pattern"
09:38:38 <Pozyomka> Ah, thanks. I had this, but the recursive case is in the middle: https://gist.github.com/eduardoleon/6df6ece235d7de7bf9b17407fe89285e
09:38:43 × az181 quits (~az181@bmly-12-b2-v4wan-164596-cust791.vm4.cable.virginm.net) (Ping timeout: 245 seconds)
09:39:41 <tomsmeding> Pozyomka: this is also an option https://paste.tomsmeding.com/ZJHa9XzF
09:40:08 <Pozyomka> That one breaks condition (b) above.
09:40:18 <tomsmeding> where?
09:40:27 <tomsmeding> i.e. for what input
09:40:39 <Pozyomka> (b) A chunk of length 1 is only allowed if the input list has length 1.
09:40:47 <Pozyomka> So take a list of length 3.
09:40:55 <tomsmeding> a list of length 3 doesn't match the first case
09:40:55 <Pozyomka> Oh, my bad.
09:40:57 <Pozyomka> I misread.
09:40:57 <tomsmeding> ;)
09:40:59 <Pozyomka> Sorry!
09:41:03 sawilagar joins (~sawilagar@user/sawilagar)
09:41:04 <tomsmeding> there's a whole lot of (:) there
09:41:15 <Pozyomka> Yeah, that's nice.
09:41:22 <Pozyomka> Then that's the one I'm taking. Thank you!
09:42:27 × simendsjo quits (~user@79.161.5.185) (Ping timeout: 276 seconds)
09:45:10 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
09:47:01 <mauke> tomsmeding: line 3 is redundant
09:48:49 <Pozyomka> What I'm really trying to do is re-implement Data.Sequence using *only* total functions everywhere. So I'm reading the finger trees paper, and there's this helper function “app3 :: FingerTree a -> [a] -> FingerTree a”, whose recursive case is when both FingerTree arguments are Deep. In this case, we take the left FingerTree's right finger (which is a list), the middle list, and the right
09:48:51 <Pozyomka> FingerTree's left finger (which is also a list), concatenate them, and chunk them as above, obtaining the list to be used in the recursive call.
09:49:03 <Pozyomka> ERRR
09:49:14 <Pozyomka> app3 :: FingerTree a -> [a] -> FingerTree a -> FingerTree a
09:51:18 <tomsmeding> mauke: no, because line two has right-hand side [] and not [[]]
09:51:56 madjestic joins (~madjestic@213.208.215.120)
09:51:59 <mauke> line 2 has rhs [[x]]
09:52:00 <tomsmeding> Pozyomka: do you want total functions, or functions that e.g. Agda can automatically prove total?
09:52:03 <tomsmeding> those are two different things
09:52:31 <tomsmeding> mauke: which paste are you referring to? :p
09:52:36 <tomsmeding> oh that one
09:52:50 <tomsmeding> how is it redundant?
09:52:53 <mauke> oh, there was another one :-)
09:53:15 <tomsmeding> oh line _three_
09:53:20 <mauke> > let f [] = []; f [x] = [[x]]; f [x,y,z] = [[x,y,z]]; f (x:y:zs) = [x,y] : f zs in f [1,2]
09:53:22 <lambdabot> [[1,2]]
09:53:23 <tomsmeding> it is!
09:53:26 <tomsmeding> funny
09:53:27 <Pozyomka> Functions that are total by some complicated argument that the type checker can't check are okay. But all the functions have to be total, including the helpers.
09:55:57 <tomsmeding> Pozyomka: have you seen this one? https://tomsmeding.com/vang/eRvkwg/3406088.3409026.pdf
09:56:01 <Pozyomka> Let me see.
09:56:12 <tomsmeding> it's been a while since I read it, and I'm not sure if all the functions in there are total
09:56:18 <tomsmeding> but I recall it was a very nice exposition
09:59:03 <Pozyomka> Oh, his toTuples in the right column of page 4 is your first version, after deleting the case mauke identified as redundant.
09:59:37 ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com)
10:01:25 <Pozyomka> Thank you!
10:02:44 ZharMeny joins (~ZharMeny@user/ZharMeny)
10:03:53 simendsjo joins (~user@79.161.5.185)
10:04:48 <tomsmeding> oh haha
10:05:34 <tomsmeding> (this paper is behind a paywall normally; the link I posted invalidates after 24h, so save the PDF if you want to read it later)
10:06:00 × madjestic quits (~madjestic@213.208.215.120) (Ping timeout: 252 seconds)
10:06:46 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-71.web.vodafone.de) (Read error: Connection reset by peer)
10:06:52 <Pozyomka> Thank you again!
10:07:09 <tomsmeding> :)
10:09:46 × krei-se quits (~krei-se@p57af29f0.dip0.t-ipconnect.de) (Quit: ZNC 1.9.1 - https://znc.in)
10:11:33 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
10:15:26 CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-71.web.vodafone.de)
10:16:54 krei-se joins (~krei-se@p57af29f0.dip0.t-ipconnect.de)
10:20:36 metabulation joins (~wootehfoo@user/wootehfoot)
10:23:42 merijn joins (~merijn@77.242.116.146)
10:23:50 × ss4 quits (~wootehfoo@user/wootehfoot) (Ping timeout: 255 seconds)
10:27:39 × troydm quits (~troydm@user/troydm) (Ping timeout: 260 seconds)
10:29:23 son0p joins (~ff@2800:e2:f80:ee7::1)
10:30:44 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
10:33:38 Smiles joins (uid551636@id-551636.lymington.irccloud.com)
10:34:41 __monty__ joins (~toonn@user/toonn)
10:38:36 merijn joins (~merijn@77.242.116.146)
10:47:10 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
10:53:14 <[exa]> Is there some kindof lens-less zoom for State and StateT? like
10:53:45 <[exa]> zoom :: (s->t) -> (t->s) -> StateT t m a -> StateT s m a
10:54:05 <[exa]> not a big issue writing this myself but see, library version would be better
10:55:07 tomsmeding actually wrote almost precisely that yesterday
10:55:30 <tomsmeding> except the t->s was s->t->s in case t is smaller than s and you need the original s to restore the full "new s"
10:56:34 <tomsmeding> hm, actually I wrote these two:
10:56:38 <tomsmeding> withMoreState :: Functor m => b -> StateT (s, b) m a -> StateT s m (a, b)
10:56:45 <tomsmeding> withLessState :: Functor m => (s -> (s', b)) -> (s' -> b -> s) -> StateT s' m a -> StateT s m a
10:57:16 <haskellbridge> <mauke> ... I was just thinking about running a subcomputation on parts of my state
10:57:20 <tomsmeding> used like `withMoreState _ $ traverse (\x -> withLessState _) _`
11:00:06 toys parts (~toys@user/toys) (WeeChat 4.4.1)
11:09:55 × rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal)
11:10:45 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 248 seconds)
11:11:00 ZharMeny` joins (~ZharMeny@user/ZharMeny)
11:13:27 × ash3en quits (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0) (Ping timeout: 276 seconds)
11:17:28 ZharMeny` is now known as ZharMeny
11:20:38 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:30:36 <[exa]> tomsmeding: oh nice
11:31:06 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Read error: Connection reset by peer)
11:31:16 ZharMeny` joins (~ZharMeny@user/ZharMeny)
11:31:36 × son0p quits (~ff@2800:e2:f80:ee7::1) (Ping timeout: 246 seconds)
11:33:15 ZharMeny` is now known as ZharMeny
11:33:31 <tomsmeding> [exa]: was this also your usecase? :P
11:37:11 × Square2 quits (~Square4@user/square) (Remote host closed the connection)
11:37:50 Square2 joins (~Square4@user/square)
11:37:53 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 245 seconds)
11:43:04 × Square2 quits (~Square4@user/square) (Ping timeout: 272 seconds)
11:56:05 esnos joins (~user@176.106.34.161)
11:58:38 <esnos> Hi, do you know why this command in ghci `:t pure @((->) String)` gives me error `No instance for (Applicative ((->) String)) arising from a use of ‘pure’ In the expression: pure @((->) String)`
11:59:43 <tomsmeding> % :t pure @((->) String)
11:59:43 <yahb2> pure @((->) String) :: a -> String -> a
12:00:14 <tomsmeding> works for me
12:04:14 <esnos> Ok, I know what I did, I hide Applicative from prelude for learning purpose...
12:04:30 <tomsmeding> ah :)
12:16:37 ski joins (~ski@145.224.119.31)
12:16:49 justsomeguy joins (~justsomeg@user/justsomeguy)
12:21:16 <[exa]> tomsmeding: basically, just needed a tiny bit of extra state somewhere which was later basically dropped
12:21:31 <tomsmeding> ah
12:23:14 × tt123109783243 quits (~tt1231@syn-075-185-104-199.res.spectrum.com) (Ping timeout: 248 seconds)
12:26:26 <Axman6> [exa]: (and tomsmeding) https://hackage.haskell.org/package/lens-5.2.2/docs/Control-Lens-Zoom.html
12:26:54 × simendsjo quits (~user@79.161.5.185) (Ping timeout: 246 seconds)
12:27:47 <Axman6> you can write do foo; zoom focus (do bar; baz); quux, where bar and baz will see only what focus points to
12:28:00 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
12:28:15 <Axman6> :t zoom _1
12:28:16 <lambdabot> (Zoom m n b s, Field1 s s b b, Functor (Zoomed m c)) => m c -> n c
12:29:03 <Axman6> Magnify lets you do the same wthing with Reader
12:29:30 <tomsmeding> Axman6: note that [exa] said "lens-less" :p
12:29:45 <Axman6> oh, I thought they asked for lens specifically!
12:29:51 <Axman6> well, just use lens, because it's great
12:30:09 <tomsmeding> :p
12:30:28 × ddellacosta quits (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Ping timeout: 252 seconds)
12:30:56 simendsjo joins (~user@79.161.5.185)
12:34:00 <dminuoso> [exa]: https://hackage.haskell.org/package/optics-extra-0.4.2.1/docs/Optics-Zoom.html#v:zoom
12:34:01 <[exa]> Axman6: yeah I was kinda trying to pull in another gigaton of dependencies
12:34:03 <dminuoso> It's lens-less!
12:34:38 <[exa]> optically valid, yes. :D
12:34:41 <[exa]> thanks guys!
12:35:07 <dminuoso> It has far better optics for when something goes wrong, yes.
12:36:36 ZharMeny` joins (~ZharMeny@user/ZharMeny)
12:37:38 × ell quits (~ellie@user/ellie) (Quit: Leaving)
12:38:38 ell joins (~ellie@user/ellie)
12:38:48 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 272 seconds)
12:39:52 ZharMeny` is now known as ZharMeny
12:45:18 cfricke joins (~cfricke@user/cfricke)
12:48:57 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
12:50:05 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 265 seconds)
12:54:38 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 272 seconds)
12:58:30 Alleria joins (~Alleria@user/alleria)
12:58:58 <jackdk> https://hackage.haskell.org/package/microlens-mtl-0.2.0.3/docs/Lens-Micro-Mtl.html#v:zoom
12:59:12 × simendsjo quits (~user@79.161.5.185) (Read error: Connection reset by peer)
13:00:05 simendsjo joins (~user@79.161.5.185)
13:12:58 justsomeguy joins (~justsomeg@user/justsomeguy)
13:13:00 × Blasius quits (~Blasius@5ec169d9.skybroadband.com) (Ping timeout: 252 seconds)
13:13:05 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:19:59 × michalz quits (~michalz@185.246.207.197) (Read error: Connection reset by peer)
13:20:17 michalz joins (~michalz@185.246.207.218)
13:20:42 × mreh quits (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 252 seconds)
13:20:45 × statusbot quits (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Remote host closed the connection)
13:20:56 statusbot joins (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com)
13:28:04 Square2 joins (~Square4@user/square)
13:29:34 Blasius joins (~Blasius@5ec169d9.skybroadband.com)
13:31:43 <mauke> https://hackage.haskell.org/package/microlens-th-0.4.3.15/docs/Lens-Micro-TH.html#g:2 this is weird
13:32:02 <mauke> why do I need the bogus type? can't I just do $(makeLenses ''Foo)?
13:34:19 cfricke joins (~cfricke@user/cfricke)
13:38:56 <c_wraith> mauke: that *looks* like confused docs.
13:40:03 <c_wraith> oh. I see what's going on.
13:40:18 <c_wraith> implicit splices strike again
13:40:38 <c_wraith> they were a mistake in the first place, and remain a mistake now
13:41:00 <c_wraith> That's about getting ghci to recognize that you're making a splice, not just running an expression
13:41:11 <mauke> yes, that's why I suggested using $( ) instead
13:41:27 <c_wraith> explicit splices are forgotten knowledge, I guess
13:41:41 <c_wraith> can we please remove implicit splices?
13:42:07 zmt01 joins (~zmt00@user/zmt00)
13:43:01 <mauke> alternatively, just use 'import Prelude' as a no-op declaration
13:45:33 × zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 276 seconds)
13:47:04 × justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6)
13:47:58 ash3en joins (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0)
13:53:42 × simendsjo quits (~user@79.161.5.185) (Ping timeout: 252 seconds)
13:58:49 ZharMeny` joins (~ZharMeny@user/ZharMeny)
13:59:17 Sgeo joins (~Sgeo@user/sgeo)
14:01:59 <dminuoso> So strange, I did not even know about implicit splices.
14:02:03 <dminuoso> I've always used explicit splices.
14:02:24 <dminuoso> Does that mean I'm.. special?
14:02:28 <c_wraith> sure!
14:02:59 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 255 seconds)
14:04:18 ZharMeny` is now known as ZharMeny
14:09:03 Guest40 joins (~Guest40@2401:4900:51f7:7237:568:1443:c04d:536e)
14:15:05 × Guest40 quits (~Guest40@2401:4900:51f7:7237:568:1443:c04d:536e) (Quit: Client closed)
14:18:14 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 272 seconds)
14:19:49 × Teacup_ quits (~teacup@user/teacup) ()
14:20:11 Teacup joins (~teacup@user/teacup)
14:24:15 × Alleria quits (~Alleria@user/alleria) (Remote host closed the connection)
14:29:27 mreh joins (~matthew@host86-160-168-12.range86-160.btcentralplus.com)
14:43:40 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-71.web.vodafone.de) (Read error: Connection reset by peer)
14:47:08 CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-71.web.vodafone.de)
14:50:20 spew joins (~spew@201.141.99.170)
14:52:36 swamp_ joins (~zmt00@user/zmt00)
14:54:08 tabemann_ joins (~tabemann@2600:1700:7990:24e0:8704:9636:2bf6:fb61)
14:56:24 × zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 276 seconds)
14:56:24 × tabemann__ quits (~tabemann@2600:1700:7990:24e0:471d:6865:e425:eedb) (Ping timeout: 276 seconds)
15:05:55 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-71.web.vodafone.de) (Read error: Connection reset by peer)
15:06:09 × Blasius quits (~Blasius@5ec169d9.skybroadband.com) (Ping timeout: 276 seconds)
15:06:37 CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-71.web.vodafone.de)
15:11:19 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-71.web.vodafone.de) (Ping timeout: 260 seconds)
15:11:27 Blasius joins (~Blasius@5ec169d9.skybroadband.com)
15:11:44 CrunchyFlakes joins (~CrunchyFl@ip-109-42-113-52.web.vodafone.de)
15:11:58 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
15:21:05 × metabulation quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
15:28:09 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-113-52.web.vodafone.de) (Read error: Connection reset by peer)
15:31:45 CrunchyFlakes joins (~CrunchyFl@ip-109-42-113-52.web.vodafone.de)
15:35:42 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
15:36:50 raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
15:41:12 L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
15:43:17 cfricke joins (~cfricke@user/cfricke)
15:49:55 × cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
15:51:38 machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
15:55:50 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-113-52.web.vodafone.de) (Read error: Connection reset by peer)
15:57:25 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
15:57:57 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
15:58:00 Alleria joins (~Alleria@user/alleria)
15:59:05 CrunchyFlakes joins (~CrunchyFl@ip-109-42-113-52.web.vodafone.de)
16:08:07 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-113-52.web.vodafone.de) (Read error: Connection reset by peer)
16:08:19 × ash3en quits (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0) (Ping timeout: 260 seconds)
16:08:32 CrunchyFlakes joins (~CrunchyFl@ip-109-42-113-52.web.vodafone.de)
16:09:08 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-113-52.web.vodafone.de) (Read error: Connection reset by peer)
16:13:19 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-127.web.vodafone.de)
16:14:30 econo_ joins (uid147250@id-147250.tinside.irccloud.com)
16:14:37 Artea joins (~Lufia@artea.pt)
16:19:47 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
16:25:36 takuan joins (~takuan@178-116-218-225.access.telenet.be)
16:28:37 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-127.web.vodafone.de) (Read error: Connection reset by peer)
16:31:23 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
16:31:42 AWizzArd joins (~code@user/awizzard)
16:32:01 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-127.web.vodafone.de)
16:32:09 lxsameer joins (~lxsameer@Serene/lxsameer)
16:34:01 madjestic joins (~madjestic@77-63-78-93.mobile.kpn.net)
16:36:46 <lxsameer> hey friends, do you know how to exclude certain characters from a megaparser Parser?
16:45:10 <ncf> noneOf
16:46:01 × madjestic quits (~madjestic@77-63-78-93.mobile.kpn.net) (Ping timeout: 252 seconds)
16:48:12 <lxsameer> cheers
16:48:30 <tomsmeding> there is always 'satisfy (`notElem` _)'
16:49:08 <tomsmeding> sure, 'noneOf' is more readable and shorter, but for basic character parsers like this one doesn't need to get stuck on trying to find the appropriate pre-made utility :)
16:50:27 <lxsameer> thank you both
16:51:53 <lxsameer> noneOf seems to be dropped in 9.6
16:52:22 <lxsameer> oh I'm wrong, nvm
16:52:45 × Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
16:57:36 × Alleria quits (~Alleria@user/alleria) (Ping timeout: 244 seconds)
17:05:20 JuanDaugherty joins (~juan@user/JuanDaugherty)
17:19:08 <monochrom> I am very special. I prefer explicit splices, explicit forall, explicit conversion between numeric types, explicit lambdas and argument names (don't laugh, look at those people who want "_ + _" or "# + #" to mean \x y -> x + y), ...
17:20:37 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
17:22:42 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
17:24:22 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Quit: Lost terminal)
17:24:42 × divya quits (~user@202.170.201.3) (Remote host closed the connection)
17:27:06 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-127.web.vodafone.de) (Ping timeout: 252 seconds)
17:28:11 <mauke> how about operator sections?
17:30:44 nyc joins (~nyc@syn-067-250-055-000.res.spectrum.com)
17:30:46 × nyc quits (~nyc@syn-067-250-055-000.res.spectrum.com) (Changing host)
17:30:46 nyc joins (~nyc@user/nyc)
17:32:29 <tomsmeding> with you on all but the explicit forall
17:34:20 son0p joins (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20)
17:37:35 <monochrom> I use sections myself, but when teaching I don't use them. Sometimes I use (:), but also explain "if you don't understand/like that syntax, it's \x xs -> x : xs". I also never used $, I wrote "\f x -> f x".
17:38:02 <monochrom> err, I never taught $. Sometimes I use it myself.
17:39:41 <monochrom> My course is not supposed to be a Haskell course, just a PL course in which I happen to find Haskell suitable to convey PL topics, so there are a lot of Haskell goodies I omit. I don't even teach newtype.
17:43:01 <EvanR> read my lips: no newtypes
17:44:03 <nyc> uncurry3 RWS.execRWST . (, readerEnv, initialState) is something I write pretty often.
17:49:26 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
17:50:05 rvalue joins (~rvalue@user/rvalue)
17:50:18 <monochrom> Actually something interesting happened when I used "data" instead of "newtype". You know the simple version of parser monad, except I use "data": "data P a = P(String -> Maybe (a, String))".
17:50:44 <monochrom> Then I coded up the Alternative instance, "P f1 <|> P f2 = ..."
17:51:11 <nyc> curryNminusK $ uncurryN nAryFunc . (,, x,,, y,, z,,,) or whatever is an easy way to fill in some args & leave others available for application it seems.
17:51:48 <monochrom> And eventually I also have parsers like "foo = bar <|> something that has a recursive call to foo".
17:52:07 <monochrom> And that hangs because I use "data" instead of "newtype". :)
17:52:27 ski wants `(2 + 3 *)' to mean `\x -> 2 + 3 * x'
17:53:10 <nyc> Speaking of parsers, I could use a library for manipulating some sort of IR for regular expressions esp. if there's some sort of regex simplifier or minimizer out there.
17:54:44 <mauke> ski: that's a syntactic abomination
17:54:56 <mauke> unless you also want to allow (2 + * 3)
17:55:02 <mauke> then it's a different syntactic abomination
17:55:11 <monochrom> tomsmeding: I am OK with implicit forall when one just wants to learn basic Haskell (say, Haskell 2010). In broader contexts and probably outside Haskell, implicit forall is why people, for example, misunderstand induction.
17:55:22 ski 's also reminded of monadic abstractions in SML including a primitive val delay : (unit -> 'a t) -> 'a t in order to allow recursive, parameterless, parser definitions (getting around the value restriction, which forbids defining recursive non-values (determined syntactically))
17:55:22 <nyc> OTOH maybe I could just sort of extend things for regex-with-pcre, throw a huge nasty regex IR at the regex to DFA compiler from some sort of notational extension & then just wing things with runghc or similar.
17:55:35 <ski> mauke : nah, only at the two ends
17:55:41 <tomsmeding> monochrom: oh I was definitely talking about the forall in Haskell type signatures. The \forall in logic is a completely different story
17:56:37 <nyc> As long as it's not like a diversion from programming the things I'm trying to use it as a tool to help program.
17:56:38 <ski> yeah, monochrom, when teaching induction, i think one should start with using explicit universals, to begin with
17:56:38 <monochrom> With implicit forall, the induction step goes as "p n => p (n+1)". People are trained to "disambiguate" that to "(forall n. p n) => (forall n. p (n+1))", and conclude that induction is circular logic.
17:57:31 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
17:57:43 <tomsmeding> monochrom: disclaimer: I have much less experience than you in teaching this stuff, but I haven't seen that particular misunderstanding yet
17:57:58 <ski> .. or `(n = k => P n) => (n = k + 1 => P n)'
17:58:17 <monochrom> That problem happens at the highschool level. :)
17:59:03 <monochrom> I think most universities happen to do a good job making quantifiers explicit, by design or by happy coincidence.
18:00:17 ski also thinks every math student, at uni/college level, should early on get expoed to (the practice of) natural deduction
18:00:40 <mauke> how is that circular?
18:00:50 <mauke> looks more like trivial to me
18:01:29 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
18:03:20 <monochrom> It is both. "circular" is a meta-level observation or interpretation.
18:05:31 <dolio> When would they be trained to disambiguate that way?
18:08:10 <monochrom> Highschool teaches the very simple model "free variables in a sentence are universally quantifier when the question asks you to prove something". Then one considers "p n" and "p (n+1)" to be separate sentences.
18:08:13 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
18:09:28 <monochrom> In fact, there is no "implies" connective in highschool logic. There are two sentences: "Assume p n, fullstop.", "Prove p (n+1), fullstop". Two sentences.
18:11:24 <dolio> Okay, well, that is indeed quite bad, if they're teaching that you just quantify every individual piece whenever you see it.
18:11:50 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 255 seconds)
18:13:03 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
18:14:50 <ski> i remember it took me a while to realize that the direction of the implication arrow, when solving an equation, determined whether you covered all solutions (but maybe had false positives), or you only had true solutions (but maybe missed some) .. (or both, in which case you had both completeness and soundness)
18:16:18 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
18:16:23 × hgolden_ quits (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) (Read error: Connection reset by peer)
18:18:40 <dolio> I kind of think that even most 'proper' logic courses aren't very good, from what I can infer from seeing people discuss logic.
18:19:01 <dolio> Although they aren't as bad as what you're describing.
18:19:19 <tomsmeding> or the people weren't taking those courses, or they weren't paying attention :)
18:19:34 <tomsmeding> one only has to get about half the exam correct in order to pass
18:19:48 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
18:19:57 <dolio> I mean like supposedly professional mathematicians talking about logic.
18:20:09 <tomsmeding> professional _mathematicians_? ah
18:20:31 <dolio> Also most books aren't great, either.
18:20:39 <dolio> Which get used to teach the courses.
18:20:52 <constxd> bros i am looking for a language that is as aesthetically pleasing as haskell (juxtaposition = application, currying, lots of handy infix operators for various sorts of composition, etc.) but is strict, and has support for imperative programming (mutable state, side effects allowed anywhere, etc.) but also lightweight (not Scala) does such a thing exist...
18:21:04 <constxd> dynamically typed is fine even
18:21:14 <tomsmeding> {-# LANGUAGE -XStrict #-}
18:21:28 <tomsmeding> (I'm half joking)
18:21:57 <Franciman> constxd: maybe ocaml
18:21:59 <tomsmeding> joking because it doesn't really cut it, because libraries aren't compiled with it, and nothing really is built for that behaviour so much
18:22:02 <dolio> -XStrict is just bad. You could suggest Haskell, though. :þ
18:22:03 <Franciman> the syntax is not as nice as haskell tho
18:22:14 <Franciman> it has various rough points, but it's similar at least
18:23:10 <EvanR> maybe try F#
18:23:30 <Franciman> does f# have a nice syntax?
18:23:41 <Franciman> now that .net is cross platform and open source, i may try it
18:23:42 <tomsmeding> that is something only you can judge for yourself
18:23:46 <constxd> i really wonder about Raku if i'm being honest
18:24:01 <Franciman> perl 6?
18:24:14 <constxd> they ditched that name but yeah
18:24:15 <EvanR> also there is koka
18:25:09 <EvanR> but writing haskell so that stuff you're doing is most eagerly evaluated isn't that hard
18:25:15 <EvanR> mostly
18:25:23 hgolden joins (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd)
18:25:46 <EvanR> avoid lists
18:26:07 <tomsmeding> -XStrictData is much less weird than -XStrict
18:26:33 <tomsmeding> you'll have to deal with... basically everything being lazy, though, such as (,), Either, Maybe, [], etc.
18:26:35 <EvanR> even though a lot of lazy list code will compile into loops, it would still be lazy and you don't want it
18:27:28 <tomsmeding> relevant is https://hackage.haskell.org/package/strict
18:29:09 ft joins (~ft@p4fc2a393.dip0.t-ipconnect.de)
18:30:42 <mauke> -XStrict breaks my brain
18:31:32 × spew quits (~spew@201.141.99.170) (Quit: spew)
18:32:30 <constxd> i wonder about PureScript too
18:32:55 <constxd> i have heard in some sense it's like Haskell but without the stuff that is considered mistakes in hindsight
18:33:56 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
18:36:32 <Franciman> constxd: if you like raku's syntax, ocaml will be awesome
18:37:41 neuroevolutus joins (~neuroevol@37.19.200.135)
18:39:53 <dmj`> constxd: if it ain't non-strict it ain't haskell :P
18:40:33 <EvanR> laziness is amazing, except for the poor souls working on the compiler
18:42:34 <dmj`> it'd probably be easier if we inlined the eval function into every program, or generate a custom eval function that operated on all closures / constructors
18:42:48 × xff0x quits (~xff0x@2405:6580:b080:900:4a8f:2c6:6e99:efb9) (Ping timeout: 246 seconds)
18:43:50 xff0x joins (~xff0x@2405:6580:b080:900:136b:65b1:e5b:b9e1)
18:44:44 <dmj`> implicit laziness is complicated to deal with, explicit would be better
18:45:05 ash3en joins (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0)
18:45:33 <[exa]> constxd: purescript elegantly trades the little mistakes of haskell for a heap of other subtle mistakes
18:47:14 <dmj`> and its effectively js only
18:47:22 <[exa]> most notably the evaluation is more of a scheme or ML than the haskell kind, in turn 99% of the usual constructions that involve functions doing functions stuff just fail to work
18:47:23 target_i joins (~target_i@user/target-i/x-6023099)
18:47:44 × son0p quits (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20) (Ping timeout: 260 seconds)
18:48:03 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds)
18:49:05 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
18:51:40 <monochrom> Do you accept Idris?
18:54:16 <EvanR> I just use the type system xD
18:54:21 <EvanR> don't try to run anything
18:55:50 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
18:57:53 × rdcdr quits (~rdcdr@user/rdcdr) (Ping timeout: 245 seconds)
18:58:19 rdcdr joins (~rdcdr@user/rdcdr)
19:00:16 × petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
19:02:06 petrichor joins (~znc-user@user/petrichor)
19:03:39 madjestic joins (~madjestic@103-135-99-95.ftth.glasoperator.nl)
19:03:56 hgolden_ joins (~hgolden@syn-172-251-233-141.res.spectrum.com)
19:04:04 × hgolden quits (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) (Ping timeout: 260 seconds)
19:05:57 × ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 248 seconds)
19:10:26 <tomsmeding> [exa]: do you have an example?
19:15:45 <Franciman> wonder how the chezscheme backend compares to ghc
19:15:49 <Franciman> produced code
19:16:20 ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com)
19:17:47 <[exa]> tomsmeding: I once tried to write the simple parsec instance for something there
19:17:58 <[exa]> turned out to be absolutely unattainable
19:18:18 × Square2 quits (~Square4@user/square) (Ping timeout: 245 seconds)
19:18:49 <tomsmeding> in what sense? I thought parsec-like stuff is just lambda calculus and inductive data types
19:18:53 <tomsmeding> surely it has that?!
19:19:47 <[exa]> hm, what are the conditions for a "record patch syntax" to work? I'm trying to do one which shold be absolutely obvious (`x{f=val}` with `x` bound by types to be the exact record type) but ghc tells me "Not a record constructor: x"
19:19:56 <[exa]> tomsmeding: yap it doesn't have lambda calculus :D
19:20:01 <[exa]> iz strict
19:20:12 <tomsmeding> but that's fine?
19:20:22 <tomsmeding> strict lambda calculus is still lambda calculus
19:21:21 <tomsmeding> if you transform the parser data type, which is morally a coproduct, into the continuation-style thing that is typical of parsec-like libraries, you do have to take care to make all of the continuations a function
19:21:31 <tomsmeding> i.e. if you have a 0-argument continuation, have to make it () -> a
19:21:40 <tomsmeding> but that's quite minor IMO
19:21:46 <mauke> [exa]: need more context
19:21:53 <EvanR> the old () -> a trick
19:23:35 <[exa]> yeah that would work, except I kinda tableflipped for some reason right in the middle
19:25:12 <davean> ((╯°□°)╯︵ ┻━┻) -> a
19:25:56 <davean> That function signature is basicly me
19:26:18 <davean> get fed up and just fix something, except I'm in IO for sure
19:26:41 [exa] invokes unsafePerformDavean
19:26:57 <davean> [exa]: that was July 1st :-p
19:27:44 <[exa]> mauke: the context was basically me going "hey why don't we have a HM inference visualizer for browsers, this must be trivial in the modern programming systems!!!111"
19:27:54 <[exa]> then I got corrected
19:28:02 <mauke> no, for the record error
19:28:27 <tomsmeding> [exa]: the JS backend of GHC exists nowadays
19:28:29 <tomsmeding> it works
19:28:39 <tomsmeding> it you're happy with downloading a tarball with a custom GHC build :p
19:29:09 <[exa]> don't really mind that. I guess I'll try next
19:29:28 <[exa]> mauke: https://paste.tomsmeding.com/mw5YY3BN, complains about the `sfi{...}`s
19:29:44 <tomsmeding> [exa]: what is the full error? :p
19:29:47 <[exa]> I hope I didn't kill it by the wildcards
19:30:08 <[exa]> https://paste.tomsmeding.com/TIwqP6sB
19:30:10 <tomsmeding> also, given that there is a wildcard involved (angry face), the definition of SkipFwdIter :p
19:30:10 <[exa]> that's literally it
19:30:29 <mauke> what language extensions are active?
19:31:20 <[exa]> only RecordWildcards
19:31:21 Square joins (~Square@user/square)
19:31:22 tomsmeding . o O ( -XNoTraditionalRecordSyntax )
19:32:01 <[exa]> tomsmeding: https://paste.tomsmeding.com/Z3cHiU8U
19:33:04 <tomsmeding> huh
19:33:08 tomsmeding gets the same
19:33:58 <[exa]> maybe it hates that the record's too polymorphic?
19:34:08 <tomsmeding> it's a _parsing_ error
19:34:17 <mauke> yes, and it's looking for a pattern
19:34:48 <tomsmeding> [exa]: you're missing a `do` on the `Just` case
19:35:02 <tomsmeding> good luck figuring out what ghc is trying to parse here
19:36:01 <[exa]> oh wow
19:36:07 <[exa]> that's it, thanks al ot
19:36:17 <[exa]> s/l / l/
19:36:29 <mauke> hah, just found that
19:37:03 <mauke> I wish I knew why that generates a backwards syntax error
19:37:23 <[exa]> ha true, it only generated one
19:37:43 <tomsmeding> "only one"?
19:37:49 <tomsmeding> ghc never gives more than one syntax error
19:38:03 <[exa]> ah, ok nvm
19:38:05 × terrorjack4 quits (~terrorjac@2a01:4f8:121:32e8::) (Quit: The Lounge - https://thelounge.chat)
19:38:34 <[exa]> I assume it did something terrible with trying to glue the <- to the previous `do` or something
19:38:43 <[exa]> cool
19:38:46 <[exa]> thanks guys
19:39:05 × hgolden_ quits (~hgolden@syn-172-251-233-141.res.spectrum.com) (Remote host closed the connection)
19:39:08 <mauke> I think it somehow parses the whole (Nothing -> do ... Just p0 -> (p1, _) <-) part as a single pattern
19:39:54 <mauke> because if you replace sfi{ by A{, the error changes to "error: do-notation in pattern" at Nothing -> do
19:39:55 hgolden joins (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd)
19:40:12 <tomsmeding> I think the `return $ sf {...} Just p0 -> (p1, _)` is a pattern on the left side of a <- in the Nothing do
19:40:34 <[exa]> O_o
19:40:49 <tomsmeding> if you reduce the code to this: https://paste.tomsmeding.com/WhFDSGvX
19:41:05 <tomsmeding> oh I lied
19:41:39 <tomsmeding> meh I haev no clue
19:41:49 <tomsmeding> [exa]: you broke haskell
19:42:16 <[exa]> naaaaaaaaaaaaaay
19:42:29 <[exa]> is this worth reporting?
19:42:42 <[exa]> or should I bury it here to the heap of other syntax gore
19:43:09 <[exa]> Franciman: what comparison metrics btw
19:43:13 mauke remembers something
19:43:24 <mauke> layout is terminated early by syntax errors
19:43:37 <tomsmeding> before reporting I'd spend some more time figuring out what's happening exactly
19:43:41 <tomsmeding> oh no
19:43:51 <tomsmeding> I HATE that part of haskell parsing
19:43:53 <mauke> so the missing 'do' causes a syntax error in the second branch, so the 'do' in the first branch retracts its '}' ... or something
19:43:57 <tomsmeding> and I refuse to believe it's fucking necessary
19:44:01 <[exa]> ah so it can glue the rest of the layout to anywhere?
19:44:21 <tomsmeding> with a stateful parser you don't need any kind of brace insertion
19:44:27 <Franciman> [exa]: memory consumption and/or speed
19:45:03 <mauke> tomsmeding: what do you mean?
19:45:24 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
19:46:40 <[exa]> Franciman: depends a lot IMO on the usecase. Look at what attoparsecs do, haskell wins there. For memory-pokey stuff Chez might just be unbeatable just on the account of being much simpler.
19:47:01 hgolden_ joins (~hgolden@204.152.216.106)
19:47:04 <Franciman> nice
19:47:05 terrorjack4 joins (~terrorjac@2a01:4f8:c17:dc9f::)
19:47:05 <[exa]> ghc is inserting indents and dedents?
19:48:23 <mauke> it's the layout of case/of that's messing things up
19:49:08 <mauke> if you add { ; } for the case/of, you get a much more sensible error: parse error on input ‘<-’; Suggested fix: Possibly caused by a missing 'do'?
19:50:12 × hgolden quits (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) (Ping timeout: 276 seconds)
19:51:25 <[exa]> Franciman: tbh looking at this https://ecraven.github.io/r7rs-benchmarks/ I'd somewhat bet on mildly optimized haskell
19:51:35 <Franciman> hahah
19:51:39 <mauke> and if you put '};' before 'return $', you get the same "not a constructor" error
19:51:44 <tomsmeding> oh meh I apparently don't have 'do' parsing in my parser yet
19:52:06 <[exa]> nvm back to useful coding :D
19:52:21 <tomsmeding> but I wrote a parser of a subset of haskell at some point that 1. I'm fairly sure does not backtrack more than a bounded number of tokens, and 2. does nothing at all with braces
19:52:38 × mreh quits (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 255 seconds)
19:52:44 <tomsmeding> it's a stateful parser combinator parser that keeps proper track of indented blocks
19:52:54 <tomsmeding> you probably can't do that in alex/happy
19:53:04 <tomsmeding> and it's probably slower than what ghc does :)
19:53:38 <monochrom> Any solution to layout is a good solution. :)
19:54:12 <mauke> > do 1 == 2 == False
19:54:13 <lambdabot> error:
19:54:13 <lambdabot> Precedence parsing error
19:54:13 <lambdabot> cannot mix ‘==’ [infix 4] and ‘==’ [infix 4] in the same infix expre...
19:55:10 <mauke> > (do 1 == 2) == False
19:55:11 <lambdabot> True
19:55:16 <mauke> hmm
19:55:36 <tomsmeding> precedence resolution comes after parsing proper
19:56:07 <tomsmeding> it first parses it as a stupid tree without any precedences, then finds all the infix* statements, then goes back and fixes all the operator trees
19:56:56 raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
19:57:10 <mauke> oh, they fixed that in Haskell 2010
19:57:17 <mauke> it was valid code in H98
19:57:24 L29Ah joins (~L29Ah@wikipedia/L29Ah)
19:57:55 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds)
19:58:02 <mauke> oh, or I'm misremembering things
19:58:04 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
19:58:09 <[exa]> I like this meaning of "fixed"
19:58:46 <mauke> > let x = 42 in x == 42 == True
19:58:48 <lambdabot> error:
19:58:48 <lambdabot> Precedence parsing error
19:58:48 <lambdabot> cannot mix ‘==’ [infix 4] and ‘==’ [infix 4] in the same infix expre...
19:58:56 <mauke> ^ this was valid in Haskell 98
19:59:27 <tomsmeding> then that's definitely a fix
20:00:19 <dmj`> it was the best of times, it was the worst of times
20:00:36 <dolio> Haskell98 says == is infix 4.
20:01:05 <tomsmeding> dolio: I think the point is that it was parsed as "hey, the second == is a syntax error, apparently the `let` ends"
20:01:06 <mauke> I don't think == was changed
20:01:22 <dolio> Oh, I see.
20:01:34 <tomsmeding> which is very awkward
20:01:36 <mauke> the let body extends to the right "as far as possible"
20:01:37 × ft quits (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: Lost terminal)
20:01:38 <dolio> Did anyone ever actually implement that parsing rule?
20:01:45 × neuroevolutus quits (~neuroevol@37.19.200.135) (Ping timeout: 256 seconds)
20:02:28 × ash3en quits (~Thunderbi@2a01:c23:8c99:e00:e1c5:8430:a907:e2c0) (Quit: ash3en)
20:04:29 <dmj`> dolio: Lennart found a new solution for it in his MicroHs project. The part where the parser gets invoked during the layout phase
20:06:31 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
20:07:47 ft joins (~ft@p4fc2a393.dip0.t-ipconnect.de)
20:09:39 machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
20:09:56 <dmj`> dolio: https://github.com/augustss/MicroHs/blob/master/src/MicroHs/Parse.hs#L274-L294
20:10:53 <dmj`> the number 5 rule, layout stack gets popped different if a parse error is detected
20:10:57 <dolio> This doesn't cover the let case, though, right?
20:11:15 <dmj`> I think he uses it for let, where, do, case, since they all have the same issue iirc
20:12:09 <dmj`> if you ctrl+f for "pBlock" it gets used in all those scenarios
20:14:37 <dolio> There's no pBlock for the relevant part of let.
20:16:35 <dmj`> https://github.com/augustss/MicroHs/blob/master/src/MicroHs/Parse.hs#L623
20:16:56 <dolio> The relevant part is after the "in".
20:18:10 <dmj`> isn't it in the "let { }", and then if you nest lets it could be problematic, trying to close the outer let prematurely inside the inner let
20:18:39 <mauke> no
20:18:48 <dolio> No. It is `let ... in x == y == z` parsing as `(let ... in x == y) == z`, because `x == y == z` is a syntax error.
20:19:29 <dolio> The weird rule is that various expressions, 'extend as far as possible such that they don't cause syntax errors.'
20:19:40 <tomsmeding> what I find surprising is that a haskell parser is even _able_ to parse that as `(let ... in x == y) == z` in the first place, because the `infix ==` statement could well come after this code!
20:19:48 <dolio> So, in principle, there might be a lambda expression example, too.
20:20:00 CrunchyFlakes joins (~CrunchyFl@ip-109-42-115-64.web.vodafone.de)
20:20:20 <dolio> Like `\x y z -> x == y == z` parsing as `(\x y z -> x == y) == z` as long as there's a z in the outer scope.
20:21:25 <tomsmeding> if the 'infix' is commented, this code ceases to parse https://paste.tomsmeding.com/e1C0p56U
20:21:49 <tomsmeding> if the parser cannot know the fixity of an operator when it needs to decide whether to terminate the `let` or not, how can it do so?
20:22:03 <tomsmeding> or is terminating the `let` part of the post-parsing precedence fixing stage
20:22:10 <dolio> And also the lexer was specified that way, too, so it could break up e.g. contiguous alphabetic characters if they would result in a syntax error.
20:22:16 <monochrom> Shoot, that is actually interesting because with "== is neither left- nor right-assoc", x==y==z is a parse error.
20:22:19 <dmj`> if its infix (without l or r specified) and the precedence is identical it should always be a layout error I thought
20:23:20 <monochrom> This complicates the issue very much.
20:24:12 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
20:25:00 <dmj`> tomsmeding: the latter, Haskell tries to close let, where, case an do statements with virtual braces to make the syntax context free, but nesting causes parse errors, so in those cases the closing virtual braces are popped off the stack and parsing continues until the end of the expression
20:25:36 <tomsmeding> dmj`: but based on what information does the parser decide to put a '}' before the second '=='?
20:26:01 <tomsmeding> if the 'infix 4 ==' statement comes later than this expression, which it can, then the relevant information is not yet available
20:27:35 <dolio> tomsmeding: I don't know if the weird 98 rule was actually implemented. It's pretty unintuitive.
20:28:01 <dmj`> tomsmeding: I think it goes lexing, layout, parsing, then during typechecking fixity resolution will occur and that's where the precedence errors are thrown
20:28:36 <dmj`> InfixOps Exp [(Op, Exp)] gets converted into a tree of InfixOp Exp Op Exp
20:29:45 <tomsmeding> dmj`: right -- but if that's how it works, then surely the parser has no clue whether to terminate the `let` body before the second '=='
20:30:02 <tomsmeding> so the misparse in question could never have occurred
20:30:30 <dmj`> yea that's true, so maybe the no. 5 layout rule might not even be relevant to this issue, it would be handled by the fixity resolution
20:30:37 <tomsmeding> dolio has the pertinent question: did GHC ever parse `let ... in x == y == z` as `(let ... in x == y) == z`?
20:31:01 <dolio> I'd be somewhat surprised.
20:31:32 <tomsmeding> if someone did, then they cared nil about parse error helpfulness :p
20:31:46 <dmj`> I don't know tbh, Lennart parses it as the list representation above and throws the double == error here https://github.com/augustss/MicroHs/blob/master/src/MicroHs/Fixity.hs#L69
20:32:05 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-115-64.web.vodafone.de) (Read error: Connection reset by peer)
20:32:18 <monochrom> Supposed "infix 4 ==" must be honoured, even when it's the very last line of the file. :)
20:32:30 <monochrom> err, Supposedly!
20:33:12 <monochrom> To be sure I appreciate that in practice it's such a pain and maybe not worth the effort.
20:33:24 <dolio> That, I think, works.
20:33:31 <tomsmeding> monochrom: I think that works perfectly
20:33:52 <tomsmeding> this fails to parse: https://paste.tomsmeding.com/e1C0p56U
20:34:44 <tomsmeding> and if someone says that this is to be taken as a parse failure that terminates a `let`, then that someone deserves a stomp
20:35:24 <dolio> I don't think you can make that example into something that parses.
20:35:34 <dolio> So H98 says it's okay to fail. :)
20:35:36 <tomsmeding> you can, by removing the `infix` statement
20:35:53 <dolio> No, you can't just throw away expressions.
20:36:00 <tomsmeding> oh by rearranging parentheses, you mean
20:36:02 <tomsmeding> right
20:36:09 <dolio> You can only end the scope of something early.
20:36:19 <tomsmeding> yes, it should definitely fail -- it was an illustration that 'infix' is honoured, even if it comes late
20:36:26 <dolio> Or split up something that looks like a single lexeme.
20:36:56 <tomsmeding> the latter of which is a mistake made in BASIC -- we learned from that
20:37:35 <dolio> Maybe you could say that the last expression parses as `infix @ $`, except that's still not valid, and I'm not sure the spec was that ridiculous.
20:37:42 <tomsmeding> :p
20:38:03 <tomsmeding> it would be valid, perhaps, if an 'infix' statement also continued until a parse error
20:38:07 <tomsmeding> but presumably it doesn't
20:38:25 <dolio> It's invalid because @ isn't a valid operator, I think.
20:38:28 <tomsmeding> though I guess the parse error would occur at the newline following the `$`
20:38:34 <dolio> Yeah.
20:38:55 <[exa]> btw is there any info on why haskells didn't adopt the prolog system? the xfy system looks quite unbeatable to me.
20:38:58 <tomsmeding> > (@) = 4
20:39:00 <lambdabot> <hint>:1:2: error: parse error on input ‘@’
20:39:14 <tomsmeding> % (@) = 4
20:39:14 <yahb2> <no output>
20:39:16 <tomsmeding> ?
20:39:22 <tomsmeding> % (@) + 1
20:39:22 <yahb2> 5
20:39:30 <tomsmeding> ghc version discrepancy?
20:39:54 <tomsmeding> > let (@) = 4 in (@)
20:39:55 <lambdabot> <hint>:1:6: error: parse error on input ‘@’
20:40:13 <monochrom> I agree that no one should expect "let in x==y==z" to mean "(let in x==y)==z" even if the spec implies it by an obscure technicality. :)
20:40:59 <monochrom> [exa]: What is the xfy system?
20:41:30 <[exa]> the one for marking the fixities in op/3
20:41:34 <[exa]> sec
20:42:09 <[exa]> ( https://www.swi-prolog.org/pldoc/doc_for?object=op/3 )
20:42:29 × ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 260 seconds)
20:42:39 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 260 seconds)
20:43:47 [exa] -> afk
20:44:53 <tomsmeding> hm, so 'infix' is xfx, 'infixl' is yfx, 'infixr' is xfy
20:45:32 <tomsmeding> the only binary operator case not describable with haskell's syntax is yfy, and I don't see any prolog operators with that precedence
20:45:36 <EvanR> yeah the three letter codes are incomprehensible
20:45:42 <tomsmeding> also that
20:45:47 × driib3 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
20:46:15 <tomsmeding> "left-associative" and "right-associative" are not much better, but at least one can mumble something like "the parentheses bunch up towards the left/right"
20:46:29 <tomsmeding> oh, yfy is not even allowed
20:46:35 <tomsmeding> [exa]: in what way is xfy better :p
20:46:43 driib31 joins (~driib@vmi931078.contaboserver.net)
20:47:00 <mauke> what precedence is afk
20:47:08 <tomsmeding> parse error
20:47:25 × gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer)
20:48:34 <tomsmeding> or hm, if y is "<= prec" and x is "< prec", i.e. "< prec-1", then w is "< prec-2", so afk would require a term with precedence prec-23 on the left and prec-13 on the right
20:49:07 ZharMeny joins (~ZharMeny@user/ZharMeny)
20:49:26 <tomsmeding> can go up to prec-25 using 'z'; unfortunately, the rest of the 1200-large range of precedence values you can't cover
20:50:52 <EvanR> precedence is another thing solved by monochromes campaign of explicitness, always use explicit parentheses
20:51:23 <tomsmeding> lisper detected
20:52:59 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
20:53:11 gentauro joins (~gentauro@user/gentauro)
20:55:03 <ski> (iirc, Mercury has some `fxy' binary prefix operators)
21:00:54 <glguy> monochrom: Your example helped me to find an optimization over using "otherwise"
21:01:23 <glguy> > let f x | even x = 1 | let = 0 in f <$> [1..5]
21:01:25 <lambdabot> [0,1,0,1,0]
21:01:51 <tomsmeding> beautiful!
21:04:29 × driib31 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
21:04:49 <mauke> is that just an empty set of bindings?
21:04:54 <tomsmeding> yes
21:05:05 <dolio> Oh, that's what's happening?
21:05:16 <tomsmeding> > let in 7
21:05:17 <lambdabot> 7
21:06:18 <mauke> % id let in 7
21:06:18 <yahb2> 7
21:06:29 <glguy> :t \case
21:06:30 <lambdabot> p1 -> p2
21:06:46 <tomsmeding> mauke: you sneaky -XBlockArguments
21:07:33 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
21:07:57 <tomsmeding> funny messed up error formatting here:
21:07:59 <tomsmeding> % id do let
21:07:59 <yahb2> <interactive>:31:7: error: ; The last statement in a 'do' block must be an expression let
21:08:14 <tomsmeding> (surely the copy of the input expression should be on a new line)
21:08:23 <mauke> % mod do { 5 * 6 } let in 3 + 4
21:08:23 <yahb2> 2
21:08:34 × madjestic quits (~madjestic@103-135-99-95.ftth.glasoperator.nl) (Ping timeout: 252 seconds)
21:08:51 × michalz quits (~michalz@185.246.207.218) (Remote host closed the connection)
21:10:01 <mauke> % runST let in pure 42
21:10:01 <yahb2> <interactive>:35:1: error: ; Variable not in scope: runST :: f0 a0 -> t
21:10:24 <mauke> % import Control.Monad.ST
21:10:24 <yahb2> <no output>
21:10:26 <mauke> % runST let in pure 42
21:10:26 <yahb2> 42
21:10:30 <mauke> excellent
21:10:39 driib31 joins (~driib@vmi931078.contaboserver.net)
21:10:47 <tomsmeding> % :set -XNoBlockArguments
21:10:47 <yahb2> <no output>
21:15:41 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
21:20:47 <ski> > [() | let]
21:20:49 <lambdabot> [()]
21:22:18 <glguy> ski: that's useful with -XOverloadedLists - it fixes the type to be []
21:22:44 pavonia joins (~user@user/siracusa)
21:23:24 <ski> to not be
21:24:05 <ncf> that is the question
21:24:12 × oo_miguel quits (~Thunderbi@78.10.207.45) (Quit: oo_miguel)
21:25:08 × driib31 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
21:29:19 driib31 joins (~driib@vmi931078.contaboserver.net)
21:30:50 × driib31 quits (~driib@vmi931078.contaboserver.net) (Client Quit)
21:31:56 <EvanR> :t (2,b)
21:31:57 <lambdabot> Num a => (a, Expr)
21:36:44 driib31 joins (~driib@vmi931078.contaboserver.net)
21:36:57 son0p joins (~ff@186.121.18.131)
21:37:13 <c_wraith> Oh no. (|| not (2, b)) is a type error!
21:37:49 <glguy> :t (/ negate (2*b))
21:37:50 <lambdabot> Expr -> Expr
21:41:33 <c_wraith> :t (|| not (2 b)) -- I "fixed" it
21:41:34 <lambdabot> Bool -> Bool
21:43:20 <ski> lambdaProlog (Teyjus (compiles to a WAM-like byte code) implementation) has `prefix',`prefixl',`postfix',`postfixr' in addition to `infix',`infixl',`infixr'
21:46:25 oo_miguel joins (~Thunderbi@78.10.207.45)
21:47:19 <ski> (these correspond to the Prolog fixities, `fx',`fy',`xf',`yf' ; `xfx',`yfx',`xfy', respectively)
21:48:40 <ski> (oh .. i suppose it's `prefixr' and `postfixl', not `prefixl' and `postfixr', actually)
21:50:32 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
21:50:44 × oo_miguel quits (~Thunderbi@78.10.207.45) (Ping timeout: 252 seconds)
21:51:42 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 272 seconds)
21:54:33 × nshepperd quits (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Ping timeout: 245 seconds)
21:54:57 × esnos quits (~user@176.106.34.161) (Ping timeout: 246 seconds)
21:56:32 hgolden__ joins (~hgolden@23.162.40.69)
21:57:13 <lystra> Hi. I'm modifying ghc-9.4.8 to take -Wl,-rpath, into consideration as output from "pkgconfig --libs". https://gist.github.com/twwlogin/33eb2db7bf4eaebb0f1712110d31787c is an example of the change I made. ghc is complaining about extraRpathDirs being out of scope. Any idea why?
21:59:05 × hgolden_ quits (~hgolden@204.152.216.106) (Ping timeout: 255 seconds)
22:07:22 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 265 seconds)
22:18:05 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:24:28 nshepperd joins (~nshepperd@li364-218.members.linode.com)
22:25:20 weary-traveler joins (~user@user/user363627)
22:30:26 <int-e> tfw you copy the Complex data type and the Num instance and rip out `abs` and `signum` so that it works for Num instead of RealFloat :-/
22:44:12 <yin> types can be infix?
22:45:23 Pixi joins (~Pixi@user/pixi)
22:51:59 <int-e> That's a GHC extension, TypeOperators
22:52:12 <int-e> data constructors can be infix in Haskell98
22:52:38 <int-e> using operators starting with : (not including : or ::)
22:55:54 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
23:04:53 × acidjnk_new quits (~acidjnk@p200300d6e72cfb18ac0e327209850a07.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
23:05:10 <yin> i see
23:07:06 <yin> can i import type operators?
23:07:31 <yin> import Data.Modular ( ? )
23:07:53 dehsou^ joins (~dehsou@c-98-242-74-66.hsd1.ga.comcast.net)
23:10:57 troojg joins (~troojg@user/troojg)
23:12:52 <geekosaur> as usual, wrap operators in parens
23:13:54 <probie> If it's at both value level and type level, you might need `import Data.Module ( type(?) )` or something (I think that's the right syntax, but I'm not 100% sure)
23:33:56 neuroevolutus joins (~neuroevol@206.217.206.115)
23:37:10 × son0p quits (~ff@186.121.18.131) (Killed (NickServ (GHOST command used by son0p-!~ff@2800:e2:f80:ee7::3)))
23:37:48 <Axman6> lystra: have you added a new field to whatever type is being constructed my mempty?
23:38:08 son0p joins (~ff@186.121.18.131)
23:38:52 × neuroevolutus quits (~neuroevol@206.217.206.115) (Quit: Client closed)
23:41:35 <yin> probie: that's it, thanks. `import Data.Modular ( type(/) )`
23:44:24 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
23:57:02 <lystra> Axman6: Nope. Let me check.
23:58:14 <Axman6> I'm a bit surprised there isn't an error on line 16 of the diff if the field doesn't exist though
23:58:29 lol_ joins (~lol@2603:3016:1e01:b960:f4ac:a003:2d11:ead1)
23:58:37 <Axman6> oh that is the error, yeah that makes sense, that field doesn't exiswt
23:58:39 <Axman6> exist*
23:59:47 × Square quits (~Square@user/square) (Ping timeout: 252 seconds)

All times are in UTC on 2024-08-29.