Is let referentially transparent?

[josh11b]

From a discussion in #typesystem started on 2022-07-06, a question arose about this code:

fn F(z:! T);
let x: T = ...;
// Allowed?
F(x);

We are considering two options here:

• If x is considered a runtime r-rvalue because it was declared let x: ... instead of let x:! ..., then the call F(x) would be forbidden.
• Instead, if we follow C++ more closely, whether an x: T or an x:! T can be used in a :! context depends on whether (symbolic) evaluation of the expression containing x succeeds or not, regardless of how x was declared, and that :! is a constraint only on how the value is provided, not on how it's used. In other words, the call F(x) may or may not be allowed depending on ....

In this second case, F(if b then x else y) may not care about the properties of x depending on the value of b.

Note that deferred question-for-leads issue #996 asks a related question about whether a let is referentially transparent under specific conditions.

[chandlerc]

I think I recall this being discussed recently, with some movement towards "no" -- I wonder if you recall and could summarize any of that here @josh11b ? (Or apologies if I've misremembered...)

[josh11b]

We have decided that the value phase of x is determined by its declaration. This was discussed on 2022-09-09 and 2022-09-14, and is being implemented in proposal #2200 . So let x: T = ... defines x as a runtime r-value. The reason for this decision is because the name lookup rules for checked and template generics are different and we don't want there to be silent selection of the template name lookup rules.

However, I believe there are still open questions, including whether F(x) is allowed. If you pass x to a function, we might want to allow the value phase to be converted in some cases. For example, #2153 may be resolved by saying we allow values with a symbolic value phase to be converted to a template constant and passed to a template function parameter.

In addition the question from #996 is still open, though the resolution above makes it a distinct question. What remains to be determined is when you write let C:! auto = Movable & Hashable, does the auto get set to Type or a singleton type that preserves the information in Movable & Hashable.

[github-actions]

We triage inactive PRs and issues in order to make it easier to find active work. If this issue should remain active or becomes active again, please comment or remove the inactive label. The long term label can also be added for issues which are expected to take time.
This issue is labeled inactive because the last activity was over 90 days ago.

[josh11b]

What remains to be determined is when you write let C:! auto = Movable & Hashable, does the auto get set to Type or a singleton type that preserves the information in Movable & Hashable.

#2360 resolves this: the Movable & Hashable is a type so its type is type, and so the auto is deduced as type and the declaration is equivalent to let C:! type = Movable & Hashable; However, as discussed in #950 and #996, the compiler does retain some knowledge that C is Movable & Hashable, equivalent to the declaration observe C == Movable & Hashable;. That information isn't going to be useful for using C as an alias for Movable & Hashable, so in this case you would need to write let template C:! type = Movable & Hashable; to get that behavior.

[josh11b]

However, I believe there are still open questions, including whether F(x) is allowed. If you pass x to a function, we might want to allow the value phase to be converted in some cases. For example, #2153 may be resolved by saying we allow values with a symbolic value phase to be converted to a template constant and passed to a template function parameter.

#2153 allows implicit conversion between symbolic and template value phases, as long as the source is known to satisfy the constraints on the target. However, I have heard that we don't want to extend this to conversion from a runtime value to a compile-time value. This would mean that x after let x: T = ...; would have runtime value phase and F(x) would be rejected, independent of what is written in .... This is in contrast to C++, where whether x may be used at compile-time after const int x = ...; does depend on whether the initializer may be constant evaluated.

I'm not aware of anywhere else documenting that decision. I propose we resolve this question with this issue, selecting the first option: value expressions may not be converted from runtime phase to any compile-time phase.