Implement generators #593

Aaron1011 · 2020-08-10T15:25:39Z

GeneratorDatum and GeneratorWitnessDatum are introduced, which
mirror TyKind::Generator and TyKind::GeneratorWitness in rustc.

We handle auto traits for GeneratorDatum using the existing
constituent_types method. For GeneratorWitnessDatum, we generate a
forall<'a, 'b, ... 'z> goal to reflect the fact that our lifetimes are
existentially bound.

Unresolved questions:

The implementation of GeneratorWitnessDatum needs careful review -
I'm not certain that I fully understand how Binders works.
The syntax implemented in parser.lalrpop can be bikesheeded. We
might want to use something other than for<> for the witness types,
to reflect that fact that we have existential rather than universal
quantification.
The generator grammar only allows quantifying over liftimes for the
witness types - however, this gets lowered to a Binders, which
supports types and constants as well. Should we do anything else
to ensure we never end up with types/consts where they're not
expected?
I added a test to ensure that we treat the witness lifetimes as
existentially quantified - for example, if we have
for<'a, 'b> Foo<'a, 'b>, we should only be able to use an auto
trait impl that is fully generic over lifetimes - e.g.
impl<'a> Send for Foo<'a, 'b> will not be used. I believe
that the test is showing this behavior - it ends up returning
region constraints that require 'a and 'b to outlive each other.
Since these are 'existential' lifetimes (which cannot be substituted),
this is an unsatisfiable constraint. However, I'm not sure where we
should be detecting that this is unsatisfiable.
In rustc, all of the existential witness lifetimes are distinct. This is not enforced by this PR e.g. you can repeat a lifetime in the witness type. I'm not sure if/where we should enforce this.

Aaron1011 · 2020-09-20T04:19:52Z

This is mostly working - however, I still need to figure out how to treat generator witness lifetime as existentially quantified when handling auto traits.

Aaron1011 · 2020-09-21T01:42:18Z

@jackh726 @nikomatsakis This is ready for review

`GeneratorDatum` and `GeneratorWitnessDatum` are introduced, which mirror `TyKind::Generator` and `TyKind::GeneratorWitness` in rustc. We handle auto traits for `GeneratorDatum` using the existing `constituent_types` method. For `GeneratorWitnessDatum`, we generate a `forall<'a, 'b, ... 'z>` goal to reflect the fact that our lifetimes are existentially bound. Unresolved questions: * The implementation of `GeneratorWitnessDatum` needs careful review - I'm not certain that I fully understand how `Binders` works. * The syntax implemented in `parser.lalrpop` can be bikesheeded. We might want to use something other than `for<>` for the witness types, to reflect that fact that we have existential rather than universal quantification. * The generator grammar only allows quantifying over liftimes for the witness types - however, this gets lowered to a `Binders`, which supports types and constants as well. Should we do anything else to ensure we never end up with types/consts where they're not expected? * I added a test to ensure that we treat the witness lifetimes as existentially quantified - for example, if we have `for<'a, 'b> Foo<'a, 'b>`, we should only be able to use an auto trait impl that is fully generic over lifetimes - e.g. `impl<'a> Send for Foo<'a, 'b>` will not be used. I *believe* that the test is showing this behavior - it ends up returning region constraints that require `'a` and `'b` to outlive each other. Since these are 'existential' lifetimes (which cannot be substituted), this is an unsatisfiable constraint. However, I'm not sure where we should be detecting that this is unsatisfiable.

jackh726 · 2020-09-22T17:09:07Z

I definitely don't know enough about generators to make a meaningful review of this, so will definitely have to defer to @nikomatsakis. However, the book builtin types table will need to be updated here.

Additionally, I really want to push for us to document generators and generator witnesses in the chalk book. I don't think it needs to be in this PR, but I am somewhat worried that if it isn't at least loosely documented here, it'll get pushed aside. Particularly, I feel like documenting this is super important since there's almost no documentation in the rustc dev guide or in the rustc codebase (that I can find).

Aaron1011 · 2020-09-22T17:10:32Z

I'll work on writing up some docs.

jackh726 · 2020-09-22T17:14:57Z

I'll work on writing up some docs.

Awesome!

I do want to stress that I understand docs can sometimes be hard to write. But I would definitely error on the side of "some docs are better than no docs" and "don't let perfect be the enemy of good enough"; we can always expand upon/clarify the docs in subsequent PRs.

nikomatsakis

This is great. I left a nit about the syntax but I'm inclined to land it.

nikomatsakis · 2020-09-29T21:08:25Z

book/src/types/rust_types/application_ty.md

+* Resume/yield/return types - the types produced/consumed by various generator methods.
+  These are not stored in the generator across yield points - they are only
+  used when the generator is running.
+* Generator witness - see the `Generator Witness` section below.


thank you for writing docs! wonderful.

nikomatsakis · 2020-09-29T21:10:44Z

