|
|
# Original Idea
|
|
|
# Making LetUp more precise
|
|
|
|
|
|
|
|
|
The [demand analyser](commentary/compiler/demand) uses two different rules for handling let bindings, as explained in the [ cardinality paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2014/01/cardinality-popl14.pdf). TLDR:
|
... | ... | @@ -10,7 +10,7 @@ The [demand analyser](commentary/compiler/demand) uses two different rules for h |
|
|
There are reasons why we currently need both rules ([ cardinality paper §3.5 and §3.6](https://www.microsoft.com/en-us/research/wp-content/uploads/2014/01/cardinality-popl14.pdf)), although the general approach of **LetDown** is more flow-sensitive and thus strictly more precise than **LetUp**.
|
|
|
|
|
|
|
|
|
Consider the following example:
|
|
|
Consider the following running example:
|
|
|
|
|
|
```wiki
|
|
|
let y = ...
|
... | ... | @@ -26,7 +26,57 @@ E.g., `y` is possibly evaluated multiple times! |
|
|
## Co-call graphs
|
|
|
|
|
|
|
|
|
Meanwhile, [Call Arity](call-arity), using a **LetUp** strategy at let-bindings exclusively, has countered the exact same loss of precision by employing \*Co-call graphs\*. Instead of having cardinality information stored in a plain identifier map, where identifiers are assumed to be evaluated with each other, co-call graphs additionally assert that some ids are never evaluated during the same evaluation of the containing expression.
|
|
|
Meanwhile, [Call Arity](call-arity), using a **LetUp** strategy at let-bindings exclusively, has countered the exact same loss of precision by employing *Co-call graphs*. Instead of having cardinality information stored in a plain identifier map, where identifiers are assumed to be evaluated with each other, co-call graphs additionally assert that some ids are never evaluated during the same evaluation of the containing expression.
|
|
|
|
|
|
|
|
|
For the above example, the co-call graph for the inner let-body would specifically *not* contain an edge between `x` and `y`, because they are evaluated on mutually exclusive code paths. Thus, substituting the co-call graph of `x`s RHS into the co-call graph of the let-body will *not* induce a loop on `y`, so y will be recognised as evaluated at most once, which is what we want here.
|
|
|
|
|
|
## BOTH/OR trees
|
|
|
|
|
|
|
|
|
The idea behind co-call graphs translates to demand analysis by *being as lazy as possible* in computing `DmdEnv`s.
|
|
|
|
|
|
|
|
|
In particular, `bothDmdType` and `lubDmdType` currently smash together both incoming `DmdEnv`s. This forgets important structure for the above example: Namely that `x` and `y` are evaluated mutually exclusively.
|
|
|
|
|
|
|
|
|
To remedy that, we could model `DmdEnv`s as a tree structure (leaving `Termination`-based nastiness aside for a moment):
|
|
|
|
|
|
```wiki
|
|
|
data DmdEnv'
|
|
|
= Empty
|
|
|
| Var Id Demand
|
|
|
| Or DmdEnv' DmdEnv'
|
|
|
| Both DmdEnv' DmdEnv'
|
|
|
|
|
|
flattenDmdEnv' :: DmdEnv' -> DmdEnv
|
|
|
flattenDmdEnv' env =
|
|
|
case env of
|
|
|
Empty -> emptyVarEnv
|
|
|
Var id dmd -> unitVarEnv id dmd
|
|
|
Or env1 env2 -> lubDmdEnv env1 env2
|
|
|
Both env1 env2 -> bothDmdEnv env1 env2
|
|
|
```
|
|
|
|
|
|
|
|
|
This is essentially the interpreter pattern, with `flattenDmdEnv'` being an interpreter in terms of old `DmdEnv`.
|
|
|
|
|
|
|
|
|
However, as we'll see in a second, this buys us the ability to perform proper substitution when resolving let-bindings with **LetUp**, instead of just deleting the bound id from the body env and `both`ing with the result of the RHS.
|
|
|
|
|
|
|
|
|
For the above example, we get `(Both (...) (Or (Var x <S,1*U>) (Var y <S,1*U>)))` as the `DmdEnv'` of the let-body and `(Var y <L,1*U>)` as the `DmdEnv'` of `x`s RHS under the recorded demand `<L,1*U>` on `x` within the body.
|
|
|
We can now *substitute* the `DmdEnv'` of `x`s RHS into all occurences of `x` within the `DmdEnv'` of the let-body:
|
|
|
|
|
|
```wiki
|
|
|
(Both (...) (Or env (Var y <S,1*U>)))[env := (Var y <L,1*U>)]
|
|
|
= (Both (...) (Or (Var y <L,1*U>) (Var y <S,1*U>)))
|
|
|
```
|
|
|
|
|
|
|
|
|
If we look up the demand on `y` in the resulting `DmdEnv'`, we find that `y` is put under demand `<L,1*U>`, so used at most once, which is what we wanted.
|
|
|
|
|
|
|
|
|
Note however that it is still not detected as being used strictly!
|
|
|
For this, we would need to analyse `x`s RHS under the demand of the use site we substitute the `DmdEnv'` into, much like **LetDown** would.
|
|
|
Let's revisit this later. |