:nothrow and :effect_free might be easier to decide, because you can scan through the typed IR and check whether there’s throw code and effectful code. You have to do this recursively by scanning every invoked method. If there’s dynamic function call then just give up and mark it conversively as throw and effectful.
However this strategy still relies on Julia’s type inferencer which is generally hard to reason (because it does a lot of tricks like union splitting to make your codes type stable). You have to perform type inference here, otherwise you can’t decide which function is called. For example, it’s possible that the constant propagation eliminates the unreachable code and remove the effectful codes. Consider this simplified example:
function f(x)
if false
error("Error")
end
end
A good news here is that if you apply the above decision procedure instead of the more dedicated and impractical one, then we can report failure easily. For example, in the above example,. we may report that the code is not effect-free because of the error there, even if the optimizer will remove the unreachable branch lately.
So it might be easier and more helpful to know the situations where Julia would definitely know this is the case and conservatively mark other cases manually, so you won’t be bitten by Julia’s type inferencer. I know it’s bad to add such remarks manually, because it’s rather unsafe and not general (much like inbounds). It would be great to deduce such things by compiler automatically. But compiler’s internal algorithms are not that stable (and undocumented and hard to reason). So relying on it to handle complicated cases may not be a good idea.
Even if we consider things conservatively, it’s still tricky however, because many people conduct type calculations at compile time, which requires Julia’ s type inferencer performing nontrival operations. I would say that a general way is to reduce such reasoning to reasoning of type stability. If you are pretty sure that every function call is invoked with concrete types and nothrow/effect_free (so you need to perform manual union splitting) and there’s no recursive function calls (which may throw StackOverflow error), then it’s safe to say that the function is no_throw/effect_free.
Termination is even harder. In addition that it relies on Julia’s type inferencer, it has to reason recursive functions and loops, which are extremely complicated (if you don’t use such constructions then it’s easier to reason termination). A general idea is that if arguments to recursive calls or loop counters are “structurally decreasing”, then by monotonicity it must terminate. In other functional languages this can be decided easier than in Julia because they use recursive functions and recursive types more frequently, so if you pattern match on a value, then it would be destructed and the result is obviously structurally decreasing. But in Julia for and while loop are more common, so you have to reason numbers and arithmetic. It’s possible but not that straightforward. To reason a simple for i in 1:x bounded for loop, you have to first observe that i is monotonically increasing, then you know that the condition to leave the loop body is i < x, since i is monotonically increasing and x is constant, this condition will eventually be false and terminate.
Anyway, I am not sure whether Julia already apply such reasoning to deduce whether a loop will terminate. But I think Julia will (or maybe already) support bounded for and while loop as long as this wouldn’t make latency problem much worse, since compiler has to spend extra time reasoning such things. This should cover many scientific programs.
If you ask my suggestions on when the effect should be used in performance critical code, then I will just say that you should not use them currently. They are new features (so may still undergo design changes in the future) and need more observations, especially how they are used in Julia’s compiler and Base library. Personally, I am strongly against exposing effect system to Julia users. It’s more risky than @inbounds and doesn’t cope well with generic functions and multiple dispatch. Plus that we don’t have any checker for it, so if your performance critical code relies on compiler’s implementation details, then your code might suffer from degradation when compiler changes, and you have no idea what happens.
One motivation of effect system is to improve performance, and this is much done by producing more “invariants”. For example, if a function call is pure enough (don’t throw any error, don’t modify memory), and it’s located in a loop, then we may move this calculation out of the loop because the result remains the same. Note that you may always do this manually, one natural question is that why not just do this kind of code transformation by hand instead of relying on the unreliable compiler optimizer. One answer is that for generic functions it may or may not be pure depending on specialization, so you cannot simply hoist it out of the loop in every case. But as I have mentioned before, we really shouldn’t use these unsafe remarks for generic functions…
Still, there are several cases where these marks can be used safely. The first case is to perform complicated compile-time type calculation. These functions are performance critical (otherwise too many dynamic types), and their inputs are usually predictable. What’ more, they are unexported and used only internally, so user won’t shot their feet by accidentally providing inappropriate inputs. But given that we already abuse generated functions and Val to perform type calculations, this may not be that useful. The second one is to deal with foreigncall, which is good candidate for these remarks (fixed input types and the semantics is stable).
In summary, normal users should not use these remarks (unless in one of the aforementioned cases). They should program in Julia as if this effect system doesn’t exist and rely solely on Julia’s effect inferencer to perform optimization safely (even without using these remarks people can get performance improvement because structure of many scientific programs is simple and easy to analysis).