<div dir="ltr"><div><div>I don't want to put it into the type system, if that's what you mean, because I don't want to complicate or lose complete type inference, and because I want to be able to annotate pure programs whose purity might be quite difficult to prove (i.e., might require an interactive proof).<br><br></div>However, in chatting with Magnus, I have been convinced that it would be good to make side effects inside purity annotations raise runtime type errors, so that the compiler has very strong assumptions to work with. There is, of course, still termination/divergence to preserve, so it's not as free as in Haskell, but it's better than having to get the semantics of a real exception right (and doing runtime checks). Runtime type errors would mean not allowing annotations in the type-inferred concrete syntax, but they can still be user-provided if the user's front-end is the translator and/or CF.<br><br></div>(A set up where the user (or some automatic proof tool like the translator) defends a purity annotation also seems like a slightly less obvious idea than purity annotations in general.)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 22 November 2016 at 09:58,  <span dir="ltr"><<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">







<div bgcolor="white" link="#0563C1" vlink="#954F72" lang="EN-GB">
<div class="m_-6556052955073653859WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri">Couldn’t you move the annotation into the type system and do away with the need for dynamic checks, at least in principle?  That would put you more into the line
 of what I understand effect-types would get you.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri">Michael<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri"><u></u> <u></u></span></p>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-family:Calibri;color:black">From: </span>
</b><span style="font-family:Calibri;color:black">Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>><br>
<b>Date: </b>Tuesday, 22 November 2016 at 03:23<br>
<b>To: </b>"<a href="mailto:developers@cakeml.org" target="_blank">developers@cakeml.org</a>" <<a href="mailto:developers@cakeml.org" target="_blank">developers@cakeml.org</a>><br>
<b>Subject: </b>[CakeML-Dev] Pure annotation<u></u><u></u></span></p>
</div><div><div class="h5">
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi CakeML developers,<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">I dreamt up an idea just now and wanted to run it by you. (A tiny bit of Googling suggested this might be related to effect systems, but I didn't find the academic treatment on purity annotations that I would
 guess should exist somewhere...) Here is the idea: add an explicit purity annotation to enable more aggressive compiler optimisations.<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">I imagine this would be a new expression-level construct in the source language, where Pure exp would have the semantics of exp except that any attempt to write to (reading is fine) the store or to call FFI
 is trapped and raises an exception. (This exception could be uncatchable if it makes things simpler.) I think this can be implemented by adding extra checks to only a couple of ops in closLang and that the performance hit from those extra checks would be quite
 small/worthwhile. Specifically, I imagine checking a global bit on whether we're inside pure-annotated code before attempting to update the store. (This is only required for functions that are used both inside and outside pure annotations; an alternative is
 to compile two versions of these functions, though some checks are still needed for higher-order arguments.)<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">I think these annotations can be added by the user explicitly, but also produced by the translator and produced by the compiler when it can infer purity. As for what optimisations they enable, I don't know specifics,
 but I would guess more aggressive re-ordering and removal of code and rewriting is possible. Getting the exception semantics right to enable aggressive optimisation might be tricky.<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Let me know if you've heard of this before, or think it's a good/bad idea.<u></u><u></u></p>
</div>
<p class="MsoNormal">Cheers,<u></u><u></u></p>
</div>
<p class="MsoNormal">Ramana<u></u><u></u></p>
</div>
</div></div></div>
</div>

</blockquote></div><br></div>