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

[Wolfram Kahl]

On Tue, Oct 25, 2016 at 04:25:32PM +0200, Ulf Norell wrote:
> 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).

Well, in Haskell, ``case'' is primitive, and (specialised to this case)
guarantees that p is evaluated only once.

In Agda, ``case_of_'' is not primitive, so call by name has the opportunity
to duplicate work. And aren't pattern matching lambdas translated into
local functions, and then presumably lambda-lifted?

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

I was more thinking along the lines of ``let's lambda lift properly'',
but without something like Haskell's ``case'', this is probably not easy...


Wolfram