<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 26, 2016 at 9:02 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2016-10-25 at 14:19 +0200, Ulf Norell wrote:<br>
> Before we discuss any particular solution to get call-by-need working,<br>
> it's useful to distinguish between two separate problems one might<br>
> envision call-by-need solving. The first, which I believe is the one<br>
> you are interested in, is to get efficient compile-time evaluation.<br>
> The second is to reduce the memory requirements of type checking by<br>
> having more sharing in terms. These are related but the second goal<br>
> requires more care during other phases of type checking than pure<br>
> evaluation (such as unification).<br>
><br>
><br>
> The current implementation of `--sharing` is a hack using `IORef`s to<br>
> see how far it would get us towards solving problem number 2 (not very<br>
> far). The main problem with it, aside from being hacky, is that<br>
> `IORef`s are too persistent, so you run into problems when working<br>
> interactively. For instance, once you've looked at the normal form of<br>
> a goal type you cannot get back the original goal type, since it's<br>
> been destructively updated to its normal form.<br>
</span>> [..]<br>
<br>
So, may it have sense to implement a special optimization for a<br>
non-interactive type checking?<br>
For example, I mainly avoid interactive usage. May be I am loosing some<br>
nice possibilities, but in my experience interactive usage does not make<br>
it essentially easier to type check the library being developed, anyway<br>
other obstacles take much more of effort.<br>
(Though, a sharing thing being hacky may present an important drawback,<br>
it depends on I do not know what).<br></blockquote><div><br></div><div>It's not only a problem for interactive use. For instance, certain phases of type</div><div>checking might perform reductions that you do not wish to be reflected in the terms</div><div>used by the compiler.</div><div><br></div><div>/ Ulf</div></div></div></div>