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

Update inference of closures with no context. #3151

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Conversation

lrhn
Copy link
Member

@lrhn lrhn commented Jun 15, 2023

Issue #3148 showed that we need to adjust the rules about function literal return type inference. This PR changes the rules accordingly.

Refactors to add the FutureOr to the context type in the individual return statements for async functions, rather than add it to the context type scheme for the function. This simplifies the rules later, but requires splitting async and plain functions. (Well, doesn't require, but most of the text would be by-case anyway.)

Also make it clear that return statements, or reaching the end of the body, does not affect the element types of generators.

@lrhn lrhn requested a review from eernstg June 15, 2023 11:20
Copy link
Member

@eernstg eernstg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

I like the fact that it is simpler because K is consistently the less complex type (it is the candidate future value type schema for an async function, the element type schema for a generator, and the return type schema for other functions), and this means that several parts of the text are simplified textually, and easier to read.

We do need to handle cases where a generator function has an imposed return type schema which is not just Stream<...> respectively Iterable<...>. For instance, nothing prevents the imposed return type schema from being Stream<int>? or void.

So that calls for some adjustments before the existing changes.

Otherwise I think it would work!

resources/type-system/inference.md Outdated Show resolved Hide resolved
resources/type-system/inference.md Outdated Show resolved Hide resolved
resources/type-system/inference.md Outdated Show resolved Hide resolved

Otherwise, if `T <: R` then let `S` be `T`. Otherwise, let `S` be `R`. The
Otherwise (_without null safety or if `R` is not `void`_),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Otherwise (_without null safety or if `R` is not `void`_),
Otherwise (_when `R` is not `void`_),

Copy link
Member Author

@lrhn lrhn Jul 21, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then we haven't specified S if R is void and without null safety.

We have one clause:
If (with null safety && R is void): S = void
And an otherwise, which should cover everything else:

  • with null safety && R is not void
  • without null safety (whatever R is)
    (aka "R is not void, or without null safety ")

resources/type-system/inference.md Show resolved Hide resolved
@@ -286,9 +291,9 @@ type schema `S` as follows:
`Stream<S1>` for some `S1`, then the context type is `S1`.
- If the function expression is declared `sync*` and `S` is of the form
`Iterable<S1>` for some `S1`, then the context type is `S1`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the imposed context type schema is Stream<int>? or Object (or a number of other types that aren't of the form Stream<S1> for any S1) then we do not get a binding of S1 here.

We already have the notion of 'the element type of a generator', so we'd need 'the element type of a type'. This would be S for any type of the form Stream<S>, Stream<S>?, Iterable<S>, Iterable<S>?, and it would be Object? for any other type. A generator function is a compile-time error unless it has a return type which is a supertype of Iterable<Never> resp. Stream<Never>, but the context type could be anything, and it could also be dynamic or void or Stream<int>? and so on.

This is going to give us a better context type for generators.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case, we want the element type schema, given a context type schema C.

The stream element type schema would then be:

  • If C is C'?, then the stream element type schema of C'
  • If C is FutureOr<C'> then the stream element type schema of C'.
  • If C is Stream<C'> then C'
  • Otherwise it's the schema _.

(Basically look at possible supertypes of Stream<Something>, ignore the parts of union types which contribute nothing, if we find Stream<Something>, use Something, otherwise use _. If we find a type which is not a supertype of Stream<Never>, it's going to separtely be reported as an error).

We don't need to go to Object? yet. If we find a good element candidate type by looking at the yields, we can use that. If not, we'll have to convert _ to a type to decide the return type, and I'm guessing the greatest closure of _ is Object?.

Same for iterable.

context `K`, and update `T` to be `UP(S, T)`.
- If the enclosing function is marekd `async`, for each `return e;` statement
in the block, let `S` be the inferred type of `e`, using the local type
inference algorithm described below with typing context `FutureOr<K>`,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this is quite right. You only want to use FutureOr<K> when K is not empty. That is, the way that this was specified before, I think () async { return e; } would infer e using _ as the context, whereas as written I think this implies that you use FutureOr<_> as the typing context. I believe this can be observable.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh wonders! :)

OK, so if K is not _, use FutureOr<K> as context type schema for e, otherwise use _.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it a problem to use FutureOr<_>, or is it just a difference. (We probably don't want a difference either, just want to make sure I'm not missing something problematic.)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(But fixed, uses _ as context type instead of FutureOr<_>).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, no. The speified context type for the async function case was:

Otherwise, without null safety, the context type is FutureOr<flatten(T)>
where T is the imposed return type schema; with null safety, the context
type is FutureOr<futureValueTypeSchema(S)>.

There's always a FutureOr in there, and if the imposed type scheme was _, then so is its flatten or futureValueTypeScheme, so the context type will be FutureOr<_>.

I don't know if that's what we're doing, but it is what we were specifiying.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused - I don't see where this happens. The text seems to uniformly infer return e in a context of FutureOr<K>, which means when K is _, it will infer it using FutureOr<_> no?

`Iterable<K>`. If there exists a type `E` such that `Iterable<E>` is a
super-interface of `S`, update `T` to be `UP(E, T)`. Otherwise update
`T` to be `UP(S, T)`.
_It is a compile-time error if *S* is not a assignable to
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems reasonable, the previous behavior was underspecified. Note that the analyzer and the CFE currently disagree here, so there is an implementation change implied. Test case to reveal the difference:

void main() {
  var f = () sync* {
    yield* (throw "hello");
  };
  int x = f();
  var g = () sync* {
    yield* (3 as dynamic);
  };
  int y = g();
}

Copy link
Member Author

@lrhn lrhn Jun 26, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At least the thing we're changing to would be more permissive, and match current compilers.

The current implementation is blatantly unsafe in other ways, so something will have to change anyway.
I've added more changes to the specification to cover those, so I'll include that in the change request.

- If the enclosing function is marked `async*`, then for each `yield* e;`
statement in the block, let `S` be the inferred type of `e`, using the
local type inference algorithm described below with a typing context of
`Stream<K>`; let `E` be the type such that `Stream<E>` is a super-interface
of `S`; and update `T` to be `UP(E, T)`.
`Stream<K>`. If there exists a type `E` such that `Stream<E>` is a
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would validate whether this implies an implementation change, as above.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With the more added changes, it does. Probably for the better ("more sound").

@leafpetersen
Copy link
Member

This looks reasonable to me, modulo some comments/corrections. We will need to file a breaking change request, write tests, and file some implementation issues.

@lrhn
Copy link
Member Author

lrhn commented Jun 26, 2023

Updated to account for =>-bodies.
Also update to compute a correct and valid "context type" for, e.g., a sync* function with context type FutureOr<Iterable<int>?>, which should be returning an Iterable<int>.

(That should also be the returned iterable type for a function with that as declared return type.)

@github-actions
Copy link

Visit the preview URL for this PR (updated for commit b9fe42d):

https://dart-specification--pr3151-lrn-inference-fix-4k6m67b7.web.app

(expires Fri, 28 Jul 2023 14:45:53 GMT)

🔥 via Firebase Hosting GitHub Action 🌎

Sign: 6941ecd630c4f067ff3d02708a45ae0f0a42b88a

@lrhn
Copy link
Member Author

lrhn commented Jul 21, 2023

Bad rebase!

@eernstg
Copy link
Member

eernstg commented Jul 24, 2023

Bad rebase!

Ah, so that's the reason why it adds extension-types/feature-specification.md.


The actual value type of a function literal with an expression body, `=> e`,
_(which cannot be a generator function)_ is computed as follows:
- If the enclosing function is marked `async`,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think "enclosing function" is ambiguous here - I think you mean "function which encloses e", but the text also supports a reading as "function which encloses the function literal".

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agree. Changed to "the function literal".

@eernstg
Copy link
Member

eernstg commented Jul 25, 2023

Maybe force-push the state of this PR at a commit which precedes the bad rebase?

I'm assuming that several modified files should simply not be modified by this PR (e.g., accepted/future-releases/extension-types/feature-specification.md, specification/dart.sty, specification/dartLangSpec.tex, working/1426-extension-types/feature-specification-inline-classes.md, working/macros/example/analysis_options.yaml, working/macros/example/benchmark/simple.dart, and several others).

Copy link
Member

@leafpetersen leafpetersen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. I'm mildly worried about unexpected behavior changes. Can we aim to have a small set of tests that capture the behavior changes that we expect from this, and then communicate that any other test changes should be punted to us for review?

inference. We refer to this type as the **imposed return type schema**.

Inference for each returned or yielded expression in the body of the
function literal is done using a **value context** type scheme derived from the
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

type scheme -> type schema?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also numerous scheme -> schema below?

type schema `S` as follows:
inference. We refer to this type as the **imposed return type schema**.

Inference for each returned or yielded expression in the body of the
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This phrasing confused me slightly, because I wasn't sure if you were introducing a new kind of thing, called a "value context type schema", or whether you were introducing a definition of a specific type schema, referred to as the "value context type schema". I think it's the latter, right? So I might phrase this something like:

Inference for each returned or .... is done using a type schema derived from the imposed return type schema.  We refer to this type schema as the **value context** type schema, and derive it from the return type schema `S` as follows:

resources/type-system/inference.md Show resolved Hide resolved
Then process relevant statements of the block, one by one in source order,
to find a value type `V` for that statement.

- If the funtion literal is a non-`async` non-generator function,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

funtion -> function

typing context `Iterable<K>`.
If `S` implements `Iterable<R>` for some `R`, let `V` be `R`.
Otherwise let `V` be `S`.
_It is a compile-time error if `S` is not a assignable to
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not a assignable -> not assignable

typing context `Stream<K>`.
If `S` implements `Stream<R>` for some `R`, let `V` be `R`.
Otherwise let `V` be `S`.
_It is a compile-time error if `S` is not a assignable to
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not a assignable -> not assignable

With null safety: if `R` is `void`, or the function literal is marked `async`
and `R` is `FutureOr<void>`, let `S` be `void` (without null-safety: no special
treatment is applicable to `void`).
_Then compute the actual value/element type, `S`, to use in the inferred return
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is the first time element type is mentioned in this doc. If you're going to use it define it, but maybe better to just delete?

and `R` is `FutureOr<void>`, let `S` be `void` (without null-safety: no special
treatment is applicable to `void`).
_Then compute the actual value/element type, `S`, to use in the inferred return
type of the function literal, based on the actual value type, but bounded
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This comment is confusing to me. You say something like "compute X, to use in Y, based on X, but bounded by Z". I think the two Xs above are meant to be different, so use different terminology?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants