[Agda] evaluation strategies of the future [issue #426]

[Wolfram Kahl]

On Tue, Oct 25, 2016 at 02:19:54PM +0200, Ulf Norell wrote:
> Before we discuss any particular solution to get call-by-need working, it's
> useful to distinguish between two separate problems one might envision
> call-by-need solving. The first, which I believe is the one you are
> interested in, is to get efficient compile-time evaluation. The second is
> to reduce the memory requirements of type checking by having more sharing
> in terms. These are related but the second goal requires more care during
> other phases of type checking than pure evaluation (such as unification).
> 
> The current implementation of `--sharing` is a hack using `IORef`s to see
> how far it would get us towards solving problem number 2 (not very far).
> The main problem with it, aside from being hacky, is that `IORef`s are too
> persistent, so you run into problems when working interactively. For
> instance, once you've looked at the normal form of a goal type you cannot
> get back the original goal type, since it's been destructively updated to
> its normal form. You could imagine ways to solve this problem, for instance
> by making deep copies of terms before working on them, but it's easy to
> miss cases and since the current implementation isn't really that nice to
> begin with we haven't spent time on that.
> 
> The lambda-lifting issue I mentioned is a standard problem with
> call-by-need. Consider the two Haskell functions pow2 and pow2':
> 
> pow2 0 = 1
> pow2 n = r + r
>   where r = pow2 (n - 1)
> 
> r n = pow2' (n - 1)
> 
> pow2' 0 = 1
> pow2' n = r n + r n
>
> In pow2' we have lambda lifted the local binding r. If you run these you'll
> find that pow2 is fast and pow2' is exponentially slow. The reason is that
> call-by-need does not memoize function calls (like you seem to expect), it
> just guarantees that named expressions are evaluated at most once.

In Haskell, the solution to that would be

pow2' 0 = 1
pow2' n = case r n of
  p -> p + p

How can the effect of this be achieved in Agda (internal) syntax?
 
> If you want to experiment with call-by-need I would suggest implementing it
> locally for the whnf-reduction in `Agda.TypeChecking.Reduce.Fast`. There's
> a single function reduceTm in which all reduction takes place (except for
> some substitution), so that should save you from having to rewrite the
> entire Agda code base.

Where does the lambda lifting happen?


Wolfram