DmdAnal: Interleaved demand representation for expressive strictness information
Currently, we store strictness and usage demands independently of another in a JointDmd
, which is basically a pair. It turns out that makes it impossible to express useful strictness demands. Here's an example:
h :: Int -> Int
h m =
let g :: Int -> (Int,Int)
g 1 = (m, 0)
g n = (2 * n, 2 `div` n)
{-# NOINLINE g #-}
in case m of
1 -> 0
2 -> snd (g m)
_ -> uncurry (+) (g m)
What is the demand on g
? Currently, we say <L,1*C1(U(1*U(U),1*U(U)))>
. Note that we have pretty precise usage demand, but the strictness demand is completely uninformative since g
is not called strictly.
But we can still have useful strictness information under the assumption that g
is called (see why that's useful below)! Here, we can see that whenever g
is called, then we evaluate the second component of the returned pair strictly. If we interleaved both demands, we could write [0,1]*C[0,1](([0,1]([0,n]),[1,1]([0,n])))
(notation is up for debate): Each [l,u]
denotes an evaluation cardinality, consisting of a lower (strictness) bound l
(ranging over {0,1}) and an upper (usage) bound u
(ranging over {0,1,n}, n meaning many times).
Note how we expressed that g
was called at most once (possibly never, lower bound 0), and that in all such evaluation contexts we evaluate the first pair component exactly once ([1,1]
).
Why is this useful
The information on g
is useful for Nested CPR (!1866 (closed)), as this allows us to safely also unbox the second pair component in the returned pair, even though evaluation of 2 / n
might not terminate on some inputs.
Similarly, we can have nested strictness on products to omit some thunks, e.g.
let x = (expensive 3, blah)
in if b then fst x else 0
If we give x
strictness demand L(S,L)
, then we can transform to
let x = case expensive 3 of y -> (y, blah)
in if b then fst x else 0
But that requires us to resolve #18885 (closed) first.