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

[Sergei Meshveliani]

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

------
Sergei