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