Version 9 (modified by kirsten, 11 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.