implement pure function annotations

[vtjnash]

this implements a @pure annotation for functions. if a pure function can be run at compile-time, it will be, so use sparingly (and don't try to make it solve the halting problem). however, it provides a less codegen-heavy alternative to several @generated functions that were in base (since the optimization now becomes optional / compile-time, rather than mandatory / runtime).

future work: the current implementation neglects to make use of this information to improve effect_free or to auto-compute this information using effect_free. both of those optimizations should be simple and beneficial.

[stevengj]

Hooray! This will close issue #414; see that issue for discussion.

[stevengj]

One of the things I was hoping to make pure was e.g. convert(::Type{Float64}, ::Rational{Int}), so that you can use rational constants like 1//3 as exact (precision-independent) constants without a runtime penalty. Presumably this will be possible with this patch?

[vtjnash]

yes, that seems possible. as written, however, it's mostly intended for type-domain functions, where the added expense at compile-time should be completely offset by better type information. also, since we don't have a constant-propagation pass, except for types, it won't be able to handle anything too complex that isn't in the type domain.

[StefanKarpinski]

But if we had constant-propagation in addition to this, then it could work, no? I don't understand the insistence that this feature only be for doing type domain computations. Why limit it?

[vtjnash]

it still wouldn't provide most of the runtime optimizations you would probably expect (such as auto-memoization and loop invariance), and it doesn't run during / after inlining as you would probably want. but yes, there's nothing inherently wrong about annotating other functions.

(travis failure seems to have been a random OOM, so this is ready to merge)

[stevengj]

Presumably, those are all optimizations that can be hooked in later with this @pure design?

[carnaval]

even if we trust the user that the function is pure, this looks dangerous. pure usually does not imply terminating (or reasonably fast anyway) so we should at least not use that name.

[carnaval]

I do like that we can get rid of the ugly special cases in inference.jl, I'm just not sure this annotation should be user facing.

[vtjnash]

we trust the user that @generated functions are sane (which is how these particular functions used to be marked). what's wrong with trusting them that @pure is marked correctly? i don't plan on exporting @pure until it is more intelligent about those additional requirements (e.g. post-green-fairy, if ever)

[stevengj]

Pure functions, and the associated compiler optimizations, are very useful for writing efficient library functions... it would be sad if this feature were planned to be confined to Base for the foreseeable future.

[carnaval]

I'm fine with trusting the user, I just think the naming at least is a little too innocent. Pure is a factual assertion ("even if it may not look like so, this function can be considered side effect free"), whereas this annotation is an intent declaration ("blindly execute at compile time").
IMO a correct implementation of "pure" would at least terminate the evaluation after some constant number of steps. I am aware that this is basically infeasible today.

[vtjnash]

@carnval i'm not convinced that those require different annotations. it's true that's how it is annotated today, but I think there are a number of heuristics that can be incorporated into inference to improve the off-nominal behavior of this annotation without actually changing its meaning. these include:

• execute an @pure function only if the return type was not perfectly inferred.
• execute @pure functions for arguments that subtype Type more than for other argument types
• implement execution time step limits

again, this is in contrast to the @generated functions and special-case functions that this PR replaces, for which the compiler has no flexibility except to blindly execute at compile time and hope it terminates / works.

but, this PR was intended to only address a couple of particular cases (and provide a slot to store the pure attribute). i'm expecting the gf to provide a more general framework and make better use of this information. in light of that, does this need tweaking now to make it compatible with your plans for that?

@stevengj I agree. However, this can only handle completely trivial expressions like pow(1, 2), and not x = 1; pow(x, 2), and it doesn't propagate the information in such a way that it could hoist this out of a loop. I'm not saying you can't mark any function with Base.@pure, but this just hasn't implement any of the associated compiler optimizations that make it useful for efficient library functions (outside of the type domain), or any of the safety measures that carnval is describing.

[stevengj]

I agree that until the associated compiler optimizations are implemented, there is no point in exporting it. But presumably those are orthogonal features that will get implemented eventually — they are well-known and well-understood optimizations that have been implemented to some degree in many other languages.

On the other hand safety checks on pure annotations seem more like an open-ended research project, and I don't think exporting @pure need wait on these.

[jakebolewski]

This feature seems a bit ripe for abuse. I think we should add a command line switch to ignore the @pure annotation for testing.

[vtjnash]

how do you think it'll get abused? the system only looks for the attribute when the result is (likely) profitable.

[jakebolewski]

If you added the @pure annotation to random functions in Base, it can discriminate methods where it is correct given the expected semantics for the annotation? I'm with @carnaval that you are asserting very specific semantics for the annotation (which may be relaxed in the future).

But I misread the above conversation, it doesn't seem like this will be user facing or exported.

[yuyichao]

It's probably fine for types (i.e. the current use case) but I'm wondering if this is fine to do with other values in general since some of them might be pure or not depending on the type of the arguments.

[stevengj]

Of course random methods aren't @pure. That's even less likely to work than adding @inbounds at random places in the code. This was all discussed in #414. (If it were possible to do automated checking of whether a @pure annotation were correct, then the annotation wouldn't be necessary.)

When more compiler optimizations are implemented and @pure is exported (i.e. not this patch), as discussed in #414, you'd probably want a way to turn it off for testing purposes, much like --check-bounds=yes turns off @inbounds.

[stevengj]

In particular, see @JeffBezanson's suggestion in #414 that @pure should be an unchecked assertion that the function f(x) satisfies x===y => f(x)===f(y) and f doesn't do I/O or write to global state.

[yuyichao]

Thanks for the pointer. Seems that what I said (edit: or what I wanted to say at least....) was basically this #414 (comment) ... (Although I don't think there's a solution for this in that thread?)

[stevengj]

@yuyichao, I don't think there was a solution. (Has any language as complex as Julia, with side effects etc., ever successfully implemented automatic purity inference? Lots of languages have unchecked pure assertions, on the other hand. It would be sad to give up on this feature unless a difficult open research problem is solved. Sparing, careful use, combined with compiler optimizations as mentioned above, could have lots of benefits.)

[stevengj]

Unless there is reason to believe that bottom-up purity inference is not that difficult for the cases where we want to use it? At minimum, you would need the ability to mark certain ccalls and intrinsics as pure.

[vtjnash]

there are cases (such as type-intersection), where the intermediates are not pure but the end result is pure. however, the computation of that would require tracking purity and escape with respect to each argument (i would guess that is a special case of the halting problem). as mentioned in the top post, the compiler could use effect_free to handle many of the trivial cases (e.g. so that it propagates up to a simple dispatch wrapper, or for a function that returns a constant, etc.).

the annotation here is on a method, not a function, in part to address the observation that sin(Float64) is pure while sin(Vector{Float64}) is not. along those lines, though, the user does need to be fairly careful when using this, since Julia is a dynamic language, so f(x) = sin(x) is pure only if sin is, and that may not be true for all x. f(x::Number) is probably safe to mark, although not necessarily (something like a BigFloat might throw it off, for example). and then there's f(x::Float64), which is known to be trivially pure due to the strictly limited dispatch signature.

[mbauman]

So what happens if I define a promote rule that ensures my custom type only ever has a concrete type parameter… and throws an error otherwise? That would mean that this pure annotation is no longer correct, no?

@inline function Base.promote_rule{T,S<:Number}(::Type{Interval{T}}, ::Type{S})
    R = promote_type(T,S)
    isleaftype(R) || throw(ArgumentError("cannot promote $T and $S to a common leaf type"))
    Interval{R}
end

On second thought, this is probably better to enforce in the constructor. But do we need to document that promote_rule needs to be a pure function now? What happens if it's not?

[vtjnash]

throwing errors is fine