Should variables be mutable?

[catamorphism]

In #402 (review) , @eemeli asked:

"For an alternative approach, could we consider changing the let keyword to be set, and for references to declarations to be changed to definitions or assignments? This might make it easier to consider them as assignments rather than initializations."

This would be a non-trivial change, so I wanted to open a separate issue to discuss it. The discussion in #310 overlaps with this issue, but for clarity I wanted to make a separate issue to discuss the specific question about whether the let construct is meant to be a definition construct or an assignment construct.

[catamorphism]

I don't think we should make this change. To explain why, I'll use an example message written using the proposed syntax:

Example 1:

set $v1 = {foo :func}
set $v2 = {$v1}
set $v3 = {$v1}
set $v1 = {42}
{{$v2}}

I'm assuming, based on #299, that the formatting spec will eventually specify some form of lazy evaluation for local variables.

There are two varieties of lazy evaluation: call-by-name and call-by-need.

If we choose call-by-name, then the result of evaluating this message is the result of sequentially replacing each declaration's LHS with its RHS. So under call-by-name semantics, Example 1 is equivalent to Example 2:

Example 2:

set $v1 = {foo :func}
set $v2 = {foo :func}
set $v3 = {foo :func}
set $v1 = {42}
{{$v2}}

The result is the result of calling func on the literal foo.

Under call-by-need, for each declaration let $v = {e}, each LHS $v would be bound to a mutable slot that contains a closure. The closure contains the code representing e, and an environment, which gives meanings to any free variables in e.

The steps in evaluating the message would be:

1. Bind $v1 to a mutable slot containing a closure that computes {foo :func}, with an empty environment (empty because {foo :func} has no free variables).
2. Bind $v2 to a mutable slot containing a closure that computes {$v1} and an environment mapping the name $v1 onto the mutable slot created in step 1.
3. Bind $v3 to a separate mutable slot containing a closure that computes {$v1} and an environment mapping the name $v1 onto the mutable slot created in step 1.
4. Overwrite the contents of $v1 with a closure that computes {42} with an empty environment.
5. Evaluate the body by invoking the closure created in step 2.

The result is the literal 42, because the closure for $v2 contains a reference to $v1 -- not the initial value of $v1 -- and during step 5, $v1 denotes a slot that (effectively) contains the literal 42.

So we see that whether we choose call-by-need or call-by-name changes the meaning of the message. This is why call-by-need is not typically used in languages with mutable data. We could commit to using call-by-name semantics, which would mean this message would resolve to what the user probably expects it to resolve to (which is to say, whatever func(foo) returns). However, that commitment potentially means repeating a lot of computation. The question is whether the benefits of allowing mutation are worth it.

[catamorphism]

You might ask: "Don't we have the same problem with the existing let-construct? After all, the only difference is whether the keyword is let or set."

Yes and no. If we also specify that the sequential lets in a message are syntactic sugar for nested lets -- which is to say, for example:

Example 3:

let $v1 = {e1}
let $v2 = {e2}
let $v3 = {e3}
{{$v1} {$v2}}

is equivalent to:

Example 4:

let $v1 = {e1} in
  let $v2 = {e2} in
    let $v3 = {e3} in
       {{$v1} {$v2}}

then we solve the problem. Example 4 isn't a valid message; the point is just to show what it means to treat the lets as conceptually nested.

This solves the problem because if we consider examples 3 and 4 to be equivalent in meaning, then we can also specify that:

Example 5:

let $v1 = {e1}
let $v2 = {$v1}
let $v1 = {e3}
{{$v1} {$v2}}

is equivalent to:

Example 6:

let $v1 = {e1}
let $v2 = {$v1}
let $v3 = {e3}
{{$v3} {$v2}}

