[CakeML-Dev] Pure annotation

[Michael.Norrish at data61.csiro.au]

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.

Michael

From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
Date: Tuesday, 22 November 2016 at 03:23
To: "developers at cakeml.org" <developers at cakeml.org>
Subject: [CakeML-Dev] Pure annotation

Hi CakeML developers,
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.
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.)
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.
Let me know if you've heard of this before, or think it's a good/bad idea.
Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161121/e9143131/attachment.html>