[StefanKarpinski]

I'm still working through the paper—reading your group's Julia papers is always a great treat—thank you for this one and all of them. Looking at the definition of "type groundedness" it seemed to me that perhaps the definition should require that "every expression’s type depends only on the argument types" rather than only variables. I haven't gotten to the proof parts, but this was just a thing that struck me early on.

[ulysses4ever]

Your intuition is right but _every_ expression is bound by a variable in this representation.

[StefanKarpinski]

Ah, ok. I hadn't gotten to that part yet. Would it make sense to change the general definition to "expressions" since that would be the correct definition for Julia code as well as the Jules IR format?

[ulysses4ever]

This may require more thinking on our end but the way we design Jules is the usual SSA form. The idea being it's easier to reason about it (and prove things) when every expression has a name. It's a bit of cheating of course but makes our life easier. We don't discuss how surface Julia (or subset of it), which is more expression-oriented, can be translated to Jules, because we have only so many pages, and also it's not all that interesting, I think.