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