wiki:Commentary/Compiler/StrictnessAnalysis/KirstenNotes

Version 9 (modified by kirsten, 7 years ago) (diff)

elaboration

Linearity

The solution is to distinguish call demands from product demands. Consider again:

let f = \ x. \ y. ... in
  ...(f 1 2)...(f 3 4)...

The demands placed on f by the first and second call get bothed together to yield SM(SM(T)). But this is incorrect. Consider:

let f = \ x. \ y. ... 
    frob = f 1 in
  ...(f 1 2)...(frob 2)...(frob 3)...

Here, the demands placed on f by the body of frob and by the call to f in the let-body get bothed together: S1(T) & S1(S1(T)) = SM(SM(T)). Note that this is the same as the demand placed on f above, yet we want to distinguish between the two situations, because in the first example, the inner lambda in f's rhs is only called once.

The solution is to treat call demands and product demands differently, and to define the both function for call demands to have the same behavior as lub. Then in the first example, f has demand SM(S1(T)) placed on it, and in the second, SM(T). This is what we want; now, if f has demand D(D(T) placed on it, that implies f is always called with two arguments.

Why does this make sense? Consider what it means if we see an example like:

let baz = lazyF p in
  case p of
    (a,b) -> strictF a b

(where lazyF is lazy in p, and strictF is strict in a and b). p is used both with demand L (in the call to lazyF and with demand S(SS) (in the call to strictF). This means it's perfectly same to strictly evaluate p, so when we both together the two demands, we should get S(SS). On the other hand, if a function is called once with one argument and once with two, we don't want to treat it as a function that's always called with two arguments; we're only interested in functions that are always called with n arguments for a given n. Hence, both should behave the same way as lub for call demands.