IRCBrowse

2023/11/09

2023-11-09 00:00:41 +0100 <EvanR> m >>= f = Hyp (\k -> invoke (f (invoke m (Hyp (invoke k . (>>=f))))) k)
2023-11-09 00:01:50 +0100 <EvanR> "I won’t pretend to understand what’s going on here, but it looks a little like a nested reader monad."
2023-11-09 00:03:30 +0100wroathe(~wroathe@50.205.197.50)
2023-11-09 00:03:30 +0100wroathe(~wroathe@50.205.197.50) (Changing host)
2023-11-09 00:03:30 +0100wroathe(~wroathe@user/wroathe)
2023-11-09 00:04:51 +0100Benzi-Junior(~BenziJuni@88-149-64-112.du.xdsl.is) (Server closed connection)
2023-11-09 00:06:38 +0100Benzi-Junior(~BenziJuni@88-149-64-112.du.xdsl.is)
2023-11-09 00:08:41 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 00:10:30 +0100terrorjack(~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat)
2023-11-09 00:12:27 +0100terrorjack(~terrorjac@2a01:4f8:c17:87f8::)
2023-11-09 00:14:42 +0100 <monochrom> c_wraith: I.e., infinite types can curse your code! >:)
2023-11-09 00:17:07 +0100neceve(~neceve@user/neceve) (Ping timeout: 255 seconds)
2023-11-09 00:17:58 +0100 <jackdk> ski: "A Poor Man's Concurrency Monad" is a really cool paper I hadn't seen before. Thanks for linking it.
2023-11-09 00:21:25 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net)
2023-11-09 00:23:18 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 00:25:51 +0100mechap(~mechap@user/mechap) (Ping timeout: 240 seconds)
2023-11-09 00:25:58 +0100[_](~itchyjunk@user/itchyjunk/x-7353470)
2023-11-09 00:27:35 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 252 seconds)
2023-11-09 00:28:06 +0100zetef(~quassel@5.2.182.98) (Remote host closed the connection)
2023-11-09 00:29:29 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 255 seconds)
2023-11-09 00:36:16 +0100Sgeo(~Sgeo@user/sgeo)
2023-11-09 00:36:55 +0100Tuplanolla(~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.)
2023-11-09 00:41:43 +0100wroathe(~wroathe@user/wroathe) (Quit: leaving)
2023-11-09 00:54:05 +0100jmdaemon(~jmdaemon@user/jmdaemon) (Read error: Connection reset by peer)
2023-11-09 00:54:50 +0100jmdaemon(~jmdaemon@user/jmdaemon)
2023-11-09 00:56:12 +0100monochrom(trebla@216.138.220.146) (Quit: ZNC 1.8.2+deb3build2 - https://znc.in)
2023-11-09 00:58:56 +0100monochrom(trebla@216.138.220.146)
2023-11-09 01:00:02 +0100jmdaemon(~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds)
2023-11-09 01:02:59 +0100notzmv(~zmv@user/notzmv)
2023-11-09 01:13:17 +0100Lycurgus(~georg@li1192-118.members.linode.com)
2023-11-09 01:13:17 +0100Lycurgus(~georg@li1192-118.members.linode.com) (Changing host)
2023-11-09 01:13:17 +0100Lycurgus(~georg@user/Lycurgus)
2023-11-09 01:29:39 +0100infinity0(~infinity0@pwned.gg) (Remote host closed the connection)
2023-11-09 01:35:25 +0100infinity0(~infinity0@pwned.gg)
2023-11-09 01:39:11 +0100falafel(~falafel@62.175.113.194.dyn.user.ono.com)
2023-11-09 01:44:53 +0100jmdaemon(~jmdaemon@user/jmdaemon)
2023-11-09 01:49:14 +0100Lycurgus(~georg@user/Lycurgus) (Quit: leaving)
2023-11-09 02:10:59 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2023-11-09 02:12:17 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2023-11-09 02:25:07 +0100falafel(~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 264 seconds)
2023-11-09 02:30:21 +0100cods(~fred@tuxee.net) (Ping timeout: 240 seconds)
2023-11-09 02:37:38 +0100cods(~fred@tuxee.net)
2023-11-09 02:41:23 +0100kimiamania468(~b4f4a2ab@user/kimiamania)
2023-11-09 02:43:03 +0100kimiamania46(~b4f4a2ab@user/kimiamania) (Ping timeout: 240 seconds)
2023-11-09 02:43:03 +0100kimiamania468kimiamania46
2023-11-09 02:43:27 +0100Jackneill(~Jackneill@20014C4E1E058A0009BBD059E8BC0D29.dsl.pool.telekom.hu) (Ping timeout: 240 seconds)
2023-11-09 02:43:37 +0100haskellbridge(~haskellbr@069-135-003-034.biz.spectrum.com) (Remote host closed the connection)
2023-11-09 02:55:30 +0100derpyxdhs(~Thunderbi@user/derpyxdhs)
2023-11-09 03:02:49 +0100Sciencentistguy0(~sciencent@hacksoc/ordinary-member)
2023-11-09 03:03:50 +0100xff0x(~xff0x@2405:6580:b080:900:568f:45bf:9aab:4d48) (Ping timeout: 255 seconds)
2023-11-09 03:05:05 +0100Sciencentistguy(~sciencent@hacksoc/ordinary-member) (Ping timeout: 240 seconds)
2023-11-09 03:05:05 +0100Sciencentistguy0Sciencentistguy
2023-11-09 03:08:26 +0100derpyxdhs(~Thunderbi@user/derpyxdhs) (Quit: derpyxdhs)
2023-11-09 03:15:25 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 03:20:01 +0100otto_s(~user@p5b044db0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2023-11-09 03:21:58 +0100otto_s(~user@p5de2fe1e.dip0.t-ipconnect.de)
2023-11-09 03:22:03 +0100ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Remote host closed the connection)
2023-11-09 03:24:04 +0100stiell_(~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds)
2023-11-09 03:25:03 +0100ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2023-11-09 03:33:23 +0100stiell_(~stiell@gateway/tor-sasl/stiell)
2023-11-09 03:41:38 +0100ChaiTRex(~ChaiTRex@user/chaitrex)
2023-11-09 03:46:38 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2023-11-09 03:51:36 +0100xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2023-11-09 03:54:20 +0100edr(~edr@user/edr) (Quit: Leaving)
2023-11-09 04:05:22 +0100finn_elija(~finn_elij@user/finn-elija/x-0085643)
2023-11-09 04:05:22 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
2023-11-09 04:05:22 +0100finn_elijaFinnElija
2023-11-09 04:12:05 +0100ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Remote host closed the connection)
2023-11-09 04:12:32 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) (Server closed connection)
2023-11-09 04:13:26 +0100dsrt^(~cd@76.145.193.217)
2023-11-09 04:14:06 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com)
2023-11-09 04:14:44 +0100kiriakos(~kiriakos@p5b03e4f0.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2023-11-09 04:15:54 +0100Katarushisu1(~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Read error: Connection reset by peer)
2023-11-09 04:17:44 +0100Katarushisu1(~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net)
2023-11-09 04:18:20 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543) (Remote host closed the connection)
2023-11-09 04:18:41 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net)
2023-11-09 04:18:54 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds)
2023-11-09 04:27:23 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds)
2023-11-09 04:34:35 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2023-11-09 04:47:11 +0100td_(~td@i53870921.versanet.de) (Ping timeout: 252 seconds)
2023-11-09 04:49:13 +0100td_(~td@i53870905.versanet.de)
2023-11-09 05:11:17 +0100chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2023-11-09 05:11:45 +0100chiselfuse(~chiselfus@user/chiselfuse)
2023-11-09 05:15:36 +0100waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 258 seconds)
2023-11-09 05:17:35 +0100aforemny_(~aforemny@2001:9e8:6ccb:5b00:f896:13f1:97ad:eaff)
2023-11-09 05:19:07 +0100aforemny(~aforemny@2001:9e8:6ce5:5c00:3494:c671:8982:8a94) (Ping timeout: 264 seconds)
2023-11-09 05:45:29 +0100michalz(~michalz@185.246.207.197)
2023-11-09 05:47:57 +0100mjs2600(~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Server closed connection)
2023-11-09 05:48:05 +0100thegman(~thegman@072-239-207-086.res.spectrum.com) (Quit: Lost terminal)
2023-11-09 05:48:14 +0100mjs2600(~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net)
2023-11-09 05:53:34 +0100trev(~trev@user/trev)
2023-11-09 05:55:47 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
2023-11-09 05:56:04 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2023-11-09 05:59:51 +0100Friendship(~Friendshi@user/Friendship) (Ping timeout: 240 seconds)
2023-11-09 06:01:06 +0100[_](~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer)
2023-11-09 06:04:28 +0100_ht(~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
2023-11-09 06:16:37 +0100accord(uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2023-11-09 06:29:41 +0100motherfsck(~motherfsc@user/motherfsck) (Ping timeout: 240 seconds)
2023-11-09 06:32:10 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2023-11-09 06:32:18 +0100euleritian(~euleritia@77.22.252.56)
2023-11-09 06:40:58 +0100euleritian(~euleritia@77.22.252.56) (Ping timeout: 255 seconds)
2023-11-09 06:56:32 +0100 <MelanieMalik> sgih
2023-11-09 06:56:45 +0100euleritian(~euleritia@77.22.252.56)
2023-11-09 06:59:04 +0100Inst(~Inst@120.244.192.250)
2023-11-09 06:59:13 +0100 <Inst> I hope you guys don't mind, but I'm wondering why I can't get fusion on -O0?
2023-11-09 06:59:37 +0100 <Inst> okay, figured it out
2023-11-09 07:01:54 +0100 <monochrom> At least -O1.
2023-11-09 07:02:43 +0100 <MelanieMalik> monochrom, i suppose
2023-11-09 07:09:31 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2023-11-09 07:27:47 +0100euleritian(~euleritia@77.22.252.56) (Ping timeout: 252 seconds)
2023-11-09 07:28:07 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de)
2023-11-09 07:35:58 +0100_ht(~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
2023-11-09 07:39:59 +0100glowcoil(sid3405@id-3405.tinside.irccloud.com) (Server closed connection)
2023-11-09 07:40:07 +0100glowcoil(sid3405@id-3405.tinside.irccloud.com)
2023-11-09 07:41:09 +0100alp(~alp@static-176-175-7-165.ftth.abo.bbox.fr)
2023-11-09 07:44:03 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2023-11-09 07:44:32 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2023-11-09 07:53:21 +0100alp(~alp@static-176-175-7-165.ftth.abo.bbox.fr) (Ping timeout: 240 seconds)
2023-11-09 07:58:17 +0100gmg(~user@user/gehmehgeh)
2023-11-09 08:01:04 +0100acidjnk(~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de)
2023-11-09 08:03:03 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-11-09 08:03:08 +0100 <albet70> newtype CoroutineT r m a = CoroutineT { runCoroutineT :: ContT r (StateT [CoroutineT r m ()] m) a }
2023-11-09 08:03:24 +0100 <albet70> how to construct a value has this type?
2023-11-09 08:16:06 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 08:22:38 +0100trev(~trev@user/trev) (Quit: trev)
2023-11-09 08:22:58 +0100trev(~trev@user/trev)
2023-11-09 08:24:31 +0100 <albet70> CoroutineT $ ContT $ (v :: (a -> StateT $ [] -> m (r, [])) -> StateT $ [] -> m (r, []))
2023-11-09 08:25:22 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2023-11-09 08:30:05 +0100thegeekinside(~thegeekin@189.141.80.123) (Ping timeout: 255 seconds)
2023-11-09 08:30:52 +0100 <[exa]> albet70: you can fake it with `pure (pure anything)`
2023-11-09 08:31:04 +0100 <[exa]> (ah +1 pure)
2023-11-09 08:34:55 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-11-09 08:36:37 +0100 <albet70> what's the point they use this type
2023-11-09 08:36:46 +0100 <albet70> beyond my imagination
2023-11-09 08:38:49 +0100 <[exa]> like, it's indeed very jumpy
2023-11-09 08:48:24 +0100misterfish(~misterfis@84-53-85-146.bbserv.nl)
2023-11-09 08:48:24 +0100 <ski> from the Claessen paper ?
2023-11-09 08:49:45 +0100 <ski> the state's for keeping track of the currently inactive threads, i'd imagine
2023-11-09 08:51:02 +0100lortabac(~lorenzo@2a01:e0a:541:b8f0:cf92:a8ae:a9da:4f45)
2023-11-09 08:57:16 +0100danza(~francesco@151.43.102.157)
2023-11-09 09:00:05 +0100misterfish(~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds)
2023-11-09 09:02:19 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543)
2023-11-09 09:07:37 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 09:14:00 +0100tzh(~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz)
2023-11-09 09:15:20 +0100fendor(~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728)
2023-11-09 09:20:18 +0100coot(~coot@89-69-206-216.dynamic.chello.pl)
2023-11-09 09:20:57 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-11-09 09:28:05 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be)
2023-11-09 09:29:08 +0100sord937(~sord937@gateway/tor-sasl/sord937)
2023-11-09 09:38:02 +0100idgaen(~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
2023-11-09 09:39:29 +0100miguelnegrao(~miguelneg@2001:818:dc71:d100:f016:1b9:e7c1:3567)
2023-11-09 09:40:39 +0100 <miguelnegrao> Hi all, I would like to create a function withSomeSingI which combines withSomeSing and withSingI but I having trouble getting the type right.
2023-11-09 09:41:03 +0100 <miguelnegrao> withSomeSingI :: SingKind k => Demote k -> (forall (a :: k). SingI a => r) -> r
2023-11-09 09:41:05 +0100 <miguelnegrao> withSomeSingI n r = withSomeSing n $ \n' -> withSingI n' r
2023-11-09 09:41:27 +0100 <miguelnegrao> Error: • Could not deduce (SingI a0) arising from a use of ‘r’
2023-11-09 09:42:23 +0100 <miguelnegrao> I can use this combination in code just fine, I just can't create a function out of it...
2023-11-09 09:44:07 +0100misterfish(~misterfis@46.44.172.198)
2023-11-09 09:51:10 +0100ubert(~Thunderbi@178.165.181.20.wireless.dyn.drei.com)
2023-11-09 09:51:47 +0100 <miguelnegrao> ChatGTP just gives up on this one...
2023-11-09 09:53:47 +0100 <[exa]> miguelnegrao: chatgpt has no clue about types
2023-11-09 09:54:04 +0100ggranberry(sid267884@id-267884.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2023-11-09 09:54:31 +0100 <[exa]> miguelnegrao: btw I guess it's unable to guess that something in the definition is SingKind, and it needs that
2023-11-09 09:54:50 +0100 <miguelnegrao> Yes, it doesn't have any clue about anything actually, but it might have crawled a solution to this on some forum, web page, etc...
2023-11-09 09:55:10 +0100 <[exa]> maybe annotate the forall a::k with an extra typeclass ?
2023-11-09 09:55:14 +0100 <[exa]> (wild guess ^)
2023-11-09 09:55:52 +0100 <[exa]> btw if you could pastebin the types of the other stuff too, it would IMO help
2023-11-09 09:57:34 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net)
2023-11-09 09:57:59 +0100 <[exa]> btw btw looks a bit like you might want to have your type signature as ... Demote k -> (forall (r::k) . SingI r => r -> r)
2023-11-09 09:58:14 +0100 <[exa]> because otherwise the `r` that gets out is completely unqualified
2023-11-09 09:59:53 +0100 <idgaen> chatgpt is stupid
2023-11-09 10:00:01 +0100alp(~alp@2001:861:5e02:eff0:a92b:16ae:f4aa:f168)
2023-11-09 10:00:09 +0100 <miguelnegrao> exa: thanks for helping out ! There are no other types, these are all types from the singletons package. The a and r really have to be different. The r is a result type which can be generated in the presence of a singleton a.
2023-11-09 10:00:25 +0100 <miguelnegrao> The type of withSomeSing is here https://hackage.haskell.org/package/singletons-3.0.2/docs/Data-Singletons.html#v:withSomeSing
2023-11-09 10:00:55 +0100 <miguelnegrao> https://paste.gnome.org/RJWfo3wcE
2023-11-09 10:01:18 +0100 <miguelnegrao> I started from that type and changed Sing a into SingI a =>
2023-11-09 10:01:34 +0100 <miguelnegrao> so from explicit singleton into implicit singleton
2023-11-09 10:02:55 +0100 <[exa]> miguelnegrao: ah you have => instead of -> there, I see
2023-11-09 10:03:52 +0100 <[exa]> ok this is gonna be one big type tetris
2023-11-09 10:04:20 +0100 <miguelnegrao> exa: pastebin with code here: https://paste.tomsmeding.com/cbiveIHJ
2023-11-09 10:06:52 +0100Jackneill(~Jackneill@20014C4E1E058A009B5587F4C6A9FB36.dsl.pool.telekom.hu)
2023-11-09 10:09:09 +0100 <Inst> https://paste.tomsmeding.com/au0L6vND
2023-11-09 10:09:18 +0100 <Inst> do you have any idea how to get this to be performant on O0?
2023-11-09 10:09:30 +0100 <Inst> comparably performant to O1, at least?
2023-11-09 10:14:08 +0100 <Inst> i'mm suspecting there's nothing i can do about the random list
2023-11-09 10:15:45 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 10:16:59 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 10:17:26 +0100 <[exa]> miguelnegrao: ok, no idea here either, but there are singleton users in the channel so maybe just wait for some time until someone appears
2023-11-09 10:18:12 +0100 <[exa]> Inst: "making something performant with O0" is basically equivalent to "inline everything yourself by hand"
2023-11-09 10:18:41 +0100 <Inst> would it be possible to do that without reimplementing the random library? ?:(
2023-11-09 10:19:05 +0100 <[Leary]> miguelnegrao: The error is an ambiguity error. You solve it by manually ferrying the right types around with ScopedTypeVariables and TypeApplications: `withSomeSingI n r = withSomeSing n \(n' :: Sing a) -> withSingI n' (r @a)`
2023-11-09 10:19:49 +0100 <[exa]> Inst: "reimplementing" probably not but "copypasting and substituing into half of the implementation" almost surely
2023-11-09 10:20:38 +0100 <[exa]> Inst: also I'd say the (***) doesn't help much without inlines; iirc it creates quite a lot of closures... can you try having an explicit lambda there?
2023-11-09 10:20:43 +0100 <[exa]> Inst: also, strict tuples
2023-11-09 10:21:30 +0100danza(~francesco@151.43.102.157) (Ping timeout: 258 seconds)
2023-11-09 10:22:16 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 258 seconds)
2023-11-09 10:23:51 +0100 <Inst> what do you mean by strict tuple?
2023-11-09 10:24:02 +0100 <Inst> well, average only gets called once
2023-11-09 10:24:11 +0100 <[exa]> https://hackage.haskell.org/package/strict-tuple
2023-11-09 10:24:22 +0100 <albet70> what's the point of ReaderT?
2023-11-09 10:24:36 +0100mastarija(~mastarija@141-136-170-52.dsl.iskon.hr)
2023-11-09 10:25:01 +0100 <[exa]> albet70: you mean, what it's used for, or why would someone care renaming (->) ?
2023-11-09 10:25:25 +0100 <mastarija> Is stream fusion not a default behavior for lists in GHC? Why did I think it was?
2023-11-09 10:25:28 +0100 <albet70> what's used for
2023-11-09 10:25:34 +0100 <Inst> "how haskell avoids having global constants, or, to provide variable bins of global constants instead of hardcoding it"
2023-11-09 10:25:37 +0100 <[exa]> Inst: ah if average is not a hotspot then you probably don't need to care
2023-11-09 10:25:54 +0100 <Inst> it should be a hotspot insofar as what's going on with foldl'
2023-11-09 10:26:29 +0100 <[exa]> albet70: if you have a monadic computation and want it to remember a global parameter for you (like, if you don't want to pass the config options manually into each single function you have), you just mix in a ReaderT and that passes the global value/config for you. (and you ask for its value using `ask`)
2023-11-09 10:26:53 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2023-11-09 10:26:58 +0100 <[exa]> albet70: if you happen to know StateT from other tutorials, ReaderT is kinda like read-only state.
2023-11-09 10:27:37 +0100 <[exa]> Inst: yeah there you could try to manually expand the foldl'
2023-11-09 10:27:56 +0100 <Inst> what do you mean by manually expand the foldl'?
2023-11-09 10:28:22 +0100 <[exa]> inline it yourself
2023-11-09 10:29:58 +0100 <albet70> [exa] , to me just like a placeholder
2023-11-09 10:30:24 +0100 <Inst> albet70: do you like global variables?
2023-11-09 10:30:31 +0100 <[exa]> Inst: one of the main performance problem with O0 is that for basically each function/parameter application it generates a closure, no matter what. You MAY get rid of that by inlining stuff yourself, so that the compiler doesn't need to generate closures in the first place. At the same time, I wouldn't say even this is very reliable
2023-11-09 10:30:44 +0100 <[exa]> Inst: btw why do you want to optimize O0 code? (just curious :D )
2023-11-09 10:30:58 +0100 <Inst> just some challenge posted on QQ
2023-11-09 10:31:10 +0100 <Inst> they were complaining it's impossible to get Haskell to be performant
2023-11-09 10:31:46 +0100 <[exa]> you can generate a piece of assembly code with O0 an unsafeJump to it
2023-11-09 10:31:54 +0100 <Inst> maybe i should just stop caring about the QQ, I can't even save myself, why should I care about their community?
2023-11-09 10:31:58 +0100 <[exa]> if we're at this nerdlevel :D
2023-11-09 10:32:11 +0100 <albet70> that need every single function defined with that r from Reader r a as the last parameter, very strict or limited?
2023-11-09 10:33:18 +0100krei-se(~krei-se@p5085dea2.dip0.t-ipconnect.de) (Quit: ZNC 1.8.2 - https://znc.in)
2023-11-09 10:33:30 +0100 <[exa]> albet70: the last parameter gets nicely hidden in the monad type.. If your function is `f :: Int -> Reader Int String`, ofc it is isomorphic to `Int -> Int -> String` but you don't need to care about the extra argument
2023-11-09 10:33:57 +0100 <[exa]> (because in the do notation it gets carried for you automatically)
2023-11-09 10:34:33 +0100econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2023-11-09 10:36:01 +0100krei-se(~krei-se@p5085dea2.dip0.t-ipconnect.de)
2023-11-09 10:38:40 +0100lottaquestions(~nick@2607:fa49:503d:b200:135c:2e9a:d788:4186)
2023-11-09 10:40:07 +0100conjunctive(sid433686@id-433686.helmsley.irccloud.com) (Server closed connection)
2023-11-09 10:40:13 +0100 <albet70> [exa] , haha, but I don't see people using it very much
2023-11-09 10:40:17 +0100conjunctive(sid433686@id-433686.helmsley.irccloud.com)
2023-11-09 10:40:41 +0100 <[exa]> mastarija: normally it behaves "almost like stream fusion", but for complete&reliable removal of overhead you need to push it a bit. I'm always looking at how Data.Text does it for reference
2023-11-09 10:41:07 +0100 <[exa]> albet70: yeah Reader is not often used directly, but I'm using it pretty much everywhere hidden in other monads
2023-11-09 10:41:42 +0100danse-nr3(~danse@151.43.102.157)
2023-11-09 10:41:57 +0100 <[exa]> albet70: also various fun expressions like `mean = div <$> sum <*> length` are technically Reader, it's just not written anywhere.
2023-11-09 10:42:24 +0100[exa]has to disappear afk, have fun guys
2023-11-09 10:42:31 +0100 <mastarija> Hm.. yeah. Answers I've found on google is are a bit unconclusive, there are references to stream-fusion package and not being implemented in GHC, but those are very old results.
2023-11-09 10:43:09 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de)
2023-11-09 10:43:22 +0100 <Inst> oh, <$> is actually useful as a replacement for (.) because it has a lower precedence
2023-11-09 10:44:02 +0100 <Inst> but there's quite a few people who think use of function arrow monad is smelly
2023-11-09 10:44:31 +0100 <Inst> monadicValue >>= (<$) <*> monadicCont is considered smelly
2023-11-09 10:45:10 +0100Friendship(~Friendshi@user/Friendship)
2023-11-09 10:45:17 +0100 <mastarija> Well, it depends. If you work in a team that can read that, then it's fine IMO, however most people will have a hard time, simply because it's not a standard "word" in a language :)
2023-11-09 10:46:29 +0100 <Inst> withM in extras might not be bad, or some other function that allows you to bind, but then return the original return value
2023-11-09 10:47:24 +0100 <Inst> withM :: m a -> (a -> m b)-> m a
2023-11-09 10:48:40 +0100 <Inst> https://hoogle.haskell.org/?hoogle=m%20a%20-%3E%20(a%20-%3E%20m%20b)%20-%3E%20m%20a
2023-11-09 10:49:02 +0100danse-nr3(~danse@151.43.102.157) (Ping timeout: 272 seconds)
2023-11-09 10:49:29 +0100danse-nr3(~danse@151.57.108.79)
2023-11-09 10:51:00 +0100 <[Leary]> miguelnegrao: BTW, I don't think you can actually use the function as written; there's no way for GHC to determine `a`. You'd need `\@a -> ...` (TypeAbstractions?) which is still waiting in the wings. The alternative is to introduce a proxy, in which case you may as well keep the `Sing a`.
2023-11-09 10:53:03 +0100 <miguelnegrao> Leary: Thanks for the help ! That doesn't quite work: https://paste.tomsmeding.com/Q9hRqWQX "Not in scope: type variable ‘a’"
2023-11-09 10:53:39 +0100 <miguelnegrao> Leary: ah, yes, we posted at the same time :-)
2023-11-09 10:54:00 +0100erty(~user@user/aeroplane)
2023-11-09 10:54:29 +0100 <[Leary]> Yes, you need ScopedTypeVariables.
2023-11-09 10:54:36 +0100 <miguelnegrao> Leary: but what is interesting is that GHC can use the function body without issue, it just can't abstract it then.
2023-11-09 10:55:35 +0100 <[Leary]> Oh, right. Well, the issue is just that using the body, the `Sing a` is in scope so you can actually reference `a`.
2023-11-09 10:55:38 +0100 <miguelnegrao> Leary: but the a is not one of the type variables of the function...
2023-11-09 10:56:00 +0100misterfish(~misterfis@46.44.172.198) (Ping timeout: 272 seconds)
2023-11-09 10:56:05 +0100 <[Leary]> (I thought you were still struggling with the function itself, not its use)
2023-11-09 10:56:32 +0100 <miguelnegrao> So I'm not sure using an explicit forall helps here.
2023-11-09 10:57:09 +0100 <miguelnegrao> If I stick the function body inside another expression it works. But I wanted obviously to abstract it into a function, so as not to repeat the same code over and over.
2023-11-09 10:57:41 +0100mastarija(~mastarija@141-136-170-52.dsl.iskon.hr) (Quit: Client closed)
2023-11-09 10:59:21 +0100 <[Leary]> Oh, you actually are, but the issue isn't STV. I'm a bit distracted and didn't actually look at your paste. I believe you need to put the `Sing a` signature on the argument in order to actually bind `a`.
2023-11-09 10:59:25 +0100sa(sid1055@id-1055.tinside.irccloud.com) (Server closed connection)
2023-11-09 10:59:49 +0100sa(sid1055@id-1055.tinside.irccloud.com)
2023-11-09 10:59:49 +0100 <[Leary]> Note that how you wrote it is not how I wrote it.
2023-11-09 11:03:25 +0100 <miguelnegrao> Leary: ah, what a stupid typo on my part ! You're absolutely right, you original code works !! Thanks a lot ! Now I will study it to make sure I understand what is going on.
2023-11-09 11:08:41 +0100xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds)
2023-11-09 11:13:16 +0100miguelnegrao(~miguelneg@2001:818:dc71:d100:f016:1b9:e7c1:3567) (Quit: miguelnegrao)
2023-11-09 11:25:50 +0100alp(~alp@2001:861:5e02:eff0:a92b:16ae:f4aa:f168) (Quit: Leaving)
2023-11-09 11:26:04 +0100alp(~alp@2001:861:5e02:eff0:e:ba9a:698b:1b65)
2023-11-09 11:26:18 +0100alp(~alp@2001:861:5e02:eff0:e:ba9a:698b:1b65) (Changing host)
2023-11-09 11:26:18 +0100alp(~alp@user/alp)
2023-11-09 11:28:31 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-11-09 11:44:24 +0100alp(~alp@user/alp) (Remote host closed the connection)
2023-11-09 11:44:42 +0100alp(~alp@2001:861:5e02:eff0:97b5:b655:9038:6771)
2023-11-09 11:48:56 +0100zmt00(~zmt00@user/zmt00)
2023-11-09 11:50:39 +0100zmt01(~zmt00@user/zmt00) (Ping timeout: 240 seconds)
2023-11-09 11:54:16 +0100alp(~alp@2001:861:5e02:eff0:97b5:b655:9038:6771) (Changing host)
2023-11-09 11:54:16 +0100alp(~alp@user/alp)
2023-11-09 11:54:28 +0100misterfish(~misterfis@37.153.233.129)
2023-11-09 11:55:20 +0100sand-witch_(~m-mzmz6l@vmi833741.contaboserver.net)
2023-11-09 11:56:05 +0100sand-witch(~m-mzmz6l@vmi833741.contaboserver.net) (Ping timeout: 240 seconds)
2023-11-09 11:57:51 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2023-11-09 11:59:48 +0100ft(~ft@p4fc2a529.dip0.t-ipconnect.de) (Quit: leaving)
2023-11-09 11:59:55 +0100ursa-major(~ursa-majo@37.19.210.38) (Ping timeout: 264 seconds)
2023-11-09 12:00:13 +0100sand-witch_sand-witch
2023-11-09 12:01:44 +0100billchenchina(~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe)
2023-11-09 12:13:34 +0100xff0x(~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531)
2023-11-09 12:21:05 +0100mmhat(~mmh@p200300f1c7445e88ee086bfffe095315.dip0.t-ipconnect.de)
2023-11-09 12:21:13 +0100mmhat(~mmh@p200300f1c7445e88ee086bfffe095315.dip0.t-ipconnect.de) (Client Quit)
2023-11-09 12:27:31 +0100jmdaemon(~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds)
2023-11-09 12:36:09 +0100lhpitn(~tn@31.172.106.163.static-pppoe.dt.ipv4.wtnet.de) (Remote host closed the connection)
2023-11-09 12:36:31 +0100lhpitn(~tn@mail.lebenshilfe-pi.de)
2023-11-09 12:42:43 +0100lhpitn(~tn@mail.lebenshilfe-pi.de) (Remote host closed the connection)
2023-11-09 12:43:06 +0100lhpitn(~tn@mail.lebenshilfe-pi.de)
2023-11-09 12:47:51 +0100misterfish(~misterfis@37.153.233.129) (Ping timeout: 255 seconds)
2023-11-09 12:49:01 +0100Friendship(~Friendshi@user/Friendship) (Read error: Connection reset by peer)
2023-11-09 12:49:21 +0100Friendship(~Friendshi@user/Friendship)
2023-11-09 12:54:08 +0100haskellbridge(~haskellbr@069-135-003-034.biz.spectrum.com)
2023-11-09 12:54:08 +0100ChanServ+v haskellbridge
2023-11-09 12:55:41 +0100accord(uid568320@id-568320.hampstead.irccloud.com)
2023-11-09 12:58:36 +0100misterfish(~misterfis@37.153.233.129)
2023-11-09 13:00:13 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
2023-11-09 13:00:32 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2023-11-09 13:01:58 +0100dibblego(~dibblego@haskell/developer/dibblego) (Ping timeout: 260 seconds)
2023-11-09 13:02:12 +0100Vq(~vq@90-225-115-195-no122.tbcn.telia.com) (Server closed connection)
2023-11-09 13:02:22 +0100Vq(~vq@90-225-115-195-no122.tbcn.telia.com)
2023-11-09 13:02:55 +0100dibblego(~dibblego@122-199-1-93.ip4.superloop.au)
2023-11-09 13:02:55 +0100dibblego(~dibblego@122-199-1-93.ip4.superloop.au) (Changing host)
2023-11-09 13:02:55 +0100dibblego(~dibblego@haskell/developer/dibblego)
2023-11-09 13:09:31 +0100zetef(~quassel@95.77.17.251)
2023-11-09 13:12:54 +0100manwithluck(manwithluc@2406:da14:5ea:e400:7863:dbc1:6a84:3050) (Quit: ZNC - https://znc.in)
2023-11-09 13:13:13 +0100manwithluck(manwithluc@ec2-52-197-234-151.ap-northeast-1.compute.amazonaws.com)
2023-11-09 13:13:55 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2023-11-09 13:14:22 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2023-11-09 13:26:56 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2023-11-09 13:27:40 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de)
2023-11-09 13:28:03 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
2023-11-09 13:28:20 +0100euleritian(~euleritia@77.22.252.56)
2023-11-09 13:30:16 +0100erty(~user@user/aeroplane) (Remote host closed the connection)
2023-11-09 13:34:12 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 13:35:24 +0100 <sawilagar> hi. i'd like to develop a guestbook website. is scotty a good choice for that?
2023-11-09 13:35:54 +0100 <danse-nr3> why not
2023-11-09 13:36:22 +0100 <danse-nr3> i think it is one of the most popular among that type of frameworks
2023-11-09 13:36:32 +0100 <sawilagar> i haven't worked with haskell web libs, so wanted to make sure it's fitting. is scotty something like express.js in js ecosystem?
2023-11-09 13:37:41 +0100 <danse-nr3> huh... not sure. I think frameworks like scotty were called "web microframeworks" at some point. It mostly takes care of organizing the routes and little more
2023-11-09 13:43:08 +0100manwithluck(manwithluc@ec2-52-197-234-151.ap-northeast-1.compute.amazonaws.com) (Quit: ZNC - https://znc.in)
2023-11-09 13:43:37 +0100 <sawilagar> gotcha. well, i think express.js is similar in its concept.
2023-11-09 13:44:10 +0100 <sawilagar> maybe, ruby sinatra is a better equivalent example, but i haven't worked that much with ruby
2023-11-09 13:46:40 +0100manwithluck(manwithluc@ec2-52-197-234-151.ap-northeast-1.compute.amazonaws.com)
2023-11-09 13:47:00 +0100danse-nr3(~danse@151.57.108.79) (Ping timeout: 272 seconds)
2023-11-09 13:52:23 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Remote host closed the connection)
2023-11-09 13:52:41 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de)
2023-11-09 14:01:44 +0100xff0x(~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531) (Ping timeout: 255 seconds)
2023-11-09 14:03:46 +0100xff0x(~xff0x@178.255.149.135)
2023-11-09 14:16:49 +0100billchenchina(~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Remote host closed the connection)
2023-11-09 14:18:31 +0100xff0x(~xff0x@178.255.149.135) (Ping timeout: 264 seconds)
2023-11-09 14:18:40 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 14:20:08 +0100xff0x(~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531)
2023-11-09 14:23:55 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds)
2023-11-09 14:29:52 +0100mc47(~mc47@xmonad/TheMC47)
2023-11-09 14:30:26 +0100idgaen(~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1)
2023-11-09 14:30:55 +0100 <[exa]> sawilagar: scotty is quite likely the most painless way
2023-11-09 14:31:34 +0100 <sawilagar> [exa] from examples that i saw, yeah, looks pretty much like that
2023-11-09 14:32:54 +0100 <[exa]> one thing that I was missing there would be a kinda built-in database interface, but there are plenty of good options and in the end I think it's better they didn't force folks to use a particular choice set
2023-11-09 14:46:13 +0100tv(~tv@user/tv) (Server closed connection)
2023-11-09 14:46:38 +0100tv(~tv@user/tv)
2023-11-09 14:47:48 +0100yvan-sraka(sid419690@id-419690.lymington.irccloud.com) (Server closed connection)
2023-11-09 14:47:56 +0100yvan-sraka(sid419690@id-419690.lymington.irccloud.com)
2023-11-09 14:53:55 +0100notzmv(~zmv@user/notzmv) (Ping timeout: 264 seconds)
2023-11-09 14:54:14 +0100danso(~danso@user/danso) (Server closed connection)
2023-11-09 14:54:30 +0100danso(~danso@user/danso)
2023-11-09 14:54:43 +0100danse-nr3(~danse@151.57.105.34)
2023-11-09 14:57:39 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 4.1.0)
2023-11-09 14:59:34 +0100euleritian(~euleritia@77.22.252.56) (Ping timeout: 255 seconds)
2023-11-09 15:00:21 +0100catilina(~user@49.235.216.139.sta.wbroadband.net.au)
2023-11-09 15:00:28 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de)
2023-11-09 15:03:31 +0100danse-nr3(~danse@151.57.105.34) (Remote host closed the connection)
2023-11-09 15:03:54 +0100danse-nr3(~danse@151.57.105.34)
2023-11-09 15:04:13 +0100accord(uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2023-11-09 15:05:26 +0100edr(~edr@user/edr)
2023-11-09 15:08:10 +0100 <catilina> I'm trying to modify https://paste.tomsmeding.com/yECA0o8o so it is able to process an org-mode file which has a 'tags' metadata field. For that, I have a Lua filter https://paste.tomsmeding.com/0qSNd2Me that keeps that field in the metadata, as is the case for markdown (which was the original pandoc reader for this codeblock). I don't understand how the Haskell code needs to be modified to call that filter though, as I've never used
2023-11-09 15:08:11 +0100 <catilina> Haskell before. Any ideas?
2023-11-09 15:11:08 +0100 <danse-nr3> more of a pandoc question, i think it has its own community channels. I don't think you need to modify the pandoc code to run a filter, just use command-line options
2023-11-09 15:11:28 +0100 <[exa]> catilina: you can "construct" the filters using e.g. `LuaFilter "somefilename.lua"` as here: https://hackage.haskell.org/package/pandoc-3.1.9/docs/Text-Pandoc-Filter.html
2023-11-09 15:11:43 +0100 <[exa]> catilina: and then you run the applyfilters (below on the same page) on your pandoc
2023-11-09 15:12:00 +0100 <danse-nr3> huh was that the code of the filter? I thought the filter was in lua...
2023-11-09 15:12:09 +0100 <[exa]> catilina: but if you never did haskell, this may get confusing, yeah. :)
2023-11-09 15:12:16 +0100 <[exa]> danse-nr3: there are 2 pastes
2023-11-09 15:13:21 +0100 <danse-nr3> i think they are using pandoc as a library from haskell?
2023-11-09 15:13:35 +0100 <[exa]> yes
2023-11-09 15:13:44 +0100 <danse-nr3> makes sense now
2023-11-09 15:17:16 +0100 <catilina> yes - that applyFilters also has a ScriptingEngine to provide though? might take your advice and ask in a pandoc channel if this is a bit off-topic. As its api is in haskell, I jumped in here first.
2023-11-09 15:18:25 +0100 <danse-nr3> i don't think it is a problem to ask here if there is anybody knowledgeable, i wrote that because i thought you wanted to use it from the command line
2023-11-09 15:20:51 +0100 <catilina> no, I got it to work on the command line, but now need to figure out how to put it in the haskell script. as [exa] points out, it gets confusing quickly.
2023-11-09 15:21:04 +0100 <catilina> (and thanks [exa])
2023-11-09 15:21:44 +0100acidjnk(~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2023-11-09 15:22:50 +0100 <jackdk> Someone asked a very similar question in #haskell-au: I don't know the pandoc stuff super well but I think you'll want to look at Text.Pandoc.Lua.applyFilter from the `pandoc-lua-engine` package, something like `pandoc' <- applyFilter (Environment readerOptions writerOptions) [] "path/to/foo.lua" pandoc`
2023-11-09 15:22:57 +0100jackdk-> zzz
2023-11-09 15:23:16 +0100thegeekinside(~thegeekin@189.141.80.123)
2023-11-09 15:29:09 +0100 <catilina> Hi jackdk, that was my question there indeed. it seemed https://hackage.haskell.org/package/pandoc-3.1.9/docs/Text-Pandoc-Filter.html should be sufficient as that also has the luafilter constructor, but I'm out of my league here...
2023-11-09 15:29:42 +0100 <danse-nr3> they went idle i think
2023-11-09 15:32:54 +0100 <probie> danse-nr3: Or just went to bed - it's 01:30 in their timezone
2023-11-09 15:33:19 +0100 <[exa]> catilina: you can copypaste line 8 in your haskell and just have applyFilters there instead of the writeHtml...something
2023-11-09 15:33:28 +0100 <[exa]> catilina: if that fails pls paste the error message here
2023-11-09 15:41:20 +0100 <catilina> [exa]: it fails - https://paste.tomsmeding.com/Rkgc7Nmz. that's with the line 7 now: pandoc <- runPandoc . Text.Pandoc.Filter.applyFilters writerOptions LuaFilter "orgTags.lua" $ pandoc
2023-11-09 15:42:42 +0100kraftwerk28(~kraftwerk@164.92.219.160) (Quit: *disconnects*)
2023-11-09 15:43:02 +0100opus(~nil@user/opus) (Server closed connection)
2023-11-09 15:43:33 +0100kraftwerk28(~kraftwerk@164.92.219.160)
2023-11-09 15:43:35 +0100 <catilina> (it would seem necessary for me to spend some time going through a tutorial to understand what all this means)
2023-11-09 15:43:50 +0100opus(~nil@user/opus)
2023-11-09 15:44:35 +0100ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2023-11-09 15:45:17 +0100 <[exa]> catilina: ok needs a bit of care... the parameters should be something like `applyFilters noEngine def [LuaFilter "orgTags.lua"] [] $ pandoc `
2023-11-09 15:45:36 +0100 <[exa]> noEngine is from here https://hackage.haskell.org/package/pandoc-3.1.9/docs/Text-Pandoc-Scripting.html#t:ScriptingEngine
2023-11-09 15:46:25 +0100 <[exa]> and `def` is from Data.Default (package data-default)
2023-11-09 15:50:03 +0100Guest|67(~Guest|67@98.98.49.194)
2023-11-09 15:50:24 +0100Guest|67(~Guest|67@98.98.49.194) (Client Quit)
2023-11-09 15:50:33 +0100Teacup(~teacup@user/teacup) (Server closed connection)
2023-11-09 15:50:44 +0100Teacup(~teacup@user/teacup)
2023-11-09 15:52:33 +0100 <danse-nr3> did not realise there was #haskell-au. Why would people segregate themselves
2023-11-09 15:53:20 +0100 <EvanR> I don't have to take this. I'm headed to #haskell-us
2023-11-09 15:53:31 +0100 <EvanR> *hides behind A Wall*
2023-11-09 15:53:40 +0100 <catilina> that seems to have made things a lot better - I now get https://paste.tomsmeding.com/sotMIpna. Not quite there yet, but it's compiling it would seem.
2023-11-09 15:54:15 +0100 <danse-nr3> had to make sure that was not a joke now EvanR ^^;
2023-11-09 15:54:28 +0100 <danse-nr3> *was a joke*
2023-11-09 15:55:23 +0100 <[exa]> catilina: ah ok so maybe `noEngine` ain't gonna cut it if you actually want to run lua :D
2023-11-09 15:56:19 +0100 <catilina> :)
2023-11-09 15:57:40 +0100 <[exa]> ahh ok found it, there's a separate package https://hackage.haskell.org/package/pandoc-lua-engine-0.2.1.2/docs/Text-Pandoc-Lua.html
2023-11-09 15:58:24 +0100 <[exa]> you should be able to do `Text.Pandoc.Lua.applyEngine def [] "orgTags.lua" $ pandoc`
2023-11-09 15:58:33 +0100 <[exa]> + you will probably need the extra package, if not included already
2023-11-09 15:59:38 +0100zaquest(~notzaques@5.130.79.72) (Remote host closed the connection)
2023-11-09 16:01:18 +0100chomwitt(~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1)
2023-11-09 16:04:51 +0100fendor_(~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728)
2023-11-09 16:04:57 +0100 <catilina> hmm, that package is not yet in my nix environment.
2023-11-09 16:05:14 +0100 <catilina> this is what jackdk had suggested earlier
2023-11-09 16:05:20 +0100fendor(~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Ping timeout: 252 seconds)
2023-11-09 16:05:24 +0100Sgeo(~Sgeo@user/sgeo)
2023-11-09 16:05:57 +0100mechap(~mechap@user/mechap)
2023-11-09 16:06:22 +0100 <[exa]> ah yeah, I misread the package name there actually
2023-11-09 16:06:23 +0100 <[exa]> good
2023-11-09 16:06:42 +0100 <[exa]> so yeah at least we replayed the error series that would get you to the solution :D
2023-11-09 16:11:39 +0100 <catilina> that gets me here: https://paste.tomsmeding.com/SfaAKp5Y - back to ugly error terrain :)
2023-11-09 16:14:44 +0100 <sawilagar> what IDE would you recommend for Haskell? I tried Emacs, IntelliJ and VSCodium, they don't seems to support something like "development environment"
2023-11-09 16:14:51 +0100 <danse-nr3> may i ask why you need to encapsulate the pandoc call in an haskell script catilina ?
2023-11-09 16:15:42 +0100 <danse-nr3> i would recommend you to start with less bells and whistles sawilagar. Eventually you can add HLS to whichever editor you choose
2023-11-09 16:15:59 +0100waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2023-11-09 16:16:25 +0100zaquest(~notzaques@5.130.79.72)
2023-11-09 16:16:53 +0100 <sawilagar> danse-nr3: but why? these features are comfy and I'm used to them while coding in more mainstream langs.
2023-11-09 16:17:05 +0100 <catilina> danse-nr3: the script does a whole lot of other things - see https://abhinavsarkar.net/code/shake-blog.html
2023-11-09 16:17:50 +0100 <danse-nr3> i see, thanks catilina
2023-11-09 16:17:52 +0100 <catilina> I thought I could just update the reader from markdown to org and be ready - a can of worms ensued
2023-11-09 16:18:04 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2023-11-09 16:18:10 +0100 <danse-nr3> sawilagar, just my opinion
2023-11-09 16:19:29 +0100waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Client Quit)
2023-11-09 16:21:26 +0100 <exarkun> is `(Traversable t, Monoid b) => (a -> b -> c) -> (a -> t b -> c)` a thing?
2023-11-09 16:21:52 +0100acidjnk(~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de)
2023-11-09 16:22:19 +0100 <exarkun> or `(Traversable t, Monoid c) => (a -> b -> c) -> (a -> t b -> c)`
2023-11-09 16:24:35 +0100 <exarkun> hm I guess it's just `foldMap (f a)`
2023-11-09 16:24:50 +0100 <exarkun> `x f a = foldMap (f a)` that is
2023-11-09 16:25:12 +0100 <danse-nr3> :t \f a -> foldMap (f a)
2023-11-09 16:25:13 +0100 <lambdabot> (Foldable t1, Monoid m) => (t2 -> a -> m) -> t2 -> t1 a -> m
2023-11-09 16:25:26 +0100 <exarkun> oh Foldable not Traversable, oops
2023-11-09 16:25:39 +0100 <exarkun> ty
2023-11-09 16:25:48 +0100danse-nr3did nothing ^^;
2023-11-09 16:26:04 +0100 <exarkun> infinite efficiency, very impressive
2023-11-09 16:26:05 +0100kitzman(~kitzman@user/dekenevs) (Quit: C-x C-c)
2023-11-09 16:26:29 +0100 <danse-nr3> it's the power of rubberduck-driven-development
2023-11-09 16:26:36 +0100misterfish(~misterfis@37.153.233.129) (Ping timeout: 272 seconds)
2023-11-09 16:26:44 +0100euleritian(~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
2023-11-09 16:27:03 +0100euleritian(~euleritia@77.22.252.56)
2023-11-09 16:30:29 +0100alp(~alp@user/alp) (Ping timeout: 245 seconds)
2023-11-09 16:33:10 +0100 <[exa]> sawilagar: I'm coding basically in vim; got a code formatter for each project (usually just :%!hindent), and ghc error messages are actually quite helpful
2023-11-09 16:33:11 +0100 <Inst> ugh, is anyone interested in helping with some dependent types exercises?
2023-11-09 16:33:36 +0100 <Inst> https://paste.tomsmeding.com/YTB52wwl this won't typecheck
2023-11-09 16:33:52 +0100 <Inst> I've done this before, but I'm trying to redo it with GHC.TypeNats
2023-11-09 16:34:01 +0100 <sawilagar> [exa]: mmm, not a fan. even emacs is kinda too minimalist for my taste
2023-11-09 16:34:42 +0100 <sawilagar> but emacs is the only IDE where hsl works properly (if older version of ghc is used)
2023-11-09 16:35:05 +0100ddellacosta(~ddellacos@ool-44c738de.dyn.optonline.net)
2023-11-09 16:35:30 +0100 <[exa]> sawilagar: like, normally for e.g. java the editors are absolutely indispensable because you're supposed to spew a bit of code for each single thing. with haskells I actively try to avoid that; on the end the code should be perfectly self-explanatory without any IDE support
2023-11-09 16:36:26 +0100 <Inst> maybe I should learn from here instead? https://hackage.haskell.org/package/sized
2023-11-09 16:37:37 +0100 <sawilagar> [exa]: for me it's more about conveniency like jumping to the definition of a function and so on. hsl supports that quite well btw, the problem is it's not so tightly integrated with any IDE.
2023-11-09 16:38:25 +0100 <[exa]> sawilagar: yeah well for these I somehow manage with the "stupid" plaintext variants in vim, like # or gD or so
2023-11-09 16:38:55 +0100 <[exa]> again, if I have to skip through multiple files to follow definitions, it's a kinda signal for me that the code sucks
2023-11-09 16:40:22 +0100 <[exa]> Inst: what's the compiler complaining about there?
2023-11-09 16:41:14 +0100 <Inst> could not deduce n1 ~ n
2023-11-09 16:41:50 +0100 <[exa]> which ones exactly?
2023-11-09 16:43:15 +0100 <Inst> https://paste.tomsmeding.com/vJVjyZw5
2023-11-09 16:43:27 +0100euleritian(~euleritia@77.22.252.56) (Read error: Connection reset by peer)
2023-11-09 16:43:29 +0100sawilagar(~sawilagar@user/sawilagar) (Remote host closed the connection)
2023-11-09 16:43:40 +0100 <[exa]> oh commutativity
2023-11-09 16:43:55 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 16:44:09 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2023-11-09 16:44:40 +0100 <[exa]> how does the typesystem know that (m+1)~(n+1) implies m~n ?
2023-11-09 16:46:35 +0100 <Inst> I mean I can do this with data Nat = Z | S Nat
2023-11-09 16:46:46 +0100 <Inst> but I sort of want to use GHC.TypeLits machinery this time
2023-11-09 16:48:32 +0100 <c_wraith> If you really want to do anything with GHC.TypeLits, you'll need to add a typechecker plugin so that it can do "obvious" arithmetic
2023-11-09 16:48:46 +0100absence(torgeihe@hildring.pvv.ntnu.no) (Ping timeout: 272 seconds)
2023-11-09 16:49:34 +0100 <c_wraith> well, anything taking advantage of the fact that they're numbers, and not some other random opaque symbols at the type level
2023-11-09 16:50:15 +0100 <Inst> crap :(
2023-11-09 16:50:35 +0100CO2(CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1)
2023-11-09 16:54:59 +0100absence(torgeihe@hildring.pvv.ntnu.no)
2023-11-09 16:57:43 +0100foul_owl(~kerry@185.219.141.160) (Read error: Connection reset by peer)
2023-11-09 17:04:12 +0100notzmv(~zmv@user/notzmv)
2023-11-09 17:05:56 +0100 <EvanR> m + 1 = n + 1 implying m = n looks like a theorem you need to prove, and the reason we still don't have dependent types xD
2023-11-09 17:12:03 +0100VioletJewel(violet@user/violetjewel) (Ping timeout: 258 seconds)
2023-11-09 17:12:39 +0100danse-nr3(~danse@151.57.105.34) (Remote host closed the connection)
2023-11-09 17:12:52 +0100 <[exa]> heavy presburger vibes
2023-11-09 17:12:59 +0100VioletJewel(~violet@user/violetjewel)
2023-11-09 17:13:02 +0100danse-nr3(~danse@151.57.105.34)
2023-11-09 17:13:42 +0100foul_owl(~kerry@185.219.141.164)
2023-11-09 17:14:46 +0100 <ski> o
2023-11-09 17:15:12 +0100 <Inst> iirc in idris, you have a bunch of functions to help the type checker along, no?
2023-11-09 17:16:07 +0100 <ski> you have dependent types
2023-11-09 17:16:32 +0100 <EvanR> manually proving everything is in every system of dependent types, what you're look for is extra intelligence beyond that
2023-11-09 17:17:08 +0100 <EvanR> idris has a proof search thing, and putting _ for terms sometimes works, it finds what to put there
2023-11-09 17:17:27 +0100 <EvanR> esp helpful when only 1 thing could ever work
2023-11-09 17:17:49 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2023-11-09 17:18:22 +0100 <ski> you can ask Twelf to find a solution for a query (a type) (just like in other logic programming)
2023-11-09 17:21:27 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542)
2023-11-09 17:22:01 +0100zetef(~quassel@95.77.17.251) (Ping timeout: 240 seconds)
2023-11-09 17:23:36 +0100 <geekosaur> AIUI there are ghc plugins for this kind of thing (look at natnormalise in particular)
2023-11-09 17:23:51 +0100 <ski> (Twelf is a dependent logic programming language. predicates are types, clauses are data constructors)
2023-11-09 17:23:56 +0100 <kuribas> you don't need to prove m + 1 = n + 1 in idris, because it is judgementally equal.
2023-11-09 17:24:32 +0100 <kuribas> I mean "m = n" implies "m + 1 = n + 1"
2023-11-09 17:24:42 +0100blurbox(~user@2001:2042:3c78:ab00:b533:32e3:87ff:593d)
2023-11-09 17:24:48 +0100 <EvanR> the other way
2023-11-09 17:24:54 +0100 <kuribas> ah...
2023-11-09 17:25:08 +0100 <EvanR> but that might also just work
2023-11-09 17:25:35 +0100 <EvanR> idris works in mysterious ways
2023-11-09 17:26:07 +0100 <kuribas> The second is Refl, then the first is Refl as well...
2023-11-09 17:26:28 +0100sawilagar(~sawilagar@user/sawilagar) (Quit: Leaving)
2023-11-09 17:26:45 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 17:27:07 +0100 <kuribas> But I think you do need to pattern match on Refl for idris to know this...
2023-11-09 17:27:55 +0100 <kuribas> Then m and n are bound to the same value.
2023-11-09 17:30:15 +0100 <EvanR> installing scheme to install idris to see xD
2023-11-09 17:30:41 +0100 <EvanR> apparently they switched from haskell to scheme
2023-11-09 17:31:13 +0100shapr(~user@2600:1700:c640:3100:d4c2:10b0:ae58:c7b2) (Ping timeout: 258 seconds)
2023-11-09 17:32:54 +0100 <kuribas> yep
2023-11-09 17:33:05 +0100 <kuribas> well, it's self hosted, but compiles to scheme.
2023-11-09 17:33:21 +0100 <ski> Chez ?
2023-11-09 17:33:30 +0100 <kuribas> Chez/Racket
2023-11-09 17:33:40 +0100 <kuribas> also javascript
2023-11-09 17:34:01 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Ping timeout: 240 seconds)
2023-11-09 17:34:11 +0100 <EvanR> all the best schemes
2023-11-09 17:34:17 +0100sawilagar(~sawilagar@user/sawilagar) (Quit: Leaving)
2023-11-09 17:34:30 +0100 <carter> Chez is pretty redonk
2023-11-09 17:34:35 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 17:34:47 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542)
2023-11-09 17:38:17 +0100deriamis(deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b) (Server closed connection)
2023-11-09 17:38:32 +0100deriamis(deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b)
2023-11-09 17:40:15 +0100sawilagar(~sawilagar@user/sawilagar) (Quit: Leaving)
2023-11-09 17:40:30 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 17:40:50 +0100blurbox(~user@2001:2042:3c78:ab00:b533:32e3:87ff:593d) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.1))
2023-11-09 17:43:03 +0100sawilagar(~sawilagar@user/sawilagar) (Client Quit)
2023-11-09 17:43:19 +0100sawilagar(~sawilagar@user/sawilagar)
2023-11-09 17:45:14 +0100_ht(~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
2023-11-09 17:46:43 +0100 <kuribas> hmm, I get a weird error Can't solve constraint between: ?_ [no locals in scope] and ?_ [no locals in scope].
2023-11-09 17:47:03 +0100 <danse-nr3> haskell or idris?
2023-11-09 17:47:06 +0100 <kuribas> idris
2023-11-09 17:48:37 +0100paddymahoney(~paddymaho@cpe883d24bcf597-cmbc4dfb741f80.cpe.net.cable.rogers.com) (Remote host closed the connection)
2023-11-09 17:48:53 +0100paddymahoney(~paddymaho@cpe883d24bcf597-cmbc4dfb741f80.cpe.net.cable.rogers.com)
2023-11-09 17:49:16 +0100 <EvanR> I can't figure out where my idris binary got installed xD
2023-11-09 17:50:07 +0100 <kuribas> oh I see why
2023-11-09 17:51:52 +0100L29Ah(~L29Ah@wikipedia/L29Ah) ()
2023-11-09 17:52:26 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543) (Remote host closed the connection)
2023-11-09 17:52:42 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net)
2023-11-09 17:54:35 +0100 <kuribas> it doesn't know (+ 1) is injective.
2023-11-09 17:54:45 +0100 <kuribas> So it cannot figure this out.
2023-11-09 17:54:56 +0100 <Inst> ahhh, i see, that's how you do it
2023-11-09 17:55:08 +0100 <Inst> it sucks that codewars took their haskell vector problem off, or at least i can't find it anymore
2023-11-09 17:55:09 +0100 <Inst> :(
2023-11-09 17:55:27 +0100Pozyomka(~pyon@user/pyon) (Quit: WeeChat 4.1.1)
2023-11-09 17:56:05 +0100 <kuribas> (1 + m = 1 + n) -> (m = n) works without problem
2023-11-09 17:56:32 +0100 <Inst> (a :op: b) ~ True
2023-11-09 17:56:56 +0100 <kuribas> (f x = f y) doesn't imply (x = y) in general
2023-11-09 17:57:06 +0100 <Franciman> hi, is haskell semantics deeply related with the stg machine? Or can it be implemented with e.g. the milner abstract machine too?
2023-11-09 17:57:12 +0100 <Franciman> [properly tweaked to become call by need]
2023-11-09 17:57:50 +0100 <[exa]> Franciman: stg was kinda created to support haskell well but there are many other machine kinds that can evaluate it
2023-11-09 17:58:12 +0100 <Franciman> nifty
2023-11-09 17:58:17 +0100 <kuribas> but it's just how (+) is implemented, if it swapped the arguments it would work.
2023-11-09 17:58:28 +0100 <Franciman> thanks [exa]
2023-11-09 17:58:49 +0100CO2(CO2@gateway/vpn/protonvpn/co2)
2023-11-09 17:59:01 +0100 <[exa]> e.g. STG has "spineful" and "tagged" variants, if you switch this on you get something more viable for lisps or so
2023-11-09 17:59:34 +0100 <[exa]> there's the very old STG paper from 1991-ish which has references to many such things
2023-11-09 18:00:44 +0100CO2(CO2@gateway/vpn/protonvpn/co2) (Client Quit)
2023-11-09 18:03:14 +0100 <kuribas> foo : {m, n : Nat} -> (1 + m = 1 + n) -> (m = n); foo {m = 0} {n = 0} Refl = Refl; foo {m = (S k)} {n = (S k)} Refl = Refl
2023-11-09 18:03:22 +0100 <kuribas> proof by induction
2023-11-09 18:04:24 +0100 <kuribas> then you can use "rewrite foo in ..." to ensure that proof is used in the given expression type.
2023-11-09 18:05:04 +0100tzh(~tzh@c-71-193-181-0.hsd1.or.comcast.net)
2023-11-09 18:05:21 +0100 <ncf> that's not induction
2023-11-09 18:05:37 +0100 <ncf> unless foo is implicitly calling itself somehow, i don't know idris
2023-11-09 18:06:49 +0100 <ncf> does idris allow you to not assume UIP?
2023-11-09 18:07:18 +0100 <ncf> apparently not
2023-11-09 18:08:30 +0100CO2(CO2@gateway/vpn/protonvpn/co2)
2023-11-09 18:09:45 +0100 <kuribas> UIP?
2023-11-09 18:09:58 +0100 <ski> Uniqueness of Identity Proofs
2023-11-09 18:10:16 +0100Pozyomka(~pyon@user/pyon)
2023-11-09 18:10:57 +0100 <ski> (p : a = b) -> (q : a = b) -> (p = q)
2023-11-09 18:11:18 +0100 <ncf> fancy pattern matching features like that tend to not work very well if you don't assume that
2023-11-09 18:11:52 +0100 <ncf> i have no idea how that proof works though; is + defined by recursion on the left or on the right?
2023-11-09 18:12:18 +0100 <ski> left, presumably
2023-11-09 18:12:38 +0100 <ncf> so why would you need to pattern match on m and n at all?
2023-11-09 18:13:08 +0100 <ncf> if 1 + m computes to S m, and idris treats S as an injective constructor when unifying S m against S n, you should get m = n
2023-11-09 18:14:11 +0100 <kuribas> \a, b => 1 + the Nat a = 1 + the Nat b
2023-11-09 18:14:12 +0100 <kuribas> \a, b => S a = S b
2023-11-09 18:14:55 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 264 seconds)
2023-11-09 18:14:59 +0100 <kuribas> that implies a = b
2023-11-09 18:15:04 +0100 <dolio> Pretty sure Agda will accept a proof like that without K.
2023-11-09 18:15:18 +0100 <kuribas> dolio: with a single case?
2023-11-09 18:15:26 +0100 <dolio> Yeah.
2023-11-09 18:15:42 +0100 <dolio> foo refl = refl
2023-11-09 18:16:33 +0100 <kuribas> wouldn't that depend on the definition of plus?
2023-11-09 18:17:03 +0100 <dolio> Yeah, of course.
2023-11-09 18:17:19 +0100 <ncf> oh right that works
2023-11-09 18:17:50 +0100 <ncf> kuribas: does your proof work if you don't pattern match?
2023-11-09 18:17:52 +0100 <kuribas> ncf: because it can only see that plus in injective by reducing the expression to a constructor.
2023-11-09 18:17:56 +0100 <ncf> on m and n, that is
2023-11-09 18:18:07 +0100 <kuribas> no
2023-11-09 18:18:20 +0100 <ncf> but 1 + m reduces to a constructor, if + recurses on the left
2023-11-09 18:18:39 +0100 <kuribas> ncf: it does
2023-11-09 18:19:08 +0100 <kuribas> dolio: how does agda knows foo is injective?
2023-11-09 18:19:16 +0100 <Inst> that's... umm, interesting
2023-11-09 18:19:29 +0100 <Inst> you can't size a vector under dependent types such that it's infinitely sized?
2023-11-09 18:20:10 +0100 <ncf> i think it assumes that all constructors of non-higher inductive types are injective, or something
2023-11-09 18:20:12 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 18:21:19 +0100 <kuribas> Inst: no
2023-11-09 18:21:50 +0100 <kuribas> ncf: + is not a constructor
2023-11-09 18:22:02 +0100 <ncf> i know.
2023-11-09 18:23:02 +0100 <dolio> 1 +_ reduces to a constructor.
2023-11-09 18:23:33 +0100 <ncf> foo Refl = Refl -- seems to typecheck for me, but i don't know for sure because i don't know how idris works
2023-11-09 18:23:53 +0100 <ncf> i basically just put your thing in a file and ran idris2 on it
2023-11-09 18:24:39 +0100 <dolio> And yeah, I think it assumes injectivity of the constructors mentioned, because that's an easily derivable fact that is one of the foundations of dependent pattern matching.
2023-11-09 18:24:55 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds)
2023-11-09 18:25:19 +0100 <EvanR> Inst, Nat is non-negative, non-infinite numbers xD
2023-11-09 18:25:42 +0100 <ncf> OTOH the foo refl = refl proof will not compute on transports in cubical agda, and it warns you about it (but that's another story)
2023-11-09 18:25:44 +0100 <dolio> Although you can't easily take advantage of it in cubical mode.
2023-11-09 18:26:27 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 18:27:16 +0100 <kuribas> oh right, I switched the plus :-O
2023-11-09 18:27:35 +0100 <kuribas> no wonder it didn't need induction.
2023-11-09 18:27:58 +0100 <dolio> Yeah, you likely need induction to prove the opposite side.
2023-11-09 18:28:01 +0100 <ncf> the pattern matching is doing the induction for you
2023-11-09 18:29:53 +0100 <EvanR> now that foo Refl = Refl trivially works, do the original task xD
2023-11-09 18:30:02 +0100 <EvanR> m + 1 = n + 1 -> m = n
2023-11-09 18:30:19 +0100 <EvanR> I tried cong sym Refl but no dice
2023-11-09 18:30:46 +0100Cale(~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com)
2023-11-09 18:30:58 +0100 <dolio> That's the side that probably requires induction.
2023-11-09 18:31:30 +0100 <kuribas> EvanR: maybe using injective?
2023-11-09 18:31:52 +0100 <EvanR> it would require induction or a combination of proof combinators
2023-11-09 18:32:00 +0100 <EvanR> doh not symmetry, commutativity
2023-11-09 18:32:33 +0100 <EvanR> which requires induction
2023-11-09 18:32:41 +0100 <dolio> Well, if you've already proved commutativity, then you can use that, yes. But that's going to require induction, probably multiple times.
2023-11-09 18:33:16 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
2023-11-09 18:33:27 +0100 <ncf> bar : {m, n : Nat} -> (m + 1 = n + 1) -> (m = n); bar p = foo (cong plus_commutes p)
2023-11-09 18:33:30 +0100 <ncf> aha
2023-11-09 18:34:18 +0100 <EvanR> where did you get plus_commutes
2023-11-09 18:34:24 +0100 <ncf> prelude
2023-11-09 18:34:28 +0100 <EvanR> :(
2023-11-09 18:34:38 +0100 <EvanR> Undefined name plus_commutes
2023-11-09 18:34:56 +0100 <ncf> idris 2?
2023-11-09 18:35:07 +0100 <EvanR> yeah but I probably didn't install it right
2023-11-09 18:35:18 +0100 <EvanR> except import Prelude works
2023-11-09 18:36:05 +0100 <EvanR> oh well, off topic
2023-11-09 18:36:25 +0100drewjose(~drewjose@129.154.40.88)
2023-11-09 18:39:37 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2023-11-09 18:40:27 +0100euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2023-11-09 18:42:08 +0100dsrt^(~cd@76.145.193.217) (Remote host closed the connection)
2023-11-09 18:45:53 +0100idgaen(~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c)
2023-11-09 18:49:07 +0100 <EvanR> ncf, idris2 version Version 0.6.0-d80bc1537 ?
2023-11-09 18:49:29 +0100 <ncf> 0.6.0
2023-11-09 18:49:38 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2023-11-09 18:51:23 +0100 <danse-nr3> :t mapAccumR
2023-11-09 18:51:24 +0100 <lambdabot> Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c)
2023-11-09 18:51:34 +0100fendor_(~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection)
2023-11-09 18:56:19 +0100danse-nr3(~danse@151.57.105.34) (Ping timeout: 258 seconds)
2023-11-09 18:56:29 +0100thegman(~thegman@072-239-207-086.res.spectrum.com)
2023-11-09 18:56:40 +0100danse-nr3(~danse@151.57.123.82)
2023-11-09 19:00:19 +0100vgtw(~vgtw@user/vgtw) (Ping timeout: 255 seconds)
2023-11-09 19:00:22 +0100vgtw_(~vgtw@user/vgtw)
2023-11-09 19:03:10 +0100 <EvanR> that's a good one
2023-11-09 19:03:42 +0100 <danse-nr3> what, mapAccum?
2023-11-09 19:05:14 +0100 <EvanR> yeah
2023-11-09 19:06:00 +0100 <danse-nr3> yeah i saw a pattern in the code and thought ... there ought to be a class for this. But probably it is not that worth abstraction
2023-11-09 19:07:10 +0100qqq(~qqq@92.43.167.61)
2023-11-09 19:08:32 +0100Lycurgus(~georg@user/Lycurgus)
2023-11-09 19:09:31 +0100 <ncf> that's traverse
2023-11-09 19:09:42 +0100 <danse-nr3> huh?
2023-11-09 19:09:46 +0100 <danse-nr3> :t mapAccumR
2023-11-09 19:09:47 +0100 <lambdabot> Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c)
2023-11-09 19:09:55 +0100 <danse-nr3> yeah, mapAccum uses traverse
2023-11-09 19:09:59 +0100 <ncf> specialised to State a, with some arguments flipped
2023-11-09 19:10:16 +0100jludwig(~justin@li657-110.members.linode.com) (Quit: ZNC - https://znc.in)
2023-11-09 19:10:31 +0100 <danse-nr3> you are talking about my problem now? This is telepathy!
2023-11-09 19:12:03 +0100 <danse-nr3> or probably some kind of exhaustion that makes me mix topics with each other. I wish i had a bit of time to study this better
2023-11-09 19:12:10 +0100 <ncf> i'm talking about mapAccumR
2023-11-09 19:12:40 +0100 <danse-nr3> well i can refresh my memory about stuff i use rarely, let us see maybe i will get enlightened
2023-11-09 19:12:43 +0100 <danse-nr3> :t traverse
2023-11-09 19:12:44 +0100 <lambdabot> (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
2023-11-09 19:14:24 +0100 <danse-nr3> :t State
2023-11-09 19:14:25 +0100 <lambdabot> error:
2023-11-09 19:14:25 +0100 <lambdabot> • Data constructor not in scope: State
2023-11-09 19:14:25 +0100 <lambdabot> • Perhaps you meant one of these:
2023-11-09 19:15:24 +0100 <danse-nr3> yes, i get a glimpse. Probably this could be an interesting applicative ... unfortunately i am afraid it will be a function abstracting over foldr at the moment
2023-11-09 19:15:36 +0100 <steew> hello, im learning haskell currently, and I am failing to understand why the groupBy function takes two arguments in its lambda like so: groupBy (\a b -> b - a < 5) [0..19]
2023-11-09 19:15:41 +0100 <steew> what are in this case a and b?
2023-11-09 19:15:51 +0100 <danse-nr3> :t groupBy
2023-11-09 19:15:52 +0100 <lambdabot> (a -> a -> Bool) -> [a] -> [[a]]
2023-11-09 19:15:55 +0100 <steew> (example taken from the documentation)
2023-11-09 19:16:21 +0100 <danse-nr3> you want to compare things to group together steew
2023-11-09 19:16:55 +0100 <EvanR> in this case it's not comparing as much as testing for equality
2023-11-09 19:17:20 +0100 <EvanR> you're passing in a custom equality test on two things
2023-11-09 19:17:28 +0100 <steew> ahhh right, I realized by looking at the source
2023-11-09 19:18:15 +0100 <EvanR> b - a < 5 doesn't seem to obey the symmetry property of equality
2023-11-09 19:19:33 +0100 <danse-nr3> looks more like a way to mess with the function ^^;
2023-11-09 19:19:36 +0100 <EvanR> 7 would equal 1, but 1 would not equal 7
2023-11-09 19:20:17 +0100 <danse-nr3> had not noticed that, very good point
2023-11-09 19:23:35 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2023-11-09 19:27:17 +0100Tuplanolla(~Tuplanoll@91-159-68-236.elisa-laajakaista.fi)
2023-11-09 19:27:23 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de)
2023-11-09 19:27:34 +0100__monty__(~toonn@user/toonn)
2023-11-09 19:27:52 +0100Guest45(~Guest45@54013D83.dsl.pool.telekom.hu)
2023-11-09 19:30:37 +0100 <monochrom> I missed the fun dependent typing discussion. :(
2023-11-09 19:31:20 +0100 <EvanR> and my unfun inability to reproduce what ncf was doing
2023-11-09 19:32:24 +0100Lycurgus(~georg@user/Lycurgus) (Quit: leaving)
2023-11-09 19:32:33 +0100waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2023-11-09 19:33:42 +0100motherfsck(~motherfsc@user/motherfsck)
2023-11-09 19:34:04 +0100 <ncf> i can't reproduce it either now. o_o
2023-11-09 19:35:13 +0100 <ncf> What Did I Do
2023-11-09 19:37:54 +0100shapr(~user@2600:1700:c640:3100:9af4:b6dd:227b:75bc)
2023-11-09 19:42:56 +0100Guest45(~Guest45@54013D83.dsl.pool.telekom.hu) (Ping timeout: 250 seconds)
2023-11-09 19:55:13 +0100 <[exa]> is there any good package that works nicely with large binary data? in particular, something that's worthy mmaping and browsing by pointers
2023-11-09 19:55:39 +0100 <[exa]> (such as a huge binary memorymapped btree or a database index or so)
2023-11-09 19:55:52 +0100 <[exa]> I'm deciding whether to prototype in haskell and some inspiration would be cool
2023-11-09 19:56:59 +0100 <EvanR> .oO(or a DOOM wad)
2023-11-09 19:57:38 +0100 <dmj`> [exa]: bytestring-mmap ?
2023-11-09 19:57:48 +0100 <[exa]> EvanR: yes, or a doom wad.
2023-11-09 19:58:47 +0100 <[exa]> dmj`: yeah that would kinda work, there's even `mmap` which kinda works for me already (in a different project)
2023-11-09 19:59:19 +0100 <[exa]> was interested more like in how to do the pointer mechanics and similar things reasonably
2023-11-09 19:59:56 +0100 <EvanR> a bytestring is basically a pointer into some binary blob with length
2023-11-09 20:00:03 +0100 <dmj`> [exa]: I'd check out haskey-btree
2023-11-09 20:00:06 +0100 <dmj`> @package haskey-btree
2023-11-09 20:00:06 +0100 <lambdabot> https://hackage.haskell.org/package/haskey-btree
2023-11-09 20:00:19 +0100 <EvanR> so to navigate your mmapped data you can just break, span, drop
2023-11-09 20:00:27 +0100 <dmj`> iirc it doesn't use mmap and traverses the Handle manually
2023-11-09 20:00:45 +0100 <EvanR> (but make sure not to copy the entire thing)
2023-11-09 20:00:48 +0100 <[exa]> ah that could work too
2023-11-09 20:02:05 +0100 <dmj`> Writing a sqlite clone in Haskell would be cool
2023-11-09 20:03:08 +0100dcoutts(~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 260 seconds)
2023-11-09 20:03:31 +0100L29Ah(~L29Ah@wikipedia/L29Ah)
2023-11-09 20:04:13 +0100danse-nr3(~danse@151.57.123.82) (Ping timeout: 255 seconds)
2023-11-09 20:07:11 +0100danse-nr3(~danse@151.57.123.82)
2023-11-09 20:11:24 +0100alp(~alp@static-176-175-7-165.ftth.abo.bbox.fr)
2023-11-09 20:14:57 +0100Vajb(~Vajb@mobile-access-2e8444-121.dhcp.inet.fi)
2023-11-09 20:19:40 +0100danse-nr3(~danse@151.57.123.82) (Ping timeout: 272 seconds)
2023-11-09 20:31:57 +0100infinity0(~infinity0@pwned.gg) (Remote host closed the connection)
2023-11-09 20:33:52 +0100infinity0(~infinity0@pwned.gg)
2023-11-09 20:34:34 +0100zetef(~quassel@95.77.17.251)
2023-11-09 20:37:22 +0100infinity0_(~infinity0@pwned.gg)
2023-11-09 20:37:22 +0100infinity0Guest605
2023-11-09 20:37:22 +0100infinity0_infinity0
2023-11-09 20:38:15 +0100Guest605(~infinity0@pwned.gg) (Ping timeout: 240 seconds)
2023-11-09 20:39:01 +0100zetef(~quassel@95.77.17.251) (Ping timeout: 240 seconds)
2023-11-09 20:39:54 +0100lortabac(~lorenzo@2a01:e0a:541:b8f0:cf92:a8ae:a9da:4f45) (Quit: WeeChat 3.5)
2023-11-09 20:44:58 +0100danza(~francesco@151.57.123.82)
2023-11-09 20:52:57 +0100 <phma> I'm trying to compute six things in parallel, but it's not running fast. I used Threadscope, and I can see that only one core is working on it, but how can I see what part of the program is running when?
2023-11-09 20:54:16 +0100eggplantade(~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2023-11-09 20:55:44 +0100trev(~trev@user/trev) (Quit: trev)
2023-11-09 20:56:43 +0100neceve(~neceve@user/neceve)
2023-11-09 20:56:52 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2023-11-09 20:56:56 +0100Pickchea(~private@user/pickchea)
2023-11-09 20:59:08 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Client Quit)
2023-11-09 20:59:20 +0100zer0bitz_(~zer0bitz@user/zer0bitz)
2023-11-09 21:03:13 +0100zer0bitz(~zer0bitz@user/zer0bitz) (Ping timeout: 260 seconds)
2023-11-09 21:09:09 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2023-11-09 21:09:28 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Ping timeout: 255 seconds)
2023-11-09 21:14:43 +0100jinsunGuest2321
2023-11-09 21:14:43 +0100jinsun_(~jinsun@user/jinsun)
2023-11-09 21:14:43 +0100Guest2321(~jinsun@user/jinsun) (Killed (tungsten.libera.chat (Nickname regained by services)))
2023-11-09 21:14:43 +0100jinsun_jinsun
2023-11-09 21:16:05 +0100danza(~francesco@151.57.123.82) (Ping timeout: 252 seconds)
2023-11-09 21:17:10 +0100todi(~todi@p4fd1a3e6.dip0.t-ipconnect.de)
2023-11-09 21:19:06 +0100ft(~ft@p4fc2a529.dip0.t-ipconnect.de)
2023-11-09 21:23:22 +0100vulpine(xfnw@tilde.team) (Quit: Connection reset by purr)
2023-11-09 21:28:39 +0100vulpine(xfnw@tilde.team)
2023-11-09 21:31:57 +0100Lycurgus(~georg@user/Lycurgus)
2023-11-09 21:34:12 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6)
2023-11-09 21:36:04 +0100accord(uid568320@id-568320.hampstead.irccloud.com)
2023-11-09 21:37:19 +0100alp(~alp@static-176-175-7-165.ftth.abo.bbox.fr) (Ping timeout: 258 seconds)
2023-11-09 21:40:00 +0100jinsun_(~jinsun@user/jinsun)
2023-11-09 21:40:00 +0100jinsunGuest3991
2023-11-09 21:40:01 +0100Guest3991(~jinsun@user/jinsun) (Killed (cadmium.libera.chat (Nickname regained by services)))
2023-11-09 21:40:01 +0100jinsun_jinsun
2023-11-09 21:43:23 +0100califax(~califax@user/califx) (Remote host closed the connection)
2023-11-09 21:43:54 +0100ddellacosta(~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 272 seconds)
2023-11-09 21:44:21 +0100califax(~califax@user/califx)
2023-11-09 21:44:44 +0100dcoutts(~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net)
2023-11-09 21:45:58 +0100buhman(sid411355@user/buhman) (Server closed connection)
2023-11-09 21:46:14 +0100buhman(sid411355@user/buhman)
2023-11-09 21:49:39 +0100L29Ah(~L29Ah@wikipedia/L29Ah) ()
2023-11-09 21:51:58 +0100michalz(~michalz@185.246.207.197) (Remote host closed the connection)
2023-11-09 21:53:31 +0100Lycurgus(~georg@user/Lycurgus) (Quit: leaving)
2023-11-09 21:56:16 +0100sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2023-11-09 21:58:14 +0100jappiejappie(~jappiejap@186-011-158-163.dynamic.caiway.nl)
2023-11-09 22:03:41 +0100kaol(~kaol@94-237-42-30.nl-ams1.upcloud.host) (Server closed connection)
2023-11-09 22:03:48 +0100kaol(~kaol@94-237-42-30.nl-ams1.upcloud.host)
2023-11-09 22:07:24 +0100coot(~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot)
2023-11-09 22:09:11 +0100 <EvanR> haskell code which writes to mutable arrays incurs additional overhead from gc book-keeping, since it can violate causality in a way that immutable data can't. Meanwhile using FFI to call out an modify 1 element at a time also has overhead. Is there tech to speak of scribbling on some blob (not managed by gc) efficiently
2023-11-09 22:09:47 +0100 <EvanR> with haskell code
2023-11-09 22:10:40 +0100 <geekosaur> pinned arrays and `Foreign.Marshal.Array`?
2023-11-09 22:12:02 +0100 <EvanR> pokeArray :: Storable a => Ptr a -> [a] -> IO ()...
2023-11-09 22:12:10 +0100machinedgod(~machinedg@d198-53-218-113.abhsia.telus.net)
2023-11-09 22:13:47 +0100 <EvanR> for Word8 it's based on writeWord8OffPtr
2023-11-09 22:15:33 +0100 <EvanR> based on a primitive of the same name
2023-11-09 22:15:37 +0100 <EvanR> cool
2023-11-09 22:17:30 +0100 <EvanR> so some stuff in Foreign doesn't involve a formal FFI call to C
2023-11-09 22:18:03 +0100 <geekosaur> mostly it's support for such calls, rather than the calls themselves
2023-11-09 22:19:16 +0100ubert1(~Thunderbi@178.165.207.175.wireless.dyn.drei.com)
2023-11-09 22:20:05 +0100ubert(~Thunderbi@178.165.181.20.wireless.dyn.drei.com) (Ping timeout: 240 seconds)
2023-11-09 22:20:05 +0100ubert1ubert
2023-11-09 22:21:42 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net)
2023-11-09 22:24:48 +0100glassribbon(~glassribb@187.19.131.51)
2023-11-09 22:25:07 +0100_ht(~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
2023-11-09 22:25:19 +0100glassribbon(~glassribb@187.19.131.51) ()
2023-11-09 22:26:21 +0100nate3(~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds)
2023-11-09 22:31:04 +0100thegman_(~thegman@072-239-207-086.res.spectrum.com)
2023-11-09 22:31:40 +0100thegman(~thegman@072-239-207-086.res.spectrum.com) (Read error: Connection reset by peer)
2023-11-09 22:31:54 +0100thegman_thegman
2023-11-09 22:33:00 +0100Pickchea(~private@user/pickchea) (Quit: Leaving)
2023-11-09 22:33:14 +0100dsrt^(~cd@76.145.193.217)
2023-11-09 22:36:46 +0100neceve(~neceve@user/neceve) (Ping timeout: 255 seconds)
2023-11-09 22:41:29 +0100thegman(~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving)
2023-11-09 22:42:50 +0100thegman(~thegman@072-239-207-086.res.spectrum.com)
2023-11-09 22:49:21 +0100gmg(~user@user/gehmehgeh) (Quit: Leaving)
2023-11-09 22:49:55 +0100takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2023-11-09 22:50:55 +0100chomwitt(~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1) (Ping timeout: 264 seconds)
2023-11-09 22:51:17 +0100Buliarous(~gypsydang@46.232.210.139) (Remote host closed the connection)
2023-11-09 22:51:35 +0100mc47(~mc47@xmonad/TheMC47) (Remote host closed the connection)
2023-11-09 23:05:05 +0100idgaen(~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1)
2023-11-09 23:10:17 +0100acidjnk(~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de) (Ping timeout: 255 seconds)
2023-11-09 23:11:51 +0100nicole(ilbelkyr@libera/staff/ilbelkyr) (*.net *.split)
2023-11-09 23:11:55 +0100nicole(ilbelkyr@libera/staff/ilbelkyr)
2023-11-09 23:19:08 +0100pavonia(~user@user/siracusa)
2023-11-09 23:27:43 +0100Vajb(~Vajb@mobile-access-2e8444-121.dhcp.inet.fi) (Ping timeout: 258 seconds)
2023-11-09 23:28:31 +0100Vajb(~Vajb@2001:999:785:c11e:a1b8:59fa:dee7:e490)
2023-11-09 23:29:36 +0100alp(~alp@2001:861:5e02:eff0:c5b5:b1c1:9abe:83f8)
2023-11-09 23:36:03 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2023-11-09 23:38:15 +0100wroathe(~wroathe@50.205.197.50)
2023-11-09 23:38:15 +0100wroathe(~wroathe@50.205.197.50) (Changing host)
2023-11-09 23:38:15 +0100wroathe(~wroathe@user/wroathe)
2023-11-09 23:43:08 +0100alp(~alp@2001:861:5e02:eff0:c5b5:b1c1:9abe:83f8) (Remote host closed the connection)
2023-11-09 23:50:32 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2023-11-09 23:52:14 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2023-11-09 23:52:18 +0100 <tomsmeding> geekosaur: is the "pinned memory" of Foreign.Marshal.Alloc.malloc the same as the "pinned memory" of a strict ByteString?
2023-11-09 23:52:41 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2023-11-09 23:53:07 +0100 <tomsmeding> somehow I always thought, without looking anything up and intuiting from the name "pinned memory", that a ByteString would have a heap allocation inside the regular heap area that the GC somehow cannot move
2023-11-09 23:53:10 +0100 <tomsmeding> which can hardly be a good idea
2023-11-09 23:53:33 +0100 <EvanR> and malloc is apparently an ffi call to actual malloc
2023-11-09 23:53:40 +0100 <tomsmeding> :o
2023-11-09 23:54:00 +0100 <tomsmeding> oh lol
2023-11-09 23:54:08 +0100 <geekosaur> my understanding is they are the same, and the point is to have something that can safely be passed to and from C (which is part of why malloc is used)
2023-11-09 23:54:14 +0100zer0bitz_(~zer0bitz@user/zer0bitz) (Ping timeout: 245 seconds)
2023-11-09 23:54:14 +0100 <tomsmeding> I guess that is so that you can work with C APIs that expect to malloc/free stuff
2023-11-09 23:54:17 +0100 <geekosaur> er, C malloc()
2023-11-09 23:54:20 +0100 <geekosaur> yes
2023-11-09 23:54:21 +0100 <tomsmeding> yeah
2023-11-09 23:54:24 +0100 <tomsmeding> cool
2023-11-09 23:54:33 +0100 <tomsmeding> things make more sense in my head now
2023-11-09 23:54:42 +0100 <tomsmeding> "pinned memory" is a bit of an awkward name though
2023-11-09 23:55:06 +0100 <geekosaur> that's what ghc calls it, for whatever reason
2023-11-09 23:55:08 +0100 <EvanR> it's so pinned but then the kernel moves it around on you with MMU shenanigans xD
2023-11-09 23:55:32 +0100 <tomsmeding> I mean, it is pinned when comparing it to GC-managed heap allocations
2023-11-09 23:55:39 +0100 <EvanR> relatively pinned
2023-11-09 23:55:43 +0100 <EvanR> more pinned than thou
2023-11-09 23:55:45 +0100 <tomsmeding> I'm just going to remember it as "C-heap allocations"
2023-11-09 23:55:51 +0100 <tomsmeding> EvanR: you are pinned
2023-11-09 23:55:53 +0100 <geekosaur> pinned within the application address space, which is what matters
2023-11-09 23:55:57 +0100 <tomsmeding> yes
2023-11-09 23:56:54 +0100eggplantade(~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 272 seconds)