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

more notes on linearity

# Linearity Patent nonsense

```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.