<div dir="ltr"><div><div><div><div>Both the type checker and the GHC backend are lazy by default. For the type checker<br></div>it would be disastrous to be strict everywhere, since you'd end up evaluating expensive<br>proof terms that you don't need to look at. For the run time it's slightly better since many<br></div>of those proof terms will get erased. It is not possible to compile an Agda program with<br></div><div>(the ghc flag) -XStrict since the GHC backend relies on laziness.<br></div><div><br></div>You can manually control strictness using Agda.Builtin.Strict.primForce. This forces<br></div><div>evaluation of its argument both at compile time and at run time. There is currently no way<br>to declare strict constructors like in Haskell.<br><br></div><div>/ Ulf<br></div><div><div><div><div><div><br><br><br></div></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 28, 2018 at 11:34 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</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 2018-03-28 10:54, Sergei Meshveliani wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
can you, please explain, what is the relation between laziness and<br>
strictness in Agda?<br>
</blockquote>
<br></span>
Agda is a language in which every program is productive (in the absence<br>
of bugs, when the termination checker has not been turned off, etc.).<br>
This gives quite a bit of freedom to those implementing compiler<br>
backends for Agda, and different backends take different approaches.<br>
<br>
I think you are mainly using the GHC backend. This backend uses lazy<br>
evaluation.<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is Agda ready to take the option "do everything strict in type checking<br>
and in the executable code" ? what will be a real effect?<br>
</blockquote>
<br></span>
It would be easy to make all *inductive* constructors strict in the GHC<br>
backend. This might be beneficial for code written in a certain way, but<br>
it could also hurt performance for code that includes proof terms that<br>
are not erased.<br>
<br>
I guess it would also be possible to make more function applications<br>
strict. However, if you make, say, if_then_else_ strict, then you could<br>
incur a substantial performance penalty.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD</font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>