wiki:Commentary/Compiler/StrictnessAnalysis/KirstenNotes

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

more notes on linearity

Linearity Patent nonsense

Instead of:

type DmdEnv = VarEnv Demand

we want:

type DmdEnv = Env CoreExpr Demand

We keep track of demands on partial applications.

After calling dmd_anal on the body of a let, which results in demand type dmd_ty with demand env dmd_env, we do the following for each let-bound variable f:

  1. Iterate through all the keys in dmd_env, finding all applications of f to n arguments.
  2. For each i from 1 through n (where n is f's arity), if each of the applications of f to i arguments has usage demand OneOrZero, then it's safe to mark the corresponding lambda-expression as a one-shot lambda.

This might work, but is kind of kludgy.

This may be way too unnecessarily complicated. Can't we just get the same information from the demand on f in the free-var environment of the let body as it is, without changing the environment?

suppose the demand on f is

S1K(S1K(LMX))

if f =

(\ x. (\ y. ...))

then we can mark the outer two lambdas as being one-shot. Right?

Not exactly. Suppose:

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

f will have demand on it:

SMK(SMK(LMX))

because it's called more than once. We really want the demand to reflect that (f 1) is called only once and (f 3) is called only once, but it doesn't. So it doesn't seem like we can figure out what we need to know just by looking at the demand on f.

Linearity =

The real 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.