In prof. Jan Vitek JuliaCon 2021 keynote, he discussed type stability and grounded type (starting at 42:30). Short definitions given at this talk are as follow.
Type is stable if we have clear relation between I/O types.
Type is grounded when
@code_warntype is green.
I make a quick search of Julia 1.6.5 and 1.7.1 documentation and it show that word “grounded” never appear in them. The closest match in both cases is “Rounding”.
I want to ask is “grounded type” prof. Vitek’s term for something know in community or is it some new concept that doesn’t take roots outside core team (who is core team can be sometimes blurry)?
This seems to be a term introduced by Prof. Vitek in their paper on type stability (linked above), where they write:
That is, they are referring to a function where concrete types of all variables (not just the return value) can be inferred by an ideal compiler (which only knows the argument types), i.e. one where
It’s not a new concept in general in the Julia community, but people have talked about in different ways, e.g. as “type stability” (of the variables, not the return value) or as “type inferability”, and Jan was pushing for more precise terminology.
It should be noted, however, that “variables” in that definition refers to variables in the simplified single static assignment lowering of Julia code introduced in the paper and not to Julia surface level variables. The requirement for groundedness translated back to surface Julia syntax is probably that the type of every expression is predictable from the types of the arguments. Otherwise you would get weird situations where whether a function is grounded or not depends on whether you pass a value directly to a function or assign it to a variable, which would be a bad definition.
I understand what is lowered Julia code (I used
@code_lowered few times), I have some understanding of “static” word in C++, but I can’t crack what it means “single static assignment lowering of Julia code”. Can you expand it a little bit?
Static single assignment form - Wikipedia, a particular intermediate form that has desirable properties
They introduce a different lowering form in the paper that’s simpler and easier to prove things about. But the high-level take away is if you can predict the types of all expressions in a function from the types of its arguments, then there are a number of compiler optimizations that are provably guaranteed to work. This requirement is moving in the direction of static typing of Julia code, although the paper does not go as far as providing an algorithm for type checking Julia functions.