[CakeML-Dev] Pure annotation

[Ramana Kumar]

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).

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.

(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.)

On 22 November 2016 at 09:58, <Michael.Norrish at data61.csiro.au> wrote:

> 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/20161122/0f49c022/attachment-0001.html>