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 +0100 | wroathe | (~wroathe@50.205.197.50) |
2023-11-09 00:03:30 +0100 | wroathe | (~wroathe@50.205.197.50) (Changing host) |
2023-11-09 00:03:30 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-11-09 00:04:51 +0100 | Benzi-Junior | (~BenziJuni@88-149-64-112.du.xdsl.is) (Server closed connection) |
2023-11-09 00:06:38 +0100 | Benzi-Junior | (~BenziJuni@88-149-64-112.du.xdsl.is) |
2023-11-09 00:08:41 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-09 00:10:30 +0100 | terrorjack | (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
2023-11-09 00:12:27 +0100 | terrorjack | (~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 +0100 | neceve | (~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 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-11-09 00:23:18 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-09 00:25:51 +0100 | mechap | (~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 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
2023-11-09 00:28:06 +0100 | zetef | (~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 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2023-11-09 00:36:55 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
2023-11-09 00:41:43 +0100 | wroathe | (~wroathe@user/wroathe) (Quit: leaving) |
2023-11-09 00:54:05 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Read error: Connection reset by peer) |
2023-11-09 00:54:50 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2023-11-09 00:56:12 +0100 | monochrom | (trebla@216.138.220.146) (Quit: ZNC 1.8.2+deb3build2 - https://znc.in) |
2023-11-09 00:58:56 +0100 | monochrom | (trebla@216.138.220.146) |
2023-11-09 01:00:02 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
2023-11-09 01:02:59 +0100 | notzmv | (~zmv@user/notzmv) |
2023-11-09 01:13:17 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) |
2023-11-09 01:13:17 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) (Changing host) |
2023-11-09 01:13:17 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-09 01:29:39 +0100 | infinity0 | (~infinity0@pwned.gg) (Remote host closed the connection) |
2023-11-09 01:35:25 +0100 | infinity0 | (~infinity0@pwned.gg) |
2023-11-09 01:39:11 +0100 | falafel | (~falafel@62.175.113.194.dyn.user.ono.com) |
2023-11-09 01:44:53 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2023-11-09 01:49:14 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-09 02:10:59 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
2023-11-09 02:12:17 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
2023-11-09 02:25:07 +0100 | falafel | (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 264 seconds) |
2023-11-09 02:30:21 +0100 | cods | (~fred@tuxee.net) (Ping timeout: 240 seconds) |
2023-11-09 02:37:38 +0100 | cods | (~fred@tuxee.net) |
2023-11-09 02:41:23 +0100 | kimiamania468 | (~b4f4a2ab@user/kimiamania) |
2023-11-09 02:43:03 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) (Ping timeout: 240 seconds) |
2023-11-09 02:43:03 +0100 | kimiamania468 | kimiamania46 |
2023-11-09 02:43:27 +0100 | Jackneill | (~Jackneill@20014C4E1E058A0009BBD059E8BC0D29.dsl.pool.telekom.hu) (Ping timeout: 240 seconds) |
2023-11-09 02:43:37 +0100 | haskellbridge | (~haskellbr@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
2023-11-09 02:55:30 +0100 | derpyxdhs | (~Thunderbi@user/derpyxdhs) |
2023-11-09 03:02:49 +0100 | Sciencentistguy0 | (~sciencent@hacksoc/ordinary-member) |
2023-11-09 03:03:50 +0100 | xff0x | (~xff0x@2405:6580:b080:900:568f:45bf:9aab:4d48) (Ping timeout: 255 seconds) |
2023-11-09 03:05:05 +0100 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Ping timeout: 240 seconds) |
2023-11-09 03:05:05 +0100 | Sciencentistguy0 | Sciencentistguy |
2023-11-09 03:08:26 +0100 | derpyxdhs | (~Thunderbi@user/derpyxdhs) (Quit: derpyxdhs) |
2023-11-09 03:15:25 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-09 03:20:01 +0100 | otto_s | (~user@p5b044db0.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2023-11-09 03:21:58 +0100 | otto_s | (~user@p5de2fe1e.dip0.t-ipconnect.de) |
2023-11-09 03:22:03 +0100 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
2023-11-09 03:24:04 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
2023-11-09 03:25:03 +0100 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
2023-11-09 03:33:23 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
2023-11-09 03:41:38 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2023-11-09 03:46:38 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2023-11-09 03:51:36 +0100 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
2023-11-09 03:54:20 +0100 | edr | (~edr@user/edr) (Quit: Leaving) |
2023-11-09 04:05:22 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-11-09 04:05:22 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-11-09 04:05:22 +0100 | finn_elija | FinnElija |
2023-11-09 04:12:05 +0100 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
2023-11-09 04:12:32 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) (Server closed connection) |
2023-11-09 04:13:26 +0100 | dsrt^ | (~cd@76.145.193.217) |
2023-11-09 04:14:06 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) |
2023-11-09 04:14:44 +0100 | kiriakos | (~kiriakos@p5b03e4f0.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2023-11-09 04:15:54 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Read error: Connection reset by peer) |
2023-11-09 04:17:44 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
2023-11-09 04:18:20 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543) (Remote host closed the connection) |
2023-11-09 04:18:41 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
2023-11-09 04:18:54 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
2023-11-09 04:27:23 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 252 seconds) |
2023-11-09 04:34:35 +0100 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
2023-11-09 04:47:11 +0100 | td_ | (~td@i53870921.versanet.de) (Ping timeout: 252 seconds) |
2023-11-09 04:49:13 +0100 | td_ | (~td@i53870905.versanet.de) |
2023-11-09 05:11:17 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2023-11-09 05:11:45 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
2023-11-09 05:15:36 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 258 seconds) |
2023-11-09 05:17:35 +0100 | aforemny_ | (~aforemny@2001:9e8:6ccb:5b00:f896:13f1:97ad:eaff) |
2023-11-09 05:19:07 +0100 | aforemny | (~aforemny@2001:9e8:6ce5:5c00:3494:c671:8982:8a94) (Ping timeout: 264 seconds) |
2023-11-09 05:45:29 +0100 | michalz | (~michalz@185.246.207.197) |
2023-11-09 05:47:57 +0100 | mjs2600 | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Server closed connection) |
2023-11-09 05:48:05 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Quit: Lost terminal) |
2023-11-09 05:48:14 +0100 | mjs2600 | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) |
2023-11-09 05:53:34 +0100 | trev | (~trev@user/trev) |
2023-11-09 05:55:47 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-09 05:56:04 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-09 05:59:51 +0100 | Friendship | (~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 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-09 06:29:41 +0100 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 240 seconds) |
2023-11-09 06:32:10 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-09 06:32:18 +0100 | euleritian | (~euleritia@77.22.252.56) |
2023-11-09 06:40:58 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 255 seconds) |
2023-11-09 06:56:32 +0100 | <MelanieMalik> | sgih |
2023-11-09 06:56:45 +0100 | euleritian | (~euleritia@77.22.252.56) |
2023-11-09 06:59:04 +0100 | Inst | (~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 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2023-11-09 07:27:47 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 252 seconds) |
2023-11-09 07:28:07 +0100 | euleritian | (~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 +0100 | glowcoil | (sid3405@id-3405.tinside.irccloud.com) (Server closed connection) |
2023-11-09 07:40:07 +0100 | glowcoil | (sid3405@id-3405.tinside.irccloud.com) |
2023-11-09 07:41:09 +0100 | alp | (~alp@static-176-175-7-165.ftth.abo.bbox.fr) |
2023-11-09 07:44:03 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-11-09 07:44:32 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-11-09 07:53:21 +0100 | alp | (~alp@static-176-175-7-165.ftth.abo.bbox.fr) (Ping timeout: 240 seconds) |
2023-11-09 07:58:17 +0100 | gmg | (~user@user/gehmehgeh) |
2023-11-09 08:01:04 +0100 | acidjnk | (~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de) |
2023-11-09 08:03:03 +0100 | tromp | (~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 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-09 08:22:38 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-11-09 08:22:58 +0100 | trev | (~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 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
2023-11-09 08:30:05 +0100 | thegeekinside | (~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 +0100 | tromp | (~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 +0100 | misterfish | (~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 +0100 | lortabac | (~lorenzo@2a01:e0a:541:b8f0:cf92:a8ae:a9da:4f45) |
2023-11-09 08:57:16 +0100 | danza | (~francesco@151.43.102.157) |
2023-11-09 09:00:05 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds) |
2023-11-09 09:02:19 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543) |
2023-11-09 09:07:37 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-09 09:14:00 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
2023-11-09 09:15:20 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) |
2023-11-09 09:20:18 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-11-09 09:20:57 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-09 09:28:05 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
2023-11-09 09:29:08 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
2023-11-09 09:38:02 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-11-09 09:39:29 +0100 | miguelnegrao | (~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 +0100 | misterfish | (~misterfis@46.44.172.198) |
2023-11-09 09:51:10 +0100 | ubert | (~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 +0100 | ggranberry | (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 +0100 | machinedgod | (~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 +0100 | alp | (~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 +0100 | Jackneill | (~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 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-09 10:16:59 +0100 | nate3 | (~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 +0100 | danza | (~francesco@151.43.102.157) (Ping timeout: 258 seconds) |
2023-11-09 10:22:16 +0100 | nate3 | (~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 +0100 | mastarija | (~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 +0100 | Sgeo | (~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 +0100 | krei-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 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-09 10:36:01 +0100 | krei-se | (~krei-se@p5085dea2.dip0.t-ipconnect.de) |
2023-11-09 10:38:40 +0100 | lottaquestions | (~nick@2607:fa49:503d:b200:135c:2e9a:d788:4186) |
2023-11-09 10:40:07 +0100 | conjunctive | (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 +0100 | conjunctive | (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 +0100 | danse-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 +0100 | todi | (~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 +0100 | Friendship | (~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 +0100 | danse-nr3 | (~danse@151.43.102.157) (Ping timeout: 272 seconds) |
2023-11-09 10:49:29 +0100 | danse-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 +0100 | erty | (~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 +0100 | misterfish | (~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 +0100 | mastarija | (~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 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) (Server closed connection) |
2023-11-09 10:59:49 +0100 | sa | (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 +0100 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
2023-11-09 11:13:16 +0100 | miguelnegrao | (~miguelneg@2001:818:dc71:d100:f016:1b9:e7c1:3567) (Quit: miguelnegrao) |
2023-11-09 11:25:50 +0100 | alp | (~alp@2001:861:5e02:eff0:a92b:16ae:f4aa:f168) (Quit: Leaving) |
2023-11-09 11:26:04 +0100 | alp | (~alp@2001:861:5e02:eff0:e:ba9a:698b:1b65) |
2023-11-09 11:26:18 +0100 | alp | (~alp@2001:861:5e02:eff0:e:ba9a:698b:1b65) (Changing host) |
2023-11-09 11:26:18 +0100 | alp | (~alp@user/alp) |
2023-11-09 11:28:31 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-09 11:44:24 +0100 | alp | (~alp@user/alp) (Remote host closed the connection) |
2023-11-09 11:44:42 +0100 | alp | (~alp@2001:861:5e02:eff0:97b5:b655:9038:6771) |
2023-11-09 11:48:56 +0100 | zmt00 | (~zmt00@user/zmt00) |
2023-11-09 11:50:39 +0100 | zmt01 | (~zmt00@user/zmt00) (Ping timeout: 240 seconds) |
2023-11-09 11:54:16 +0100 | alp | (~alp@2001:861:5e02:eff0:97b5:b655:9038:6771) (Changing host) |
2023-11-09 11:54:16 +0100 | alp | (~alp@user/alp) |
2023-11-09 11:54:28 +0100 | misterfish | (~misterfis@37.153.233.129) |
2023-11-09 11:55:20 +0100 | sand-witch_ | (~m-mzmz6l@vmi833741.contaboserver.net) |
2023-11-09 11:56:05 +0100 | sand-witch | (~m-mzmz6l@vmi833741.contaboserver.net) (Ping timeout: 240 seconds) |
2023-11-09 11:57:51 +0100 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2023-11-09 11:59:48 +0100 | ft | (~ft@p4fc2a529.dip0.t-ipconnect.de) (Quit: leaving) |
2023-11-09 11:59:55 +0100 | ursa-major | (~ursa-majo@37.19.210.38) (Ping timeout: 264 seconds) |
2023-11-09 12:00:13 +0100 | sand-witch_ | sand-witch |
2023-11-09 12:01:44 +0100 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
2023-11-09 12:13:34 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531) |
2023-11-09 12:21:05 +0100 | mmhat | (~mmh@p200300f1c7445e88ee086bfffe095315.dip0.t-ipconnect.de) |
2023-11-09 12:21:13 +0100 | mmhat | (~mmh@p200300f1c7445e88ee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
2023-11-09 12:27:31 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
2023-11-09 12:36:09 +0100 | lhpitn | (~tn@31.172.106.163.static-pppoe.dt.ipv4.wtnet.de) (Remote host closed the connection) |
2023-11-09 12:36:31 +0100 | lhpitn | (~tn@mail.lebenshilfe-pi.de) |
2023-11-09 12:42:43 +0100 | lhpitn | (~tn@mail.lebenshilfe-pi.de) (Remote host closed the connection) |
2023-11-09 12:43:06 +0100 | lhpitn | (~tn@mail.lebenshilfe-pi.de) |
2023-11-09 12:47:51 +0100 | misterfish | (~misterfis@37.153.233.129) (Ping timeout: 255 seconds) |
2023-11-09 12:49:01 +0100 | Friendship | (~Friendshi@user/Friendship) (Read error: Connection reset by peer) |
2023-11-09 12:49:21 +0100 | Friendship | (~Friendshi@user/Friendship) |
2023-11-09 12:54:08 +0100 | haskellbridge | (~haskellbr@069-135-003-034.biz.spectrum.com) |
2023-11-09 12:54:08 +0100 | ChanServ | +v haskellbridge |
2023-11-09 12:55:41 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) |
2023-11-09 12:58:36 +0100 | misterfish | (~misterfis@37.153.233.129) |
2023-11-09 13:00:13 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-09 13:00:32 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-09 13:01:58 +0100 | dibblego | (~dibblego@haskell/developer/dibblego) (Ping timeout: 260 seconds) |
2023-11-09 13:02:12 +0100 | Vq | (~vq@90-225-115-195-no122.tbcn.telia.com) (Server closed connection) |
2023-11-09 13:02:22 +0100 | Vq | (~vq@90-225-115-195-no122.tbcn.telia.com) |
2023-11-09 13:02:55 +0100 | dibblego | (~dibblego@122-199-1-93.ip4.superloop.au) |
2023-11-09 13:02:55 +0100 | dibblego | (~dibblego@122-199-1-93.ip4.superloop.au) (Changing host) |
2023-11-09 13:02:55 +0100 | dibblego | (~dibblego@haskell/developer/dibblego) |
2023-11-09 13:09:31 +0100 | zetef | (~quassel@95.77.17.251) |
2023-11-09 13:12:54 +0100 | manwithluck | (manwithluc@2406:da14:5ea:e400:7863:dbc1:6a84:3050) (Quit: ZNC - https://znc.in) |
2023-11-09 13:13:13 +0100 | manwithluck | (manwithluc@ec2-52-197-234-151.ap-northeast-1.compute.amazonaws.com) |
2023-11-09 13:13:55 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-11-09 13:14:22 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-11-09 13:26:56 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-09 13:27:40 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) |
2023-11-09 13:28:03 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-09 13:28:20 +0100 | euleritian | (~euleritia@77.22.252.56) |
2023-11-09 13:30:16 +0100 | erty | (~user@user/aeroplane) (Remote host closed the connection) |
2023-11-09 13:34:12 +0100 | sawilagar | (~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 +0100 | manwithluck | (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 +0100 | manwithluck | (manwithluc@ec2-52-197-234-151.ap-northeast-1.compute.amazonaws.com) |
2023-11-09 13:47:00 +0100 | danse-nr3 | (~danse@151.57.108.79) (Ping timeout: 272 seconds) |
2023-11-09 13:52:23 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Remote host closed the connection) |
2023-11-09 13:52:41 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
2023-11-09 14:01:44 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531) (Ping timeout: 255 seconds) |
2023-11-09 14:03:46 +0100 | xff0x | (~xff0x@178.255.149.135) |
2023-11-09 14:16:49 +0100 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Remote host closed the connection) |
2023-11-09 14:18:31 +0100 | xff0x | (~xff0x@178.255.149.135) (Ping timeout: 264 seconds) |
2023-11-09 14:18:40 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-09 14:20:08 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531) |
2023-11-09 14:23:55 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
2023-11-09 14:29:52 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2023-11-09 14:30:26 +0100 | idgaen | (~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 +0100 | tv | (~tv@user/tv) (Server closed connection) |
2023-11-09 14:46:38 +0100 | tv | (~tv@user/tv) |
2023-11-09 14:47:48 +0100 | yvan-sraka | (sid419690@id-419690.lymington.irccloud.com) (Server closed connection) |
2023-11-09 14:47:56 +0100 | yvan-sraka | (sid419690@id-419690.lymington.irccloud.com) |
2023-11-09 14:53:55 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 264 seconds) |
2023-11-09 14:54:14 +0100 | danso | (~danso@user/danso) (Server closed connection) |
2023-11-09 14:54:30 +0100 | danso | (~danso@user/danso) |
2023-11-09 14:54:43 +0100 | danse-nr3 | (~danse@151.57.105.34) |
2023-11-09 14:57:39 +0100 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 4.1.0) |
2023-11-09 14:59:34 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 255 seconds) |
2023-11-09 15:00:21 +0100 | catilina | (~user@49.235.216.139.sta.wbroadband.net.au) |
2023-11-09 15:00:28 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) |
2023-11-09 15:03:31 +0100 | danse-nr3 | (~danse@151.57.105.34) (Remote host closed the connection) |
2023-11-09 15:03:54 +0100 | danse-nr3 | (~danse@151.57.105.34) |
2023-11-09 15:04:13 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-09 15:05:26 +0100 | edr | (~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 +0100 | acidjnk | (~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 +0100 | jackdk | -> zzz |
2023-11-09 15:23:16 +0100 | thegeekinside | (~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 +0100 | kraftwerk28 | (~kraftwerk@164.92.219.160) (Quit: *disconnects*) |
2023-11-09 15:43:02 +0100 | opus | (~nil@user/opus) (Server closed connection) |
2023-11-09 15:43:33 +0100 | kraftwerk28 | (~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 +0100 | opus | (~nil@user/opus) |
2023-11-09 15:44:35 +0100 | ezzieyguywuf | (~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 +0100 | Guest|67 | (~Guest|67@98.98.49.194) |
2023-11-09 15:50:24 +0100 | Guest|67 | (~Guest|67@98.98.49.194) (Client Quit) |
2023-11-09 15:50:33 +0100 | Teacup | (~teacup@user/teacup) (Server closed connection) |
2023-11-09 15:50:44 +0100 | Teacup | (~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 +0100 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
2023-11-09 16:01:18 +0100 | chomwitt | (~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1) |
2023-11-09 16:04:51 +0100 | fendor_ | (~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 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Ping timeout: 252 seconds) |
2023-11-09 16:05:24 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2023-11-09 16:05:57 +0100 | mechap | (~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 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2023-11-09 16:16:25 +0100 | zaquest | (~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 +0100 | bitdex | (~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 +0100 | waleee | (~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 +0100 | acidjnk | (~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 +0100 | danse-nr3 | did nothing ^^; |
2023-11-09 16:26:04 +0100 | <exarkun> | infinite efficiency, very impressive |
2023-11-09 16:26:05 +0100 | kitzman | (~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 +0100 | misterfish | (~misterfis@37.153.233.129) (Ping timeout: 272 seconds) |
2023-11-09 16:26:44 +0100 | euleritian | (~euleritia@dynamic-046-114-202-140.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-09 16:27:03 +0100 | euleritian | (~euleritia@77.22.252.56) |
2023-11-09 16:30:29 +0100 | alp | (~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 +0100 | ddellacosta | (~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 +0100 | euleritian | (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
2023-11-09 16:43:29 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
2023-11-09 16:43:40 +0100 | <[exa]> | oh commutativity |
2023-11-09 16:43:55 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-09 16:44:09 +0100 | euleritian | (~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 +0100 | absence | (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 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
2023-11-09 16:54:59 +0100 | absence | (torgeihe@hildring.pvv.ntnu.no) |
2023-11-09 16:57:43 +0100 | foul_owl | (~kerry@185.219.141.160) (Read error: Connection reset by peer) |
2023-11-09 17:04:12 +0100 | notzmv | (~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 +0100 | VioletJewel | (violet@user/violetjewel) (Ping timeout: 258 seconds) |
2023-11-09 17:12:39 +0100 | danse-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 +0100 | VioletJewel | (~violet@user/violetjewel) |
2023-11-09 17:13:02 +0100 | danse-nr3 | (~danse@151.57.105.34) |
2023-11-09 17:13:42 +0100 | foul_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 +0100 | pavonia | (~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 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-11-09 17:22:01 +0100 | zetef | (~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 +0100 | blurbox | (~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 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Quit: Leaving) |
2023-11-09 17:26:45 +0100 | sawilagar | (~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 +0100 | shapr | (~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 +0100 | Unicorn_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 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Quit: Leaving) |
2023-11-09 17:34:30 +0100 | <carter> | Chez is pretty redonk |
2023-11-09 17:34:35 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-09 17:34:47 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-11-09 17:38:17 +0100 | deriamis | (deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b) (Server closed connection) |
2023-11-09 17:38:32 +0100 | deriamis | (deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b) |
2023-11-09 17:40:15 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Quit: Leaving) |
2023-11-09 17:40:30 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-09 17:40:50 +0100 | blurbox | (~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 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Client Quit) |
2023-11-09 17:43:19 +0100 | sawilagar | (~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 +0100 | paddymahoney | (~paddymaho@cpe883d24bcf597-cmbc4dfb741f80.cpe.net.cable.rogers.com) (Remote host closed the connection) |
2023-11-09 17:48:53 +0100 | paddymahoney | (~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 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
2023-11-09 17:52:26 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:3c67:344e:72ec:4543) (Remote host closed the connection) |
2023-11-09 17:52:42 +0100 | eggplantade | (~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 +0100 | Pozyomka | (~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 +0100 | CO2 | (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 +0100 | CO2 | (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 +0100 | tzh | (~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 +0100 | CO2 | (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 +0100 | Pozyomka | (~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 +0100 | machinedgod | (~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 +0100 | nate3 | (~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 +0100 | nate3 | (~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 +0100 | tromp | (~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 +0100 | Cale | (~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 +0100 | kuribas | (~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 +0100 | drewjose | (~drewjose@129.154.40.88) |
2023-11-09 18:39:37 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-09 18:40:27 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-09 18:42:08 +0100 | dsrt^ | (~cd@76.145.193.217) (Remote host closed the connection) |
2023-11-09 18:45:53 +0100 | idgaen | (~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 +0100 | tromp | (~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 +0100 | fendor_ | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection) |
2023-11-09 18:56:19 +0100 | danse-nr3 | (~danse@151.57.105.34) (Ping timeout: 258 seconds) |
2023-11-09 18:56:29 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) |
2023-11-09 18:56:40 +0100 | danse-nr3 | (~danse@151.57.123.82) |
2023-11-09 19:00:19 +0100 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 255 seconds) |
2023-11-09 19:00:22 +0100 | vgtw_ | (~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 +0100 | qqq | (~qqq@92.43.167.61) |
2023-11-09 19:08:32 +0100 | Lycurgus | (~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 +0100 | jludwig | (~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 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2023-11-09 19:27:17 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
2023-11-09 19:27:23 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
2023-11-09 19:27:34 +0100 | __monty__ | (~toonn@user/toonn) |
2023-11-09 19:27:52 +0100 | Guest45 | (~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 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-09 19:32:33 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2023-11-09 19:33:42 +0100 | motherfsck | (~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 +0100 | shapr | (~user@2600:1700:c640:3100:9af4:b6dd:227b:75bc) |
2023-11-09 19:42:56 +0100 | Guest45 | (~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 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 260 seconds) |
2023-11-09 20:03:31 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-11-09 20:04:13 +0100 | danse-nr3 | (~danse@151.57.123.82) (Ping timeout: 255 seconds) |
2023-11-09 20:07:11 +0100 | danse-nr3 | (~danse@151.57.123.82) |
2023-11-09 20:11:24 +0100 | alp | (~alp@static-176-175-7-165.ftth.abo.bbox.fr) |
2023-11-09 20:14:57 +0100 | Vajb | (~Vajb@mobile-access-2e8444-121.dhcp.inet.fi) |
2023-11-09 20:19:40 +0100 | danse-nr3 | (~danse@151.57.123.82) (Ping timeout: 272 seconds) |
2023-11-09 20:31:57 +0100 | infinity0 | (~infinity0@pwned.gg) (Remote host closed the connection) |
2023-11-09 20:33:52 +0100 | infinity0 | (~infinity0@pwned.gg) |
2023-11-09 20:34:34 +0100 | zetef | (~quassel@95.77.17.251) |
2023-11-09 20:37:22 +0100 | infinity0_ | (~infinity0@pwned.gg) |
2023-11-09 20:37:22 +0100 | infinity0 | Guest605 |
2023-11-09 20:37:22 +0100 | infinity0_ | infinity0 |
2023-11-09 20:38:15 +0100 | Guest605 | (~infinity0@pwned.gg) (Ping timeout: 240 seconds) |
2023-11-09 20:39:01 +0100 | zetef | (~quassel@95.77.17.251) (Ping timeout: 240 seconds) |
2023-11-09 20:39:54 +0100 | lortabac | (~lorenzo@2a01:e0a:541:b8f0:cf92:a8ae:a9da:4f45) (Quit: WeeChat 3.5) |
2023-11-09 20:44:58 +0100 | danza | (~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 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
2023-11-09 20:55:44 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-11-09 20:56:43 +0100 | neceve | (~neceve@user/neceve) |
2023-11-09 20:56:52 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2023-11-09 20:56:56 +0100 | Pickchea | (~private@user/pickchea) |
2023-11-09 20:59:08 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Client Quit) |
2023-11-09 20:59:20 +0100 | zer0bitz_ | (~zer0bitz@user/zer0bitz) |
2023-11-09 21:03:13 +0100 | zer0bitz | (~zer0bitz@user/zer0bitz) (Ping timeout: 260 seconds) |
2023-11-09 21:09:09 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2023-11-09 21:09:28 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2023-11-09 21:14:43 +0100 | jinsun | Guest2321 |
2023-11-09 21:14:43 +0100 | jinsun_ | (~jinsun@user/jinsun) |
2023-11-09 21:14:43 +0100 | Guest2321 | (~jinsun@user/jinsun) (Killed (tungsten.libera.chat (Nickname regained by services))) |
2023-11-09 21:14:43 +0100 | jinsun_ | jinsun |
2023-11-09 21:16:05 +0100 | danza | (~francesco@151.57.123.82) (Ping timeout: 252 seconds) |
2023-11-09 21:17:10 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
2023-11-09 21:19:06 +0100 | ft | (~ft@p4fc2a529.dip0.t-ipconnect.de) |
2023-11-09 21:23:22 +0100 | vulpine | (xfnw@tilde.team) (Quit: Connection reset by purr) |
2023-11-09 21:28:39 +0100 | vulpine | (xfnw@tilde.team) |
2023-11-09 21:31:57 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-09 21:34:12 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
2023-11-09 21:36:04 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) |
2023-11-09 21:37:19 +0100 | alp | (~alp@static-176-175-7-165.ftth.abo.bbox.fr) (Ping timeout: 258 seconds) |
2023-11-09 21:40:00 +0100 | jinsun_ | (~jinsun@user/jinsun) |
2023-11-09 21:40:00 +0100 | jinsun | Guest3991 |
2023-11-09 21:40:01 +0100 | Guest3991 | (~jinsun@user/jinsun) (Killed (cadmium.libera.chat (Nickname regained by services))) |
2023-11-09 21:40:01 +0100 | jinsun_ | jinsun |
2023-11-09 21:43:23 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2023-11-09 21:43:54 +0100 | ddellacosta | (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 272 seconds) |
2023-11-09 21:44:21 +0100 | califax | (~califax@user/califx) |
2023-11-09 21:44:44 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-11-09 21:45:58 +0100 | buhman | (sid411355@user/buhman) (Server closed connection) |
2023-11-09 21:46:14 +0100 | buhman | (sid411355@user/buhman) |
2023-11-09 21:49:39 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
2023-11-09 21:51:58 +0100 | michalz | (~michalz@185.246.207.197) (Remote host closed the connection) |
2023-11-09 21:53:31 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-09 21:56:16 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
2023-11-09 21:58:14 +0100 | jappiejappie | (~jappiejap@186-011-158-163.dynamic.caiway.nl) |
2023-11-09 22:03:41 +0100 | kaol | (~kaol@94-237-42-30.nl-ams1.upcloud.host) (Server closed connection) |
2023-11-09 22:03:48 +0100 | kaol | (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
2023-11-09 22:07:24 +0100 | coot | (~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 +0100 | machinedgod | (~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 +0100 | ubert1 | (~Thunderbi@178.165.207.175.wireless.dyn.drei.com) |
2023-11-09 22:20:05 +0100 | ubert | (~Thunderbi@178.165.181.20.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
2023-11-09 22:20:05 +0100 | ubert1 | ubert |
2023-11-09 22:21:42 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-09 22:24:48 +0100 | glassribbon | (~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 +0100 | glassribbon | (~glassribb@187.19.131.51) () |
2023-11-09 22:26:21 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-11-09 22:31:04 +0100 | thegman_ | (~thegman@072-239-207-086.res.spectrum.com) |
2023-11-09 22:31:40 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Read error: Connection reset by peer) |
2023-11-09 22:31:54 +0100 | thegman_ | thegman |
2023-11-09 22:33:00 +0100 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
2023-11-09 22:33:14 +0100 | dsrt^ | (~cd@76.145.193.217) |
2023-11-09 22:36:46 +0100 | neceve | (~neceve@user/neceve) (Ping timeout: 255 seconds) |
2023-11-09 22:41:29 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving) |
2023-11-09 22:42:50 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) |
2023-11-09 22:49:21 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2023-11-09 22:49:55 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2023-11-09 22:50:55 +0100 | chomwitt | (~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1) (Ping timeout: 264 seconds) |
2023-11-09 22:51:17 +0100 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
2023-11-09 22:51:35 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-11-09 23:05:05 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
2023-11-09 23:10:17 +0100 | acidjnk | (~acidjnk@p200300d6e72b9321b052fa9090e40cc7.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2023-11-09 23:11:51 +0100 | nicole | (ilbelkyr@libera/staff/ilbelkyr) (*.net *.split) |
2023-11-09 23:11:55 +0100 | nicole | (ilbelkyr@libera/staff/ilbelkyr) |
2023-11-09 23:19:08 +0100 | pavonia | (~user@user/siracusa) |
2023-11-09 23:27:43 +0100 | Vajb | (~Vajb@mobile-access-2e8444-121.dhcp.inet.fi) (Ping timeout: 258 seconds) |
2023-11-09 23:28:31 +0100 | Vajb | (~Vajb@2001:999:785:c11e:a1b8:59fa:dee7:e490) |
2023-11-09 23:29:36 +0100 | alp | (~alp@2001:861:5e02:eff0:c5b5:b1c1:9abe:83f8) |
2023-11-09 23:36:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-09 23:38:15 +0100 | wroathe | (~wroathe@50.205.197.50) |
2023-11-09 23:38:15 +0100 | wroathe | (~wroathe@50.205.197.50) (Changing host) |
2023-11-09 23:38:15 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-11-09 23:43:08 +0100 | alp | (~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 +0100 | FinnElija | (~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 +0100 | FinnElija | (~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 +0100 | zer0bitz_ | (~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 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 272 seconds) |