[CakeML-Dev] Pure annotation

[Ramana Kumar]

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/20161122/4c35b099/attachment.html>