book/src/types/rust_types/application_ty.md

+### Generator witness types
+
+The `GeneratorWitness` variant represents the generator witness of
+the generator with id `GeneratorId`. 


I think it'd be good to explain the purpose of a witness:

The witness type captures the types of all variables that may be live across a yield point.

I just moved this entire block from a different section of the book :) - I'm happy to expand on it.

nikomatsakis · 2020-09-29T21:22:51Z

chalk-solve/src/clauses.rs

+        // If we have `Foo<'a, 'b>` stored as a witness type, we will
+        // not currently use this information to determine a more precise
+        // relationship between 'a and 'b. In the future, we will likely
+        // do this to avoid incorrectly rejecting correct code.


Another great comment.

nikomatsakis · 2020-09-29T21:27:00Z

tests/test/generators.rs

+
+            generator send_any_lifetime<T>[resume = (), yield = ()] {
+                upvars []
+                witnesses for<'a, 'b> [SendAnyLifetime<'a, 'b, T>; u8]


the for syntax here seems a bit misleading, I guess?

Yeah, it's not great. Do you think exists<> would be better?

Aaron1011 · 2020-09-29T22:42:46Z

@nikomatsakis: I've addressed your comments

jackh726 · 2020-09-29T23:26:37Z

@bors r=nikomatsakis

bors · 2020-09-29T23:26:39Z

📌 Commit e7a0892 has been approved by nikomatsakis

bors · 2020-09-29T23:26:46Z

⌛ Testing commit e7a0892 with merge 8f28056...

bors · 2020-09-29T23:33:36Z

☀️ Test successful - checks-actions
Approved by: nikomatsakis
Pushing 8f28056 to master...

Aaron1011 force-pushed the feature/generators branch from f360594 to ab3efa5 Compare September 20, 2020 04:10

Aaron1011 force-pushed the feature/generators branch from 58b87d4 to 1c6ef1d Compare September 21, 2020 01:41

Aaron1011 marked this pull request as ready for review September 21, 2020 01:41

Aaron1011 changed the title ~~[WIP] Generators~~ Implement generators Sep 21, 2020

Aaron1011 force-pushed the feature/generators branch from 1c6ef1d to 457b8bb Compare September 21, 2020 01:44

Aaron1011 mentioned this pull request Sep 22, 2020

extend chalk TypeName with builtin types #368

Closed

18 tasks

Start working on some docs

905bb94

nikomatsakis approved these changes Sep 29, 2020

View reviewed changes

Aaron1011 added 2 commits September 29, 2020 18:41

Further explain witness types in book

b982f80

Define generator witness syntax to use exists<> instead of for<>

e7a0892

bors merged commit 8f28056 into rust-lang:master Sep 29, 2020

Aaron1011 mentioned this pull request Oct 3, 2020

create a "generator witness" type #504

Closed

jackh726 mentioned this pull request Oct 3, 2020

Generator followup work #618

Closed

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement generators #593

Implement generators #593

Aaron1011 commented Aug 10, 2020 •

edited

Loading

Aaron1011 commented Sep 20, 2020

Aaron1011 commented Sep 21, 2020

jackh726 commented Sep 22, 2020

Aaron1011 commented Sep 22, 2020

jackh726 commented Sep 22, 2020

nikomatsakis left a comment

nikomatsakis Sep 29, 2020

nikomatsakis Sep 29, 2020

Aaron1011 Sep 29, 2020

nikomatsakis Sep 29, 2020

nikomatsakis Sep 29, 2020

Aaron1011 Sep 29, 2020

Aaron1011 commented Sep 29, 2020

jackh726 commented Sep 29, 2020

bors commented Sep 29, 2020

bors commented Sep 29, 2020

bors commented Sep 29, 2020

Implement generators #593

Implement generators #593

Conversation

Aaron1011 commented Aug 10, 2020 • edited Loading

Aaron1011 commented Sep 20, 2020

Aaron1011 commented Sep 21, 2020

jackh726 commented Sep 22, 2020

Aaron1011 commented Sep 22, 2020

jackh726 commented Sep 22, 2020

nikomatsakis left a comment

Choose a reason for hiding this comment

nikomatsakis Sep 29, 2020

Choose a reason for hiding this comment

nikomatsakis Sep 29, 2020

Choose a reason for hiding this comment

Aaron1011 Sep 29, 2020

Choose a reason for hiding this comment

nikomatsakis Sep 29, 2020

Choose a reason for hiding this comment

nikomatsakis Sep 29, 2020

Choose a reason for hiding this comment

Aaron1011 Sep 29, 2020

Choose a reason for hiding this comment

Aaron1011 commented Sep 29, 2020

jackh726 commented Sep 29, 2020

bors commented Sep 29, 2020

bors commented Sep 29, 2020

bors commented Sep 29, 2020

Aaron1011 commented Aug 10, 2020 •

edited

Loading