Skip to content

Widen incoming demands to avoid them growing unbounded in size.

Andreas Klebinger requested to merge wip/andreask/dmd_widening into master

Given a data type like this:

  data T = C { ... , next :: T }   -- NB: a single-constructor type

and a function

    f x = ..
      .. -> f (next x)

usage information would be unbounded in it's size.

The reason is that we figure out f will use the next field of x. Giving us useage information of U. Armed with this information we analyse f (next x) in the body again on the next iteration giving usage of U<U>. We can repeat this for infinity and will never reach a fixpoint.

We used to deal with this simply by limiting the number of iterations to 10 and giving up if we could not find a fix point in this time.

While this works well for small recursive groups it doesn't work for large ones. This happened in #18304 (closed).

The reason is simple. We analyse a recursive group of functions like below:

f1 x = ...
  -> f1 (next x)
  -> f2 (next x)

f2 x = ...
  -> f1 (next x)
  -> f2 (next x)
  -> fn ...

We analyse f1 under the default demand resulting in U. We analyse f2 and see the call f1 (next x) in the body. Since f1 x has U "f1 (next x)" in the body of f2 will result in U<U> as usage demand of f2.

For each additional function fn in the group of this pattern usage information will become nested deeper by one level.

This means depth of usage information will grow linear in the number of functions in the recursive group. Being capped at iterations * n.

This is still tractable, the issue in #18304 (closed) addone one more dimension to the problem by not having one, but two "next" fields.

data T = C { ... , next1 :: T, next2 :: T}

f1 x = ...
  .. -> f1 (next1 x)
  .. -> f1 (next2 x)
  .. -> f2 (next1 x)
  .. -> f2 (next2 x)

Suddenly the size of usage information was growing exponentially in 2 ^ (n * iterations).

This very quickly becomes untractable!

This is a well known problem which is usually solved by adding a widening operator.

For simplicity however we apply this operator to the incoming demand instead of the result. This has the same result of allowing us to reach a fixpoint but has two benefits:

  • There is only a single place where we need to care (in the argument of dmdAnal).
  • We can fully analyze functions taking apart deeply nested non-recursive types only losing precision in the recursive case.
Edited by Simon Peyton Jones

Merge request reports