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

[Ulf Norell]

On Tue, Oct 25, 2016 at 3:37 PM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:

> 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?
>

pow2' n = case r n of λ { p → p + p }

(note the pattern matching lambda).


>
> > 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?
>

In Agda.TypeChecking.Monad.Signature.addConstant. Of course, it's not as
simple as saying "let's not lambda lift then". There's no way to represent
a function that is not lambda lifted in the Agda internals.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161025/52e96da8/attachment.html