Skip to content

Unfoldings for lambda-bound variables

Currently GHC has an optimization which creates lambda-bound variables with unfoldings. It is described in Note [Case binders and join points], originally added in 72462499. In this situation, if we'd like to create a join point:

case ... of c {
   I# c# -> ....c....
}

we take both the case binder and the deconstructed fields:

letjoin $j = \c# -> \c -> ...c.... in
  case ... of c { I# c# -> $j c# c }

and we add an unfolding to the binder c: it is equal to I# c#.

I propose to remove this transformation. The reasons are:

  • Unfoldings attached to lambda-bound variables are a rather weird concept. They mean that a function can no longer be called on arbitrary values. Lint does not check whether the calls to the join point are consistent with unfolding.
  • This leads to bugs and addition of special cases (e.g. 71c7067b, #13890 (closed)).
  • In linear types, this transformation does not preserve linearity unless we complicate Lint significantly (in both function abstraction and function calls).

Proposed alternative:

  • If the case binder is not used, we just pass the arguments: letjoin $j = \c# -> ...c#...
  • If the case binder is used, we recreate it inside the join point: letjoin $j = \c# -> let c = I# c# in ...c...

There are two performance regressions, but I believe the tradeoff is worthwhile.

  • There's one perf test failing, T9872d, where compile-time allocation goes up by 1.2%. I think we can just mark it as Metric Increase.

  • nofib results: https://gist.github.com/facundominguez/3482c11ab2be94492843c843f41c755e.

    There is one regression in allocations, cichelli +9%.

    The regression happens because of reboxing in the function hinsert. Core before and after can be seen at https://github.com/tweag/ghc/issues/412#issuecomment-559213720.

    The relevant join point is called $j_s3No in the version with the optimization, or $j_s3Nq in the version without the optimization.

    When the optimization is enabled, it gets two parameters, y :: Int# and wild1 :: Int (= I# y), and returns a structure containing wild1. Without the optimization, $j gets only y and has to recreate I# y.

    The program wave4main, which was the motivation for this transformation as described in the Note [Case binders and join points], is no longer affected.

Edited by Krzysztof Gogolewski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information