Version 9 (modified by kirsten, 9 years ago) (diff) |
---|

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