IRCBrowse

2023/02/11

2023-02-11 00:00:04 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-02-11 00:06:36 +0100hpc(~juzz@ip98-169-35-163.dc.dc.cox.net)
2023-02-11 00:07:18 +0100tjakway(~tjakway@cpe-107-184-74-161.socal.res.rr.com)
2023-02-11 00:11:34 +0100mc47(~mc47@xmonad/TheMC47) (Ping timeout: 260 seconds)
2023-02-11 00:14:21 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2023-02-11 00:15:21 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2023-02-11 00:17:14 +0100michalz(~michalz@185.246.204.107) (Remote host closed the connection)
2023-02-11 00:19:02 +0100Guest51(~Guest51@205.175.106.161) (Quit: Client closed)
2023-02-11 00:19:19 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 00:23:23 +0100waleee(~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 246 seconds)
2023-02-11 00:28:58 +0100gnalzo(~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8)
2023-02-11 00:29:14 +0100tjakway(~tjakway@cpe-107-184-74-161.socal.res.rr.com) (Quit: WeeChat 3.5)
2023-02-11 00:34:03 +0100werneta(~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 248 seconds)
2023-02-11 00:53:20 +0100sphynx(~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) (Ping timeout: 260 seconds)
2023-02-11 00:58:33 +0100sphynx(~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288)
2023-02-11 01:01:37 +0100Ranhir(~Ranhir@157.97.53.139) (Read error: Connection reset by peer)
2023-02-11 01:01:48 +0100shriekingnoise(~shrieking@186.137.175.87)
2023-02-11 01:04:38 +0100Ranhir(~Ranhir@157.97.53.139)
2023-02-11 01:12:12 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com)
2023-02-11 01:14:54 +0100thegeekinside(~thegeekin@189.180.83.186)
2023-02-11 01:29:17 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds)
2023-02-11 01:29:22 +0100Guest51(~Guest51@205.175.106.161)
2023-02-11 01:31:47 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 01:34:23 +0100acidjnk(~acidjnk@p200300d6e715c445102af608dfe0cdc6.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2023-02-11 01:35:47 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 01:37:59 +0100Guest3111(~Guest31@45.247.234.245)
2023-02-11 01:47:55 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds)
2023-02-11 01:50:03 +0100thongpv(~thongpv87@2402:9d80:3cf:957d:72ad:8548:e70a:725a)
2023-02-11 01:52:03 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2023-02-11 01:54:30 +0100ddellacosta(~ddellacos@143.244.47.81)
2023-02-11 01:56:39 +0100chomwitt(~chomwitt@2a02:587:7a12:aa00:1ac0:4dff:fedb:a3f1) (Ping timeout: 256 seconds)
2023-02-11 01:59:44 +0100werneta(~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net)
2023-02-11 02:07:58 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
2023-02-11 02:10:42 +0100Guest51(~Guest51@205.175.106.161) (Quit: Client closed)
2023-02-11 02:10:44 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2023-02-11 02:10:59 +0100wroathe(~wroathe@207-153-38-140.fttp.usinternet.com)
2023-02-11 02:10:59 +0100wroathe(~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host)
2023-02-11 02:10:59 +0100wroathe(~wroathe@user/wroathe)
2023-02-11 02:16:51 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2023-02-11 02:19:27 +0100thongpv(~thongpv87@2402:9d80:3cf:957d:72ad:8548:e70a:725a) (Ping timeout: 248 seconds)
2023-02-11 02:31:48 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 02:31:54 +0100thongpv(~thongpv87@2402:9d80:388:1a03:a17f:d9a6:bc5e:2ad)
2023-02-11 02:35:28 +0100Sinbad(~Sinbad@user/sinbad) (Ping timeout: 248 seconds)
2023-02-11 02:36:05 +0100shinjipf(~shinjipf@2a01:4f8:1c1c:c1be::1) (Quit: Shinji leaves)
2023-02-11 02:36:14 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 260 seconds)
2023-02-11 02:38:20 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 02:42:37 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 252 seconds)
2023-02-11 02:42:55 +0100shinjipf(~shinjipf@2a01:4f8:1c1c:c1be::1)
2023-02-11 02:43:26 +0100shinjipf(~shinjipf@2a01:4f8:1c1c:c1be::1) (Client Quit)
2023-02-11 02:47:46 +0100shinjipf(~shinjipf@2a01:4f8:1c1c:c1be::1)
2023-02-11 02:56:38 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 02:59:40 +0100Guest77(~Guest77@pool-173-49-47-184.phlapa.fios.verizon.net)
2023-02-11 03:08:42 +0100harveypwca(~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67)
2023-02-11 03:08:43 +0100tinwood(~tinwood@canonical/tinwood) (Remote host closed the connection)
2023-02-11 03:11:12 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 248 seconds)
2023-02-11 03:11:42 +0100tinwood(~tinwood@general.default.akavanagh.uk0.bigv.io)
2023-02-11 03:11:42 +0100tinwood(~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host)
2023-02-11 03:11:42 +0100tinwood(~tinwood@canonical/tinwood)
2023-02-11 03:15:44 +0100aljer(~jonathon@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 03:17:19 +0100 <aljer> fset
2023-02-11 03:17:35 +0100 <aljer> whoops :)
2023-02-11 03:21:39 +0100thegeekinside(~thegeekin@189.180.83.186) (Ping timeout: 256 seconds)
2023-02-11 03:24:32 +0100razetime(~Thunderbi@117.193.3.217) (Ping timeout: 248 seconds)
2023-02-11 03:24:35 +0100razetime1(~Thunderbi@117.193.3.217)
2023-02-11 03:24:46 +0100gehmehgeh(~user@user/gehmehgeh)
2023-02-11 03:26:17 +0100gmg(~user@user/gehmehgeh) (Ping timeout: 255 seconds)
2023-02-11 03:26:21 +0100mtjm(~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection)
2023-02-11 03:26:23 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
2023-02-11 03:26:52 +0100razetime1razetime
2023-02-11 03:27:13 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2023-02-11 03:27:46 +0100mtjm(~mutantmel@2604:a880:2:d0::208b:d001)
2023-02-11 03:30:40 +0100gehmehgeh(~user@user/gehmehgeh) (Remote host closed the connection)
2023-02-11 03:30:50 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 03:31:17 +0100jakalx(~jakalx@base.jakalx.net) ()
2023-02-11 03:31:23 +0100gehmehgeh(~user@user/gehmehgeh)
2023-02-11 03:38:39 +0100razetime(~Thunderbi@117.193.3.217) (Ping timeout: 260 seconds)
2023-02-11 03:40:32 +0100 <yushyin> weechat user detected
2023-02-11 03:46:03 +0100aljer(~jonathon@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Ping timeout: 248 seconds)
2023-02-11 03:51:22 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 03:53:36 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 03:55:25 +0100 <aljer> that's correct; a tired one at that
2023-02-11 04:04:02 +0100rettahcay(~kaushikv@c-24-20-37-193.hsd1.or.comcast.net)
2023-02-11 04:05:21 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 04:06:53 +0100 <rettahcay> how well does the haskell language server work on aarch64 (like raspberry pi)? installing using ghcup. Thanks!
2023-02-11 04:08:07 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection)
2023-02-11 04:12:00 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 248 seconds)
2023-02-11 04:12:00 +0100gentauro_(~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net) (Read error: Connection reset by peer)
2023-02-11 04:12:46 +0100finn_elija(~finn_elij@user/finn-elija/x-0085643)
2023-02-11 04:12:46 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
2023-02-11 04:12:46 +0100finn_elijaFinnElija
2023-02-11 04:16:17 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 04:17:47 +0100gentauro(~gentauro@user/gentauro)
2023-02-11 04:20:05 +0100wroathe(~wroathe@207-153-38-140.fttp.usinternet.com)
2023-02-11 04:20:05 +0100wroathe(~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host)
2023-02-11 04:20:05 +0100wroathe(~wroathe@user/wroathe)
2023-02-11 04:20:30 +0100Guest77(~Guest77@pool-173-49-47-184.phlapa.fios.verizon.net) (Quit: Client closed)
2023-02-11 04:22:42 +0100rettahcay(~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) ()
2023-02-11 04:26:46 +0100jero98772(~jero98772@2800:484:1d80:d8ce:9815:cfda:3661:17bb) (Remote host closed the connection)
2023-02-11 04:31:33 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Ping timeout: 252 seconds)
2023-02-11 04:37:35 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 248 seconds)
2023-02-11 04:40:37 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
2023-02-11 04:44:00 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
2023-02-11 04:44:40 +0100foul_owl(~kerry@193.29.61.35) (Ping timeout: 252 seconds)
2023-02-11 04:52:31 +0100razetime(~Thunderbi@117.193.3.217) (Ping timeout: 248 seconds)
2023-02-11 04:55:30 +0100azimut(~azimut@gateway/tor-sasl/azimut)
2023-02-11 04:58:23 +0100td_(~td@i53870923.versanet.de) (Ping timeout: 264 seconds)
2023-02-11 04:59:50 +0100td_(~td@i53870908.versanet.de)
2023-02-11 05:00:02 +0100haasn`(~nand@haasn.dev) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
2023-02-11 05:00:28 +0100foul_owl(~kerry@71.212.143.88)
2023-02-11 05:00:48 +0100snoot(~snoot@user/snoot)
2023-02-11 05:01:06 +0100jonathanx_(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Remote host closed the connection)
2023-02-11 05:01:33 +0100jonathanx_(~jonathan@h-178-174-176-109.a357.priv.bahnhof.se)
2023-02-11 05:04:12 +0100opticblast(~Thunderbi@172.58.80.43) (Quit: opticblast)
2023-02-11 05:04:26 +0100opticblast(~Thunderbi@172.58.83.168)
2023-02-11 05:07:55 +0100bilegeek(~bilegeek@2600:1008:b059:33a6:3874:3d26:7f6d:f6e5) (Quit: Leaving)
2023-02-11 05:08:33 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 05:09:04 +0100opticblast(~Thunderbi@172.58.83.168) (Ping timeout: 268 seconds)
2023-02-11 05:12:59 +0100razetime(~Thunderbi@117.193.3.217) (Ping timeout: 248 seconds)
2023-02-11 05:14:02 +0100jakalx(~jakalx@base.jakalx.net)
2023-02-11 05:19:12 +0100troydm1(~troydm@host-176-37-124-197.b025.la.net.ua)
2023-02-11 05:19:50 +0100opticblast(~Thunderbi@172.58.82.191)
2023-02-11 05:21:56 +0100Midjak(~Midjak@82.66.147.146) (Quit: This computer has gone to sleep)
2023-02-11 05:26:19 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 260 seconds)
2023-02-11 05:26:28 +0100opticblast(~Thunderbi@172.58.82.191) (Ping timeout: 252 seconds)
2023-02-11 05:26:39 +0100thongpv(~thongpv87@2402:9d80:388:1a03:a17f:d9a6:bc5e:2ad) (Ping timeout: 248 seconds)
2023-02-11 05:29:47 +0100MasseR460(thelounge@2001:bc8:47a0:1521::1)
2023-02-11 05:30:16 +0100h2t_(~h2t@user/h2t)
2023-02-11 05:30:23 +0100MasseR46(thelounge@2001:bc8:47a0:1521::1) (Quit: Ping timeout (120 seconds))
2023-02-11 05:30:23 +0100gawen(~gawen@user/gawen) (Quit: cya)
2023-02-11 05:30:23 +0100h2t(~h2t@user/h2t) (Quit: ZNC - https://znc.in)
2023-02-11 05:30:23 +0100bgamari(~bgamari@64.223.169.135) (Quit: ZNC 1.8.2 - https://znc.in)
2023-02-11 05:30:23 +0100MasseR460MasseR46
2023-02-11 05:30:39 +0100troydm1(~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 260 seconds)
2023-02-11 05:30:43 +0100bgamari(~bgamari@2a06:a000:b00d::2)
2023-02-11 05:31:07 +0100gawen(~gawen@user/gawen)
2023-02-11 05:31:50 +0100troydm(~troydm@user/troydm)
2023-02-11 05:43:13 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 05:46:29 +0100razetime(~Thunderbi@117.193.3.217) (Client Quit)
2023-02-11 05:50:31 +0100johnw(~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in)
2023-02-11 05:50:45 +0100rodental(~rodental@38.146.5.222) (Remote host closed the connection)
2023-02-11 05:57:37 +0100codaraxis(~codaraxis@user/codaraxis)
2023-02-11 05:57:40 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2023-02-11 05:59:21 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 06:02:01 +0100azimut(~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection)
2023-02-11 06:02:42 +0100azimut(~azimut@gateway/tor-sasl/azimut)
2023-02-11 06:04:32 +0100Guest7038(~Guest70@88.133.232.163)
2023-02-11 06:05:04 +0100 <Guest7038> ?srcIfactorial)
2023-02-11 06:05:04 +0100 <lambdabot> Unknown command, try @list
2023-02-11 06:05:39 +0100 <Guest7038> ? src (factorial)
2023-02-11 06:05:45 +0100 <Guest7038> ?src (factorial)
2023-02-11 06:05:45 +0100 <lambdabot> Source not found. Do you think like you type?
2023-02-11 06:06:02 +0100 <Guest7038> ?src($)
2023-02-11 06:06:02 +0100 <lambdabot> Unknown command, try @list
2023-02-11 06:07:10 +0100berberman(~berberman@user/berberman) (Ping timeout: 260 seconds)
2023-02-11 06:07:31 +0100berberman(~berberman@user/berberman)
2023-02-11 06:07:37 +0100 <Guest7038> ?src(@list)
2023-02-11 06:07:37 +0100 <lambdabot> Unknown command, try @list
2023-02-11 06:07:53 +0100 <Guest7038> ?@lidy
2023-02-11 06:08:02 +0100 <Guest7038> ?@list
2023-02-11 06:08:09 +0100 <glguy> Guest7038: you can play with lambdabot in /query
2023-02-11 06:08:10 +0100 <Guest7038> @list
2023-02-11 06:08:11 +0100 <lambdabot> What module? Try @listmodules for some ideas.
2023-02-11 06:08:28 +0100 <Guest7038> @list Prelude
2023-02-11 06:08:28 +0100 <lambdabot> No module "Prelude" loaded
2023-02-11 06:08:58 +0100Guest7038(~Guest70@88.133.232.163) (Client Quit)
2023-02-11 06:17:35 +0100 <ski> @src ($)
2023-02-11 06:17:35 +0100 <lambdabot> f $ x = f x
2023-02-11 06:18:54 +0100 <ski> the `list' command is about listing info about lambdabot commands and lambdabot modules, not about listing Haskell modules
2023-02-11 06:19:00 +0100 <Inst> davean: the thing I value most about Haskell is the syntax, and every time Haskell's syntax is somehow suboptimal, I get annoyed. But Haskell's syntax is so nice because it's dedicated to specific use cases and paradigms, and Haskell for scientific computing got abandoned
2023-02-11 06:19:24 +0100 <Inst> so it's no big deal that we don't have first-class support for matrices. If we did, someone would write a {-# LANGUAGE MatrixSyntax -#} and we'd be done
2023-02-11 06:20:19 +0100 <ski> @list list
2023-02-11 06:20:19 +0100 <lambdabot> system provides: listchans listmodules listservers list echo uptime
2023-02-11 06:20:22 +0100 <ski> @list eval
2023-02-11 06:20:22 +0100 <lambdabot> eval provides: run let define undefine
2023-02-11 06:24:19 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 06:25:36 +0100 <Inst> I wonder how the accelerate fundraiser is going; I had a toy program that was algorithmically suboptimal, optimized it for weeks from 30 seconds per check to less than 1 ms per check, but I still needed 24 hours to pre-build certain needed maps
2023-02-11 06:25:58 +0100 <Inst> I wanted to put accelerate to it, but it didn't support 9.x, so...
2023-02-11 06:27:17 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 06:30:11 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2023-02-11 06:31:09 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 06:34:23 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 06:35:09 +0100flukiluke(~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Remote host closed the connection)
2023-02-11 06:35:33 +0100flukiluke(~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962)
2023-02-11 06:35:40 +0100flukiluke(~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Remote host closed the connection)
2023-02-11 06:36:32 +0100flukiluke(~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962)
2023-02-11 06:36:44 +0100phma_(~phma@host-67-44-208-71.hnremote.net)
2023-02-11 06:36:56 +0100phma(~phma@2001:5b0:212a:e8d8:156a:28d7:9925:258) (Read error: Connection reset by peer)
2023-02-11 06:39:09 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
2023-02-11 06:49:28 +0100nattiestnate(~nate@202.138.250.6) (Ping timeout: 265 seconds)
2023-02-11 06:49:59 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f)
2023-02-11 06:51:10 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-02-11 06:56:32 +0100nattiestnate(~nate@202.138.250.17)
2023-02-11 06:59:05 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f) (Ping timeout: 260 seconds)
2023-02-11 07:00:18 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 07:02:13 +0100monochrom(trebla@216.138.220.146) (Quit: NO CARRIER)
2023-02-11 07:02:27 +0100phma(~phma@host-67-44-208-154.hnremote.net)
2023-02-11 07:02:47 +0100Guest3111(~Guest31@45.247.234.245) (Quit: Client closed)
2023-02-11 07:03:20 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 07:03:46 +0100phma_(~phma@host-67-44-208-71.hnremote.net) (Read error: Connection reset by peer)
2023-02-11 07:04:16 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f)
2023-02-11 07:06:43 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-02-11 07:07:35 +0100 <Athas> Inst: Accelerate has a fundraiser? What kind?
2023-02-11 07:07:51 +0100 <Athas> Oh, I see.
2023-02-11 07:07:53 +0100 <Inst> there was a petition for a fundraiser
2023-02-11 07:08:53 +0100 <Athas> Yeah, I found it on Reddit just now.
2023-02-11 07:09:07 +0100 <Athas> "accelerate fundraiser" is not a good Google search term!
2023-02-11 07:10:19 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f) (Read error: Connection reset by peer)
2023-02-11 07:17:36 +0100monochrom(trebla@216.138.220.146)
2023-02-11 07:17:40 +0100jonathanx_(~jonathan@h-178-174-176-109.a357.priv.bahnhof.se) (Remote host closed the connection)
2023-02-11 07:20:16 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f)
2023-02-11 07:21:05 +0100theproffesor(~theproffe@2601:282:8880:20::7430)
2023-02-11 07:21:05 +0100theproffesor(~theproffe@2601:282:8880:20::7430) (Changing host)
2023-02-11 07:21:05 +0100theproffesor(~theproffe@user/theproffesor)
2023-02-11 07:23:56 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f) (Read error: Connection reset by peer)
2023-02-11 07:26:36 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f)
2023-02-11 07:27:09 +0100snoot(~snoot@user/snoot) (Quit: leaving)
2023-02-11 07:33:29 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 246 seconds)
2023-02-11 07:38:00 +0100thebinary(~thebinary@2400:1a00:b040:da84:bcbc:d375:edb9:2f1f) (Read error: Connection reset by peer)
2023-02-11 07:39:27 +0100jonathanx(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se)
2023-02-11 07:40:16 +0100_xor(~xor@74.215.182.83) (Quit: bbiab)
2023-02-11 07:40:27 +0100jonathanx(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Client Quit)
2023-02-11 07:40:43 +0100codaraxis__(~codaraxis@user/codaraxis)
2023-02-11 07:44:27 +0100codaraxis(~codaraxis@user/codaraxis) (Ping timeout: 248 seconds)
2023-02-11 07:55:25 +0100Guest3728(~m-mzmz6l@vmi833741.contaboserver.net) (Remote host closed the connection)
2023-02-11 07:58:20 +0100root(~m-mzmz6l@vmi833741.contaboserver.net)
2023-02-11 07:58:44 +0100rootGuest4659
2023-02-11 08:00:33 +0100harveypwca(~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving)
2023-02-11 08:02:20 +0100Guest13(~Guest13@250.79-105-213.static.virginmediabusiness.co.uk)
2023-02-11 08:02:46 +0100 <Guest13> hi, can you use ::: to make dependent type signatures?
2023-02-11 08:03:28 +0100 <Guest13> i dont like having to write type functions for each function definition
2023-02-11 08:04:05 +0100 <Guest13> is there some way to hotwire template haskell to do this?
2023-02-11 08:04:25 +0100codedmart(~codedmart@li335-49.members.linode.com) (Ping timeout: 260 seconds)
2023-02-11 08:04:28 +0100 <Guest13> so it would generate the corresponding type family
2023-02-11 08:04:47 +0100 <Guest13> and you would only use ::: when it made sense to do so
2023-02-11 08:05:30 +0100 <Guest13> because you had taken care to curate that environment to ensure all the right type families exist to support the implementation
2023-02-11 08:06:16 +0100 <Guest13> im guessing there is some reason it doesnt make sense to make all function definitions into type familes
2023-02-11 08:06:55 +0100 <Guest13> maybe because of insane defunctionalisation requirements or something to do with partial type function application and passing type level functions as arguments
2023-02-11 08:07:35 +0100 <Guest13> idk if this overhead makes it practically impossible to do in most cases infact
2023-02-11 08:08:04 +0100 <Guest13> so you would have to have some way of ensuring that plumbing was in place before you could use ::: anywhere where that sort of thing happens
2023-02-11 08:08:50 +0100 <Guest13> i cant think of a more elegant stanza that would require the correct data to be provided in syntax
2023-02-11 08:09:28 +0100eruditass(uid248673@id-248673.uxbridge.irccloud.com)
2023-02-11 08:09:29 +0100 <Guest13> i used to be quite adept at all that defunctionalisation, and it ended up being totally formulaic
2023-02-11 08:10:02 +0100 <Guest13> and im sure iv seen TH used for that
2023-02-11 08:10:37 +0100 <Guest13> basically wrapping everything in datatypes so it supports partial applications, the whole singletons machinery
2023-02-11 08:11:35 +0100 <Guest13> but anyway, youd have to be able to manage to imagine what it looks like if instead of TH its done by some extension to the compiler
2023-02-11 08:11:43 +0100 <Guest13> language extension
2023-02-11 08:12:03 +0100 <Guest13> the fabled DependentTypes
2023-02-11 08:12:30 +0100 <Guest13> basically its going to generate a bunch of type families and defunctionalisations
2023-02-11 08:13:08 +0100 <Guest13> i say, using ::: to disambiguate when all this is supposed to happen, would help the user keep track
2023-02-11 08:13:45 +0100 <Guest13> and also, potentially prevent from inadvertently trying to get it to do something it cant
2023-02-11 08:14:36 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de)
2023-02-11 08:14:48 +0100 <Guest13> perhaps even requiring some extra things have happened, like the user has remembered to create all the required defunctionalisations of provided arguments or internal functions as they are passed around and made synonyms of at various stages of partial application
2023-02-11 08:15:21 +0100 <Guest13> each basically requiering a new datatype iiuc for the version at type level
2023-02-11 08:15:37 +0100 <Guest13> which is a total pain to do by hand
2023-02-11 08:16:35 +0100 <Guest13> ok for a small library, so i had get and set all the way up to traverse done with defunctionalisation!
2023-02-11 08:16:43 +0100 <Guest13> had type level convolutions
2023-02-11 08:17:08 +0100 <Guest13> but the type heterogeneity was going to drive me spare!
2023-02-11 08:17:30 +0100 <Guest13> everything requiring a corresponding type level container of the same shape to store type level parameters
2023-02-11 08:17:50 +0100 <Guest13> which you end up having to traverse at some point!
2023-02-11 08:18:07 +0100 <Guest13> with the comonadically extended pointer
2023-02-11 08:18:22 +0100 <Guest13> in order to get your convolutional type level stencils with type hetroginaity
2023-02-11 08:18:38 +0100 <Guest13> and all this automatic from get and set instances, and a whole bunch of defunctionalisation
2023-02-11 08:19:03 +0100 <Guest13> and basically yeilding a pretty decent type level prelude including standard classes
2023-02-11 08:20:20 +0100 <Guest13> it looked pretty neat, i liked seeing the type family versions alongside the function definitions
2023-02-11 08:20:38 +0100 <Guest13> basically became like a kind of inconvenient convention
2023-02-11 08:20:42 +0100 <Guest13> but i forgot how to do it
2023-02-11 08:21:01 +0100 <Guest13> i tried using idris to no avail
2023-02-11 08:21:43 +0100 <Guest13> i think what id like to see is a convinent syntax for specifying the type family
2023-02-11 08:22:01 +0100 <Guest13> like, maybe if you use ::: then you can use extra directives within the type signature
2023-02-11 08:22:22 +0100 <Guest13> possibly within the body of the function at term level?
2023-02-11 08:22:55 +0100 <Guest13> i kind of feel like the defunctionalisation arrow would have to become part of ghc
2023-02-11 08:23:05 +0100 <Guest13> otherwise a language extension cant rest on it?
2023-02-11 08:23:41 +0100 <Guest13> so many Apply instances!
2023-02-11 08:24:34 +0100 <Guest13> im guessing a lot of it is scoping. we dont have "where" in types
2023-02-11 08:24:48 +0100 <Guest13> or let, or even lambda
2023-02-11 08:25:04 +0100 <Guest13> the whole argument passing business is a total pain!
2023-02-11 08:25:16 +0100 <Guest13> the haskell type system has a lot to be desired in this respect
2023-02-11 08:28:32 +0100trev(~trev@user/trev)
2023-02-11 08:29:24 +0100cheater_(~Username@user/cheater)
2023-02-11 08:29:29 +0100 <Guest13> its quite cool though, as soon as you do something like matching lengths of type level lists when zipping them together, or like, calculating the length of a new list from concatinating two type level lengthed lists...
2023-02-11 08:29:55 +0100rettahcay(~kaushikv@c-24-20-37-193.hsd1.or.comcast.net)
2023-02-11 08:30:39 +0100 <Guest13> idk, i never like, extend the algebra up into kind level. always seems easier to like, just take the length of the list. rather than having a type level lengthed list, since this extra type information is basically redundant, given the list is a peano expression of a nat if you ignore the contents
2023-02-11 08:31:30 +0100 <Guest13> but if your being faithful to mirroring term to type, then you should do the same thing, as the "stronger conventional priority"
2023-02-11 08:32:02 +0100 <Guest13> rather than getting in this bad habbit of being like "oh well, the correct data already exists at type level, it doesnt matter what format its in"
2023-02-11 08:32:42 +0100 <Guest13> so if concatinating type lengthed lists at type level, the nat algebra takes place at kind level where it belongs
2023-02-11 08:32:59 +0100cheater(~Username@user/cheater) (Ping timeout: 260 seconds)
2023-02-11 08:33:01 +0100cheater_cheater
2023-02-11 08:33:06 +0100Guest13(~Guest13@250.79-105-213.static.virginmediabusiness.co.uk) (Quit: Connection closed)
2023-02-11 08:33:49 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de) (Ping timeout: 260 seconds)
2023-02-11 08:35:10 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 08:37:43 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea) (Remote host closed the connection)
2023-02-11 08:43:08 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea)
2023-02-11 08:47:17 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-02-11 08:47:58 +0100codaraxis___(~codaraxis@user/codaraxis)
2023-02-11 08:51:39 +0100codaraxis__(~codaraxis@user/codaraxis) (Ping timeout: 248 seconds)
2023-02-11 08:55:03 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 08:56:25 +0100thebinary(~thebinary@27.34.45.24)
2023-02-11 08:57:00 +0100 <tomsmeding> Inst: if you're willing to live on accelerate master, it supports 9.2
2023-02-11 08:57:22 +0100 <tomsmeding> also the fundraiser calls haven't really penetrated to the people who are actually working on it :p
2023-02-11 08:58:30 +0100 <Athas> If you want to accelerate Accelerate development, helping the maintainers apply for academic grants is probably the most useful avenue. That's how it has been funded so far.
2023-02-11 08:58:48 +0100thebinary(~thebinary@27.34.45.24) (Read error: Connection reset by peer)
2023-02-11 08:58:50 +0100 <tomsmeding> that is true
2023-02-11 08:59:38 +0100thongpv(~thongpv87@2402:9d80:3b2:6b24:28fa:15ca:dbc7:5055)
2023-02-11 09:02:58 +0100johnw(~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net)
2023-02-11 09:06:46 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2023-02-11 09:09:29 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
2023-02-11 09:13:59 +0100razetime(~Thunderbi@117.193.3.217) (Ping timeout: 246 seconds)
2023-02-11 09:15:49 +0100Tuplanolla(~Tuplanoll@91-159-68-152.elisa-laajakaista.fi)
2023-02-11 09:20:23 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 09:32:46 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 09:32:56 +0100coot(~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba)
2023-02-11 09:37:31 +0100thebinary(~thebinary@27.34.45.24)
2023-02-11 09:39:26 +0100thebinary(~thebinary@27.34.45.24) (Read error: Connection reset by peer)
2023-02-11 09:43:15 +0100enoq(~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7)
2023-02-11 09:44:44 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds)
2023-02-11 09:46:15 +0100Goodbye_Vincent(cyvahl@198.244.205.143) (Read error: Connection reset by peer)
2023-02-11 09:46:53 +0100Goodbye_Vincent(cyvahl@freakshells.net)
2023-02-11 09:48:57 +0100thongpv(~thongpv87@2402:9d80:3b2:6b24:28fa:15ca:dbc7:5055) (Read error: Connection reset by peer)
2023-02-11 09:50:28 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 09:51:17 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 09:53:26 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea) (Remote host closed the connection)
2023-02-11 09:57:30 +0100tzh(~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz)
2023-02-11 10:00:04 +0100nicm[m](~nicmollel@2001:470:69fc:105::1:feeb) (Quit: You have been kicked for being idle)
2023-02-11 10:00:05 +0100dykai[m](~dykaimatr@2001:470:69fc:105::2:f326) (Quit: You have been kicked for being idle)
2023-02-11 10:00:06 +0100Deide(~deide@user/deide) (Quit: You have been kicked for being idle)
2023-02-11 10:03:07 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 10:03:40 +0100thebinary(~thebinary@36.252.54.140) (Client Quit)
2023-02-11 10:03:54 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 10:04:30 +0100mmhat(~mmh@p200300f1c72570f7ee086bfffe095315.dip0.t-ipconnect.de)
2023-02-11 10:07:46 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 10:10:45 +0100jtza8(~user@165.255.88.238)
2023-02-11 10:12:23 +0100razetime(~Thunderbi@117.193.3.217) (Remote host closed the connection)
2023-02-11 10:12:27 +0100gnalzo(~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
2023-02-11 10:13:19 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2023-02-11 10:16:15 +0100xff0x(~xff0x@2405:6580:b080:900:161d:e8bd:9253:e61c) (Ping timeout: 260 seconds)
2023-02-11 10:16:38 +0100xff0x(~xff0x@178.255.149.135)
2023-02-11 10:18:31 +0100Sinbad(~Sinbad@user/sinbad)
2023-02-11 10:20:38 +0100 <jtza8> How would I go about creating a custom type constructor? For example:
2023-02-11 10:20:49 +0100 <jtza8> LowerText = T.toLower :: Text -> LowerText
2023-02-11 10:21:45 +0100acidjnk(~acidjnk@p200300d6e715c445a05d634093e239a0.dip0.t-ipconnect.de)
2023-02-11 10:22:33 +0100 <jtza8> (Where T is actually Data.Text)
2023-02-11 10:22:46 +0100 <sayola> iirc these go by smart constructors
2023-02-11 10:23:23 +0100 <jtza8> Thanks.
2023-02-11 10:23:45 +0100kuribas(~user@ptr-17d51emc5fl5behj2tb.18120a2.ip6.access.telenet.be)
2023-02-11 10:23:53 +0100 <mauke> "smart constructors" are just functions
2023-02-11 10:24:51 +0100coot(~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot)
2023-02-11 10:25:23 +0100coot(~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba)
2023-02-11 10:27:03 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-02-11 10:28:54 +0100 <jtza8> mauke: I mainly wanted to make sure I wasn't going about things the wrong way round.
2023-02-11 10:30:59 +0100 <jtza8> From what I've seen so far in Haskell, the paradox is it's always simpler than you'd think. (Simple doesn't always mean easy though.)
2023-02-11 10:31:51 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 10:33:49 +0100 <jtza8> Often language designs fail due to the oposite reason. That complex doesn't always mean hard.
2023-02-11 10:33:58 +0100mechap(~mechap@user/mechap) (Ping timeout: 252 seconds)
2023-02-11 10:35:47 +0100mechap(~mechap@user/mechap)
2023-02-11 10:36:24 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 10:38:17 +0100mmhat(~mmh@p200300f1c72570f7ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.8)
2023-02-11 10:42:48 +0100 <kuribas> I always ran into problems when learning haskell, but in contrast to other languages, there also always was a solution.
2023-02-11 10:43:05 +0100 <kuribas> Most of the time, in other language you hear "it's just the way it is, deal with it".
2023-02-11 10:43:25 +0100 <kuribas> In haskell, for example you have to deal with awkward nested records, then learn about lens.
2023-02-11 10:43:58 +0100 <kuribas> Or you want to use a argument function using different types, then you can use RankN.
2023-02-11 10:44:41 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 10:45:09 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2023-02-11 10:46:31 +0100 <c_wraith> there are edges to that
2023-02-11 10:46:42 +0100 <c_wraith> But yeah, it covers quite a large space
2023-02-11 10:47:01 +0100xff0x(~xff0x@178.255.149.135) (Ping timeout: 252 seconds)
2023-02-11 10:47:44 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 10:48:51 +0100xff0x(~xff0x@2405:6580:b080:900:161d:e8bd:9253:e61c)
2023-02-11 10:48:56 +0100 <kuribas> The main thing I get in haskell, and miss in other languages is the ability to hide low level functionality, and to create a nice abstraction over it.
2023-02-11 10:48:58 +0100coot(~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot)
2023-02-11 10:49:28 +0100 <kuribas> When you try do it with OO for example, you usually end up with some hack.
2023-02-11 10:50:03 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 10:50:43 +0100 <kuribas> Or in Python abusing syntax, and using "clever" hacking. For example hacking default arguments in pydantic.
2023-02-11 10:51:12 +0100 <kuribas> But in haskell abstractions are usually sound, except for the low level part.
2023-02-11 10:51:51 +0100 <tomsmeding> kuribas: "except" as in, you have to do some hacking but can encapsulate it?
2023-02-11 10:52:49 +0100 <kuribas> yeah
2023-02-11 10:53:10 +0100 <kuribas> like unsafePerformIO for bytestrings
2023-02-11 10:53:13 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
2023-02-11 10:53:15 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 252 seconds)
2023-02-11 10:53:23 +0100 <tomsmeding> right
2023-02-11 10:53:56 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net)
2023-02-11 10:56:39 +0100troydm(~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset)
2023-02-11 10:57:29 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 10:58:14 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 246 seconds)
2023-02-11 11:00:06 +0100mc47(~mc47@xmonad/TheMC47)
2023-02-11 11:00:39 +0100theproffesor(~theproffe@user/theproffesor) (Ping timeout: 256 seconds)
2023-02-11 11:05:13 +0100bgs(~bgs@212-85-160-171.dynamic.telemach.net)
2023-02-11 11:05:24 +0100thongpv(~thongpv87@14.164.57.133)
2023-02-11 11:06:46 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 11:11:13 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 252 seconds)
2023-02-11 11:11:26 +0100 <jtza8> kuribas: Good to hear. I used Common Lisp some time ago and I've often lamented that other languages are nowhere near as malleable.
2023-02-11 11:12:43 +0100 <kuribas> jtza8: haskell isn't as malleable as CL, but IMO that is a good thing most of the time.
2023-02-11 11:12:58 +0100 <jtza8> Agreed :)
2023-02-11 11:13:12 +0100 <kuribas> Because the freedom that lisps give also makes those DSL hard to understand, they often don't compose with eachother, etc...
2023-02-11 11:13:40 +0100 <kuribas> I don't know why people think haskell is such a hard language.
2023-02-11 11:14:43 +0100 <kuribas> Maybe because of the math terminology being thrown around.
2023-02-11 11:14:49 +0100 <tomsmeding> unfamiliarity
2023-02-11 11:14:51 +0100 <[Leary]> Because it's actually another language, not just another dialect of a language they already know.
2023-02-11 11:14:52 +0100thebinary(~thebinary@36.252.54.140) (Read error: Connection reset by peer)
2023-02-11 11:14:55 +0100 <tomsmeding> that
2023-02-11 11:15:15 +0100 <kuribas> Yes sure, but once you get further into other language, they aren't easy either.
2023-02-11 11:15:17 +0100Inst_(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240)
2023-02-11 11:15:27 +0100 <tomsmeding> that's just exploring the nooks and crannies of the dialect
2023-02-11 11:15:42 +0100 <tomsmeding> here they need to get over the hill before they can write anything interesting
2023-02-11 11:16:53 +0100 <kuribas> just write everything in IO?
2023-02-11 11:16:58 +0100 <tomsmeding> and like with natural languages, learning a third is much easier than learning a second
2023-02-11 11:17:08 +0100 <tomsmeding> if you don't start early
2023-02-11 11:17:14 +0100 <kuribas> you IORef instead of StateT
2023-02-11 11:17:35 +0100 <tomsmeding> kuribas: that will get them turned off right away due to being 1. no better than the languages they know and 2. clumsy syntax
2023-02-11 11:17:51 +0100thebinary(~thebinary@36.252.54.140)
2023-02-11 11:17:53 +0100 <tomsmeding> stateful haskell is clumsy
2023-02-11 11:17:56 +0100 <tomsmeding> with reason, but it is
2023-02-11 11:18:04 +0100MQ-17J(~MQ-17J@104.28.216.166)
2023-02-11 11:18:27 +0100 <tomsmeding> you can write array code with STArray, but it won't be as fast as C (I tried) and it's 5x as clumsy
2023-02-11 11:18:33 +0100 <kuribas> not sure, I find "ReaderT env IO" the best pattern, I am even using it now in other languages.
2023-02-11 11:18:39 +0100Inst(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240) (Ping timeout: 248 seconds)
2023-02-11 11:18:48 +0100 <tomsmeding> but then still 90% of your code is not actively in IO using mutable variables, is it?
2023-02-11 11:19:09 +0100 <tomsmeding> people want to write for (i = 0; i < n; i++)
2023-02-11 11:19:20 +0100 <tomsmeding> if you want to do that with a mutable variable 'i' in haskell, you're gonna suffer
2023-02-11 11:19:27 +0100 <tomsmeding> you _can_
2023-02-11 11:19:37 +0100 <kuribas> traverse_ [1..n-1] $ \x -> ...
2023-02-11 11:19:37 +0100 <tomsmeding> just like you can write functional code in C++ -- you _can_
2023-02-11 11:20:08 +0100 <tomsmeding> kuribas: where's my break and continue
2023-02-11 11:20:33 +0100 <tomsmeding> I grant you not being able to 'i++' halfway through the loop though
2023-02-11 11:20:34 +0100 <kuribas> right :)
2023-02-11 11:21:03 +0100 <tomsmeding> I've written C code that does that though, in option parsing
2023-02-11 11:21:21 +0100 <tomsmeding> when consuming an option with an argument, i++ after reading the argument so that it gets skipped in finding the next flag
2023-02-11 11:21:39 +0100 <tomsmeding> turning that into a while loop in C is not necessarily better, but it sure is not clean :D
2023-02-11 11:22:03 +0100 <kuribas> myFun it | it < n = do ...; myFun (it+1)
2023-02-11 11:22:25 +0100 <tomsmeding> yes, we're transforming it into something slightly more haskelly already, recursion instead of a loop
2023-02-11 11:22:46 +0100 <kuribas> I am sure most, if not all imperative code can be rewritten simply using recursion.
2023-02-11 11:22:47 +0100 <tomsmeding> we're exploring the space cautiously
2023-02-11 11:23:00 +0100 <tomsmeding> kuribas: isn't that mostly just clever CPSing?
2023-02-11 11:23:19 +0100 <kuribas> I don't see a continuation?
2023-02-11 11:23:21 +0100 <tomsmeding> like, the continuation of the loop happens to be extremely similar to the one you're in now, so just call the same thing again (i.e. recurse)
2023-02-11 11:23:27 +0100 <tomsmeding> the continuation is myFun
2023-02-11 11:23:40 +0100 <tomsmeding> *the continuation of a loop _iteration_
2023-02-11 11:23:55 +0100 <kuribas> the function is the fixed point, or the return address from the for loop.
2023-02-11 11:24:50 +0100 <kuribas> granted, it's not elegant or idiomatic haskell. But it dispells the myth that you need to know a lot of haskell to write something simple or stupid.
2023-02-11 11:24:57 +0100 <tomsmeding> my point is, you can translate everything to CPS, that's the point of CPS translation
2023-02-11 11:25:05 +0100 <tomsmeding> and CPS of a loop turns out to be recursion
2023-02-11 11:25:08 +0100 <tomsmeding> so yes
2023-02-11 11:25:16 +0100 <tomsmeding> kuribas: fair
2023-02-11 11:25:21 +0100 <kuribas> ah I see. In that way yes.
2023-02-11 11:25:45 +0100 <kuribas> well, I came from scheme, so doing this felt natural to me.
2023-02-11 11:25:55 +0100 <kuribas> Perhaps it is weird for a java or Python programmer.
2023-02-11 11:26:04 +0100 <tomsmeding> introducing recursion here?
2023-02-11 11:26:24 +0100 <kuribas> translating loops into recursion.
2023-02-11 11:26:30 +0100 <kuribas> and using tail recursion.
2023-02-11 11:26:50 +0100 <tomsmeding> the thing is that a loop is usually just a part of a function, so you'll need to introduce a function now in order to loop
2023-02-11 11:26:54 +0100 <tomsmeding> which will feel clumsy
2023-02-11 11:27:10 +0100 <tomsmeding> though a sufficiently determined programmer may accept it for the moment and continue
2023-02-11 11:27:26 +0100 <kuribas> yeah, that's how you do it in scheme.
2023-02-11 11:27:55 +0100 <tomsmeding> I mean, in _pure haskell_ code we use go functions sometimes, and those are clumsy for sure, for the same reasons as this
2023-02-11 11:28:01 +0100 <tomsmeding> I see
2023-02-11 11:28:11 +0100tomsmedinghas never used scheme more than 5 minutes
2023-02-11 11:28:16 +0100thongpv87(~thongpv87@2402:9d80:3ad:3939:eed6:8b36:cbf5:81bd)
2023-02-11 11:28:23 +0100thebinary(~thebinary@36.252.54.140) (Ping timeout: 246 seconds)
2023-02-11 11:28:49 +0100thongpv(~thongpv87@14.164.57.133) (Ping timeout: 252 seconds)
2023-02-11 11:28:57 +0100 <kuribas> maybe that's why haskell felt natural. I went from ruby > lisp > scheme > ocaml > haskell
2023-02-11 11:28:57 +0100thebinary(~thebinary@2400:1a00:b050:273:bcbc:d375:edb9:2f1f)
2023-02-11 11:29:11 +0100 <tomsmeding> Logo > C > C++ > Javascript > Haskell
2023-02-11 11:29:19 +0100 <tomsmeding> :D
2023-02-11 11:29:24 +0100 <kuribas> "javascript > haskell" is a real shock
2023-02-11 11:29:30 +0100 <tomsmeding> I mean I had been doing C++ before
2023-02-11 11:29:35 +0100 <tomsmeding> and was still doing it
2023-02-11 11:30:06 +0100 <tomsmeding> and I was predestined to like haskell
2023-02-11 11:30:38 +0100 <kuribas> Me to I guess. But I like idris more now. At least for any kind of type level programming.
2023-02-11 11:30:53 +0100 <tomsmeding> I should try idris again
2023-02-11 11:31:01 +0100 <tomsmeding> I've used agda a bit in the past and it was okay
2023-02-11 11:31:05 +0100 <tomsmeding> but slightly odd?
2023-02-11 11:31:29 +0100 <kuribas> idris is more haskell-like, but it does miss a lot of stuff from haskell.
2023-02-11 11:31:34 +0100 <kuribas> libraries mostly
2023-02-11 11:31:41 +0100 <tomsmeding> recommendations for a good idris tutorials for a haskell programmer proficient in type-level stuff?
2023-02-11 11:32:02 +0100 <kuribas> the standard documentation is quite good.
2023-02-11 11:32:04 +0100 <tomsmeding> (such a tutorial would probably look like "here's the syntax for the stuff you want to do, have fun")
2023-02-11 11:32:22 +0100 <tomsmeding> > libraries mostly <- that's not why I come to idris
2023-02-11 11:32:28 +0100 <tomsmeding> so that's fine :)
2023-02-11 11:32:34 +0100 <kuribas> or read "TDD in idris", and skip the first 5 chapters or so.
2023-02-11 11:32:39 +0100 <tomsmeding> :p
2023-02-11 11:33:15 +0100 <tomsmeding> why is literally the first hit "TDD with Idris: Updates Required" (for idris 2)
2023-02-11 11:33:26 +0100 <tomsmeding> idris really has a python 3 situation going on, doesn't it
2023-02-11 11:33:48 +0100 <tomsmeding> oh the changes seem tame
2023-02-11 11:34:10 +0100 <kuribas> yeah
2023-02-11 11:34:21 +0100 <tomsmeding> until "Lots of changes necessary here" in ch.10
2023-02-11 11:34:26 +0100 <tomsmeding> anyway, thanks for the recs!
2023-02-11 11:34:28 +0100 <kuribas> idris2 is a better language
2023-02-11 11:34:43 +0100 <kuribas> it has linear types, and type erasure.
2023-02-11 11:34:56 +0100 <kuribas> and constraints as proof search is also cool.
2023-02-11 11:35:20 +0100 <tomsmeding> "type erasure" meaning relevance?
2023-02-11 11:35:35 +0100 <kuribas> QTT it's called I believe.
2023-02-11 11:35:42 +0100 <tomsmeding> yeah that rings a bell
2023-02-11 11:35:51 +0100 <tomsmeding> cool
2023-02-11 11:35:57 +0100 <kuribas> you can say (0 a : Type) -> a -> a
2023-02-11 11:36:00 +0100 <kuribas> a is erased
2023-02-11 11:36:02 +0100 <tomsmeding> also edwin brady is the maker of Whitespace
2023-02-11 11:36:15 +0100 <tomsmeding> which is instant bonus points
2023-02-11 11:36:35 +0100 <kuribas> oh cool, I didn't know that! He looks like friendly chap.
2023-02-11 11:36:45 +0100cheater(~Username@user/cheater) (Read error: Connection reset by peer)
2023-02-11 11:37:24 +0100 <kuribas> In idris I can write "MyProof a => ..." and it will do a proof search for a, basically by trying to find constructors that match the types.
2023-02-11 11:37:29 +0100cheater(~Username@user/cheater)
2023-02-11 11:37:31 +0100thebinary(~thebinary@2400:1a00:b050:273:bcbc:d375:edb9:2f1f) (Ping timeout: 248 seconds)
2023-02-11 11:38:18 +0100 <tomsmeding> huh? oh does that mean that it's an inferred proof argument and idris will do proof search to try to infer it?
2023-02-11 11:38:31 +0100 <kuribas> tomsmeding: exactly!
2023-02-11 11:39:05 +0100 <tomsmeding> neat
2023-02-11 11:39:13 +0100 <tomsmeding> is => the "inferred" argument notation in idris?
2023-02-11 11:39:23 +0100 <tomsmeding> I think agda uses {} around the argument for that
2023-02-11 11:39:27 +0100 <kuribas> it means "inferred" + proof search.
2023-02-11 11:39:42 +0100 <tomsmeding> ah
2023-02-11 11:40:43 +0100 <kuribas> it is equivalent to {auto _ : MyProof a}
2023-02-11 11:40:50 +0100 <ski> jtza8 : <https://paste.tomsmeding.com/1FHHWYDc>
2023-02-11 11:40:58 +0100 <kuribas> so it is inferred, and additionally it does a proof search (looking for a matchin constructor).
2023-02-11 11:42:02 +0100 <kuribas> tomsmeding: without auto you also get inferrence, but using the type checker, not by proof search.
2023-02-11 11:42:21 +0100 <tomsmeding> kuribas: ah
2023-02-11 11:42:31 +0100 <tomsmeding> I should really try this it's cool
2023-02-11 11:42:32 +0100 <ski> the proof search part is backtracking ?
2023-02-11 11:42:40 +0100 <kuribas> ski: yeah
2023-02-11 11:43:05 +0100 <kuribas> ski: well, looking for suitable constructors, which involves backtracking I suppose.
2023-02-11 11:43:31 +0100 <tomsmeding> the backtracking bit is super relevant though
2023-02-11 11:43:45 +0100 <tomsmeding> without backtracking you have ghc typeclass inference -level tricks
2023-02-11 11:43:49 +0100 <tomsmeding> with backtracking you have prolog level tricks
2023-02-11 11:43:57 +0100 <ski> i think in Twelf you can do proof search, inferring instantiations for parameters (logic programming execution), ior inferring the proof term itself
2023-02-11 11:43:58 +0100 <tomsmeding> the latter is _much_ more powerful
2023-02-11 11:44:13 +0100 <kuribas> https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.List.Elem.html
2023-02-11 11:44:44 +0100 <ski> kuribas : well, the question is whether it can try some constructor, and then later, for subterms, realize it's at a deadend, and go back and change the original constructor (rather than having committed to it)
2023-02-11 11:44:49 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-02-11 11:44:59 +0100 <kuribas> ski: I believe so, yes.
2023-02-11 11:44:59 +0100zer0bitz(~zer0bitz@2001:2003:f443:d600:9572:8ab3:f7ab:9ef6) (Read error: Connection reset by peer)
2023-02-11 11:45:14 +0100skinods
2023-02-11 11:45:53 +0100tomsmedingsees "Hints: ... Uninhabited (Here = There e)"
2023-02-11 11:45:57 +0100 <ski> (Twelf is a dependently typed logic programming language)
2023-02-11 11:45:59 +0100 <tomsmeding> does the user have to write that
2023-02-11 11:46:06 +0100 <kuribas> yes
2023-02-11 11:46:14 +0100 <tomsmeding> that seems a direct consequence of this being a data type
2023-02-11 11:46:24 +0100foul_owl(~kerry@71.212.143.88) (Ping timeout: 248 seconds)
2023-02-11 11:47:23 +0100 <kuribas> I don't know why it is not derived...
2023-02-11 11:47:37 +0100 <kuribas> Maybe to enable proofs than cannot be derived?
2023-02-11 11:47:57 +0100 <tomsmeding> why would you want to prevent provable things from being proved easily
2023-02-11 11:48:50 +0100 <kuribas> I find proving stuff in idris not so easy though.
2023-02-11 11:49:22 +0100 <kuribas> It's good for "correct by construction".
2023-02-11 11:50:22 +0100 <kuribas> tomsmeding: I don't know. But it doesn't have Show or Eq deriving either.
2023-02-11 11:50:32 +0100 <kuribas> low hanging fruit perhaps?
2023-02-11 11:50:37 +0100 <tomsmeding> indeed
2023-02-11 11:51:10 +0100 <kuribas> BTW, (Here = There e) is a separate thing from Elem
2023-02-11 11:51:14 +0100 <kuribas> separate "type".
2023-02-11 11:51:16 +0100Maeda(~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving)
2023-02-11 11:51:31 +0100 <tomsmeding> what's a separate type, the Uninhabited claim?
2023-02-11 11:51:59 +0100 <ski> i wonder what the difference between `Uninhabited' and `Not' is
2023-02-11 11:52:20 +0100 <ski> (compare the last hint with `neitherHereNorThere')
2023-02-11 11:52:30 +0100 <tomsmeding> https://github.com/idris-lang/Idris2/blob/main/libs/prelude/Prelude/Basics.idr#L9
2023-02-11 11:52:38 +0100 <tomsmeding> Not x = x -> Void
2023-02-11 11:52:51 +0100 <tomsmeding> https://github.com/idris-lang/Idris2/blob/main/libs/base/Data/List/Elem.idr
2023-02-11 11:52:54 +0100 <ski> hmm .. maybe `Uninhabited t' is some kind of constraint thing
2023-02-11 11:53:08 +0100 <tomsmeding> Uninhabited seems to be a built in thing?
2023-02-11 11:53:19 +0100 <ski> note `=>' vs. `->'
2023-02-11 11:53:43 +0100 <kuribas> Not is a type function (haskell type synonym). Uninhabited is a typeclass.
2023-02-11 11:53:47 +0100 <ski> right
2023-02-11 11:54:14 +0100 <ski> so, the hints are basically instances, then ?
2023-02-11 11:54:42 +0100 <kuribas> yes, hints help interface (type class) resolution.
2023-02-11 11:56:39 +0100 <kuribas> "interface resolution" and "proof search" are the same thing in idris.
2023-02-11 11:56:43 +0100zer0bitz(~zer0bitz@2001:2003:f443:d600:7430:975b:6114:c350)
2023-02-11 11:57:10 +0100 <tomsmeding> with or without backtracking?
2023-02-11 11:57:35 +0100 <kuribas> with
2023-02-11 12:00:07 +0100 <ski> `neitherHereNorThere' is basically a specialization of `caseElem : (x = y -> o) -> (Elem x xs -> o) -> (Elem x (y :: xs) -> o)'
2023-02-11 12:00:42 +0100 <tomsmeding> not implemented in terms of it though
2023-02-11 12:00:49 +0100 <tomsmeding> but that's probably neither here nor there :)
2023-02-11 12:01:01 +0100foul_owl(~kerry@157.97.134.60)
2023-02-11 12:01:17 +0100 <ski> you could just generalize the type signature, the implementation stays the same
2023-02-11 12:01:23 +0100 <kuribas> So I can write "Show a => a -> String" or "(l : List Int) -> Elem 2 l => ..."
2023-02-11 12:01:55 +0100 <ski> what if there's multiple resolution solutions ?
2023-02-11 12:02:05 +0100 <c_wraith> pick a different one at random every time
2023-02-11 12:04:00 +0100 <kuribas> Not sure...
2023-02-11 12:04:02 +0100 <ski> heh, apparently `Prelude/Basics.idr' has `(.:)' :)
2023-02-11 12:05:42 +0100 <jtza8> ski: Thanks.
2023-02-11 12:08:47 +0100 <ski> jtza8 : `pattern GetLowerText :: LowerText -> Text' is a pattern synonym that both allows you to match a `Text' on `GetLowerText lt', getting a `LowerText' back (in case it was already all lower, otherwise the match fails), as well as to extract a `Text', from `lt' a `LowerText', using the expression `GetLowerText lt'
2023-02-11 12:08:55 +0100 <kuribas> https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html#named-implementations
2023-02-11 12:09:21 +0100 <kuribas> ski: you can pass the dictionary by name.
2023-02-11 12:09:35 +0100 <kuribas> otherwise it uses the first one it finds I think.
2023-02-11 12:10:07 +0100 <ski> if you don't care about the pattern synonym, you could just define `getLowerText :: LowerText -> Text; getLowerText (PromiseLowerText t) = t' .. or simply define `newtype LowerText = PromiseLowerText {getLowerText :: Text} deriving (Eq,Ord)'
2023-02-11 12:10:24 +0100 <ski> kuribas, ic
2023-02-11 12:12:07 +0100Kuttenbrunzer(~Kuttenbru@2a02:8108:8b80:1d48::6ccb)
2023-02-11 12:14:09 +0100merijn(~merijn@86-86-29-250.fixed.kpn.net)
2023-02-11 12:18:00 +0100 <kuribas> The nice thing about proof search is that now "isJust" and "tail" are total.
2023-02-11 12:18:46 +0100 <ski> with which types ?
2023-02-11 12:20:34 +0100 <kuribas> tail : (l : List a) -> NonEmpty l => List a
2023-02-11 12:20:54 +0100 <kuribas> fromJust : (v : Maybe a) -> IsJust v => a
2023-02-11 12:21:26 +0100 <kuribas> tail [] => Error: Can't find an implementation for NonEmpty [].
2023-02-11 12:22:12 +0100 <ski> does `isJust v' provide evidence of `IsJust v' ?
2023-02-11 12:22:28 +0100 <jtza8> ski: I haven't had anything to do with pattern synonyms before. This is quite interesting, thanks again.
2023-02-11 12:22:47 +0100 <kuribas> ski: no, isJust just returns a Bool.
2023-02-11 12:23:06 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 12:23:13 +0100 <ski> jtza8 : `GetLowerText' is a bidirectional pattern synonym, with separate implementations for its two modes (construct vs. deconstruct)
2023-02-11 12:23:59 +0100 <kuribas> ski: you cannot do "if isJust x then fromJust x else def"
2023-02-11 12:24:06 +0100shriekingnoise(~shrieking@186.137.175.87) (Ping timeout: 252 seconds)
2023-02-11 12:24:19 +0100 <kuribas> ski: but you can do "case x of Just _ => fromJust x; Nothing => def"
2023-02-11 12:25:09 +0100 <ski> kuribas : ah, .. i was hoping it had something like `isJust : (v : Maybe a) -> {False | IsNothing v} | {True | IsJust v}'
2023-02-11 12:25:24 +0100 <ski> kuribas : *nod*, makes sense
2023-02-11 12:26:43 +0100 <ski> jtza8 : have you seen view patterns, before ?
2023-02-11 12:27:27 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 12:27:29 +0100 <kuribas> ski: you don't need that
2023-02-11 12:28:05 +0100 <ski> wouldn't something like that be needed, for something akin to `if isJust x then fromJust x else def' ?
2023-02-11 12:29:16 +0100 <kuribas> ski: that is what `Dec` is for
2023-02-11 12:29:44 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 265 seconds)
2023-02-11 12:29:59 +0100_leo___(~emmanuelu@user/emmanuelux)
2023-02-11 12:31:27 +0100 <ski> jtza8 : anyway .. the `Show' and `Read' instance show one valid reason to do them manually, rather than using `deriving', which is that we want `LowerText' to be an abstract data type (conceptually implementing a subset type, `LowerText' being a subset of `Type', only some `Text' values are valid, inside `PromiseLowerText'), and so we don't want these instances to leak implementation details (and possibly
2023-02-11 12:31:31 +0100 <kuribas> ski: isItJust : (v : Maybe a) -> Dec (IsJust v)
2023-02-11 12:31:33 +0100 <ski> even allow breaking encapsulation), but rather want them to express values in terms of exported operations
2023-02-11 12:31:40 +0100 <ski> mhm
2023-02-11 12:32:46 +0100 <ski> (s/Type/Text/)
2023-02-11 12:33:11 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 264 seconds)
2023-02-11 12:33:38 +0100_leo___(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 12:35:06 +0100 <jtza8> ski: Sorry for not responding, I am messing with the provided code in ghci. I figured out how to use it though.
2023-02-11 12:35:21 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10)
2023-02-11 12:35:34 +0100oldfashionedcow(~Rahul_San@user/oldfashionedcow)
2023-02-11 12:36:23 +0100 <kuribas> ski: "case isJust x of Yes prf => fromJust x; No contra => def"
2023-02-11 12:36:47 +0100Inst__(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240)
2023-02-11 12:36:55 +0100 <ski> makes sense
2023-02-11 12:36:58 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 12:37:22 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 12:38:19 +0100 <kuribas> ski: case isItJust x ...
2023-02-11 12:38:41 +0100 <ski> (i figured)
2023-02-11 12:39:34 +0100 <kuribas> ski: this typechecks: https://gist.github.com/kuribas/eb6b2c38b228fcfe46c28525901996ba
2023-02-11 12:39:57 +0100Inst_(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240) (Ping timeout: 252 seconds)
2023-02-11 12:40:40 +0100Kuttenbrunzer(~Kuttenbru@2a02:8108:8b80:1d48::6ccb) (Quit: Where is it)
2023-02-11 12:41:39 +0100 <ski> is there anything like `cxt *> ty' or `{x : ty | cxt}' ?
2023-02-11 12:41:48 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2023-02-11 12:42:11 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 264 seconds)
2023-02-11 12:43:43 +0100 <kuribas> passing a constraint?
2023-02-11 12:43:55 +0100 <ski> returning a constraint
2023-02-11 12:44:18 +0100 <kuribas> you mean x + a proof on x?
2023-02-11 12:44:20 +0100 <jtza8> ski: Your notes are clear, as is your implementation.
2023-02-11 12:45:44 +0100 <kuribas> ski: dependent pair? (x : Just Int ** IsJust x)
2023-02-11 12:45:48 +0100 <ski> sort :: (o : Ord a) => List a -> {l : List a | IsSorted @{o} l} -- stuff like this, kuribas
2023-02-11 12:46:07 +0100 <ski> s/::/:/
2023-02-11 12:46:39 +0100 <ski> (you could add a constraint that the output is a permutation of the input, if you like)
2023-02-11 12:47:24 +0100 <ski> kuribas : i assume you need to match on the data constructor of `(**)', to extract `x' (and the implicit constraint) ?
2023-02-11 12:48:23 +0100merijn(~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds)
2023-02-11 12:48:27 +0100 <kuribas> ski: it's just syntax for: DPair (Just Int) Isjust
2023-02-11 12:49:38 +0100 <ski> jtza8 : fwiw, i also made `Read' be "tolerant", and be able to parse serialization that `Show' doesn't produce, lowercasing the text. one could instead have used `(GetLowerText lt,s2) <- readsPrec 11 s1', and had the result be `(lt,s2)' instead, making the parse fail in such cases
2023-02-11 12:50:28 +0100 <ski> kuribas : where `data DPair t p = MkDPair (x : t) (p x)', or somesuch ?
2023-02-11 12:50:29 +0100jmdaemon(~jmdaemon@user/jmdaemon) (Ping timeout: 255 seconds)
2023-02-11 12:50:50 +0100 <kuribas> ski: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#dependent-pairs
2023-02-11 12:51:50 +0100 <ski> right
2023-02-11 12:52:13 +0100 <ski> .. there's no parameter vs. index distinction, wrt type arguments to `data' types ?
2023-02-11 12:53:01 +0100 <kuribas> ski: I don't understand the question
2023-02-11 12:53:21 +0100 <ski> it says
2023-02-11 12:53:24 +0100 <ski> data DPair : (a : Type) -> (p : a -> Type) -> Type
2023-02-11 12:53:26 +0100 <ski> rather than
2023-02-11 12:53:37 +0100 <ski> data DPair (a : Type) (p : a -> Type) : Type
2023-02-11 12:54:00 +0100 <kuribas> ski: ah right, the second syntax is not supported.
2023-02-11 12:54:06 +0100 <kuribas> you have to use the first
2023-02-11 12:54:23 +0100 <kuribas> or use regular ADT syntax.
2023-02-11 12:54:37 +0100 <ski> in Agda, in the latter case, `a',`p' would be parameters, must be the same, in the result type of the data constructors. in the former case, they'd both be indices, and so need not be exactly `a' and `p', in the return types. (this latter case is comparable to GADTs)
2023-02-11 12:56:29 +0100 <ski> (one reason for using parameters, rather than indices, is that that can lower the universe level of the defined type, making it be at the same level as type parameters, rather than one (or more) higher)
2023-02-11 12:58:00 +0100 <kuribas> ski: I don't think the `a` in the constructor refers to the `a` in the type constructor.
2023-02-11 12:58:55 +0100 <ski> right, my reading was that `{a : Type} -> ' was inferred for the data constructor
2023-02-11 12:59:15 +0100 <ski> (but apparently, it couldn't infer the kind of `p' ?)
2023-02-11 12:59:15 +0100 <kuribas> ski: yes, that's right
2023-02-11 13:00:02 +0100 <kuribas> ski: I'd say it could...
2023-02-11 13:00:02 +0100lackita(~lackita@73.114.250.252)
2023-02-11 13:00:59 +0100 <kuribas> ski: yes, it checks just fine ommitting {p : a -> Type}
2023-02-11 13:03:42 +0100 <kuribas> ski: you can put anything in the return type of MkDPair, as long matches the DPair constructor types.
2023-02-11 13:03:47 +0100 <ski> can you supply implicit parameters, unnamed ?
2023-02-11 13:04:10 +0100 <kuribas> yes
2023-02-11 13:04:21 +0100 <ski> .. if you write `MkDPair {x}', does `x' correspond to `a' or to `p' ?
2023-02-11 13:04:23 +0100 <kuribas> {_ : a -> Type} => ...
2023-02-11 13:05:18 +0100 <kuribas> ski: neither. That's not idris syntax :) MkdPair {a=Int}
2023-02-11 13:05:33 +0100 <kuribas> or MkDPair {p=IsJust}
2023-02-11 13:05:53 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 13:05:54 +0100 <ski> so you can't *supply* it, unnamed ?
2023-02-11 13:06:01 +0100 <kuribas> ah, that's right.
2023-02-11 13:06:27 +0100 <kuribas> you can declare them unnamed, but not *supply* them unnamed.
2023-02-11 13:06:30 +0100 <ski> so in the `{_ : a -> Type} => ...' case, it would always be inferred ?
2023-02-11 13:07:02 +0100 <kuribas> auto proofs can be supplied with @{}
2023-02-11 13:07:03 +0100econo(uid147250@user/econo) (Quit: Connection closed for inactivity)
2023-02-11 13:07:08 +0100 <ski> mhm, okay
2023-02-11 13:07:32 +0100 <kuribas> but no `{_ : a -> Type} -> ...'
2023-02-11 13:07:51 +0100 <ski> does `forall a : t. ..a..' unify with `forall b : t. ..b..' ?
2023-02-11 13:08:41 +0100 <ski> hm, right. `=>' vs. `->' there .. i overlooked that
2023-02-11 13:08:41 +0100 <kuribas> I suppose so...
2023-02-11 13:09:18 +0100 <ski> so, if inferring, you have to make sure which exact names are used for implicits, since those become part of the public interface
2023-02-11 13:09:35 +0100 <kuribas> "forall a. t. ..a.." == "{0 a : Type} -> t . .. a ..."
2023-02-11 13:09:51 +0100 <kuribas> ski: right
2023-02-11 13:09:55 +0100 <ski> (well, i guess that basically means that you must give an explicit signature, if you want a stable interface)
2023-02-11 13:10:19 +0100Maeda(~Maeda@91-161-10-149.subs.proxad.net)
2023-02-11 13:10:20 +0100 <kuribas> yes
2023-02-11 13:10:37 +0100 <ski> (cf. `TypeApplications' and `forall' in Haskell)
2023-02-11 13:11:04 +0100michalz(~michalz@185.246.204.121)
2023-02-11 13:11:51 +0100 <kuribas> λΠ> (the ({0 b : Type} -> b -> b) (the (forall a. a -> a) id)) => id
2023-02-11 13:12:00 +0100 <ski> .. so it could infer either `forall a,b. ..a..b..' or `forall b,a. ..a..b..', so if you write just `..a..b..', it's not so obvious which order they'll appear in (assuming there's no type dependency between them)
2023-02-11 13:12:11 +0100 <kuribas> ski: like TypeApplications, but by name, which is much better IMO.
2023-02-11 13:12:55 +0100 <kuribas> ski: I guess order doesn't matter if you supply my name.
2023-02-11 13:13:10 +0100 <ski> i've wondered if it would be better to have `x' in `MkDPair {x}' match with `p', rather than `a'. iow, not the first, but the last, implicit, that's possible, given the context
2023-02-11 13:13:20 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Ping timeout: 248 seconds)
2023-02-11 13:13:35 +0100 <ski> (obviously, in `MkDPair {x} {y}', `x' would feed `a', and `y' feed `p')
2023-02-11 13:14:06 +0100 <kuribas> ski: but that's not valid idris syntax
2023-02-11 13:14:50 +0100 <ski> it seems like this could be a better choice, keeping things more stable, when generalizing (commonly adding more implicits "to the front") .. however, there is a potential issue with the return type being a type variable, which could possibly be instantiated with a function type with implicit parameter
2023-02-11 13:15:26 +0100 <ski> yea, i'm talking generally about dependent types (as well as polymorphism, and types vs. kinds, i suppose) here, rather than specifically about Idris
2023-02-11 13:16:32 +0100 <kuribas> ski: right, return types with implicit parameter are messy.
2023-02-11 13:16:43 +0100 <ski> already, in Idris ?
2023-02-11 13:16:49 +0100 <kuribas> yes
2023-02-11 13:17:13 +0100 <ski> okay .. perhaps it wouldn't be an effective loss, in that case
2023-02-11 13:17:17 +0100 <kuribas> I think it resolves those at the definition site, not caller site.
2023-02-11 13:17:48 +0100 <kuribas> let me test it...
2023-02-11 13:17:50 +0100biberu(~biberu@user/biberu) (Read error: Connection reset by peer)
2023-02-11 13:19:07 +0100 <kuribas> ski: you cannot pass a function with implicits to another function, those implicits will be resolved. Or rather throw an error.
2023-02-11 13:19:23 +0100 <ski> ok. no higher-rank implicits
2023-02-11 13:20:42 +0100 <ski> you can have `{foo : {bar : T} -> ...} -> ...', i presume, though ?
2023-02-11 13:20:52 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 13:21:09 +0100 <ski> hmm .. on second though, i suspect not that, either
2023-02-11 13:21:35 +0100 <kuribas> yes
2023-02-11 13:21:46 +0100 <ski> can or can't ?
2023-02-11 13:21:56 +0100 <kuribas> ah an implicit...
2023-02-11 13:22:18 +0100accord(uid568320@id-568320.hampstead.irccloud.com)
2023-02-11 13:23:05 +0100 <kuribas> I don't think that makes sense...
2023-02-11 13:23:54 +0100 <ski> if you can't have explicit parameters themselves take implcit parameters, it seems unlikely that you could have implicit parameters themselves take implicit parameters
2023-02-11 13:25:21 +0100biberu(~biberu@user/biberu)
2023-02-11 13:25:29 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 260 seconds)
2023-02-11 13:26:16 +0100 <kuribas> Hard to see without concrete example...
2023-02-11 13:27:12 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 13:29:54 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-02-11 13:30:22 +0100beteigeuze1(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 13:30:29 +0100beteigeuze1(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Client Quit)
2023-02-11 13:30:53 +0100Sinbad(~Sinbad@user/sinbad) (Ping timeout: 246 seconds)
2023-02-11 13:31:45 +0100beteigeuze1(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 13:32:05 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 265 seconds)
2023-02-11 13:32:06 +0100beteigeuze1beteigeuze
2023-02-11 13:33:55 +0100 <ski> .. sometimes i'd like non-pattern arguments to pattern synonyms
2023-02-11 13:35:26 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (WeeChat 3.8)
2023-02-11 13:35:31 +0100 <kuribas> ski: it works: https://gist.github.com/kuribas/f61ee0a2566c7123728c6494800da6d3
2023-02-11 13:35:33 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 13:36:28 +0100 <ski> interesting
2023-02-11 13:37:46 +0100 <ski> but `hogemenuett : (foo : {len : Nat} -> String -> Vect len String) -> Vect 2 String; hogemenuett foo = foo {len=2} "foobar"' doesn't work ?
2023-02-11 13:37:59 +0100 <ski> kuribas : what about calling/using the operation ?
2023-02-11 13:39:22 +0100skiidly ponders a way to make the `<expr> -> <pat>' view pattern syntax definable, as a pattern synonym (given two extensions to them, one being non-pattern arguments)
2023-02-11 13:41:00 +0100lechner(~lechner@debian/lechner) (Ping timeout: 260 seconds)
2023-02-11 13:42:34 +0100_aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 13:42:34 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Read error: Connection reset by peer)
2023-02-11 13:42:52 +0100 <kuribas> ski: https://gist.github.com/kuribas/f61ee0a2566c7123728c6494800da6d3
2023-02-11 13:43:04 +0100_aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Client Quit)
2023-02-11 13:44:54 +0100Inst_(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240)
2023-02-11 13:45:36 +0100jtza8(~user@165.255.88.238) (ERC 5.4 (IRC client for GNU Emacs 28.2))
2023-02-11 13:45:46 +0100lechner(~lechner@debian/lechner)
2023-02-11 13:47:08 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 13:47:18 +0100 <ski> kuribas : and if you make `foo' explicit, passing `motif' explicitly ?
2023-02-11 13:47:34 +0100 <kuribas> ski: works with typeclasses as well https://gist.github.com/kuribas/f61ee0a2566c7123728c6494800da6d3
2023-02-11 13:48:23 +0100Inst__(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240) (Ping timeout: 256 seconds)
2023-02-11 13:48:37 +0100 <kuribas> ski: yes, making foo explicit also works
2023-02-11 13:50:24 +0100 <kuribas> ski: you can also pass names for explicit arguments, which is something else I like about idris.
2023-02-11 13:51:06 +0100 <kuribas> ski: Good luck if you need to pass 10 arguments to a haskell functions. Well you could make an intermediate record for that.
2023-02-11 13:51:44 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 260 seconds)
2023-02-11 13:52:57 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 13:54:25 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 13:55:32 +0100 <kuribas> it can infer a and len: https://gist.github.com/kuribas/f61ee0a2566c7123728c6494800da6d3#file-infer-idr
2023-02-11 13:56:06 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 13:57:08 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 246 seconds)
2023-02-11 14:00:08 +0100 <ski> kuribas : "making foo explicit also works" -- ok, so i guess "higher-rank implicits" do work, then
2023-02-11 14:01:06 +0100 <kuribas> yes, indeed
2023-02-11 14:01:07 +0100 <ski> hm, OCaml also has labelled arguments, <https://v2.ocaml.org/manual/lablexamples.html>
2023-02-11 14:01:22 +0100zer0bitz(~zer0bitz@2001:2003:f443:d600:7430:975b:6114:c350) (Read error: Connection reset by peer)
2023-02-11 14:02:35 +0100lackita(~lackita@73.114.250.252) (Ping timeout: 248 seconds)
2023-02-11 14:03:29 +0100lackita(~lackita@73.114.250.252)
2023-02-11 14:04:46 +0100zer0bitz(~zer0bitz@2001:2003:f443:d600:50e1:610d:453c:bdaa)
2023-02-11 14:07:57 +0100lackita(~lackita@73.114.250.252) (Ping timeout: 252 seconds)
2023-02-11 14:08:26 +0100lackita(~lackita@73.114.250.252)
2023-02-11 14:09:37 +0100taylork
2023-02-11 14:10:47 +0100patrl(~patrl@user/patrl)
2023-02-11 14:13:44 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 14:15:26 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 14:19:39 +0100analoq(~yashi@user/dies) (Ping timeout: 248 seconds)
2023-02-11 14:22:52 +0100kuribas(~user@ptr-17d51emc5fl5behj2tb.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 27.1))
2023-02-11 14:26:33 +0100analoq(~yashi@user/dies)
2023-02-11 14:26:42 +0100thongpv87(~thongpv87@2402:9d80:3ad:3939:eed6:8b36:cbf5:81bd) (Read error: Connection reset by peer)
2023-02-11 14:28:37 +0100lackita(~lackita@73.114.250.252) (Ping timeout: 256 seconds)
2023-02-11 14:29:47 +0100lackita(~lackita@73.114.250.252)
2023-02-11 14:31:13 +0100Midjak(~Midjak@82.66.147.146)
2023-02-11 14:34:23 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 14:41:15 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 14:43:42 +0100thongpv87(~thongpv87@2402:9d80:32d:55ba:b7b4:35d:88f:7d73)
2023-02-11 14:45:43 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 252 seconds)
2023-02-11 14:46:01 +0100 <lackita> I'm just getting back into Haskell, and going through learn you a Haskell to refresh my memory. It seems like there's some newer stuff not covered by that tutorial, though, such as stack, and I was wondering if there was anything out there that provides a more up to date survey of
2023-02-11 14:46:08 +0100 <lackita> the ecosystem
2023-02-11 14:47:59 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 14:49:13 +0100 <Axman6> I wouldnt consider stack newer, it's an alternative, and cabal is capable of doing much of what stack was developed for these days. it's also easier to write pqckages everyone can use with cabal, because stack users can use them easily too
2023-02-11 14:51:10 +0100 <lackita> Ah, I see. That's exactly why I asked😀
2023-02-11 14:52:12 +0100 <lackita> Mostly I wanted to avoid using outdated tools out of ignorance
2023-02-11 14:57:18 +0100 <ski> lackita : "The Cabal/Stack Disambiguation Guide" <https://gist.github.com/merijn/8152d561fb8b011f9313c48d876ceb07> might be helpful to get some bearings
2023-02-11 15:04:50 +0100 <lackita> Oh, great! I'll check that out, thank you.
2023-02-11 15:10:59 +0100oldfashionedcow(~Rahul_San@user/oldfashionedcow) (Ping timeout: 264 seconds)
2023-02-11 15:14:13 +0100oldfashionedcow(~Rahul_San@user/oldfashionedcow)
2023-02-11 15:19:24 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de)
2023-02-11 15:19:34 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 268 seconds)
2023-02-11 15:26:14 +0100nattiestnate(~nate@202.138.250.17) (Ping timeout: 260 seconds)
2023-02-11 15:28:37 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 15:28:51 +0100 <[exa]> lackita: this is a pretty good introduction into the tooling https://wiki.haskell.org/How_to_write_a_Haskell_program
2023-02-11 15:30:47 +0100thebinary(~thebinary@27.34.30.111) (Client Quit)
2023-02-11 15:31:07 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 15:35:57 +0100 <jean-paul[m]> Can the most lazy IO [a] be as lazy as the most lazy [IO a]?
2023-02-11 15:36:09 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de) (Ping timeout: 260 seconds)
2023-02-11 15:37:35 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de)
2023-02-11 15:41:10 +0100 <[exa]> jean-paul[m]: I'd say yes, but it's probably not a very good idea to have more than 1 lazy IO[a] in the program and rely on any kind of ordering there
2023-02-11 15:41:34 +0100 <int-e> Not safely; IO [a] has to perform its IO effects in a fixed order, execpt for the unsafeInterleaveIO loophole.
2023-02-11 15:41:45 +0100 <[exa]> normally these contain the accursed unuterable interleaveIO (ha yes ^)
2023-02-11 15:41:45 +0100 <int-e> (which underlies "lazy IO")
2023-02-11 15:41:57 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-02-11 15:42:27 +0100 <int-e> Uh, in a fixed order, *and* they have to complete before the IO action returns a value.
2023-02-11 15:42:44 +0100 <[exa]> btw there are libraries that remove most of the surprise there, e.g. https://hackage.haskell.org/package/safe-lazy-io
2023-02-11 15:42:46 +0100 <int-e> :t mapM System.IO.Unsafe.unsafeInterleaveIO
2023-02-11 15:42:47 +0100 <lambdabot> Traversable t => t (IO b) -> IO (t b)
2023-02-11 15:43:22 +0100 <int-e> This is the "as lazy as a plain list" version and it's full of potential surprises.
2023-02-11 15:43:39 +0100 <[exa]> ( oh wait that one's from 2009, might not be valid anymore. )
2023-02-11 15:44:04 +0100 <jean-paul[m]> Okay, thanks. I have an encoded format and it supports random access but decoding is in IO, trying to figure out what API to put on top of this. [IO (Either DecodeError a)] looks kind of funny but it seems like the right path, I guess.
2023-02-11 15:44:10 +0100 <int-e> If the IO action reads and increments a counter in an IORef, the resulting list will reflect the order in which the elements are evaluated. That's fairly harmless because it doesn't involve IO.
2023-02-11 15:44:27 +0100ddellacosta(~ddellacos@143.244.47.81) (Ping timeout: 248 seconds)
2023-02-11 15:44:28 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 15:45:08 +0100 <jean-paul[m]> the decode operation probably doesn't have side-effects, but it has FFI :/
2023-02-11 15:45:25 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 15:45:41 +0100 <lackita> exa: Thanks for the link. I noticed the outdated warning at the top, are there any parts I should ignore because of that, or will it become obvious as I start searching around?
2023-02-11 15:46:50 +0100 <jean-paul[m]> [exa]: safe-lazy-io looks like fun reading, at least, thanks for the link
2023-02-11 15:47:46 +0100 <[exa]> lackita: it doesn't seem super outdated to me but if you find something that is completely borked pls report here
2023-02-11 15:48:29 +0100 <[exa]> jean-paul[m]: btw the source of `interact` and similar things might be interesting too
2023-02-11 15:48:47 +0100 <lackita> Absolutely! Have a lot of reading ahead of me, so I might take a while to get to this one, but I'll report back here if I come across something.
2023-02-11 15:49:01 +0100 <[exa]> (esp. `interact` will kinda copy the latest ghc's trends in the accursedPerformIO)
2023-02-11 15:50:55 +0100 <[exa]> lackita: well the TLDR version is: have a git repo, follow `cabal init` comments and don't overengineer it, ghcup+cabal will do in 99% cases, beware of distro packages, and if you need to have a project made of multiple packages, there's now cabal.project functionality: https://cabal.readthedocs.io/en/3.4/cabal-project.html .
2023-02-11 15:51:30 +0100skiidly wonders why jean-paul[m]'s adding starting, but not ending, monospace markup codes
2023-02-11 15:51:31 +0100 <int-e> jean-paul[m]: If decoding doesn't do any actual IO but only accesses memory, you /may/ even have a valid use case for unsafePerformIO. Of course venturing there is always scary.
2023-02-11 15:51:39 +0100 <lackita> Oh, I see. That's interesting
2023-02-11 15:51:57 +0100 <ski> jean-paul[m] : does those FFI operations perform (I/O) effects ?
2023-02-11 15:52:01 +0100 <jean-paul[m]> int-e: Yea too scary for me for now.
2023-02-11 15:52:32 +0100 <int-e> ski: wait is that what this does?
2023-02-11 15:52:47 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 248 seconds)
2023-02-11 15:53:28 +0100 <ski> `mapM unsafeInterleaveIO' is probably mostly useless .. comparable to spawning one thread for each action
2023-02-11 15:53:29 +0100 <[exa]> wait guys your terminal font isn't monospace by default?
2023-02-11 15:53:39 +0100 <ski> int-e : .. at least in some clients, yes
2023-02-11 15:53:48 +0100 <int-e> [exa]: mine is, but I see the control character as an inverted Q
2023-02-11 15:53:52 +0100td_(~td@i53870908.versanet.de) (Ping timeout: 248 seconds)
2023-02-11 15:53:57 +0100 <jean-paul[m]> ski: What counts as I/O effects? They allocate memory and copy bytes around. Actually, I said "just FFI" but the memory is allocated by Haskell APIs (like `allocaBytes`) on the way to the actual FFI.
2023-02-11 15:54:10 +0100 <int-e> (it's ASCII 0x11 = Ctrl-Q)
2023-02-11 15:55:41 +0100__monty__(~toonn@user/toonn)
2023-02-11 15:58:23 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea)
2023-02-11 15:59:29 +0100lackita(~lackita@73.114.250.252) (Remote host closed the connection)
2023-02-11 15:59:48 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 16:00:12 +0100lackita(~lackita@73.114.250.252)
2023-02-11 16:00:36 +0100 <ski> int-e : BboldB,_underlined_,VinverseV,]italicized],FblinkingF,^struckthrough^,QmonospacedQ
2023-02-11 16:00:54 +0100td_(~td@i53870908.versanet.de)
2023-02-11 16:01:23 +0100MQ-17J(~MQ-17J@104.28.216.166) (Ping timeout: 246 seconds)
2023-02-11 16:01:29 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 16:02:05 +0100 <ski> (included inverse-glyphs, for emphasis / description of which control code is used)
2023-02-11 16:02:41 +0100 <ski> jean-paul[m] : do they overwrite initialized memory that could be accessed before ?
2023-02-11 16:03:05 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea) (Ping timeout: 255 seconds)
2023-02-11 16:04:13 +0100Sinbad(~Sinbad@user/sinbad)
2023-02-11 16:05:22 +0100merijn(~merijn@86-86-29-250.fixed.kpn.net)
2023-02-11 16:07:28 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 16:08:08 +0100 <geekosaur> ski, the bridge adds the monospace starting cde but uses the "back to normal" (ctrl-O iirc) to end it
2023-02-11 16:08:49 +0100 <geekosaur> rather than treating as a toggle
2023-02-11 16:09:03 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 16:09:05 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 16:10:55 +0100merijn(~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds)
2023-02-11 16:11:26 +0100ski. o O ( <https://modern.ircdocs.horse/formatting.html#characters>,<https://www.mirc.com/help/html/control_codes.html>,<https://www.mirc.com/colors.html>,<https://web.archive.org/web/20120211151852/http://ircle.com:80/colorfaq.shtml> )
2023-02-11 16:11:35 +0100 <ski> geekosaur : ah, that explains it. ty
2023-02-11 16:12:19 +0100 <ski> [exa] : i imagine some (by default) non-monospace (/ variable-width) clients interpret it
2023-02-11 16:16:04 +0100analoq(~yashi@user/dies) (Ping timeout: 252 seconds)
2023-02-11 16:16:23 +0100 <ski> .. perhaps there ought to be a `mapInterleaveIO :: forall a b. (a -> IO b) -> (t a -> IO (t b))', that uses `unsafeInterleaveIO's around each substructure
2023-02-11 16:17:54 +0100analoq(~yashi@user/dies)
2023-02-11 16:19:36 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 16:22:09 +0100gnalzo(~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8)
2023-02-11 16:22:21 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 16:23:01 +0100Deide(~deide@user/deide)
2023-02-11 16:23:55 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 16:27:12 +0100 <ski> % let mapListInterleaveIO :: forall a b. (a -> IO b) -> ([a] -> IO [b]); mapListInterleaveIO _ [] = pure []; mapListInterleaveIO f (x:xs) = unsafeInterleaveIO (liftM2 (:) (f x) (mapListInterleaveIO f xs))
2023-02-11 16:27:12 +0100 <yahb2> <no output>
2023-02-11 16:27:31 +0100 <ski> % let mapTreeInterleaveIO :: forall a b. (a -> IO b) -> (Tree a -> IO (Tree b)); mapTreeInterleaveIO f (Node x ts) = unsafeInterleaveIO (liftM2 Node (f x) (mapListInterleaveIO (mapTreeInterleaveIO f) ts))
2023-02-11 16:27:31 +0100 <yahb2> <no output>
2023-02-11 16:27:37 +0100gurkenglas(~gurkengla@dynamic-046-114-182-197.46.114.pool.telefonica.de) (Ping timeout: 252 seconds)
2023-02-11 16:29:19 +0100gurkenglas(~gurkengla@dynamic-002-247-242-221.2.247.pool.telefonica.de)
2023-02-11 16:38:17 +0100ddellacosta(~ddellacos@143.244.47.100)
2023-02-11 16:39:52 +0100Feuermagier_(~Feuermagi@user/feuermagier)
2023-02-11 16:41:01 +0100 <jean-paul[m]> ski: no, they only write to memory they allocate
2023-02-11 16:42:47 +0100Feuermagier(~Feuermagi@user/feuermagier) (Ping timeout: 264 seconds)
2023-02-11 16:43:40 +0100 <ski> jean-paul[m] : and that memory is never changed thereafter ?
2023-02-11 16:44:27 +0100zeenk(~zeenk@2a02:2f04:a214:1e00::7fe)
2023-02-11 16:45:19 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt) (Remote host closed the connection)
2023-02-11 16:45:47 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-02-11 16:45:59 +0100razetime(~Thunderbi@117.193.3.217)
2023-02-11 16:46:20 +0100beteigeuze(~Thunderbi@bl14-81-220.dsl.telepac.pt)
2023-02-11 16:46:23 +0100 <jean-paul[m]> yes, it gets fed into something like packCStringLen and then freed before the IO is over
2023-02-11 16:47:26 +0100 <jean-paul[m]> However, I was previously using a version of the decoder that used unsafePerformIO instead of presenting the interface in IO and I got result corruption that I could never explain
2023-02-11 16:47:53 +0100 <jean-paul[m]> so I'm not confident I fully understand it
2023-02-11 16:48:13 +0100 <jean-paul[m]> (although I guess I also tested a version w/o unsafePerformIO and still got result corruption ... :shrug:)
2023-02-11 16:51:55 +0100infinity0(~infinity0@pwned.gg) (Remote host closed the connection)
2023-02-11 16:52:02 +0100 <ski> jean-paul[m] : that could be okay, not counted as (visible) I/O effects, i think, then. but you'd still most likely need `IO' all over "on the inside", to properly sequence the allocation, initialization, access, deallocation .. the access is on the other side of the FFI (only), i assume ?
2023-02-11 16:52:22 +0100codedmart(~codedmart@li335-49.members.linode.com)
2023-02-11 16:54:03 +0100infinity0(~infinity0@pwned.gg)
2023-02-11 16:58:11 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 16:58:36 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 16:58:47 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542)
2023-02-11 16:59:38 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-02-11 17:00:33 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2023-02-11 17:01:24 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 17:03:29 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 17:06:52 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 17:08:06 +0100lackita(~lackita@73.114.250.252) (Ping timeout: 268 seconds)
2023-02-11 17:08:16 +0100lackita(~lackita@73.114.250.252)
2023-02-11 17:11:43 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5)
2023-02-11 17:12:00 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 265 seconds)
2023-02-11 17:12:28 +0100Guest13(~Guest13@2001:9e8:33db:6300:99e:8fec:c423:bf5)
2023-02-11 17:12:28 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 17:13:26 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 17:15:01 +0100shapr(~user@host-79-37-239-243.retail.telecomitalia.it)
2023-02-11 17:16:06 +0100thongpv87(~thongpv87@2402:9d80:32d:55ba:b7b4:35d:88f:7d73) (Read error: Connection reset by peer)
2023-02-11 17:17:31 +0100lackita(~lackita@73.114.250.252) (Ping timeout: 260 seconds)
2023-02-11 17:17:49 +0100lackita(~lackita@73.114.250.252)
2023-02-11 17:18:58 +0100 <rendar> where can i get a cheatsheet of all haskell vector operations? like fold, and others?
2023-02-11 17:19:20 +0100Guest13(~Guest13@2001:9e8:33db:6300:99e:8fec:c423:bf5) (Quit: Client closed)
2023-02-11 17:19:37 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 17:19:49 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 17:22:23 +0100gehmehgeh(~user@user/gehmehgeh) (Ping timeout: 255 seconds)
2023-02-11 17:22:57 +0100 <Hecate> :qa!
2023-02-11 17:23:00 +0100 <Hecate> (woops)
2023-02-11 17:23:18 +0100gehmehgeh(~user@user/gehmehgeh)
2023-02-11 17:24:03 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5) (Ping timeout: 260 seconds)
2023-02-11 17:24:40 +0100 <jean-paul[m]> ski: Read access to the data? It's on the Haskell side
2023-02-11 17:28:46 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 17:29:05 +0100 <jean-paul[m]> (The code is public fwiw, https://gitlab.com/exarkun/chk.hs/-/blob/master/src/Tahoe/ZFEC.hs#L43 and corresponding decode below it)
2023-02-11 17:29:31 +0100 <jean-paul[m]> although I notice now the comment about memory management responsibilities is outdated and incorrect
2023-02-11 17:31:07 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 17:31:56 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 17:33:26 +0100gehmehgeh(~user@user/gehmehgeh) (Remote host closed the connection)
2023-02-11 17:33:47 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 248 seconds)
2023-02-11 17:34:14 +0100gehmehgeh(~user@user/gehmehgeh)
2023-02-11 17:34:38 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 17:37:41 +0100jpds(~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds)
2023-02-11 17:38:51 +0100rettahcay(~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) ()
2023-02-11 17:39:01 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 256 seconds)
2023-02-11 17:40:21 +0100wootehfoot(~wootehfoo@user/wootehfoot)
2023-02-11 17:40:49 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 17:41:08 +0100jpds(~jpds@gateway/tor-sasl/jpds)
2023-02-11 17:42:09 +0100Sinbad(~Sinbad@user/sinbad) (Quit: WeeChat 3.8)
2023-02-11 17:43:36 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5)
2023-02-11 17:44:23 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 17:45:35 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5) (Remote host closed the connection)
2023-02-11 17:48:55 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5)
2023-02-11 17:54:42 +0100dsrt^(~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Ping timeout: 255 seconds)
2023-02-11 17:59:24 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 17:59:34 +0100tremon(~tremon@83-85-213-108.cable.dynamic.v4.ziggo.nl)
2023-02-11 18:00:25 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 18:01:12 +0100 <docter_d> Cool idea with the cheat sheet, I don't know, where you can get one, but could you provide a link, if you found one, please?
2023-02-11 18:01:28 +0100Guest13(~Guest13@2001:9e8:33db:6300:99e:8fec:c423:bf5)
2023-02-11 18:01:43 +0100Guest13(~Guest13@2001:9e8:33db:6300:99e:8fec:c423:bf5) (Client Quit)
2023-02-11 18:04:21 +0100waleee(~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7)
2023-02-11 18:06:38 +0100jero98772(~jero98772@2800:484:1d80:d8ce:9815:cfda:3661:17bb)
2023-02-11 18:07:44 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 246 seconds)
2023-02-11 18:09:00 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net)
2023-02-11 18:14:43 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
2023-02-11 18:16:01 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2023-02-11 18:22:15 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Quit: au revoir)
2023-02-11 18:25:13 +0100razetime(~Thunderbi@117.193.3.217) (Remote host closed the connection)
2023-02-11 18:27:16 +0100[docter_d](~{docter_d@183-182-142-46.pool.kielnet.net)
2023-02-11 18:27:53 +0100 <ddellacosta> rendar: are you talking about https://hackage.haskell.org/package/vector-0.13.0.0/docs/Data-Vector.html or something else?
2023-02-11 18:28:41 +0100 <rendar> ddellacosta, well, Foldable seems like an interface, not a real function like 'fold'
2023-02-11 18:29:53 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 18:30:04 +0100oldfashionedcowrrogalski[rich]
2023-02-11 18:30:40 +0100docter_d(~{docter_d@2001:9e8:33db:6300:99e:8fec:c423:bf5) (Ping timeout: 248 seconds)
2023-02-11 18:31:49 +0100 <ddellacosta> rendar: I'm not sure I understand what you're looking for, sorry--but the API docs for vector provide documentation of the operations you can perform on them, if that helps
2023-02-11 18:34:10 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 265 seconds)
2023-02-11 18:36:57 +0100rrogalski[rich]oldfashionedcow
2023-02-11 18:37:34 +0100tzh(~tzh@c-24-21-73-154.hsd1.or.comcast.net)
2023-02-11 18:37:55 +0100 <ddellacosta> just realized all the vector APIs are all implemented through the Generic API, that's pretty neat
2023-02-11 18:40:38 +0100zeenk(~zeenk@2a02:2f04:a214:1e00::7fe) (Quit: Konversation terminated!)
2023-02-11 18:42:10 +0100 <rendar> ok
2023-02-11 18:43:30 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 18:47:34 +0100NanaLi96(~NanaLi96@37.140.28.200)
2023-02-11 18:48:24 +0100gnalzo(~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
2023-02-11 18:51:21 +0100NanaLi96(~NanaLi96@37.140.28.200) (Client Quit)
2023-02-11 18:55:07 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 19:04:16 +0100oldfashionedcow(~Rahul_San@user/oldfashionedcow) (Ping timeout: 248 seconds)
2023-02-11 19:04:19 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Changing host)
2023-02-11 19:04:19 +0100aljer(~j@user/aljer)
2023-02-11 19:04:30 +0100aljer(~j@user/aljer) (WeeChat 3.8)
2023-02-11 19:04:37 +0100aljer(~j@user/aljer)
2023-02-11 19:05:28 +0100[docter_d](~{docter_d@183-182-142-46.pool.kielnet.net) (Ping timeout: 252 seconds)
2023-02-11 19:10:49 +0100econo(uid147250@user/econo)
2023-02-11 19:14:23 +0100aljer(~j@user/aljer) (Ping timeout: 248 seconds)
2023-02-11 19:22:10 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.)
2023-02-11 19:23:26 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10)
2023-02-11 19:26:06 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2023-02-11 19:28:50 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds)
2023-02-11 19:31:36 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 19:40:16 +0100jakalx(~jakalx@base.jakalx.net) ()
2023-02-11 19:43:13 +0100thebinary(~thebinary@27.34.30.111)
2023-02-11 19:45:02 +0100thebinary(~thebinary@27.34.30.111) (Read error: Connection reset by peer)
2023-02-11 19:45:28 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 19:48:34 +0100eruditass(uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2023-02-11 19:49:54 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 260 seconds)
2023-02-11 19:57:56 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea)
2023-02-11 19:59:19 +0100Inst(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240)
2023-02-11 20:00:13 +0100Inst(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240) (Remote host closed the connection)
2023-02-11 20:00:30 +0100Inst(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240)
2023-02-11 20:01:52 +0100Inst_(~Inst@2601:6c4:4081:54f0:d621:5cdd:9051:c240) (Ping timeout: 248 seconds)
2023-02-11 20:07:44 +0100eruditass(uid248673@id-248673.uxbridge.irccloud.com)
2023-02-11 20:08:58 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 20:14:02 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2023-02-11 20:14:15 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666)
2023-02-11 20:14:15 +0100aljer(~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Changing host)
2023-02-11 20:14:15 +0100aljer(~j@user/aljer)
2023-02-11 20:15:48 +0100aljer(~j@user/aljer) (Client Quit)
2023-02-11 20:16:03 +0100aljer(~j@user/aljer)
2023-02-11 20:19:23 +0100shapr(~user@host-79-37-239-243.retail.telecomitalia.it) (Ping timeout: 264 seconds)
2023-02-11 20:31:20 +0100im_bad_at_haskel(~im_bad_at@2a02:a03f:acfa:b800:11d9:a516:6526:b192)
2023-02-11 20:31:47 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 20:31:48 +0100 <im_bad_at_haskel> is this an appropriate place to ask questions?
2023-02-11 20:31:55 +0100 <geekosaur> yes
2023-02-11 20:32:10 +0100 <hpc> you only get one though, and that was it :P
2023-02-11 20:32:31 +0100 <im_bad_at_haskel> ``run :: (a -> Maybe b) -> [a] -> ([b], [a])
2023-02-11 20:32:31 +0100 <im_bad_at_haskel> run  = first reverse . go []
2023-02-11 20:32:32 +0100 <im_bad_at_haskel>   where
2023-02-11 20:32:32 +0100 <im_bad_at_haskel>     go :: [b] -> (a -> Maybe b) -> [a] -> ([b], [a])
2023-02-11 20:32:33 +0100 <im_bad_at_haskel>     go _ _ []           = ([], [])
2023-02-11 20:32:33 +0100 <im_bad_at_haskel>     go accum f l@(a:as) =
2023-02-11 20:32:34 +0100 <im_bad_at_haskel>         case f a of
2023-02-11 20:32:34 +0100 <im_bad_at_haskel>             Nothing -> (accum, l)
2023-02-11 20:32:35 +0100 <im_bad_at_haskel>             Just b  -> go (b:accum) f as
2023-02-11 20:32:35 +0100 <im_bad_at_haskel> `` my intuition tells me that this should typecheck but ghc says otherwise
2023-02-11 20:33:26 +0100 <im_bad_at_haskel> sorry for the messed up markdown, still figuring this out
2023-02-11 20:33:32 +0100 <im_bad_at_haskel> `run :: (a -> Maybe b) -> [a] -> ([b], [a])
2023-02-11 20:33:32 +0100 <im_bad_at_haskel> run  = first reverse . go []
2023-02-11 20:33:33 +0100 <im_bad_at_haskel>   where
2023-02-11 20:33:33 +0100 <im_bad_at_haskel>     go :: [b] -> (a -> Maybe b) -> [a] -> ([b], [a])
2023-02-11 20:33:34 +0100 <im_bad_at_haskel>     go _ _ []           = ([], [])
2023-02-11 20:33:34 +0100 <im_bad_at_haskel>     go accum f l@(a:as) =
2023-02-11 20:33:35 +0100 <im_bad_at_haskel>         case f a of
2023-02-11 20:33:35 +0100 <im_bad_at_haskel>             Nothing -> (accum, l)
2023-02-11 20:33:36 +0100 <im_bad_at_haskel>             Just b  -> go (b:accum) f as
2023-02-11 20:33:36 +0100 <im_bad_at_haskel> `
2023-02-11 20:33:39 +0100 <hpc> @where paste
2023-02-11 20:33:39 +0100 <lambdabot> Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com
2023-02-11 20:34:21 +0100 <hpc> what is the error?
2023-02-11 20:34:35 +0100 <im_bad_at_haskel> https://paste.tomsmeding.com/4bPEEbcT
2023-02-11 20:35:30 +0100 <hpc> :t first
2023-02-11 20:35:31 +0100 <lambdabot> Arrow a => a b c -> a (b, d) (c, d)
2023-02-11 20:35:50 +0100 <im_bad_at_haskel> oh sorry, first is from BiFunctor if this is not clear
2023-02-11 20:36:11 +0100 <im_bad_at_haskel> this one https://hackage.haskell.org/package/base-4.17.0.0/docs/src/Data.Bifunctor.html#first
2023-02-11 20:36:16 +0100 <sm> meta: what is the chat client / pasting method that causes one message per line ? I see it happen quite a bit
2023-02-11 20:37:04 +0100 <hpc> hmm
2023-02-11 20:37:27 +0100 <hpc> oh, you're not doing the function composition right
2023-02-11 20:37:52 +0100 <geekosaur> any normal IRC client. things like matrix or irccloud will make pastebins out of multiline pastes, but normal clients paste lines
2023-02-11 20:37:59 +0100 <hpc> (first reverse . go []) is \x -> (\y -> first reverse (go [] y)) x
2023-02-11 20:38:08 +0100aljer(~j@user/aljer) (Ping timeout: 248 seconds)
2023-02-11 20:38:11 +0100 <yushyin> sm: that's the usual behavior for irc chat clients with c&p that contains newlines, some clients do warn you if you try to do that (e.g. weechat)
2023-02-11 20:38:21 +0100 <hpc> so it thinks the result of (first reverse subexpr) is a function that you can apply x to
2023-02-11 20:38:32 +0100 <im_bad_at_haskel> hmm
2023-02-11 20:38:40 +0100 <hpc> try just writing "run f as = first reverse (go [] f as)
2023-02-11 20:38:54 +0100 <sm> hmm.. I guess you're right, you'd think they would all have built-in protection in 2023
2023-02-11 20:39:39 +0100 <geekosaur> well, I just used it productively in another channel. but it all went into the buffer with visible-ized newlines, and I edited it there to make it fit better
2023-02-11 20:39:42 +0100 <im_bad_at_haskel> hpc thanks this typechecks
2023-02-11 20:39:44 +0100 <geekosaur> (hexchat)
2023-02-11 20:40:14 +0100 <im_bad_at_haskel> but im still wondering because i told that when a function argument appears on both sides of = i could remove it
2023-02-11 20:40:19 +0100 <im_bad_at_haskel> *got told
2023-02-11 20:40:36 +0100 <hpc> that's the nice thing about irssi, pasting a bunch of stuff carelessly into a terminal is a mistake just in general so it doesn't need a did-you-mean :P
2023-02-11 20:41:00 +0100 <yushyin> you would also think that ircv3 multiline would have finally been finalized in 2023
2023-02-11 20:41:14 +0100 <hpc> im_bad_at_haskel: for one argument it works, for more you have to do more function composition
2023-02-11 20:41:26 +0100 <hpc> @pl \x y -> f (g x y)
2023-02-11 20:41:26 +0100 <lambdabot> (f .) . g
2023-02-11 20:41:35 +0100 <hpc> @pl \a b c d e f g -> f (g a b c d e f g)
2023-02-11 20:41:36 +0100 <lambdabot> ((((ap (.) .) .) .) .) . flip flip id . ((flip . ((flip . ((flip . ((flip . (ap .) . flip) .) . flip) .) . flip) .) . flip) .) . flip . flip id
2023-02-11 20:41:56 +0100 <hpc> er
2023-02-11 20:42:03 +0100 <hpc> @pl \a b c d e -> f (g a b c d e)
2023-02-11 20:42:03 +0100 <lambdabot> ((((f .) .) .) .) . g
2023-02-11 20:42:05 +0100 <geekosaur> using f and g twice there didn't help 🙂
2023-02-11 20:45:40 +0100jero98772(~jero98772@2800:484:1d80:d8ce:9815:cfda:3661:17bb) (Ping timeout: 260 seconds)
2023-02-11 20:48:25 +0100harveypwca(~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67)
2023-02-11 20:58:13 +0100jero98772(~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff)
2023-02-11 20:59:02 +0100gehmehgehgmg
2023-02-11 21:00:45 +0100 <monochrom> Recall "simplify (x-a)(x-b)...(x-z)" >:)
2023-02-11 21:04:20 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds)
2023-02-11 21:06:32 +0100 <hpc> my only regret is never answering one of those questions with "it's already pretty simple"
2023-02-11 21:07:09 +0100 <hpc> i did that in a logic class though, we had to rewrite this big long mess of forall/exists in a way that didn't use logical negation
2023-02-11 21:07:17 +0100 <hpc> so i just worked it out and wrote "true"
2023-02-11 21:07:59 +0100nattiestnate(~nate@202.138.250.62)
2023-02-11 21:13:26 +0100AWizzArd(~code@user/awizzard)
2023-02-11 21:14:35 +0100ddellacosta(~ddellacos@143.244.47.100) (Ping timeout: 248 seconds)
2023-02-11 21:14:54 +0100 <darkling> That sort of behaviour will get you either no marks at all, or full marks and "don't do that again". :)
2023-02-11 21:16:41 +0100ddellacosta(~ddellacos@146.70.165.10)
2023-02-11 21:17:02 +0100gurkenglas(~gurkengla@dynamic-002-247-242-221.2.247.pool.telefonica.de) (Ping timeout: 246 seconds)
2023-02-11 21:17:50 +0100 <hpc> i got a red "?" that was crossed out and a checkmark :D
2023-02-11 21:18:10 +0100 <hpc> also i was the only one to get 100% on that test
2023-02-11 21:18:51 +0100 <darkling> :)
2023-02-11 21:19:10 +0100jeetelongname(~jeet@217.79.169.181)
2023-02-11 21:22:26 +0100 <mauke> reminds me of https://www.spoj.com/problems/TAUT/
2023-02-11 21:22:32 +0100 <mauke> I solved that one using regexes
2023-02-11 21:23:42 +0100trev(~trev@user/trev) (Remote host closed the connection)
2023-02-11 21:24:10 +0100simeon(~simeon@143.231.7.51.dyn.plus.net)
2023-02-11 21:25:37 +0100 <hpc> hah, i can see it
2023-02-11 21:33:40 +0100pavonia(~user@user/siracusa)
2023-02-11 21:34:36 +0100lackita(~lackita@73.114.250.252) (Read error: Connection reset by peer)
2023-02-11 21:35:09 +0100lackita(~lackita@73.114.250.252)
2023-02-11 21:41:22 +0100jakalx(~jakalx@base.jakalx.net)
2023-02-11 21:45:07 +0100MQ-17J(~MQ-17J@d192-24-122-179.try.wideopenwest.com)
2023-02-11 21:51:33 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 21:52:05 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 21:53:47 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:54db:de44:4607:1cea) (Remote host closed the connection)
2023-02-11 21:56:15 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Ping timeout: 260 seconds)
2023-02-11 21:56:25 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10)
2023-02-11 21:56:41 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 21:57:06 +0100Sgeo(~Sgeo@user/sgeo)
2023-02-11 21:57:16 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 21:58:55 +0100wroathe(~wroathe@50.205.197.50)
2023-02-11 21:58:55 +0100wroathe(~wroathe@50.205.197.50) (Changing host)
2023-02-11 21:58:55 +0100wroathe(~wroathe@user/wroathe)
2023-02-11 22:02:53 +0100fryguybob(~fryguybob@cpe-24-94-51-210.stny.res.rr.com)
2023-02-11 22:03:41 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 22:04:37 +0100emmanuelux(~emmanuelu@user/emmanuelux)
2023-02-11 22:07:36 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678)
2023-02-11 22:11:26 +0100jmdaemon(~jmdaemon@user/jmdaemon)
2023-02-11 22:17:01 +0100takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2023-02-11 22:23:17 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.)
2023-02-11 22:23:24 +0100sammelweis(~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10)
2023-02-11 22:25:36 +0100Me-me(~me-me@2602:ff16:3:0:1:dc:beef:d00d) (Changing host)
2023-02-11 22:25:36 +0100Me-me(~me-me@user/me-me)
2023-02-11 22:27:05 +0100nabaiste^(~nabaiste@c-24-30-76-89.hsd1.ga.comcast.net)
2023-02-11 22:29:44 +0100tremon(~tremon@83-85-213-108.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
2023-02-11 22:38:01 +0100wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2023-02-11 22:45:14 +0100justsomeguy(~justsomeg@user/justsomeguy)
2023-02-11 22:46:29 +0100im_bad_at_haskel(~im_bad_at@2a02:a03f:acfa:b800:11d9:a516:6526:b192) (Quit: Client closed)
2023-02-11 22:46:46 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection)
2023-02-11 22:47:02 +0100freeside(~mengwong@103.252.202.170)
2023-02-11 22:51:27 +0100freeside(~mengwong@103.252.202.170) (Ping timeout: 248 seconds)
2023-02-11 22:52:31 +0100MQ-17J(~MQ-17J@d192-24-122-179.try.wideopenwest.com) (Read error: Connection reset by peer)
2023-02-11 22:53:09 +0100MQ-17J(~MQ-17J@104.28.216.166)
2023-02-11 22:58:07 +0100ddellacosta(~ddellacos@146.70.165.10) (Ping timeout: 252 seconds)
2023-02-11 22:58:56 +0100Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 248 seconds)
2023-02-11 23:01:24 +0100Guest18(~Guest18@2601:580:c081:42a0:cc14:d8d2:eb40:8988)
2023-02-11 23:02:28 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
2023-02-11 23:06:38 +0100_leo___(~emmanuelu@user/emmanuelux)
2023-02-11 23:10:07 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 248 seconds)
2023-02-11 23:11:07 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection)
2023-02-11 23:12:12 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2023-02-11 23:14:43 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
2023-02-11 23:15:13 +0100Guest18(~Guest18@2601:580:c081:42a0:cc14:d8d2:eb40:8988) (Quit: Client closed)
2023-02-11 23:18:55 +0100Maxdamantus(~Maxdamant@user/maxdamantus)
2023-02-11 23:23:28 +0100justsomeguy(~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds)
2023-02-11 23:30:30 +0100 <geekosaur> mm, it looks like I have a proposal. (not filed yet, but I have everything I need to know)
2023-02-11 23:31:19 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl)
2023-02-11 23:32:25 +0100 <geekosaur> basically, generalize exclusion of implicit Prelude import from import warnings so explicit imports can also use it. likely to be of interest for alternative preludes, Linear.Prelude, XMonad, probably some other "import everything" / EDSL "prelude" modules
2023-02-11 23:32:30 +0100simeon(~simeon@143.231.7.51.dyn.plus.net) (Ping timeout: 260 seconds)
2023-02-11 23:32:50 +0100 <geekosaur> the machinery exists and can be reused as is, all that's needed is syntax for it
2023-02-11 23:34:52 +0100 <[exa]> `importprelude` ?
2023-02-11 23:38:56 +0100 <geekosaur> currently thinking either `import Module (..)` or `import Module {-# EVERYTHING #-}`
2023-02-11 23:40:28 +0100merijn(~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds)
2023-02-11 23:40:32 +0100 <geekosaur> I'll include a few possibilities for discussion in the proposal when I file it
2023-02-11 23:41:36 +0100 <geekosaur> considered reusing {-# COMPLETE #-} but that gives older compilers heartburn, whereas one of the intents of using a pragma is -Wno-unrecognized-pragmas is enough for backward compatibility
2023-02-11 23:41:47 +0100Midjak(~Midjak@82.66.147.146) (Ping timeout: 252 seconds)
2023-02-11 23:43:00 +0100_leo___(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 23:43:04 +0100Midjak(~Midjak@82.66.147.146)
2023-02-11 23:43:20 +0100_leo___(~emmanuelu@user/emmanuelux)
2023-02-11 23:43:47 +0100 <[exa]> {-# ECOSYSTEM #-} import MyPrelude could work
2023-02-11 23:44:05 +0100 <[Leary]> (..) is much better than a big ugly pragma, since it already means the right thing.
2023-02-11 23:44:16 +0100 <geekosaur> the proposal process was almost enough to put me off it, but the fact that all that's needed is a way to set `ifaceImplicit` makes me a little more hopeful it'll be accepted
2023-02-11 23:44:31 +0100 <[exa]> would be good to actually give a bit of semantics, for other kinds of everythingimports stuff might need to be different
2023-02-11 23:44:41 +0100 <geekosaur> yeh, [Leary], plus I'm thinking that being explicit is Good
2023-02-11 23:45:10 +0100 <[exa]> anyway yeah (..) is almost self-explanatory
2023-02-11 23:45:25 +0100_leo___(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2023-02-11 23:45:48 +0100_leo___(~emmanuelu@user/emmanuelux)
2023-02-11 23:47:14 +0100 <geekosaur> my other thought was (_) since _ already means "wildcard", but (a) typed holes and such weaken that (b) import lists already use (..) for that
2023-02-11 23:47:41 +0100bgs(~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection)
2023-02-11 23:48:29 +0100 <geekosaur> my main reasons for spitballing a pragma were (1) using new syntax to silence a warning seems like swatting a fly with a sledgehammer (2) easier backwards compatibility
2023-02-11 23:48:47 +0100mechap(~mechap@user/mechap) (Ping timeout: 264 seconds)
2023-02-11 23:50:18 +0100mechap(~mechap@user/mechap)
2023-02-11 23:50:44 +0100 <geekosaur> so I'll include all this in the proposal and let the community decide what if anything they prefer for it
2023-02-11 23:51:02 +0100 <hpc> hmm, it has a nice consistency
2023-02-11 23:51:05 +0100 <[Leary]> We already have at least one extension that changes import syntax for no better reason.