Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generic let with auto? #996

Open
josh11b opened this issue Dec 20, 2021 · 9 comments
Open

Generic let with auto? #996

josh11b opened this issue Dec 20, 2021 · 9 comments
Labels
leads question A question for the leads team long term Issues expected to take over 90 days to resolve.

Comments

@josh11b
Copy link
Contributor

josh11b commented Dec 20, 2021

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
Copy link
Contributor Author

josh11b commented Jan 6, 2022

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
Copy link
Contributor

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
Copy link
Contributor

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
Copy link

github-actions bot commented Jul 2, 2022

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.

@github-actions github-actions bot added the inactive Issues and PRs which have been inactive for at least 90 days. label Jul 2, 2022
@jonmeow jonmeow added leads question A question for the leads team long term Issues expected to take over 90 days to resolve. and removed inactive Issues and PRs which have been inactive for at least 90 days. labels Aug 10, 2022
@josh11b
Copy link
Contributor Author

josh11b commented Sep 18, 2023

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
Copy link
Contributor Author

josh11b commented Sep 18, 2023

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
Copy link
Contributor

chandlerc commented Sep 18, 2023

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
Copy link
Contributor Author

josh11b commented Sep 18, 2023

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
Copy link
Contributor Author

josh11b commented Sep 18, 2023

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.

github-merge-queue bot pushed a commit that referenced this issue Oct 3, 2023
Continued from part 1: #3231. Second step updating
`docs/design/generics/details.md`. There remains some work to
incorporate proposal #2200.

- The biggest changes are incorporating much of the text of proposals:
  - #2173
  - #2687
- It incorporates changes from proposals:
  - #989
  - #1178
  - #2138
  - #2200
  - #2360
  - #2964
  - #3162
- It also updates the text to reflect the latest thinking from leads
issues:
  - #996
  - #2153 -- most notably deleting the section on `TypeId`.
- Update to rule for prioritization blocks with mixed type structures
from [discussion on
2023-07-18](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.7jxges9ojgy3)
- Adds reference links to proposals, issues, and discussions relevant to
the text.
- Also tries to use more precise language when talking about
implementations, to avoid confusing `impl` declaration and definitions
with the `impls` operator used in `where` clauses, an issue brought up
in
  - #2495 
  - #2483

---------

Co-authored-by: Richard Smith <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
leads question A question for the leads team long term Issues expected to take over 90 days to resolve.
Projects
None yet
Development

No branches or pull requests

3 participants