Example 6 is the result of uniquely renaming each variable. If we know that all variables are unique, then we can explain variable resolution by repeated substitution (for spec purposes; it doesn't have to be implemented as substitution):

{{$v3} {$v2}}   # after unique renaming
{e3 {$v1}}       # after substituting `$v3`⟼`e3` and `$v2`⟼`{$v1}`
{e3 e1}           # after substituting `$v1`⟼`e1`

In other words: with the existing let syntax, it's unsurprising to say that alpha-renaming (giving each distinct declaration a unique name and performing substitutions so as to preserve the message's meaning) is a meaning-preserving transformation.

On the other hand, if we moved towards set and treating declarations like assignments, it would be counterintuitive to treat examples 5 and 6 as equivalent. Going back to example 2, if you think the $v1 assigned on line 1 and the $v1 assigned on line 4 are the same mutable variable, you will be surprised. And the syntax encourages you to think that. With call-by-need, this difference is observable.

(Edited for clarity, 2023-07-05)

[catamorphism]

So in my opinion, if everybody agrees that local variable declarations should be evaluated lazily, we should keep the let syntax and give it a semantics in which unique renaming doesn't change the meaning of the message. The combination of mutation and call-by-need is confusing and I'm not aware of any significant programming languages that have it.

Moreover, I don't know how to precisely specify the meaning of name shadowing without specifying how the sequential let construct desugars to nested lets: in other words, why lets are lexically scoped. Or, alternately, specifying how alpha-renaming works. Either of those seems very challenging to do at the level of formality of the current spec. That's why I also believe that name shadowing should be disallowed, but that's a separate question.

[eemeli]

@catamorphism Would it be possible for you to replace the expressions like {e1} and patterns like {p} in the above with valid syntax? I'm getting rather lost in trying to figure out what each might mean, end e.g. can't tell what the difference is between examples 5 and 6.

So in my opinion, if everybody agrees that local variable declarations should be evaluated lazily, [...]

This is not necessarily a valid premise, and I don't think we've explicitly established any explicit preference or requirement for laziness or eagerness in the spec at least so far. In fact, we've gone out of way to ensure that either approach is valid.

In that spirit, the recent formatting PR added this to the Error Handling section:

message-format-wg/spec/formatting.md

Lines 781 to 783 in 4a1e367

	Resolution and Formatting errors in _expressions_ that are not used
	in _pattern selection_ or _formatting_ MAY be ignored,
	as they do not affect the output of the formatter.

This is intended to allow for either eager or lazy behaviour in an implementation. So if it made the explanation simpler, with that language being included we could specify something like this in the spec and still support both:

Each declaration is processed in source order.
A declaration modifies the formatting context variable mapping of string identifiers to values
by assigning the resolved value of its expression as the value for its variable name.
If a declaration expression includes variables,
their values are resolved using the variable mapping values as they were before the current declaration.

This kind of formulation would simplify our scopes to just one, which should be easier to understand.

With that as a starting point, the declarations of your first example

set $v1 = {foo :func}
set $v2 = {$v1}
set $v3 = {$v1}
set $v1 = {42}
{{$v2}}

would modify the formatting context variable mapping as follows:

0. Start with an empty set {}
1. After set $v1 = {foo :func} we have { v1: func('foo') }
2. After set $v2 = {$v1} we have { v1: func('foo'), v2: func('foo') }
3. After set $v3 = {$v1} we have { v1: func('foo'), v2: func('foo'), v3: func('foo') }
4. After set $v1 = {42} we have { v1: '42', v2: func('foo'), v3: func('foo') }

And so during the pattern formatting, {$v2} would get its value for func('foo').

[macchiati]

If we disallow mutating variables, we also avoid the issue completely.

[catamorphism]

@catamorphism Would it be possible for you to replace the expressions like {e1} and patterns like {p} in the above with valid syntax? I'm getting rather lost in trying to figure out what each might mean, end e.g. can't tell what the difference is between examples 5 and 6.

Sure, I edited it -- let me know if it makes sense now.

[catamorphism]

This is not necessarily a valid premise, and I don't think we've explicitly established any explicit preference or requirement for laziness or eagerness in the spec at least so far. In fact, we've gone out of way to ensure that either approach is valid.

