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