DmdAnal: Cardinalitites in nested product demands should apply relatively
This ticket is about persuading the reader that cardinalities in nested product demands should apply relatively rather than absolutely. Let's first clear up
Definitions
Relative
Let's first look at how cardinalities in call demands work. For example, the usage demand C(C1(U))
denotes a term that is called multiple times, and whenever we call it, we call the resulting application at most once with a second argument. This is useful information, because it allows us to eta-expand from arity 1 to arity 2. The inner 1
of the call demand applies relative to the outer many-call demand: Although the inner lambda will be entered multiple times, it will be entered at most as often as the outer lambda.
In general, relative cardinality means that the cardinality (0, 1, omega) applies relative to exactly one evaluation of the surrounding expression.
Absolute
The field demands of product demands on the other hand carry absolute cardinalities. If (x, y)
is used according to U(1*U, 1*U)
, that means the pair may be used many times (we always omit the omega*
prefix on the outer U), but its components are only used once. If there are no other uses of x
and y
, this means the bindings of x
and y
are single-entry and we can omit update frames. But clearly, the inner evaluation cardinalities 1
are certainly not relative to one evaluation of the pair, but relative to all evaluations of the (x,y)
expression, e.g. absolute.
What if call demands were absolute
If we have code like ... f x y ... f a b ...
with two calls to f
of arity 2, we'd no longer give f
the demand C(C1(U))
, but C(C(U))
, because the inner lambda was entered twice in absolute numbers. I can't think of any scenario the resulting annotations would be useful in, certainly we'd lose the ability to eta-expand f
above. It's just a worthless denotation.
What if product demands were relative
What we lose
We'd lose used-once information in some cases, like
g p 0 = 0
g p y = fst p + snd p + y
In absolute terms, g
places a demand of U(1*U,1*U)
on its first argument: Both fst
and snd
evaluate the pair, but they evaluate disjoint components. At call sites of g
, we could use call-by-name for the components (but not the pair).
In relative terms, g
also places a demand of U(1*U,1*U)
on its first argument. But this demand has different semantics: It says "the pair constructor might be evaluated multiple times, but whenever it is evaluated, the components of the pair are used at most once". This is not enough to use call-by-name for the pair components, as can be seen by considering the following function that places the exact same demand on its first argument:
h p 0 = 0
h p y = fst p + fst p + snd p + snd p
The same narrative holds: "the pair constructor might be evaluated multiple times, but whenever it is evaluated, the components of the pair are used at most once". But in absolute terms, the components will be evaluated multiple times.
In practice, that means we have to multiply all field cardinalities (1
) by the outer cardinality (omega
) when analysis enters the product components.
What we gain
Symmetry to call demands, for starters.
Also the post-processing/reusing family of functions can be simplified, as they don't need to recurse through the entire demand structure with relative cardinalities. It suffices to update the outer cardinality.
The last and hopefully most convincing reason is strictness information. Currently, strictness demands stop whenever we have one Lazy
in there. But nothing actually stops us from going deeper; example
let x = (expensive 3, blah)
in if b then fst x else 0
Although x
is used lazily, whenever its outer pair is evaluated, its first component is also evaluated strictly! That amounts to (relative!) strictness L(SL)
and would allow us to transform to
let x = case expensive 3 of y -> (y, blah)
in if b then fst x else 0
which gets rid of a closure.
Summary
I propose to switch from absolute to relative cardinalities in nested product demands.
Cons:
- We lose some usage information, to the point where product usage (at least the 1 vs. many distinction) becomes quite useless. It's unclear how much that deteriorates performance.
Pros:
- Symmetry with call demands
- Generally simpler (and marginally faster) analysis code, I think
- Symmetry with nested strictness demands as proposed above.
An alternative that eschews the symmetry aspects would simply be to have relative product strictness, but absolute product usage. I think that will lead to quite hairy code in some cases and a ultimately a maintenance burden. Still, that option is also on the table.