<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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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>
&gt; Before we discuss any particular solution to get call-by-need working,<br>
&gt; it&#39;s useful to distinguish between two separate problems one might<br>
&gt; envision call-by-need solving. The first, which I believe is the one<br>
&gt; you are interested in, is to get efficient compile-time evaluation.<br>
&gt; The second is to reduce the memory requirements of type checking by<br>
&gt; having more sharing in terms. These are related but the second goal<br>
&gt; requires more care during other phases of type checking than pure<br>
&gt; evaluation (such as unification).<br>
&gt;<br>
&gt;<br>
&gt; The current implementation of `--sharing` is a hack using `IORef`s to<br>
&gt; see how far it would get us towards solving problem number 2 (not very<br>
&gt; far). The main problem with it, aside from being hacky, is that<br>
&gt; `IORef`s are too persistent, so you run into problems when working<br>
&gt; interactively. For instance, once you&#39;ve looked at the normal form of<br>
&gt; a goal type you cannot get back the original goal type, since it&#39;s<br>
&gt; been destructively updated to its normal form.<br>
</span>&gt; [..]<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&#39;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>