Note [Demand signatures semantically]
Demand analysis interprets expressions in the abstract domain of demand
transformers. Given a (sub-)demand that denotes the evaluation context, the
abstract transformer of an expression gives us back a demand type denoting
how other things (like arguments and free vars) were used when the expression
was evaluated. Here's an example:
f x y =
if x + expensive
then \z -> z + y * ...
else \z -> z * ...
The abstract transformer (let's call it F_e) of the if expression (let's
call it e) would transform an incoming (undersaturated!) head sub-demand A
into a demand type like {x-><1L>,y-><L>}<L>. In pictures:
SubDemand ---F_e---> DmdType
<A> {x-><1L>,y-><L>}<L>
Let's assume that the demand transformers we compute for an expression are
correct wrt. to some concrete semantics for Core. How do demand signatures fit
in? They are strange beasts, given that they come with strict rules when to
it's sound to unleash them.
Fortunately, we can formalise the rules with Galois connections. Consider
f's strictness signature, {}<1L><L>. It's a single-point approximation of
the actual abstract transformer of f's RHS for arity 2. So, what happens is that
we abstract *once more* from the abstract domain we already are in, replacing
the incoming Demand by a simple lattice with two elements denoting incoming
arity: A_2 = {<2, >=2} (where '<2' is the top element and >=2 the bottom
element). Here's the diagram:
A_2 -----f_f----> DmdType
^ |
| α γ |
| v
SubDemand --F_f----> DmdType
With
α(C(1,C(1,_))) = >=2
α(_) = <2
γ(ty) = ty
and F_f being the abstract transformer of f's RHS and f_f being the abstracted
abstract transformer computable from our demand signature simply by
f_f(>=2) = {}<1L><L>
f_f(<2) = multDmdType C_0N {}<1L><L>
where multDmdType makes a proper top element out of the given demand type.
In practice, the A_n domain is not just a simple Bool, but a Card, which is
exactly the Card with which we have to multDmdType. The Card for arity n
is computed by calling @peelManyCalls n@, which corresponds to α above. References 0
This Note does not link to any other.
Referenced by 1
- DmdSig: demand signatures, and demand-sig arity GHC.Types.Demand