<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>The JavaScript backend is the only exception here I guess, it
uses strict evaluation. The main reason is that having strict
semantics matches the JS evaluation model much more closely which
simplified the backend implementation.</p>
<p>While this is permitted by Agdas semantics, I suspect most
existing Agda code assumes laziness and there are probably some
performance problems lurking around when using e.g. the stdlib
with a strict evaluation model.<br>
</p>
<p>Philipp</p>
<br>
<div class="moz-cite-prefix">On 03/28/2018 11:52 AM, Ulf Norell
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJjNqYG+m6WDvTtYoa6KaM6g0sbc8K1LvwN8JZvjVVZVnx2D7Q@mail.gmail.com">
<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"
moz-do-not-send="true">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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank"
moz-do-not-send="true">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>