'lub' and 'both' on strictness - what does it mean for products to have different arity?
Ömer Sinan Ağacan
omeragacan at gmail.com
Fri Mar 4 14:26:22 UTC 2016
Simon, your GADT example clearly shows how lub sometimes needs to handle
products with different arities, but the case with bothDmd is still confuses
me. I think we need have a code like this:
f x + g x
Where f puts a S(SS) demand on x and g puts a S(SSS). This looks like a
bug/type error to me. Do you have any example for bothDmd too?
(I started D1968 for documenting these)
2016-03-02 3:47 GMT-05:00 Simon Peyton Jones <simonpj at microsoft.com>:
>
> | -- lubUse (UProd {}) Used = Used
> | lubUse (UProd ux) Used = UProd (map (`lubArgUse`
> | useTop) ux)
> | lubUse Used (UProd ux) = UProd (map (`lubArgUse`
> | useTop) ux)
> |
> | And then somewhere around that code there's this:
> |
> | Note [Used should win]
> | ~~~~~~~~~~~~~~~~~~~~~~
> | Both in lubUse and bothUse we want (Used `both` UProd us) to be
> | Used.
> | Why? Because Used carries the implication the whole thing is used,
> | box and all, so we don't want to w/w it. If we use it both boxed
> | and
> | unboxed, then we are definitely using the box, and so we are quite
> | likely to pay a reboxing cost. So we make Used win here.
> |
> | ...
> |
> | It seems like at some point the note was valid, but now the code seems
> | to be doing the opposite. Any ideas which one needs an update?
>
> I have no idea. It seems that the entire definition of lubUse, including the Note and the commented-out line, appeared in a single big patch 99d4e5b4. So no clues there.
>
> However the Note has some nofib numbers.
>
> So yes, it's puzzling. The argument in the Note seems plausible. Would you like to try reverting to "Used should win" and see what happens to performance? Probably something will get worse and you'll have do some digging with ticky-ticky.
>
>
> | I'm also a bit confused about why both and lub are not commutative, or
> | if they're commutative, why do they have redundant cases.
>
> Yes: lub and both should be commutative; yell if not. (In contrast see Note [Asymmetry of 'both' for DmdType and DmdResult]; but that's well documented.)
>
> | For example,
> | lubUse has
> | this:
> |
> | lubUse UHead u = u
> | lubUse (UCall c u) UHead = UCall c u
> |
> | instead of something like:
> |
> | lubUse UHead u = u
> | lubUse u UHead = u
>
> I think this is just stylistic. I was dealing with all the cases for UHead in the first arg, then all the cases for UCall, and so on. That way I know I've got coverage.
>
> (And perhaps it's more efficient: we pattern match at most once on each argument.
>
> Simon
>
> |
> | I didn't check all the cases to see if it's really commutative or not,
> | but can I assume that they need to be commutative and simplify the
> | code? Otherwise let's add a note about why they're not commutative?
> |
> | Thanks..
> |
> | 2016-03-02 1:07 GMT-05:00 Ömer Sinan Ağacan <omeragacan at gmail.com>:
> | >> Could I ask that you add this example as a Note to the relevant
> | >> functions, so that the next time someone asks this question they'll
> | >> find the answer right there?
> | >
> | > Yep, I'll do that soon.
> | >
> | > 2016-03-01 12:01 GMT-05:00 Simon Peyton Jones
> | <simonpj at microsoft.com>:
> | >> Omer
> | >>
> | >> Joachim is right. The strictness analyser just looks inside casts,
> | >> so these unexpectedly ill-typed cases could show up. For example
> | >>
> | >> f :: T a -> a -> Int
> | >> f x y = case x of
> | >> P1 -> case y of (a,b,c) -> a+b+c
> | >> P2 -> case y of (p,q) -> p+q
> | >>
> | >> data T a where
> | >> P1 :: T (Int,Int,Int)
> | >> P2 :: T (Int,Int)
> | >>
> | >> In the P1 branch we have that y::(Int,Int,Int), so we'll get a
> | demand S(SSS). And similarly in the P2 branch. Now we combine them.
> | And there you have it.
> | >>
> | >>
> | >> Could I ask that you add this example as a Note to the relevant
> | functions, so that the next time someone asks this question they'll
> | find the answer right there?
> | >>
> | >> Thanks
> | >>
> | >> Simon
> | >>
> | >> | -----Original Message-----
> | >> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
> | >> | Ömer Sinan Agacan
> | >> | Sent: 19 February 2016 17:27
> | >> | To: ghc-devs <ghc-devs at haskell.org>
> | >> | Subject: 'lub' and 'both' on strictness - what does it mean for
> | >> | products to have different arity?
> | >> |
> | >> | I was looking at implementations of LUB and AND on demand
> | >> | signatures and I found this interesting case:
> | >> |
> | >> | lubStr (SProd s1) (SProd s2)
> | >> | | length s1 == length s2 = mkSProd (zipWith lubArgStr
> | s1 s2)
> | >> | | otherwise = HeadStr
> | >> |
> | >> | The "otherwise" case is interesting, I'd expect that to be an
> | error.
> | >> | I'm trying to come up with an example, let's say I have a case
> | >> | expression:
> | >> |
> | >> | case x of
> | >> | P1 -> RHS1
> | >> | P2 -> RHS2
> | >> |
> | >> | and y is used in RHS1 with S(SS) and in RHS2 with S(SSS). This
> | >> | seems to me like a type error leaked into the demand analysis.
> | >> |
> | >> | Same thing applies to `bothDmd` too. Funnily, it has this extra
> | >> | comment on this same code:
> | >> |
> | >> | bothStr (SProd s1) (SProd s2)
> | >> | | length s1 == length s2 = mkSProd (zipWith bothArgStr
> | s1 s2)
> | >> | | otherwise = HyperStr -- Weird
> | >> |
> | >> | Does "Weird" here means "type error and/or bug" ?
> | >> |
> | >> | Should I try replacing these cases with panics and try to
> | validate?
> | >> | _______________________________________________
> | >> | ghc-devs mailing list
> | >> | ghc-devs at haskell.org
> | >> |
> | >> |
> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmai
> | >> | l.ha
> | >> | skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | >> |
> | >> |
> | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd8ae326a8e1
> | >> | 4ef8
> | >> |
> | 9e8608d339520cb9%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=sRFRK
> | >> | gj3y zQdEZT4y7KLk18cP43Rv1J%2bx8oPZyr1QzA%3d
More information about the ghc-devs
mailing list