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

[Ulf Norell]

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

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

Yes, you are right of course. That code only works if the pattern matching
lambda is strict in its argument (which it isn't in the example). Adding a
primForce on p should make it work though.

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