Generic let with auto?

[josh11b]

Proposal #950 defines generic let in a function body as a way to create an erased type. let T:! C = U defines T to be U erased to have the API of the constraint C. What is the behavior when the constraint is replaced with auto?

Simple case:

let X:! T = ...;
let Y:! auto = X;

In this case, the auto should clearly mean T, the type of X.

What about these other cases where the type isn't as clear?

// Value is a literal
let K:! auto = 4;
// Value is a type
let T:! auto = Array(i32, 4);
// Value is a constraint or type-of-type
let C:! auto = Movable & Hashable;

In particular, this last case came up in #950 since I wasn't sure how to give a name to a constraint expression. Could C be used in place of Movable & Hashable with the exact same meaning? What type does auto mean here? Does any erasing happen? I thought I might have to write let template C:! auto = Movable & Hashable to make something that didn't do any erasing, but I am not at all sure.

[josh11b]

Talking with @chandlerc , it seemed like let X:! auto = Y should be referentially transparent, and so there might not be a need for let template. This means we would allow things like:

let T:! auto = Array(i32, 4);
let a: T = (1, 2, 3, 4);

and

fn F[template T:! Type](x: T) {
  let U:! auto = T.IteratorType;
  let iter:! U = x.Begin();
}

[chandlerc]

It seems like we're experimenting effectively with let X:! auto = Y being referentially transparent as @josh11b described. It isn't clear we need to make a more firm decision on this.

What do folks think about deferring the issue for now, or resolving it with that answer and letting it be re-opened if needed in the future?

[chandlerc]

Talked with @josh11b about this, and it doesn't seem urgent to really settle/decide this. There is a rough approach in the current design and the best way to make more progress is to revisit when we have experience to reflect on with the choice. Moving this to the "deferred" bucket.

[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]

I believe #144, #2153, and #2360 answer these questions.

The resolution of #2153 combined with the semantics of let matching the binding done in function calls is that let T:! auto = ... will make T a symbolic value and let template T:! auto = ... will make T a template value, independent of the expression phase of ... (except that the statement will be rejected unless the ... is compile-time).

#2360 defines the type of types like Array(i32, 4) and facet types like Movable & Hashable as type.

I believe the resolution of questions is:

• let K:! auto = 4; is answered by Numeric literal semantics #144: "For every integer, there is a type representing literals with that integer value."
• let T:! auto = Array(i32, 4); is answered by Types are values of type type #2360: Array is a type so its type is type, so this is equivalent to let T:! type where .Self == Array(i32, 4) = Array(i32, 4);. By Checked generics calling templates #2153, T is a symbolic value, and so erases all API beyond type except that it may be converted to an Array(i32, 4), so let a: T = (1, 2, 3, 4); is illegal.
• let C:! auto = Movable & Hashable; is like the previous case, and so C may be used as a type, but the information about what constraints it implements are lost, except that it may be converted back to Movable & Hashable.

The last example:

fn F[template T:! Type](x: T) {
  let U:! auto = T.IteratorType;
  let iter:! U = x.Begin();
}

looks like it would be allowed since U would have type type where .Self == T.IteratorType, but other uses of iter are not likely to work.

[josh11b]

Discussing with @zygoloid , the let T:! Foo = Bar; shouldn't add the where .Self == Bar clause, but instead should do a observe T == Bar;

[chandlerc]

Discussing with @zygoloid , the let T:! Foo = Bar; shouldn't add the where .Self == Bar clause, but instead should do a observe T == Bar;

Would be good to capture somewhere the nuance of why and what the implications are of this... I find it both believable but also quite mysterious.

[josh11b]

The idea is that the ability to convert Bar values to T values isn't dependent on using auto, it is just a fact available to the compiler introduced by the let statement for use, like an observe declaration.

[josh11b]

The where .Self == bit was originally introduced in #950 and is documented here. See the alternatives considered which points to this discussion on Discord.

I think it makes sense to use observe to implement this mechanism, rather than reflecting it in the type. However, the where clause may still be needed when simulating a symbolic let using a function call.