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

[Ulf Norell]

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.

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.

/ Ulf

On Mon, Oct 24, 2016 at 4:42 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> Despite my best efforts
> <https://github.com/agda/agda/issues/426#issuecomment-254111273> to try
> to get around the performance problems that are seemingly inherent in
> call-by-name, I have not found a satisfactory solution, so I've come to
> agree that we need a different evaluation strategy. Exactly what, I don't
> know, but I'm starting to read through the Agda (Haskell) code, hoping to
> put myself in a position to help.
>
> I'd like some explanation how the current call-by-need implementation,
> `--sharing`, works (or doesn't) and get your thoughts on what a promising
> solution might look like.
>
> On the subject of `--sharing`, Ulf Norell mentioned here
> <https://github.com/agda/agda/pull/1867#issuecomment-187596312> that it's
> too problematic to continue improving. I'd like to know what's
> fundamentally wrong with it. He mentions here
> <https://github.com/agda/agda/issues/426#issuecomment-129023261> that
> substitution is not memoizing pointers, but I'm guessing that that could be
> fixed and is *not* what's fundamentally wrong with `--sharing`. In the same
> comment he mentions that a particular where clause is problematic for
> `--sharing` "because of lambda lifting". I'm unclear on how this is
> breaking call-by-need. Is the function in the where clause getting lambda
> lifted? Does that somehow lead to the top-level function not getting
> memoized?
>
> What's the future of Agda's evaluation strategy?
>
> (If this should have been posted in the issue tracker, please continue the
> conversation there.)
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161025/92df04ea/attachment.html