<div dir="ltr"><div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">On Wed, Mar 27, 2019 at 2:28 PM Dmitry Belyaev <<a href="mailto:be.dmitry@gmail.com">be.dmitry@gmail.com</a>> wrote:<br></div></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>If I remember correctly Idris has eager evaluation and also defines 'if then else' in the standard library. So I believe lazy evaluation is not really required for that.<br><br></div></blockquote><div><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">Two points:</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* In a total language, evaluation order only matters insofar efficiency is concerned. The result would be the same, regardless of evaluation order.</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">* Idris implementation types the branches as Lazy, so it explicitly marks those as lazily evaluated. Evaluation order is but a mode of execution, so converting between them is possible. A lazy by default language often requires strictness annotations for efficiency reasons. And likewise, a strict language enjoy having explicit laziness for efficiency reasons, where efficiency encompasses execution time as well as space usage.</div><br></div></div>