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