Home liberachat/#haskell: Logs Calendar

Logs on 2024-09-04 (liberachat/#haskell)

00:00:46 × jespada quits (~jespada@r190-64-133-178.su-static.adinet.com.uy) (Ping timeout: 252 seconds)
00:00:58 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:02:19 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
00:05:42 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
00:05:42 × xff0x quits (~xff0x@2405:6580:b080:900:3618:2400:ae18:e1a3) (Ping timeout: 246 seconds)
00:08:05 × acidjnk_new quits (~acidjnk@p200300d6e72cfb5469ca77b0637d5192.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
00:10:49 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
00:10:53 → Square2 joins (~Square4@user/square)
00:14:19 × Fooo quits (~Square@user/square) (Ping timeout: 252 seconds)
00:16:43 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:21:41 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
00:27:09 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
00:28:40 <haskellbridge> <Bowuigi> Leary what about the "infinite-ness" of codata tho? You can't fold/traverse over infinite structures without taking infinite time on normal order (thus, breaking Church-Rosser and disproving totality)
00:29:30 <haskellbridge> <Bowuigi> If the only valid operations are pretty much "zip" (over codata) and take (to data) variants it makes sense though
00:31:27 <Inst> are the or patterns from GHC 9.12 actually useful?
00:31:48 <Inst> i'm sort of disappointed you can't condense multiple pattern matches into the same term, though
00:32:06 <Inst> like, say, Foo pat; Bar pat = pat * 3
00:32:30 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:35:14 × myxos quits (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 255 seconds)
00:37:25 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
00:40:44 → myxos joins (~myxos@syn-065-028-251-121.res.spectrum.com)
00:41:23 <Leary> Bowuigi: GFP_F := forall r. (forall x. (x -> F x) -> x -> r) -> r; ana_F := /\a. \coalg:a -> F a. \seed:a. /\r. \expair:forall x. (x -> F x) -> x -> r. expair a coalg seed; out_F := \ff:GFP_F. ff (F GFP_F) /\a. \coalg:a -> F a. \seed:a. map_F a GFP_F (ana_F a coalg) (coalg seed)
00:42:28 <Leary> The infiniteness is in the semantics we ascribe, not in the program that actually runs. Of course that limits which operations we can support, but this is all the same whether in Haskell or System F.
00:42:32 → gmg joins (~user@user/gehmehgeh)
00:45:07 <Leary> (in Haskell the limits are just softer, bottoming out at runtime rather than failing to type check)
00:48:03 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
00:48:18 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
00:48:47 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
00:50:59 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
00:53:48 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
00:57:25 × motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit)
00:58:54 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds)
00:59:09 → motherfsck joins (~motherfsc@user/motherfsck)
01:01:41 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
01:04:05 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:08:42 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
01:18:29 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds)
01:19:59 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:24:44 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds)
01:30:32 → weary-traveler joins (~user@user/user363627)
01:35:39 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:40:33 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
01:41:36 × Batzy quits (~quassel@user/batzy) (Ping timeout: 252 seconds)
01:49:05 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
01:51:24 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
01:56:31 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
02:05:33 <haskellbridge> <Bowuigi> I see, it works more like a generator
02:06:14 <haskellbridge> <Bowuigi> Also this means that you can get total anamorphisms (and above), which means more recursion schemes for my total lang! Thanks!
02:06:36 <monochrom> Python generators secretly dream to be codata. System F and Haskell have real codata. :)
02:07:08 <haskellbridge> <Bowuigi> Yeah, the magic of PL theory
02:07:13 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:08:13 <haskellbridge> <Bowuigi> And speaking about that, is it possible to efficiently run bulk combinators ala Kiselyov in "Lambda to SKI, semantically"?
02:08:15 <monochrom> In the next episode, I will talk about how OO secretly dreams to be codata with linearity, and Haskell has real codata with linearity. >:)
02:09:15 × nadja quits (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds)
02:09:49 → nadja joins (~dequbed@banana-new.kilobyte22.de)
02:10:46 <haskellbridge> <Bowuigi> https://crypto.stanford.edu/~blynn/lambda/kiselyov.html has an optimized compilation algorithm ("bulkOpt") and linear+logaritmic expansions. The structure of the combinators seems to hint at a way to run them as is, but I can't find it
02:11:54 <haskellbridge> <Bowuigi> If this is possible, then making a tiny and reasonably fast functional compiler is as well, which is fantastic
02:12:03 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
02:12:18 <haskellbridge> <Bowuigi> (As an alternative, the eta-optimized version is a good choice)
02:15:19 × zlqrvx quits (~zlqrvx@user/zlqrvx) (Quit: %quit%)
02:15:40 → zlqrvx joins (~zlqrvx@user/zlqrvx)
02:22:58 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:23:48 × random-jellyfish quits (~random-je@user/random-jellyfish) (Quit: Client closed)
02:27:47 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
02:31:57 × codaraxis quits (~codaraxis@user/codaraxis) (Ping timeout: 276 seconds)
02:38:45 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:43:33 → youthlic joins (~Thunderbi@user/youthlic)
02:43:34 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
02:54:32 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
02:55:27 × td_ quits (~td@i5387093B.versanet.de) (Ping timeout: 246 seconds)
02:57:31 → td_ joins (~td@i5387092A.versanet.de)
02:59:33 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
03:02:45 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
03:14:09 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:19:08 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
03:25:33 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds)
03:28:39 → Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
03:29:56 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:31:51 → athan joins (~athan@syn-098-153-145-140.biz.spectrum.com)
03:34:42 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
03:38:35 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:39:57 → aforemny joins (~aforemny@i59F516D7.versanet.de)
03:40:57 × aforemny_ quits (~aforemny@i59F516FC.versanet.de) (Ping timeout: 246 seconds)
03:45:34 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
03:50:17 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
04:01:22 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:06:09 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
04:14:00 → robobub joins (uid248673@id-248673.uxbridge.irccloud.com)
04:17:09 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:21:54 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
04:22:41 → Fooo joins (~Square@user/square)
04:25:34 <haskellbridge> <thirdofmay18081814goya> what guarantees termination in system f?
04:25:57 × Square2 quits (~Square4@user/square) (Ping timeout: 248 seconds)
04:27:45 <Axman6> ^C
04:32:56 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:36:42 <Leary> thirdofmay18081814goya: Strong normalisation.
04:37:39 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
04:48:43 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
04:50:49 × Fooo quits (~Square@user/square) (Ping timeout: 260 seconds)
04:53:27 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
04:56:15 × Pixi` quits (~Pixi@user/pixi) (Quit: Leaving)
04:56:35 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
04:57:23 <haskellbridge> <thirdofmay18081814goya> ty!
04:59:01 → michalz joins (~michalz@185.246.207.201)
05:11:10 → rosco joins (~rosco@175.136.158.234)
05:15:11 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:15:39 → Pixi joins (~Pixi@user/pixi)
05:17:07 × rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal)
05:20:08 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
05:22:18 → codaraxis joins (~codaraxis@user/codaraxis)
05:24:00 → rosco joins (~rosco@175.136.158.234)
05:30:57 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:36:07 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
05:38:41 <haskellbridge> <thirdofmay18081814goya> hm, what extension of system F provides infinite recursion?
05:39:08 <haskellbridge> <thirdofmay18081814goya> just inductive types right?
05:46:44 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
05:51:18 <Leary> thirdofmay18081814goya: The simplest way is to extend the expression langugae with a fixpoint operator `Y : forall a. (a -> a) -> a`. Infinite or negative-recursive types will also do it. Inductive types don't suffice---System F encodes these anyway.
05:51:39 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
05:52:32 <haskellbridge> <thirdofmay18081814goya> Leary: hm I see, thank you!
05:56:00 × Leary quits (~Leary@user/Leary/x-0910699) (Remote host closed the connection)
05:56:12 → Leary joins (~Leary@user/Leary/x-0910699)
05:56:24 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
06:00:24 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:00:57 → acidjnk joins (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de)
06:04:25 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
06:05:09 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
06:16:11 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:16:54 → euleritian joins (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de)
06:20:54 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
06:21:38 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
06:25:06 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
06:31:59 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
06:37:05 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
06:51:07 → alioguzhan1 joins (~Thunderbi@78.173.89.238)
06:51:39 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
06:52:18 × alioguzhan quits (~Thunderbi@78.173.89.238) (Ping timeout: 272 seconds)
06:52:18 alioguzhan1 is now known as alioguzhan
06:54:07 → crvs joins (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se)
07:00:18 × JamesMowery quits (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Quit: Goodbye)
07:00:35 → JamesMowery joins (~JamesMowe@ip98-167-207-182.ph.ph.cox.net)
07:00:57 × vglfr quits (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 252 seconds)
07:01:24 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
07:01:42 → vglfr joins (~vglfr@2607:fb91:81e:c43f:ac39:6af1:b007:6687)
07:03:36 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
07:06:27 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
07:08:17 × vglfr quits (~vglfr@2607:fb91:81e:c43f:ac39:6af1:b007:6687) (Ping timeout: 252 seconds)
07:08:28 → vglfr joins (~vglfr@2607:fb91:864:caf7:ad3:f751:af48:34dc)
07:09:04 × troydm quits (~troydm@user/troydm) (Ping timeout: 260 seconds)
07:12:54 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
07:13:21 × alioguzhan quits (~Thunderbi@78.173.89.238) (Ping timeout: 252 seconds)
07:17:27 → alioguzhan joins (~Thunderbi@78.173.89.238)
07:18:29 → acidjnk_new joins (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de)
07:18:42 → codaraxis__ joins (~codaraxis@user/codaraxis)
07:19:18 → EvanR_ joins (~EvanR@user/evanr)
07:19:49 → pavonia_ joins (~user@user/siracusa)
07:20:31 → oo_miguel joins (~Thunderbi@78.10.207.45)
07:20:38 → econo__ joins (uid147250@id-147250.tinside.irccloud.com)
07:21:08 → DrachenMaus joins (~dragonmau@user/dragonmaus)
07:21:14 → athan_ joins (~athan@syn-098-153-145-140.biz.spectrum.com)
07:21:21 → machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
07:21:27 → tzh_ joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
07:21:39 × pointlessslippe1 quits (~pointless@62.106.85.17) (Ping timeout: 246 seconds)
07:21:39 × euleritian quits (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) (Ping timeout: 246 seconds)
07:21:39 × kaskal quits (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518) (Quit: ZNC - https://znc.in)
07:21:39 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Read error: Connection reset by peer)
07:21:39 × connrs quits (~connrs@user/connrs) (Remote host closed the connection)
07:21:39 × pavonia quits (~user@user/siracusa) (Ping timeout: 246 seconds)
07:21:39 → kaskal joins (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518)
07:21:39 × athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Remote host closed the connection)
07:21:39 × DragonMaus quits (~dragonmau@user/dragonmaus) (Quit: No Ping reply in 180 seconds.)
07:21:39 × tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 246 seconds)
07:21:39 × dostoyevsky2 quits (~sck@user/dostoyevsky2) (Ping timeout: 246 seconds)
07:21:39 → dostoyevsky2 joins (~sck@static.251.39.47.78.clients.your-server.de)
07:21:39 × acidjnk quits (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
07:21:39 × motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 246 seconds)
07:21:39 econo__ is now known as econo_
07:21:40 × dostoyevsky2 quits (~sck@static.251.39.47.78.clients.your-server.de) (Changing host)
07:21:40 → dostoyevsky2 joins (~sck@user/dostoyevsky2)
07:21:48 × codaraxis quits (~codaraxis@user/codaraxis) (Ping timeout: 246 seconds)
07:21:48 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Ping timeout: 246 seconds)
07:21:48 × EvanR quits (~EvanR@user/evanr) (Ping timeout: 246 seconds)
07:21:53 → motherfsck joins (~motherfsc@user/motherfsck)
07:22:06 pavonia_ is now known as pavonia
07:22:08 → pointlessslippe- joins (~pointless@62.106.85.17)
07:26:31 × hammond quits (proscan@gateway04.insomnia247.nl) (Ping timeout: 264 seconds)
07:27:01 → hammond joins (proscan@gateway04.insomnia247.nl)
07:27:27 → connrs joins (~connrs@user/connrs)
07:34:56 → tomboy64 joins (~tomboy64@user/tomboy64)
07:35:22 × vglfr quits (~vglfr@2607:fb91:864:caf7:ad3:f751:af48:34dc) (Ping timeout: 272 seconds)
07:35:35 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
07:43:30 × motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 246 seconds)
07:43:46 → __monty__ joins (~toonn@user/toonn)
07:47:29 → merijn joins (~merijn@77.242.116.146)
07:56:44 → CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-254.web.vodafone.de)
07:57:05 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 248 seconds)
07:58:08 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:01:23 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
08:02:19 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
08:08:23 × rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal)
08:10:13 <bwe> Hi, I've got a list that I want to map over and put the results under each other in a `do`. Do I just need to bind them with the bind operator?
08:10:33 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
08:10:44 → vglfr joins (~vglfr@c-73-163-164-68.hsd1.md.comcast.net)
08:13:08 <haskellbridge> <sm> hi @bwe, perhaps you're looking for "sequence" in Control.Monad ?
08:17:27 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
08:17:56 → euleritian joins (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de)
08:18:37 × euleritian quits (~euleritia@dynamic-176-006-131-176.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
08:18:54 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
08:18:58 × ft quits (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving)
08:21:39 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
08:23:21 → merijn joins (~merijn@77.242.116.146)
08:25:31 → sourcetarius joins (~sourcetar@user/sourcetarius)
08:25:49 <haskellbridge> <sm> -in Control.Monad
08:25:52 <[exa]> bwe: either of traverse (or for), sequence, and foldM should do it
08:26:58 <bwe> It's a pity, hoogle is down :(
08:27:11 <bwe> I correct, it was.
08:27:29 × tzh_ quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:30:59 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
08:36:04 → misterfish joins (~misterfis@84.53.85.146)
08:42:11 <bwe> [exa]: oh, actually foldl did it for me with (>>)
08:46:52 <[exa]> bwe: ah cool, that's exactly `sequence_`
08:49:21 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
08:49:41 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
08:52:44 → sawilagar joins (~sawilagar@user/sawilagar)
08:58:22 <bwe> [exa]: I didn't get `sequence` to work, but wasn't aware of `sequence_`. Thanks for bringing it up!
08:59:07 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
09:08:12 × Patternmaster quits (~georg@user/Patternmaster) (Ping timeout: 252 seconds)
09:08:24 → Patternmaster joins (~georg@user/Patternmaster)
09:11:38 × ubert quits (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Remote host closed the connection)
09:22:49 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
09:25:03 → ubert joins (~Thunderbi@178.165.175.79.wireless.dyn.drei.com)
09:29:44 → chele joins (~chele@user/chele)
09:30:32 <[exa]> bwe: there are many variants of that thing
09:31:18 <[exa]> map, mapM, traverse, traverse_, for, for_, sequence, sequenceA, both of sequences with _, ...
09:31:23 × CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-254.web.vodafone.de) (Read error: Connection reset by peer)
09:34:33 → CrunchyFlakes joins (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de)
09:35:45 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 276 seconds)
09:41:57 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
09:44:31 → ZharMeny joins (~ZharMeny@user/ZharMeny)
09:52:33 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
09:52:52 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
09:53:25 → Smiles joins (uid551636@id-551636.lymington.irccloud.com)
09:59:24 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds)
10:03:28 × EvanR_ quits (~EvanR@user/evanr) (Remote host closed the connection)
10:03:30 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds)
10:03:47 → EvanR_ joins (~EvanR@user/evanr)
10:03:51 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
10:04:17 → sawilagar joins (~sawilagar@user/sawilagar)
10:05:35 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
10:06:18 × CrunchyFlakes quits (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
10:09:25 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
10:15:30 → CrunchyFlakes joins (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de)
10:15:58 → merijn joins (~merijn@77.242.116.146)
10:19:11 × CrunchyFlakes quits (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Client Quit)
10:22:00 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
10:22:14 → CrunchyFlakes joins (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de)
10:23:00 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
10:25:40 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Remote host closed the connection)
10:25:49 → merijn joins (~merijn@77.242.116.146)
10:27:46 × youthlic quits (~Thunderbi@user/youthlic) (Ping timeout: 252 seconds)
10:31:39 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
10:31:59 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
10:35:05 → jespada joins (~jespada@r190-64-133-178.su-static.adinet.com.uy)
10:36:07 → Guest21 joins (~Guest21@217.64.164.1)
10:36:22 × Guest21 quits (~Guest21@217.64.164.1) (Client Quit)
10:36:48 <yin> -/g
10:38:26 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
10:40:54 → gmg joins (~user@user/gehmehgeh)
10:41:50 → rosco joins (~rosco@175.136.158.234)
10:42:29 → ZharMeny joins (~ZharMeny@user/ZharMeny)
10:43:24 <yin> why did i just get a list of bans from 2 years ago?
10:43:43 → youthlic joins (~Thunderbi@user/youthlic)
10:52:05 <tomsmeding> yin: who sent you that list
10:54:49 × jespada quits (~jespada@r190-64-133-178.su-static.adinet.com.uy) (Ping timeout: 260 seconds)
10:57:10 <yin> helium.libera.chat, apparently
10:57:46 → xff0x joins (~xff0x@2405:6580:b080:900:ccef:b4d3:d1ad:38b8)
10:58:51 <yin> must have been an error
10:58:52 <tomsmeding> interesting?
11:01:15 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
11:02:37 <yin> so apparently as soon as my bouncer synced i received the last few entries of the ban list, unprompted
11:02:59 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
11:03:18 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
11:03:46 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
11:04:19 <yin> /mode #haskell +b gives me the complete list and it checks out
11:04:34 <yin> must be a bug in znc
11:06:03 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
11:06:52 → merijn joins (~merijn@77.242.116.146)
11:09:28 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
11:10:37 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 244 seconds)
11:20:20 × mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Quit: mesaoptimizer)
11:20:28 → mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet)
11:21:13 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:22:36 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
11:25:05 → euleritian joins (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de)
11:26:12 × euleritian quits (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
11:27:10 → euleritian joins (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de)
11:30:45 × Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection)
11:32:01 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
11:32:36 × Me-me quits (~me-me@kc.randomserver.name) (Changing host)
11:32:36 → Me-me joins (~me-me@user/me-me)
11:33:16 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
11:38:55 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en)
11:39:14 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
11:40:23 × euleritian quits (~euleritia@dynamic-176-006-148-177.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
11:40:45 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
11:44:12 <geekosaur> yeh, znc requests all that stuff on entering a channel, and I've seen it get out of sync before (have also gotten a very large chunk of userlist in the past)
11:45:33 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
11:50:11 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
11:58:45 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 276 seconds)
12:01:23 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
12:06:31 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
12:12:46 → youthlic1 joins (~Thunderbi@user/youthlic)
12:15:27 × youthlic quits (~Thunderbi@user/youthlic) (Ping timeout: 246 seconds)
12:15:28 youthlic1 is now known as youthlic
12:16:47 → kalj joins (~kalj@h-158-174-207-174.NA.cust.bahnhof.se)
12:17:36 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
12:20:15 × kalj quits (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) (Client Quit)
12:22:16 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
12:34:08 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
12:39:11 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
12:40:05 <bwe> which file watcher do you recommend to run `cabal run my-exec`? the options listed on stackoverflow sadly don't feel right
12:41:52 × Luj9 quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat)
12:42:18 <tomsmeding> ghcid
12:42:35 → Luj9 joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5)
12:43:00 <tomsmeding> i.e. `ghcid -r` probably
12:43:22 <tomsmeding> possibly `ghcid -c 'cabal repl my-exec' -r`
12:47:41 <Leary> bwe: It doesn't take much more than `inotifywait`. I have a little shell script putting a ghcid-like interface over it: https://gist.github.com/LSLeary/a7ddc196d119d52e2767f66873e24bdd
12:49:12 <bwe> tomsmeding: it's weird, why does `ghcid --restart="src" -c "cabal run web-server" -r` not react on changed file in src folder?
12:49:52 → vlad_ joins (~vlad@102.217.157.32)
12:50:08 <bwe> seriously, why is haskell community not being able to just integrate a file watcher into cabal?
12:50:12 → akegalj joins (~akegalj@89-164-111-213.dsl.iskon.hr)
12:50:32 <Leary> That's really not cabal's job.
12:50:55 <vlad_> i take it haskell has enter as the command terminator char
12:51:16 <bwe> Leary: whose job is it?
12:51:28 <Leary> inotifywait
12:51:31 <vlad_> could i string two commands together on one line?
12:51:40 × youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic)
12:51:57 <Leary> vlad_: With a semi-colon.
12:52:06 <vlad_> oh ok so it does use ;
12:53:20 <vlad_> hmm
12:53:23 <geekosaur> bwe, this is not at all unusual or tools like inotifywait wouldn't already exist
12:54:13 <vlad_> ghci> 1
12:54:13 <vlad_> 1
12:54:13 <vlad_> ghci> 1;3;
12:54:13 <vlad_> <interactive>:17:1: error:
12:54:13 <vlad_> Parse error: module header, import declaration
12:54:14 <vlad_> or top-level declaration expected.
12:54:16 <vlad_> ghci>
12:54:24 <bwe> wow, there is even: https://github.com/mercurytechnologies/ghciwatch
12:54:26 <geekosaur> (and indeed there are a bunch of other tools similar to it; which means there's a lot of demand for them)
12:54:35 <vlad_> guess i shouldn't paste
12:54:39 <akegalj> When I run `toRational 12.34` I get `3473401212609495 % 281474976710656` , but when I create rational myself `1234 % 100` I get `617 % 50`. Why? I would espect `toRational 12.34 == 1234 % 100` to be True but its not. On another hand `fromRational (toRational 12.34) == fromRational (1234 % 100)` is True. Am I doing something stupid here?
12:54:54 <tomsmeding> bwe: ghcid wants a ghci repl, it will work with 'cabal repl' but not with 'cabal run'
12:55:04 <bwe> tomsmeding: :(
12:55:22 <tomsmeding> akegalj: 0.34 is not precisely representable as a sum of (negative) powers of two
12:55:38 <tomsmeding> the floating point number "12.34" is hence not exactly equal to 1234 / 100
12:55:45 <tomsmeding> toRational gives you reality
12:56:04 <tomsmeding> bwe: but with a repl you get faster reloading too!
12:56:07 <geekosaur> as for your semicolon issue with ghci, it's just being consistent with Haskell: semicolons separate declarations, definitions, or statements (the latter being restricted to "do" blocks and having a specific meaning)
12:56:31 <vlad_> i guess i'd better read the whole book before bothering you guys
12:56:34 <vlad_> thanks!
12:56:36 <geekosaur> it's not meaningful between expressions
12:56:57 <bwe> tomsmeding: still, I am waiting for the day of hot-reloading of haskell apps.
12:57:30 <akegalj> tomsmeding: thanks. My reality is shattered
12:57:47 <geekosaur> IEEE floating point does that to a lot of people
12:58:21 <tomsmeding> > toRational (12.34 :: Float) - 1234 % 100
12:58:23 <lambdabot> 1 % 6553600
12:58:26 <tomsmeding> > toRational (12.34 :: Double) - 1234 % 100
12:58:27 <lambdabot> (-1) % 7036874417766400
12:58:38 <tomsmeding> akegalj: Double gets closer than Float (as expected)
12:59:12 <tomsmeding> > toRational (4.0625 :: Float) - 625 % 10000
12:59:13 <lambdabot> 4 % 1
12:59:21 <tomsmeding> > toRational (4.0625 :: Float) - 40625 % 10000
12:59:22 <lambdabot> 0 % 1
12:59:33 <tomsmeding> > 1 / 16
12:59:34 <lambdabot> 6.25e-2
13:00:00 <tomsmeding> 0.0625 is an exact (sum of) (negative) powers of 2, and furthermore those powers aren't too large, so it's exactly representable
13:02:11 <tomsmeding> akegalj: if you want base-10 floating point numbers, check out https://hackage.haskell.org/package/scientific
13:03:04 <sprout> > 9007199254740993.0 + 1.0
13:03:05 <lambdabot> 9.007199254740992e15
13:03:10 <Leary> akegalj: The behaviour you expect does at least hold for literals and `Data.Fixed.Fixed 100`.
13:03:37 <Leary> Only Float and Double are sinful.
13:03:42 <sprout> at least ieee compliant
13:03:48 <tomsmeding> > 9007199254740993.0
13:03:50 <lambdabot> 9.007199254740992e15
13:07:25 → Square2 joins (~Square4@user/square)
13:07:28 <akegalj> thanks guys! Will have to think a bit now
13:08:22 <bwe> which testing suite for parametrised tests is state of the art today? tasty, hedgehog, skeletest…?
13:09:28 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
13:09:29 <bwe> tomsmeding: as of now I've settled with `watchexec -w src -r -e hs -- cabal run web-server`
13:10:13 × Luj9 quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat)
13:10:52 → Luj9 joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5)
13:11:31 <tomsmeding> tasty is a framework that you can plug other stuff in, so it doesn't belong in the same list as hedgehog/quickcheck
13:11:55 → weary-traveler joins (~user@user/user363627)
13:12:00 <geekosaur> skeletest is quite new (past month) so I'd hold out or use it for experiments
13:12:15 <geekosaur> hedgehog is probably the go-to
13:13:14 <tomsmeding> if you're looking for a test framework, tasty is the "nobody got fired for choosing tasty"; for property-based tests, hedgehog tends to be nicer in practice than QuickCheck for more involved usecases
13:13:30 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 276 seconds)
13:13:39 <tomsmeding> both hedgehog and quickcheck can hook into tasty
13:14:16 <bwe> tomsmeding: what would be the "so. got fired for choosing…" then :) ?
13:14:44 <tomsmeding> I dunno :p
13:14:46 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
13:14:55 <tomsmeding> you own hand-rolled framework, undoubtedly
13:15:18 <akegalj> tomsmeding: Leary: thanks for scientific and Data.Fixed pointers!
13:16:04 <bwe> akegalj: (there is also safe-money, if you deal with money)
13:17:14 <geekosaur> I've also used CReal from the numbers package; it's very accurate but also very slow. (I'd used a `type` so I could experiment and switch out the actual type; started with Double which was fast but inaccurate, then CReal which was accurate but very slow, then Rational which I expected to be the worst of both worlds but for my use case it turned out to be almost as fast as Double and almost as accurate as CReal
13:17:20 <geekosaur> )
13:17:24 <akegalj> bwe: thanks!
13:19:23 <tomsmeding> geekosaur: in what sense is Rational not accurate?
13:20:01 <akegalj> geekosaur: thanks!
13:20:36 <tomsmeding> sure, you can't express sqrt 2 as a Rational, but then Ratio doesn't implement Floating
13:20:58 <geekosaur> tomsmeding, actually I think I misphrased that. I was expecting accuracy but slowness due to huge denominators, but it was actually very fast
13:21:17 <tomsmeding> right
13:21:21 <tomsmeding> (I would expect the same)
13:21:27 <tomsmeding> interesting
13:22:23 → sp1ff joins (~user@c-73-11-70-111.hsd1.wa.comcast.net)
13:24:36 <mauke> sqrt($1.50)
13:24:50 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
13:25:35 × Luj9 quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat)
13:25:46 → Alleria joins (~Alleria@user/alleria)
13:26:16 → Luj9 joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5)
13:29:02 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:31:06 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
13:41:47 EvanR_ is now known as EvanR
13:42:30 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
13:42:59 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
13:48:01 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
13:49:02 × athan_ quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 255 seconds)
13:50:40 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en)
13:51:31 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
13:52:25 → youthlic joins (~Thunderbi@user/youthlic)
13:52:27 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
13:53:38 × weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!)
13:54:34 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
13:54:54 → alexherbo2 joins (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net)
13:54:55 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
13:59:19 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
13:59:19 × alexherbo2 quits (~alexherbo@2a02-8440-3214-9c5e-8d74-bed8-dfc4-641c.rev.sfr.net) (Remote host closed the connection)
14:03:06 → ystael joins (~ystael@user/ystael)
14:03:51 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
14:06:06 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 260 seconds)
14:10:40 → weary-traveler joins (~user@user/user363627)
14:18:40 → gioyik joins (~gioyik@gateway/tor-sasl/gioyik)
14:21:15 × Alleria quits (~Alleria@user/alleria) (Ping timeout: 252 seconds)
14:26:01 × rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal)
14:33:15 → jinsun_ joins (~jinsun@user/jinsun)
14:33:15 × jinsun quits (~jinsun@user/jinsun) (Killed (erbium.libera.chat (Nickname regained by services)))
14:33:15 jinsun_ is now known as jinsun
14:36:30 × misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 246 seconds)
14:39:17 × _________ quits (~nobody@user/noodly) (Quit: leaving)
14:42:37 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Remote host closed the connection)
14:43:19 → ZharMeny joins (~ZharMeny@user/ZharMeny)
14:45:33 → _________ joins (~nobody@user/noodly)
14:46:08 → Alleria joins (~Alleria@user/alleria)
14:50:29 × ystael quits (~ystael@user/ystael) (Ping timeout: 248 seconds)
14:55:20 → alexherbo2 joins (~alexherbo@2a02-8440-3216-51e1-289d-5592-bb15-27a5.rev.sfr.net)
14:55:47 × alexherbo2 quits (~alexherbo@2a02-8440-3216-51e1-289d-5592-bb15-27a5.rev.sfr.net) (Remote host closed the connection)
14:56:56 → alexherbo2 joins (~alexherbo@119.13.23.93.rev.sfr.net)
14:57:31 × alexherbo2 quits (~alexherbo@119.13.23.93.rev.sfr.net) (Remote host closed the connection)
14:57:40 → CiaoSen joins (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da)
14:58:12 × Alleria quits (~Alleria@user/alleria) (Ping timeout: 246 seconds)
15:03:06 → sayola joins (~sayola@ip-109-43-114-38.web.vodafone.de)
15:06:59 × CiaoSen quits (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds)
15:07:17 → ystael joins (~ystael@user/ystael)
15:09:17 <albet70> I just feed LLM some context about fixed-point, and asked it how to use fixed-point to implement infinite type, and it generate something I haven't seen, LLM is so powerful now? here is its generated msg https://paste.tomsmeding.com/upmI7IN8
15:11:46 → athan_ joins (~athan@2600:382:3a1c:6a61:4450:dec8:4148:5c75)
15:12:33 × Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
15:13:26 → spew joins (~spew@201.141.99.170)
15:17:11 → Sgeo joins (~Sgeo@user/sgeo)
15:18:21 × sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: nyaa~)
15:20:35 → misterfish joins (~misterfis@84.53.85.146)
15:21:06 → ski joins (~ski@ext-1-196.eduroam.chalmers.se)
15:21:08 → Smiles joins (uid551636@id-551636.lymington.irccloud.com)
15:22:52 × Square2 quits (~Square4@user/square) (Remote host closed the connection)
15:27:06 × chele quits (~chele@user/chele) (Remote host closed the connection)
15:28:51 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
15:33:02 → alexherbo2 joins (~alexherbo@119.13.23.93.rev.sfr.net)
15:33:37 × alexherbo2 quits (~alexherbo@119.13.23.93.rev.sfr.net) (Remote host closed the connection)
15:33:40 → sawilagar joins (~sawilagar@user/sawilagar)
15:35:09 → alexherbo2 joins (~alexherbo@2a02-8440-3216-51e1-7938-060c-1c69-e43c.rev.sfr.net)
15:48:53 × akegalj quits (~akegalj@89-164-111-213.dsl.iskon.hr) (Quit: leaving)
15:54:45 × infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 252 seconds)
15:56:51 × ystael quits (~ystael@user/ystael) (Ping timeout: 244 seconds)
16:04:36 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
16:07:13 <EvanR> albet70, as long as someone at some point delivered it codexes on that topic
16:07:19 × machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 264 seconds)
16:07:30 <EvanR> it can remix the content in ... creative ways
16:07:52 <EvanR> it really works great in D&D where the stakes for being wrong are much less xD
16:08:55 → ystael joins (~ystael@user/ystael)
16:13:37 <albet70> haha
16:14:49 → infinity0 joins (~infinity0@pwned.gg)
16:15:19 × gioyik quits (~gioyik@gateway/tor-sasl/gioyik) (Quit: WeeChat 4.4.1)
16:16:32 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
16:17:10 × sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection)
16:17:20 → sawilagar joins (~sawilagar@user/sawilagar)
16:22:49 × ystael quits (~ystael@user/ystael) (Ping timeout: 265 seconds)
16:26:36 → czy joins (~user@global-5-173.n-2.net.cam.ac.uk)
16:30:37 mceresa is now known as mceresaSlack
16:39:49 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
16:43:34 × sayola quits (~sayola@ip-109-43-114-38.web.vodafone.de) (Read error: Connection reset by peer)
16:43:35 → sayola1 joins (~sayola@ip-109-43-114-38.web.vodafone.de)
16:46:03 × EvanR quits (~EvanR@user/evanr) (Ping timeout: 276 seconds)
16:46:10 × vglfr quits (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 252 seconds)
16:46:25 → vglfr joins (~vglfr@2607:fb91:876:943b:ac39:c391:b163:cf47)
16:47:09 mceresaSlack is now known as mceresa
16:47:14 × sayola1 quits (~sayola@ip-109-43-114-38.web.vodafone.de) (Client Quit)
16:47:28 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 265 seconds)
16:48:39 × crvs quits (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) (Ping timeout: 252 seconds)
16:52:39 × vglfr quits (~vglfr@2607:fb91:876:943b:ac39:c391:b163:cf47) (Ping timeout: 246 seconds)
16:53:33 → vglfr joins (~vglfr@2607:fb90:ea4d:129c:ad3:f751:4fc7:4632)
16:55:06 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Ping timeout: 246 seconds)
17:04:54 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
17:07:33 × hovsater quits (sid499516@user/hovsater) (Ping timeout: 248 seconds)
17:07:57 × jonrh quits (sid5185@ilkley.irccloud.com) (Read error: Connection reset by peer)
17:08:09 → jonrh joins (sid5185@id-5185.ilkley.irccloud.com)
17:09:37 → sourcetarius joins (~sourcetar@user/sourcetarius)
17:11:08 → hovsater joins (sid499516@user/hovsater)
17:15:28 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
17:16:37 → ystael joins (~ystael@user/ystael)
17:27:20 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
17:28:32 → EvanR joins (~EvanR@user/evanr)
17:30:06 → tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
17:31:51 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
17:42:45 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
17:47:15 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
17:51:17 × czy quits (~user@global-5-173.n-2.net.cam.ac.uk) (Ping timeout: 248 seconds)
17:56:24 <Inst> btw, standard chartered is finally backing Haskell Foundation? cheer!
17:58:17 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
18:02:53 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
18:03:10 × codaraxis__ quits (~codaraxis@user/codaraxis) (Quit: Leaving)
18:04:39 → sawilagar joins (~sawilagar@user/sawilagar)
18:07:31 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
18:08:23 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
18:13:20 → Inst_ joins (~Inst@user/Inst)
18:14:04 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
18:15:03 → euphores joins (~SASL_euph@user/euphores)
18:15:45 × Inst quits (~Inst@user/Inst) (Ping timeout: 276 seconds)
18:16:39 <tomsmeding> albet70: "It's important to note that the actual implementation of fixed-point combinators like the Y combinator is quite complex and involves advanced type-level programming and category theory concepts." -- that's not at all true
18:16:54 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
18:17:02 <tomsmeding> sure, the Y combiantor as commonly phrased does not quite type-check in haskell because of the self-application `x x`
18:17:33 <tomsmeding> but the trick to get around that, if you want to stay close to the original Y combinator, has nothing to do with type-level trickery or category theory
18:17:46 → crvs joins (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se)
18:18:16 <EvanR> chat-gpt should include what GPA it got during its undergrad with relevant answers
18:18:45 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
18:19:48 × athan_ quits (~athan@2600:382:3a1c:6a61:4450:dec8:4148:5c75) (Ping timeout: 246 seconds)
18:19:57 × vglfr quits (~vglfr@2607:fb90:ea4d:129c:ad3:f751:4fc7:4632) (Ping timeout: 252 seconds)
18:20:35 <haskellbridge> <Bowuigi> Note that LLMs are bad at most of the functional stuff because they involve actual thought. Consider them as "professional yappers" for now, at least until AlphaProof evolves and goes Cubical
18:20:46 <tomsmeding> albet70: https://en.wikipedia.org/wiki/Fixed-point_combinator#Type_for_the_Y_combinator
18:20:52 × sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: sourcetarius)
18:21:16 <tomsmeding> the second code block there is an implementation of the Y combinator in haskell that does typecheck
18:21:39 <tomsmeding> not a lot of deep stuff happening
18:25:09 <Inst_> EvanR: that would be a fun experiment
18:25:35 <Inst_> i'm susprised no one tried grading chatgpt's work, because tbh, i wouldn't be surprised if chatgpt could eek out a 2 / C
18:25:40 Inst_ is now known as Inst
18:25:59 <EvanR> it got an F for Frankenstein
18:26:27 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
18:27:02 → ash3en joins (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029)
18:27:54 → euleritian joins (~euleritia@dynamic-176-006-139-128.176.6.pool.telefonica.de)
18:29:52 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
18:32:33 × Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
18:34:42 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
18:35:24 × ystael quits (~ystael@user/ystael) (Quit: Lost terminal)
18:42:26 × euleritian quits (~euleritia@dynamic-176-006-139-128.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
18:42:43 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
18:44:16 → Fooo joins (~Square@user/square)
18:45:38 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
18:45:44 Fooo is now known as Square
18:49:47 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
18:50:23 → vglfr joins (~vglfr@2601:14d:4e01:1370:919a:c941:4142:9778)
18:50:36 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
18:54:57 → athan_ joins (~athan@syn-098-153-145-140.biz.spectrum.com)
18:56:05 → mikess joins (~mikess@user/mikess)
18:59:51 → CiaoSen joins (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da)
18:59:53 × youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic)
19:01:25 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
19:02:41 <[exa]> albet70: there might be a blogpost somewhere on the deep internets that says precisely the same with similar but sufficiently different words, identifiers and code structure
19:05:57 × spew quits (~spew@201.141.99.170) (Quit: spew)
19:06:40 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
19:17:13 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
19:20:26 → ystael joins (~ystael@user/ystael)
19:22:06 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
19:28:44 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
19:28:58 × gentauro_ quits (~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net) (Ping timeout: 252 seconds)
19:30:48 × siers quits (~ij@user/ij) (Ping timeout: 252 seconds)
19:30:53 → gentauro joins (~gentauro@user/gentauro)
19:31:07 <Inst> does chatgpt imply grade deflation?
19:31:09 → siers joins (~ij@user/ij)
19:31:33 × alexherbo2 quits (~alexherbo@2a02-8440-3216-51e1-7938-060c-1c69-e43c.rev.sfr.net) (Remote host closed the connection)
19:31:35 <Inst> as in, would it result in harsher, and more aggressive grading as a way to shut down 0 effort chatgpt grabs?
19:32:31 <EvanR> lol
19:32:57 <EvanR> everyone has to get smarter to compete with chatgpt grading curve. Artificial Intelligence indeed
19:33:44 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
19:34:21 <monochrom> Grade deflation is happening. My colleagues and I are seeing a decrease of 10-15 percentiles in marks in 3rd-year students; they are also more passive. But we think it's COVID rather than LLMs.
19:36:56 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
19:37:02 <monochrom> LLMs are as good or as bad as what they were trained on. Essay courses and easy courses will get grade inflation because current LLMs are well-trained on those. Advanced courses will get deflation because LLMs are poorly trained on those, "insufficient data for a meaningful answer" (haha).
19:38:35 <monochrom> I am skeptical about the "it requires thinking so LLMs will do poorly" theory. I don't buy it until LLMs are trained on high-quality high-quantity data and still perform poorly.
19:39:09 <monochrom> Currently you don't even have enough Haskell code on the internet for chatgpt to steal and train on.
19:39:49 <Inst> https://knowledge.wharton.upenn.edu/article/is-chatgpt-a-better-entrepreneur-than-most/
19:40:57 <monochrom> I say that because Copilot is doing OK with mainstream languages. Believe it or not, coding things up in mainstream languages requires just as much thinking, or "thinking".
19:41:23 × crvs quits (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) (Ping timeout: 255 seconds)
19:43:33 <monochrom> (You think mutable states are really all that easier to get right than pure functions?)
19:44:27 <mauke> no, but I've also seen chatgpt spit out hilariously (or subtly) broken code
19:44:31 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
19:44:33 × CrunchyFlakes quits (~CrunchyFl@ip1f126623.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
19:44:37 <mauke> it's a frickin' chat bot
19:45:05 <monochrom> (You think passing an object as an argument---recall that an object is at least a bundle of half a dozen functions---is really less complex than passing one single function as an argument?)
19:46:01 → justsomeguy joins (~justsomeg@user/justsomeguy)
19:46:22 <Inst> (FP is easier than imperative programming, it's just substantially different)
19:46:24 <mauke> an object is no functions :-)
19:46:30 <Inst> Hmmm, I wonder how the math community is doing with chatgpt proofs
19:46:31 → CrunchyFlakes joins (~CrunchyFl@31.18.102.35)
19:46:35 <mauke> I've been a C++ compiler before
19:46:37 <Inst> there's a huge corpus there
19:47:14 <mauke> "hoc est corpus meum" -- chatgpt, probably
19:47:57 <EvanR> I heard there has been success generating proofs using this LLM stuff
19:48:22 <EvanR> I don't know if it's in any remotely relevant realm to haskell
19:48:25 <monochrom> Oh, that. In 1st- and 2nd-year courses, we recognize which homework submissions are from chatgpt. :) Namely, those that look way too well-organized like in textbooks, e.g., complete with introduction, bullet points, conclusion.
19:48:50 <justsomeguy> Why does fmap length Just [1,2,3] evaluate to 1 instead of 3?
19:49:05 <Inst> that doesn't evaluate
19:49:06 → ft joins (~ft@p4fc2a393.dip0.t-ipconnect.de)
19:49:13 <Inst> you mean fmap length (Just [1,2,3]), right?
19:49:18 <monochrom> Because fmap length (Just whatever) = 1, regardless of whatever.
19:49:31 <monochrom> Err sorry, misread.
19:49:38 <monochrom> I need tea. I'll be back.
19:49:47 <Inst> oh, that does
19:49:55 <monochrom> > fmap length (Just [1,2,3])
19:49:55 <dolio> > (length . Just) [1,2,3]
19:49:56 <lambdabot> Just 3
19:49:57 <lambdabot> 1
19:50:10 <mauke> > fmap length Just [1,2,3]
19:50:12 <lambdabot> 1
19:50:22 <monochrom> Oh haha, didn't realize that it type-checks.
19:50:25 <dolio> fmap length Just = length . Just
19:50:45 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
19:50:57 <monochrom> OK then correction: length (Just whatever) = 1, regardless of whatever. length Nothing = 0.
19:51:39 <justsomeguy> When I try (\x -> Just (length x)) [1,2,3] it returns Just 3.
19:51:50 <justsomeguy> I think I made a mistake in the evaulation process somewhere.
19:52:03 <justsomeguy> (I tried writing out each step.)
19:52:09 <dolio> That is Just . length.
19:52:09 <EvanR> > length (Just 3)
19:52:11 <lambdabot> 1
19:52:14 <ash3en> > fmap length $ Just [1,2,3]
19:52:15 <lambdabot> Just 3
19:52:16 <Inst> do you know what the Functor instance for (a ->) is?
19:52:21 <EvanR> > length (1,3)
19:52:23 <lambdabot> 1
19:52:24 <ash3en> fmap length Just [1,2,3]
19:52:29 <ash3en> > fmap length Just [1,2,3]
19:52:30 <lambdabot> 1
19:52:34 <EvanR> > length ()
19:52:35 <dmj`> the curse of FTP
19:52:36 <lambdabot> error:
19:52:36 <lambdabot> • Couldn't match expected type ‘t0 a0’ with actual type ‘()’
19:52:36 <lambdabot> • In the first argument of ‘length’, namely ‘()’
19:52:43 <justsomeguy> Inst: fmap
19:52:51 <Inst> fmap = (.)
19:52:55 <EvanR> really, () doesn't have a Foldable instance?
19:52:55 <Inst> like dolio said
19:53:01 <mauke> > (fmap length Just) "widdershins"
19:53:02 <lambdabot> 1
19:53:02 <Inst> EvanR: do the kinds match?
19:53:06 <EvanR> oh
19:54:32 <Inst> more annoying, (a,b,c) is not instanced into Foldable
19:54:40 <ash3en> eh, i too don't really get why > fmap length Just [1,2,3] = 1 and > fmap length $ Just [1,2,3] = Just 3?
19:55:06 <Inst> fmap length Just [1,2,3] = (length . Just) [1,2,3]
19:56:27 × ubert quits (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 265 seconds)
19:56:31 <Inst> = length (Just [1,2,3]) = 1
19:58:24 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds)
19:58:42 <ash3en> ok, slowly I get it
20:00:07 <Inst> there's also an applicative and monad instance for (r ->), which people golf with, but a ton of people call smelly because you'd have to know how it works
20:00:27 <tomsmeding> not only that, because often it's golfing for golfing's sake :p
20:00:41 <Inst> > :t (<*>)
20:00:42 <mauke> wouldn't want people to have fun
20:00:42 <lambdabot> <hint>:1:1: error: parse error on input ‘:’
20:00:50 <tomsmeding> which is good if you're at codegolf.stackexchange.com, but not so good if you're writing code that should be read
20:00:59 <mauke> only ctional programming here
20:01:04 <Inst> @:t (<*>)
20:01:04 <lambdabot> Maybe you meant: wn v sm rc pl let id do bf @ ? .
20:01:31 <tomsmeding> mauke: fun in programming does not always go together with writing maintainable code :p
20:01:50 <Inst> > t
20:01:51 <lambdabot> t
20:01:51 <tomsmeding> doesn't mean that either is not worth doing
20:01:57 <Inst> > t (<*>)
20:01:59 <lambdabot> error:
20:01:59 <lambdabot> • Couldn't match expected type ‘(f0 (a0 -> b0) -> f0 a0 -> f0 b0)
20:01:59 <lambdabot> -> t’
20:02:07 <tomsmeding> :t (<*>)
20:02:07 <Inst> ugh, which bot can give you types?
20:02:08 <lambdabot> Applicative f => f (a -> b) -> f a -> f b
20:02:14 <mauke> lambdabot
20:02:19 <tomsmeding> % :t (<*>)
20:02:19 <yahb2> (<*>) :: Applicative f => f (a -> b) -> f a -> f b
20:02:22 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
20:02:35 <Inst> let f be (r ->)
20:02:43 <tomsmeding> % :set -XTypeApplications
20:02:43 <yahb2> <no output>
20:02:49 <tomsmeding> % :t (<*>) @((->) r)
20:02:49 <yahb2> <interactive>:1:14: error: Not in scope: type variable ‘r’
20:02:49 <Inst> try that as an exercise, ash3en
20:02:52 <tomsmeding> % :t (<*>) @((->) Bool)
20:02:52 <yahb2> (<*>) @((->) Bool) ; :: (Bool -> (a -> b)) -> (Bool -> a) -> Bool -> b
20:03:47 <mauke> @djinn (Bool -> (a -> b)) -> (Bool -> a) -> Bool -> b
20:03:47 <lambdabot> f a b c =
20:03:47 <lambdabot> case c of
20:03:47 <lambdabot> False -> a False (b False)
20:03:47 <lambdabot> True -> a True (b False)
20:04:12 <tomsmeding> @djinn (r -> (a -> b)) -> (r -> a) -> r -> b
20:04:12 <lambdabot> f a b c = a c (b c)
20:04:26 tomsmeding . o O ( f a d c )
20:06:45 × itaipu quits (~itaipu@168.121.98.169) (Ping timeout: 248 seconds)
20:07:06 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
20:08:39 → machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net)
20:10:09 <ash3en> oof, ok
20:10:26 <Inst> it just works out that way because of the type definition
20:10:55 <Inst> % :t (>>=)
20:10:55 <yahb2> (>>=) :: Monad m => m a -> (a -> m b) -> m b
20:11:13 <Inst> % :t (>>=) @(r ->)
20:11:13 <yahb2> <interactive>:1:13: error: parse error on input ‘)’
20:11:19 × Square quits (~Square@user/square) (Ping timeout: 260 seconds)
20:11:27 <Inst> % :t (>>=) @((->) r)
20:11:27 <yahb2> <interactive>:1:14: error: Not in scope: type variable ‘r’
20:11:41 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
20:11:56 <Inst> (r -> a) -> (a -> r -> b) -> r -> b
20:12:02 <tomsmeding> % :t (>>=) @((->) Bool)
20:12:02 <yahb2> (>>=) @((->) Bool) :: (Bool -> a) -> (a -> Bool -> b) -> Bool -> b
20:14:08 <tomsmeding> (<*>) = flip (>>=) . flip
20:15:11 <tomsmeding> :t (=<<) <$> flip
20:15:12 <lambdabot> (a1 -> a2 -> b) -> (a1 -> a2) -> a1 -> b
20:16:38 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
20:16:47 <tomsmeding> 1. (<*>) = (=<<) <$> flip 2. (=<<) = (<*>) <$> flip
20:17:31 <tomsmeding> (<$> flip) is involutive (at the right type)
20:19:22 <tomsmeding> no actually, (<$> flip) is just involutive always
20:19:36 <tomsmeding> (<$> flip) <$> (<$> flip) = id
20:19:50 → itaipu joins (~itaipu@168.121.99.142)
20:20:16 <tomsmeding> which is: flip fmap flip `fmap` flip fmap flip
20:20:36 <tomsmeding> mauke: is this functional enough for you :p
20:20:56 → justsomeguy joins (~justsomeg@user/justsomeguy)
20:20:58 × ash3en quits (~Thunderbi@2a02:3100:7dd1:6200:ae40:c3a4:b9f6:6029) (Quit: ash3en)
20:21:38 <dmj`> what even is functional
20:23:03 <tomsmeding> well I think flip fmap flip `fmap` flip fmap flip is quite functional
20:24:38 <Hecate> :26
20:24:41 <Hecate> (hi)
20:24:46 <tomsmeding> :)
20:25:17 <Inst> oh, condolences on your recent coup
20:25:48 <Inst> and support, but off-topic
20:25:53 <Franciman> hi, is haskell experimenting new language paradigms?
20:26:06 <Franciman> are we gonna see major changes?
20:27:23 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
20:28:12 <Inst> what are actually new language paradigms these days?
20:30:54 <EvanR> fresh paradigms, right outta the book industry oven?
20:31:13 <EvanR> smell those crispy acronyms
20:31:31 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
20:32:06 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
20:38:03 <dmj`> Franciman: there was some linear types added
20:38:17 <Franciman> nice
20:41:16 <dmj`> someone might be able to add row types into the type system, that'd be a big change
20:43:10 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
20:45:28 <justsomeguy> What do you think of Serokell's work on dependent types? https://serokell.io/blog/ghc-dependent-types-in-haskell
20:48:17 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
20:50:01 → czy joins (~user@2a00:23c6:54a8:6301:5024:a70a:b7d6:6a68)
20:58:21 <haskellbridge> <thirdofmay18081814goya> in an extrinsically typed model of system f, do I need to introduce new syntax if I introduce the type-variable type and quantified-type type, can the syntax for lambda abstraction "\lambda x. term" be used for type application and type abstraction or do I need to introduce new syntax?
20:58:30 → kaskal- joins (~kaskal@213-225-32-95.nat.highway.a1.net)
20:58:42 × kaskal quits (~kaskal@2001:4bb8:2c3:301f:344f:f795:68cb:7518) (Ping timeout: 246 seconds)
20:58:57 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
20:59:27 × dostoyevsky2 quits (~sck@user/dostoyevsky2) (Quit: leaving)
20:59:46 → dostoyevsky2 joins (~sck@user/dostoyevsky2)
21:01:53 <EvanR> chatgpt says yes, you need new syntax xD
21:02:08 <EvanR> like capital lambda
21:02:38 <ncf> stop using chatgpt
21:02:46 <haskellbridge> <thirdofmay18081814goya> uh give me a second this question is ill-typed lmao
21:03:12 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
21:03:56 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:05:06 <monochrom> :)
21:06:52 <monochrom> I don't know extrinsically type model. But System F syntax goes like (Λt. λx:t. x) : ∀t. t->t
21:07:59 <monochrom> Type theory tends to use Π instead of Λ.
21:09:11 <monochrom> But then type theory's Π also covers more things.
21:09:12 <haskellbridge> <thirdofmay18081814goya> What I want to ask: would I run into any issues if I have expressions "\lambda x. term" typed "TypeVariable -> Nat" but also expressions "\lambda x. term" typed "Nat -> Nat"
21:11:52 <haskellbridge> <thirdofmay18081814goya> "forall TypeVariable. TypeVariable -> Nat" I meant
21:12:53 <monochrom> I understand "forall t. t -> Nat", but I don't understnad "forall TypeVariable. TypeVariable -> Nat".
21:13:04 <EvanR> you just said the same thing has two different types
21:13:19 <monochrom> unless you say that by alpha conversion, they are the same damn thing.
21:14:01 <EvanR> maybe you meant lambda x . type
21:14:09 <EvanR> where type is a type not a variable
21:14:26 <haskellbridge> <thirdofmay18081814goya> EvanR: i meant: the following would be two typed expressions in this system: "\lambda x. term1 : forall t. t -> Nat", and "\lambda x. term2. : Nat -> Nat"
21:14:39 <monochrom> "lambda x. type" would happen in type theory, but not in System F.
21:14:45 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
21:15:45 <monochrom> System F also doesn't like unannotated lambdas.
21:16:38 <EvanR> thirdofmaycan'tautocompleteuhg: you still didn't give an example of a type abstraction or type application
21:16:42 <EvanR> which I thought was the original question
21:19:21 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
21:20:27 → srazkvt joins (~sarah@user/srazkvt)
21:20:57 <tomsmeding> thirdofmay: do you mean that the following would be a valid type judgement? \t. \x. x : \forall t. t -> t
21:21:14 <tomsmeding> i.e. merging the big-lambda and small-lambda syntaxes
21:21:16 <monochrom> "(Λt. λx:t. term1) : ∀t. t->Nat" works, "(λx:Nat. term2) : Nat->Nat" also works, but note the manual annotation of x. "λx. term" System F be like "I won't do type inference for you".
21:21:19 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
21:21:33 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
21:22:04 × ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds)
21:22:23 <monochrom> and by extension, "not let-generalization" either, so if you don't have Λ you won't get ∀.
21:23:16 <tomsmeding> if you only have a type on the outside, stuff inside gets ambiguous too. Consider: `(\p -> fst p) (42, foo) : Nat`. What is the type of that `foo`?
21:23:30 <tomsmeding> (if you don't like pairs, choose your favourite lambda encoding of pairs)
21:24:22 <haskellbridge> <thirdofmay18081814goya> am instantiating examples from your comments, very helpful ty
21:24:44 <tomsmeding> (and if you say "well foo is out of scope", read "\x -> x" for foo. That could be Nat -> Nat, Bool -> Bool, (Nat -> Bool) -> (Nat -> Bool), or anything else)
21:26:18 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:27:29 × michalz quits (~michalz@185.246.207.201) (Remote host closed the connection)
21:30:27 <monochrom> This gives me an interesting thought. System F is strongly normalizing. That sounds assuring at first. But it is only after your term passes type-checking. If you write an arbitrary unnannotated unchecked term, type inference is undecidable. So in a sense the proof of termination is put on your shoulder in the form of manual annotations.
21:32:11 <EvanR> same as simply typed LC
21:37:02 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
21:42:04 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:46:00 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
21:47:43 <int-e> EvanR: not quite; there, type inference is decidable
21:48:03 <int-e> of course you pay for that by having fewer terms that can be typed successfully
21:49:27 <EvanR> oh right
21:52:20 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds)
21:52:48 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
21:57:30 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
22:06:40 → justsomeguy joins (~justsomeg@user/justsomeguy)
22:06:57 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
22:08:13 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
22:08:36 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
22:09:23 <haskellbridge> <thirdofmay18081814goya> is the following a correct statement? Consider the type "\forall t -> t". There exist values inhabiting this type whose type is "Bool -> Bool", "Nat -> Nat", "Int -> Int".
22:10:55 <haskellbridge> <thirdofmay18081814goya> whoops didn't mean to put a backslash
22:10:56 <monochrom> Do you mean "\forall t. t -> t"?
22:11:14 <haskellbridge> <thirdofmay18081814goya> ah, right
22:11:15 <haskellbridge> <thirdofmay18081814goya> yeah
22:12:39 <haskellbridge> <thirdofmay18081814goya> so, reformulating
22:13:08 <monochrom> On second thought, I don't actually know how to interpret the statement.
22:13:36 <haskellbridge> <thirdofmay18081814goya> yeah am somewhat confused here
22:13:49 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
22:13:50 <haskellbridge> <thirdofmay18081814goya> "Bool -> Bool", "Nat -> Nat", "Int -> Int" are some types inhabited by values inhabiting "forall t. t -> t"?
22:15:33 <monochrom> System F is not an interesction type system (or a union type system, for that matter). So the type "Bool->Bool" and the type "forall t. t->t" are disjoint.
22:15:34 <EvanR> did you explicitly explain the syntax of your language yet
22:15:48 <EvanR> "a model of" system F is... I'm not sure
22:16:13 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:16:14 <monochrom> (or a subtyping system)
22:17:47 <monochrom> You need at least one of {subtyping, intersection} to talk about one term having two types and so the two types have some overlap.
22:17:48 <haskellbridge> <thirdofmay18081814goya> monochrom: i.e. they do not have any common values?
22:17:48 <EvanR> a specific term can get assigned specific typings. Your question kind of sounds like we're talking about platonic values out in space being in one or more sets
22:18:09 × paddymahoney quits (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 246 seconds)
22:18:28 <haskellbridge> <thirdofmay18081814goya> EvanR: sorry I'm not really unconfused enough to be able to state a syntax lol
22:18:47 <EvanR> you don't have system F spelled out in front of you? xD
22:18:50 <monochrom> The Platonic Plane is untyped set theory in the first place. :)
22:19:16 <haskellbridge> <thirdofmay18081814goya> EvanR: yeah tapl's, but am slowly working through its meaning
22:19:55 <haskellbridge> <Bowuigi> thirdofmay18081814goya re:single-lambda Henk Barendegt's (might have mispelled that) lambda cube has a single lambda that works as both type application and abstraction, tho you might need type annotations or some way to disambiguate between them (upper/lower case variables could work)
22:20:05 <EvanR> the "values" you ask about need to be sentences in the allowed language
22:20:09 → pavonia joins (~user@user/siracusa)
22:20:25 <EvanR> like lambda (x:Int) . x, or something
22:20:26 <haskellbridge> <thirdofmay18081814goya> EvanR: hm this might be my problem, i might be confusing values and terms
22:20:57 <haskellbridge> <thirdofmay18081814goya> Bowuigi: ah I see!
22:21:30 <haskellbridge> <thirdofmay18081814goya> oh, i think I found the issue
22:21:35 <haskellbridge> <thirdofmay18081814goya> terms unify, values inhabit
22:21:36 <EvanR> dependent types are at the pinnacle of the lambda cube and have one lambda
22:23:05 <EvanR> in one sense values are expressions which are fully evaluated. In another sense values are semantic, like \x -> x and \y -> y being "really the same value"
22:23:24 <monochrom> terms inhabit types too. I haven't heard of "terms unify".
22:24:12 <EvanR> stick to terms
22:24:27 <EvanR> void where prohibited
22:27:27 × sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (Ping timeout: 244 seconds)
22:27:52 <ski> dependently typed languages may've term reconstruction, as well
22:28:06 <monochrom> You can treat ∀ as an epic intersection; then your questions have meaning. But System F does not require it, it allows me to, alternatively, treat ∀ as waiting for instantiation; then your questions are meaningless, two types are disjoint, there is no "my term inhabits two types", a term inhabits only one type.
22:28:41 <EvanR> that's a theorem of system F, terms have at most 1 typing?
22:29:06 <haskellbridge> <thirdofmay18081814goya> monochrom: I'll focus on this, thank you
22:29:20 <haskellbridge> <thirdofmay18081814goya> a term inhabits only a single type (in system F)
22:29:49 <ski> (Henk Barendregt)
22:29:55 <monochrom> E.g., "clearly", (Λt. λx:t. x) does not inhabit Nat->Nat, and (λx:Nat. x) does not inhabit ∀t. t->t.
22:30:22 <monochrom> (λx.
22:31:16 <monochrom> (λx. x) is illegal in System F. In an intersection type system, it could inhabit both Nat->Nat and ∀t. t->t, but then that's not System F.
22:31:37 ski idly ponders monic unions
22:31:38 <dolio> No, it isn't illegal in System F. It's illegal in a particular presentation of System F.
22:32:37 <EvanR> back to asking for the specific language and typing rules
22:32:59 <monochrom> Would that require a heavy dose of type inference?
22:36:07 <dolio> Well, you can't do type inference in general. But you can require people to give you full derivations for terms.
22:36:20 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
22:36:35 <haskellbridge> <thirdofmay18081814goya> so dumb question but what is the type of the identity function, with explicit forall and parentheses?
22:37:00 <EvanR> "the identity function", the platonic entity out in mathemagic land xD
22:37:18 <monochrom> ∀t. t->t
22:38:02 <monochrom> Parametricity says that it has only one inhabitant, so "the" is OK for this. :)
22:38:03 <EvanR> what term has that type and has that behavior, with explicit forall and parentheses
22:38:16 <monochrom> (Λt. λx:t. x)
22:38:28 <EvanR> \o/
22:38:39 <monochrom> I have been using that for running examples for 3 times already.
22:39:09 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds)
22:39:12 <haskellbridge> <thirdofmay18081814goya> am profoundly meditating on it thank you sorry for repeat
22:39:26 → paddymahoney joins (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com)
22:40:10 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
22:40:11 → szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
22:41:01 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
22:41:22 × acidjnk_new quits (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
22:41:31 ski . o O ( `snd : (t : Type) * t -> t' )
22:42:23 <haskellbridge> <Bowuigi> That looks odd
22:42:44 <dolio> It doesn't, actually.
22:42:52 <haskellbridge> <Bowuigi> Isn't it "snd : (t t' : Type) -> t * t' -> t'"?
22:43:17 <EvanR> lol
22:43:21 <monochrom> (t : Type) * t -> t
22:43:29 <monochrom> The ' is just to close the `
22:43:30 <EvanR> unknown type variable t'
22:43:58 <monochrom> This is why I just use "
22:44:12 <monochrom> We need html over irc.
22:44:31 <EvanR> Isn't it t'
22:44:38 ski sprinkles some anaphora, chases donkeys
22:45:08 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
22:45:23 <monochrom> So that I can write <code>t -&gt; t</code> &gt;:)
22:47:03 <ski> some people use Qt -> tQ
22:47:21 <EvanR> o_O
22:48:43 × srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!)
22:49:19 <haskellbridge> <thirdofmay18081814goya> the only thing "Λt. λx:t. x" can take, in System F, is a type, right? including a function type?
22:49:39 <ski> "can take" ?
22:50:17 <monochrom> Yeah the first lambda is to be instantiated to a type. "type-level lambda"
22:50:53 <monochrom> actually just "type lambda". GHC may get it soon.
22:50:54 <haskellbridge> <thirdofmay18081814goya> ski: i.e. the only step that is defined to reduce this expression is the one of substituting t for any type
22:51:15 <ski> when applying it to a type, yes
22:51:29 <haskellbridge> <thirdofmay18081814goya> ski: can you apply it to anything else?
22:51:35 <ski> no
22:51:44 <haskellbridge> <thirdofmay18081814goya> ok i see, ty
22:51:51 <ski> (but you didn't mention anything about application)
22:52:03 <ski> (just substitution)
22:53:29 → sprout joins (~sprout@84-80-106-227.fixed.kpn.net)
22:55:06 <ski> it's
22:55:50 <EvanR> (Λt. λx:t. x) Nat could reduce
22:55:53 <ski> (Λt. λx:t. x) u ⟿ λx:u. x
22:55:54 <ski> not
22:55:58 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
22:56:00 <ski> Λt. λx:t. x ⟿ λx:u. x
22:56:22 ddb1 is now known as ddb
22:57:03 <ski> (sometimes with a syntactic difference for applying a term to a type)
22:57:11 <EvanR> because t is a bound variable, substituting seems problematic
22:57:31 <ski> in the body
22:58:17 <EvanR> substituting stuff for free variables always works
22:58:33 <EvanR> where stuff doesn't capture bound variables
22:58:54 <EvanR> or you void your warranty
23:01:31 <ski> you can substitute for code variables, when meta-programming, not avoiding variable capture
23:03:24 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
23:06:07 × ZharMeny quits (~ZharMeny@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4))
23:06:22 <haskellbridge> <thirdofmay18081814goya> hm "λx:t. x : t -> t" is somewhat ambiguous outside of context right? we could mean either "Λt. λx:t. x : ∀t. t -> t" or "[y ↦ t] λx:y. x : y -> y", right?
23:07:40 <EvanR> hence the syntax rules of your language needing to exist
23:08:16 <haskellbridge> <thirdofmay18081814goya> nice, i think i've got it, thanks a lot
23:09:33 × CiaoSen quits (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds)
23:12:42 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
23:13:58 → gmg joins (~user@user/gehmehgeh)
23:14:43 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
23:15:59 → spew joins (~spew@201.141.99.170)
23:19:43 → Batzy joins (~quassel@user/batzy)
23:19:49 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
23:20:09 × CAT_S quits (apic@brezn3.muc.ccc.de) (Ping timeout: 244 seconds)
23:30:29 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
23:31:19 × spew quits (~spew@201.141.99.170) (Quit: spew)
23:32:16 × xff0x quits (~xff0x@2405:6580:b080:900:ccef:b4d3:d1ad:38b8) (Quit: xff0x)
23:35:22 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
23:36:38 × Sciencentistguy quits (~sciencent@hacksoc/ordinary-member) (Ping timeout: 245 seconds)
23:46:16 → merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl)
23:46:34 <haskellbridge> <GunpowderGuy> Hello i am computer science interested in functional programming. I think by the end of the year i will be skilled enough to work on a high performance compiler
23:46:50 <haskellbridge> <GunpowderGuy> like grin : https://www.reddit.com/r/haskell/comments/ku1zsm/nextgen_haskell_compilation_techniques/
23:47:07 <haskellbridge> <GunpowderGuy> Anyone else is interested in working with me?
23:47:21 <haskellbridge> <GunpowderGuy> -is
23:47:40 <haskellbridge> <GunpowderGuy> Hello i am computer science student researching functional programming. I think by the end of the year i will be skilled enough to work on a high performance compiler
23:48:34 <monochrom> I can consider "λx:t. x : t -> t" to mean that "t" is specified from the surrounding context but I don't need to know.
23:49:35 → Sciencentistguy joins (~sciencent@hacksoc/ordinary-member)
23:49:38 <monochrom> Am I allowed to mock? I have a PhD in computer science, I think by the end of the year I will solve P vs NP.
23:49:57 → Square2 joins (~Square4@user/square)
23:50:58 <monochrom> OK this channel isn't very interested in P vs NP. I will finish Dependent Linear Haskell instead. >:)
23:52:53 → emmanuelux joins (~emmanuelu@user/emmanuelux)
23:53:08 <haskellbridge> <thirdofmay18081814goya> monochrom: pls do
23:53:41 <monochrom> :)
23:54:22 <monochrom> I don't actually even know where to start. Don't hold your breath.
23:56:09 × Sciencentistguy quits (~sciencent@hacksoc/ordinary-member) (Ping timeout: 246 seconds)
23:57:21 <haskellbridge> <GunpowderGuy> monochrom: so idris2?
23:57:38 <haskellbridge> <GunpowderGuy> idrsi2 is dependent linear haskell
23:57:39 × merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
23:57:50 <haskellbridge> <GunpowderGuy> * idris2

All times are in UTC on 2024-09-04.