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

[Ulf Norell]

On Wed, Oct 26, 2016 at 9:02 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Tue, 2016-10-25 at 14:19 +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.
> > [..]
>
> So, may it have sense to implement a special optimization for a
> non-interactive type checking?
> For example, I mainly avoid interactive usage. May be I am loosing some
> nice possibilities, but in my experience interactive usage does not make
> it essentially easier to type check the library being developed, anyway
> other obstacles take much more of effort.
> (Though, a sharing thing being hacky may present an important drawback,
> it depends on I do not know what).
>

It's not only a problem for interactive use. For instance, certain phases
of type
checking might perform reductions that you do not wish to be reflected in
the terms
used by the compiler.

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