I'm assuming, perhaps wrongly, that if the difference between laziness and eagerness is observable, then the spec has to require either laziness or eagerness (there are really (at least) three options: call-by-value (eager), call-by-name (lazy with substitution), and call-by-need (lazy with memoization). That is: when the difference between laziness and eagerness is observable, the spec dictates which behavior the implementation has to produce. (Of course an implementation could simulate laziness with eagerness, or vice versa, if it wanted to, as long as the observable result is the same.)

There are two ways the difference could be observable:
a. The same message formats to a different string (without loss of generality I'm assuming "formatting to a string" rather than "formatting to parts" for the sake of this discussion) depending on the evaluation strategy.
b. For the same message, the formatter processes it with no errors under one evaluation strategy, but emits errors under a different evaluation strategy.

I'm assuming the spec has to be precise enough to rule out both (1) and (2).

Example 1 falls into category (a): with either call-by-value or call-by-name, the result is func('foo'); with call-by-need, the result is 42.

An example that falls into category (b) is:

Example 7:

let $v1 = {$oops}
{foo}

Assuming no externally defined variables: under call-by-value, an "Unresolved Variable" error is emitted because $oops is not defined. Under either call-by-name or call-by-need, no errors are emitted because $v1 is never referenced.

So if it's a requirement to avoid category (a) ambiguities, then the spec does have to require observably call-by-value, call-by-name, or call-by-need semantics. If the single-assignment property is enforced (either requiring all let-defined names to be unique, or not allowing multiple set-assignments to the same variable, depending on the chosen syntax), then that makes the difference between call-by-name and call-by-need unobservable for category (a) ambiguities.

Even with the single-assignment property, call-by-name and call-by-need are still distinguishable for messages in category (b) -- for example:

Example 8:

let $v1 = {$oops}
{{$v1} {$v1}}

In an implementation that emits all errors, call-by-name means this emits two "Unresolved Variable" errors since the body is equivalent to {{$oops} {$oops}}. Call-by-need means it only emits one error, since {$oops} is evaluated exactly once.

Maybe category (b) isn't important since the spec implies that implementations aren't required to report more than one error in a given message.

I'm assuming category (a) is important, since if two different implementations can format the same message with the same arguments and function registry (with observationally equivalent implementations of all the functions) to different strings and both be spec-compliant, that seems undesirable to me. But maybe that assumption isn't shared.

[catamorphism]

With that as a starting point, the declarations of your first example

set $v1 = {foo :func}
set $v2 = {$v1}
set $v3 = {$v1}
set $v1 = {42}
{{$v2}}

would modify the formatting context variable mapping as follows:

0. Start with an empty set {}
1. After set $v1 = {foo :func} we have { v1: func('foo') }
2. After set $v2 = {$v1} we have { v1: func('foo'), v2: func('foo') }
3. After set $v3 = {$v1} we have { v1: func('foo'), v2: func('foo'), v3: func('foo') }
4. After set $v1 = {42} we have { v1: '42', v2: func('foo'), v3: func('foo') }

And so during the pattern formatting, {$v2} would get its value for func('foo').

Not necessarily. In a call-by-need implementation, the "resolved values" are thunks (closures paired with environments), and as I outlined in the first comment, the result is 42, not func('foo'). The thunk created when evaluating $v2 contains a reference to the contents of $v1 -- {foo :func} can't be fully evaluated before creating this thunk. If it was, then the implementation would be using call-by-value semantics (eager evaluation). The reference to $v1 means whatever the name $v1 means when the thunk is invoked, not when it's created. In the absence of mutation, the meaning of $v1 never changes and so there's no difference. This is why call-by-need doesn't interact well with mutation: it sneaks dynamic scope in through the back door.

If the observable difference between call-by-need and call-by-name implementations is undesirable, then the spec has to either specify what the "resolved values" are, concretely; or be more detailed about requiring either call-by-value or call-by-name (but not call-by-need) semantics.

[eemeli]

There are two ways the difference could be observable:
a. The same message formats to a different string (without loss of generality I'm assuming "formatting to a string" rather than "formatting to parts" for the sake of this discussion) depending on the evaluation strategy.
b. For the same message, the formatter processes it with no errors under one evaluation strategy, but emits errors under a different evaluation strategy.

I'm assuming the spec has to be precise enough to rule out both (a) and (b).

The assumption about (b) is currently false, given the paragraph in Error Handling that I referenced in my previous comment.

Even with the single-assignment property, call-by-name and call-by-need are still distinguishable for messages in category (b) -- for example:

Example 8:

let $v1 = {$oops}
{{$v1} {$v1}}

In an implementation that emits all errors, call-by-name means this emits two "Unresolved Variable" errors since the body is equivalent to {{$oops} {$oops}}. Call-by-need means it only emits one error, since {$oops} is evaluated exactly once.

Maybe category (b) isn't important since the spec implies that implementations aren't required to report more than one error in a given message.

That's correct. For messages that include multiple errors, we do not specify which of them would be emitted, or really any errors beyond the first.

I'm assuming category (a) is important, since if two different implementations can format the same message with the same arguments and function registry (with observationally equivalent implementations of all the functions) to different strings and both be spec-compliant, that seems undesirable to me. But maybe that assumption isn't shared.

This I agree with, and that's why I've been trying to resolve our current ambiguity by clarifying the spec text as in #381 or my previous comment to make it clear how variable resolution works.

[...] The thunk created when evaluating $v2 contains a reference to the contents of $v1 -- {foo :func} can't be fully evaluated before creating this thunk. If it was, then the implementation would be using call-by-value semantics (eager evaluation).

My intent with our current spec language has been to enforce what I understand you refer to as "call-by-value", but this is admittedly unfortunately vague with respect to variable resolution. Specifically, regarding a declaration let $v2 = {$v1}, we have:

message-format-wg/spec/formatting.md

Lines 70 to 71 in 4a1e367

	In a _declaration_, the resolved value of the _expression_ is assigned to a _variable_,
	which may then be used in other _expressions_.

message-format-wg/spec/formatting.md

Lines 97 to 99 in 4a1e367

	- If the _expression_ contains no _annotation_,
	its resolved value is determined by _literal resolution_ or _variable resolution_,
	depending on the shape of the _operand_.

message-format-wg/spec/formatting.md

Lines 123 to 125 in 4a1e367

	To resolve the value of a _variable_,
	its _name_ is used to identify either a local variable,
	or a variable defined elsewhere.

message-format-wg/spec/formatting.md

Lines 129 to 130 in 4a1e367

	It is an error for a local variable definition to
	refer to a local variable that's defined after it in the message.

This is intended to mean that the variable $v1 is resolved to whatever value it holds without consideration of the current declaration or any later declaration, and that value is then assigned to $v2. After this declaration, the value of $v2 is no longer influenced by any potential changes in $v1, as the variable lookup has already taken place.

If the observable difference between call-by-need and call-by-name implementations is undesirable, then the spec has to either specify what the "resolved values" are, concretely; or be more detailed about requiring either call-by-value or call-by-name (but not call-by-need) semantics.

I think the simplest choice that does not prohibit mutability is to define the spec in terms of an eager call-by-value approach, while ensuring that a compliant implementation may choose to internally follow lazy call-by-name semantics instead. This is why the Error Handling includes the MAY statement about ignoring errors in unused variables.

Is anyone advocating that we should follow call-by-need semantics?

[stasm]

Thanks, @catamorphism, for the in-depth analysis.

I'm assuming, based on #299, that the formatting spec will eventually specify some form of lazy evaluation for local variables.

Perhaps we were too quick to dismiss eager evaluation. I just commented about this in #299 (comment).

I think the simplest choice that does not prohibit mutability is to define the spec in terms of an eager call-by-value approach, while ensuring that a compliant implementation may choose to internally follow lazy call-by-name semantics instead.

This sound reasonable to me.