Logs: freenode/#haskell
| 2021-03-12 22:30:37 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:1715:de72:a1c7:dcd1) (Ping timeout: 272 seconds) |
| 2021-03-12 22:32:49 | <wz1000> | dmj`: I was finally able to defeat the demand analyser using `f = foldl (\ (!x,!y) n -> (x + n, y + 1)) (0,0); avg = uncurry (/) . f` |
| 2021-03-12 22:33:00 | <wz1000> | no amount of optimisation could fix that |
| 2021-03-12 22:33:29 | <wz1000> | inlining the f doesn't sort of arcane magic I haven't been able to figure out |
| 2021-03-12 22:33:34 | <wz1000> | *does |
| 2021-03-12 22:33:40 | <dmj`> | wz1000: this ooms? |
| 2021-03-12 22:33:43 | <wz1000> | yes |
| 2021-03-12 22:33:56 | → | cfvnhtsp^ joins (cfvnhtsp@ip98-184-89-2.mc.at.cox.net) |
| 2021-03-12 22:34:21 | <monochrom> | That's very strange. |
| 2021-03-12 22:35:10 | <Gurkenglas> | mwahaha when your line starts with "let ~(Left l)=x; ~(Right r)=x;" |
| 2021-03-12 22:35:15 | <dmj`> | wz1000: are you positive, can you check your code and ensure it's ooming w/ the bangs present |
| 2021-03-12 22:35:22 | <wz1000> | dmj`: yes |
| 2021-03-12 22:36:13 | <wz1000> | dmj`: only if you call avg from another module though |
| 2021-03-12 22:36:37 | <monochrom> | Is this []'s foldl? |
| 2021-03-12 22:36:44 | <wz1000> | Or you can use {-# NOINLINE avg #-} |
| 2021-03-12 22:36:46 | <wz1000> | yes |
| 2021-03-12 22:36:46 | <dmj`> | wz1000: ah, okay. Can you confirm that foldl' still OOMs it? |
| 2021-03-12 22:37:21 | <wz1000> | dmj`: no OOM with foldl' |
| 2021-03-12 22:37:51 | → | spoonm joins (~spoonm@tokyo.spoonm.org) |
| 2021-03-12 22:38:05 | × | redmp_ quits (~redmp@172.58.30.247) (Quit: leaving) |
| 2021-03-12 22:38:21 | <dmj`> | That doesn't really make too much sense to me tbh then. The foldl vs. foldl' shouldn't really matter as long as you're strictly pattern matching on the tuple and forcing the Double inside. The foldl' is just going to force the tuple to WHNF and that's not where the thunk accumulation is happening anyways (rather its inside the tuple). |
| 2021-03-12 22:38:26 | <monochrom> | Oh nevermind, s/foldl/foldl'/ is O(1) space, foldl is meant to be linear space. |
| 2021-03-12 22:38:26 | <monochrom> | foldl op z (x:xs) = foldl (op z x) xs see how it doesn't even care how strict op is. |
| 2021-03-12 22:38:51 | <wz1000> | yeah |
| 2021-03-12 22:39:12 | <wz1000> | but the demand analyser is able to figure it out and rewrite it to foldl' if you inline f |
| 2021-03-12 22:39:13 | <monochrom> | But if you can get f to inline, probably some rewrite rule changes foldl to something else entirely. |
| 2021-03-12 22:39:38 | <Gurkenglas> | Aww only one @ per pattern? |
| 2021-03-12 22:39:58 | <dmj`> | wz1000: how do you explain the oom if you're banging the Doubles, what's not getting forced? |
| 2021-03-12 22:40:06 | <Gurkenglas> | I wanted to write x@~(Left l)@~(Right r) but it only works without the x@ |
| 2021-03-12 22:40:22 | <wz1000> | dmj`: the result of the lambda is not getting forced |
| 2021-03-12 22:40:53 | × | myShoggoth quits (~myShoggot@75.164.81.55) (Ping timeout: 245 seconds) |
| 2021-03-12 22:40:56 | <dmj`> | wz1000: ah, I see. That makes sense. Sweet. |
| 2021-03-12 22:41:00 | × | Psybur quits (~user@unaffiliated/psybur) (Remote host closed the connection) |
| 2021-03-12 22:41:04 | <monochrom> | :) |
| 2021-03-12 22:41:16 | <wz1000> | dmj`: this is also why foldl (+) leaks |
| 2021-03-12 22:41:25 | <wz1000> | since (+) is also strict |
| 2021-03-12 22:41:31 | <wz1000> | like your lambda |
| 2021-03-12 22:41:47 | → | myShoggoth joins (~myShoggot@75.164.81.55) |
| 2021-03-12 22:41:48 | <wz1000> | so the strictness of the function doesn't matter |
| 2021-03-12 22:43:56 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-12 22:44:00 | <shapr> | Hm, looks like debian/buster has libffi7 but not libffi6, so ghcup doesn't install ghc for me |
| 2021-03-12 22:44:12 | <dmj`> | so the foldl' is ensuring in this case the result of the lambda is being forced during the fold's recursion, otherwise the expression just builds up. The tuple has to be forced. |
| 2021-03-12 22:44:42 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 268 seconds) |
| 2021-03-12 22:45:24 | <wz1000> | monochrom: I'm pretty sure its not a rewrite rule, -ddump-rule-rewrites shows nothing interesting: http://78.47.113.11/rules |
| 2021-03-12 22:45:32 | <wz1000> | it is the demand analyser |
| 2021-03-12 22:45:45 | <wz1000> | since uncurry is strict in its second argument |
| 2021-03-12 22:45:48 | <wz1000> | I think |
| 2021-03-12 22:46:15 | <dmj`> | @src uncurry |
| 2021-03-12 22:46:15 | <lambdabot> | uncurry f p = f (fst p) (snd p) |
| 2021-03-12 22:46:21 | <wz1000> | oh, its not |
| 2021-03-12 22:47:01 | <wz1000> | some other magic going on |
| 2021-03-12 22:47:06 | <wz1000> | I still don't understand this |
| 2021-03-12 22:47:08 | × | jespada quits (~jespada@90.254.243.187) (Ping timeout: 245 seconds) |
| 2021-03-12 22:47:33 | <wz1000> | yes, `uncurry' f ~(a,b) = f a b` still doesn't oom if f is inlined |
| 2021-03-12 22:48:22 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 2021-03-12 22:49:09 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 264 seconds) |
| 2021-03-12 22:50:03 | <Gurkenglas> | Has anyone proven that for x less defined than y, every finest-grained sequence of steps to make x as defined as y has the same length? |
| 2021-03-12 22:50:43 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 2021-03-12 22:50:53 | → | jespada joins (~jespada@90.254.243.187) |
| 2021-03-12 22:51:01 | <wz1000> | as usual, GHC is simulataneously smarter and dumber than I expect |
| 2021-03-12 22:52:19 | <monochrom> | Can x be made as defined as y at all? |
| 2021-03-12 22:52:34 | <wz1000> | maybe this would be easier to understand if I learned how to read the demand signatures |
| 2021-03-12 22:52:51 | <monochrom> | More meta-ly I'm afraid the question mixes up denotational semantics and operational semantics. |
| 2021-03-12 22:52:59 | <Gurkenglas> | monochrom, what i mean is that every finest-grained chain of values, each of which is more defined than the last, with the same start and end has the same length |
| 2021-03-12 22:54:00 | → | ezrakilty joins (~ezrakilty@75-172-115-167.tukw.qwest.net) |
| 2021-03-12 22:54:06 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-12 22:54:10 | <monochrom> | "() : bottom" can be refined to "() : []" but also to "() : () : () : []". They have different heights. |
| 2021-03-12 22:54:29 | <Gurkenglas> | yea but ():[] is not the same as ():():():[] |
| 2021-03-12 22:54:49 | <Gurkenglas> | (bottom,bottom) can be made into ((),()) in two ways, both of length 2 |
| 2021-03-12 22:55:14 | <monochrom> | If you know ():bottom is detined to be only () : () : () : [], then there is only one chain. |
| 2021-03-12 22:55:23 | <monochrom> | Oh, that. |
| 2021-03-12 22:56:12 | <Gurkenglas> | no, there's one through ():bottom:():[] and one through ():():bottom:[] |
| 2021-03-12 22:56:49 | <monochrom> | Yeah sorry. |
| 2021-03-12 22:57:00 | × | fendor_ quits (~fendor@178.115.131.242.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2021-03-12 22:58:25 | → | j joins (jess@freenode/staff/jess) |
| 2021-03-12 22:58:34 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-101-29.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-03-12 22:58:46 | × | ezrakilty quits (~ezrakilty@75-172-115-167.tukw.qwest.net) (Ping timeout: 276 seconds) |
| 2021-03-12 22:58:56 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-101-29.w86-212.abo.wanadoo.fr) |
| 2021-03-12 22:58:57 | <monochrom> | ooooo interesting, I'm sure it's true, but I have no idea how to prove it |
| 2021-03-12 23:01:57 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:b401:41f7:a4d0:94d7) (Remote host closed the connection) |
| 2021-03-12 23:03:13 | j | is now known as jess |
| 2021-03-12 23:03:48 | × | myShoggoth quits (~myShoggot@75.164.81.55) (Ping timeout: 245 seconds) |
| 2021-03-12 23:04:44 | <dmj`> | wz1000: maybe GHC has savant syndrome |
| 2021-03-12 23:04:45 | × | bergey` quits (~user@107.181.19.30) (Ping timeout: 264 seconds) |
| 2021-03-12 23:06:34 | × | pera quits (~pera@unaffiliated/pera) (Ping timeout: 276 seconds) |
| 2021-03-12 23:06:51 | → | pera joins (~pera@unaffiliated/pera) |
| 2021-03-12 23:06:54 | × | coot quits (~coot@37.30.55.141.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-03-12 23:07:15 | <infinisil> | monochrom: That worked really well in fact! |
| 2021-03-12 23:07:40 | <monochrom> | :) |
| 2021-03-12 23:07:41 | <infinisil> | Other than passing the recursion depth around, I only needed to change the K1 implementation |
| 2021-03-12 23:09:19 | × | forgottenone quits (~forgotten@176.42.24.172) (Quit: Konversation terminated!) |
| 2021-03-12 23:09:31 | <monochrom> | Gurkenglas: I think I know how to prove it. E.g., "4 : (5 : [])" is a tree of 5 nodes. Do structural induction on such trees, or natural number strong induction on the number of nodes. |
| 2021-03-12 23:09:38 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:5883:2b2b:203d:3c57) |
| 2021-03-12 23:10:07 | <Gurkenglas> | monochrom, function types can have inf nodes |
| 2021-03-12 23:11:03 | <infinisil> | Actually infinite lists can't be printed yet, those need special handling |
| 2021-03-12 23:11:33 | → | mouseghost joins (~draco@87-206-9-185.dynamic.chello.pl) |
| 2021-03-12 23:11:33 | × | mouseghost quits (~draco@87-206-9-185.dynamic.chello.pl) (Changing host) |
| 2021-03-12 23:11:33 | → | mouseghost joins (~draco@wikipedia/desperek) |
| 2021-03-12 23:11:42 | <Gurkenglas> | (function |
| 2021-03-12 23:11:48 | <Gurkenglas> | s can have inf nodes, i should say) |
All times are in UTC.