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.

Sign up for GitHub

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

Jump to bottom

Update inference of closures with no context. #3151

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

Update inference of closures with no context. #3151

Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
8e27f3d
Update inference of closures with no context.
lrhn Jun 15, 2023
16190b7
Address comments. More details on Stream/Iterable.
lrhn Jun 26, 2023
87b0904
Tweak phrasing
lrhn Jun 26, 2023
a23e438
Use `_` as context type for async return instead of `FutureOr<_>`
lrhn Jun 26, 2023
e349009
Addressed comments.
lrhn Jul 21, 2023
90b9b73
Replace "enclosing function" with "function literal".
lrhn Aug 7, 2023
42dd5cf
Update inference.md
lrhn Mar 19, 2024
fe4b6b1
Update inference.md
lrhn Mar 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
214 changes: 150 additions & 64 deletions resources/type-system/inference.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,13 @@ Status: Draft

## CHANGELOG

2023.06.24
- Adjust function literal return type inference to avoid spurious application
of `flatten`, and make sure return statements do not affect generator
functions.
- Specify the value context to use for generator functions for more
non-trivial return types (not just `Iterable<X>` for some `X`).

2022.05.12
- Define the notions of "constraint solution for a set of type variables" and
"Grounded constraint solution for a set of type variables". These
Expand Down Expand Up @@ -260,11 +267,11 @@ unlike normal fields, the initializer for a `late` field may reference `this`.
Function literals which are inferred in an empty typing context (see below) are
inferred using the declared type for all of their parameters. If a parameter
has no declared type, it is treated as if it was declared with type `dynamic`.
Inference for each returned expression in the body of the function literal is
done in an empty typing context (see below).
Inference for each returned or yielded expression in the body of the function
literal is done with an empty _value context_ scheme (see below).

Function literals which are inferred in an non-empty typing context where the
context type is a function type are inferred as described below.
context type is a function type are inferred as described here.

Each parameter is assumed to have its declared type if present. If no type is
declared for a parameter and there is a corresponding parameter in the context
Expand All @@ -276,19 +283,21 @@ corresponding parameter in the context type schema, the variable is treated as
having type `dynamic`.

The return type of the context function type is used at several points during
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 context type derived from the imposed return
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:

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?

imposed return type schema `S` as follows:
- If function is declared `async`, then without null safety,
the value context scheme is **flatten**(`S`);
with null safety the value context scheme is
**futureValueTypeSchema**(`S`), as defined below.
- If the function expression is declared `async*` then the value context
scheme is **streamElementTypeSchema**(`S`), as defined below.
- If the function expression is declared `sync*` then the value context
scheme is **iterableElementTypeSchema**(`S`), as defined below.
- If the function expression is neither `async` nor a generator, then the
context type is `S`.
- If the function expression is declared `async*` and `S` is of the form
`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`.
- 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)>`.
value context scheme is `S`.

The function **futureValueTypeSchema** is defined as follows:

Expand All @@ -299,66 +308,143 @@ The function **futureValueTypeSchema** is defined as follows:
- **futureValueTypeSchema**(`void`) = `void`.
- **futureValueTypeSchema**(`dynamic`) = `dynamic`.
- **futureValueTypeSchema**(`_`) = `_`.
- Otherwise, for all `S`, **futureValueTypeSchema**(`S`) = `Object?`.

_Note that it is a compile-time error unless the return type of an asynchronous
non-generator function is a supertype of `Future<Never>`, which means that
the last case will only be applied when `S` is `Object` or a top type._
- Otherwise, for all other `S`, **futureValueTypeSchema**(`S`) = `Object?`.

The function **streamElementTypeSchema** is defined as follow:

- **streamElementTypeSchema**(`S?`) = **streamElementTypeSchema**(`S`),
leafpetersen marked this conversation as resolved.
Show resolved Hide resolved
for all `S`.
- **streamElementTypeSchema**(`S*`) = **streamElementTypeSchema**(`S`),
for all `S`.
- **streamElementTypeSchema**(`FutureOr<S>`) = **streamElementTypeSchema**(`S`),
leafpetersen marked this conversation as resolved.
Show resolved Hide resolved
for all `S`.
- **streamElementTypeSchema**(`Stream<S>`) = `S`, for all `S`.
- **streamElementTypeSchema**(`void`) = `void`
- **streamElementTypeSchema**(`dynamic`) = `dynamic`
- **streamElementTypeSchema**(`_`) = `_`
- Otherwise, for all other `S`, **streamElementTypeSchema**(`S`) = `Object?`.

The function **iterableElementTypeSchema** is defined as follow:

- **iterableElementTypeSchema**(`S?`) = **iterableElementTypeSchema**(`S`),
for all `S`.
- **iterableElementTypeSchema**(`S*`) = **iterableElementTypeSchema**(`S`),
for all `S`.
- **iterableElementTypeSchema**(`FutureOr<S>`) =
**iterableElementTypeSchema**(`S`), for all `S`.
- **iterableElementTypeSchema**(`Iterable<S>`) = `S`, for all `S`.
- **iterableElementTypeSchema**(`void`) = `void`
- **iterableElementTypeSchema**(`dynamic`) = `dynamic`
- **iterableElementTypeSchema**(`_`) = `_`
- Otherwise, for all other `S`, **iterableElementTypeSchema**(`S`) = `Object?`.

_Note that it is a compile-time error unless the return type of an
asynchronous non-generator function is a supertype of `Future<Never>`,
which means that the last case of **futureValueTypeScheme** will only
be applied when `S` is `Object`.
Similarly for `async*` and `sync*` functions whose return types
must be a supertypes of `Stream<Never>` and `Iterable<Never>`.
These requirements also prevent the return type from being a type variable._

In order to infer the return type of a function literal, we first infer the
**actual returned type** of the function literal.

The actual returned type of a function literal with an expression body is the
inferred type of the expression body, using the local type inference algorithm
described below with a typing context as computed above.

The actual returned type of a function literal with a block body is computed as
follows. Let `T` be `Never` if every control path through the block exits the
block without reaching the end of the block, as computed by the **definite
completion** analysis specified elsewhere. Let `T` be `Null` if any control
path reaches the end of the block without exiting the block, as computed by the
**definite completion** analysis specified elsewhere. Let `K` be the typing
context for the function body as computed above from the imposed return type
schema.
- 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 `K`, and update `T` to be `UP(flatten(S), T)` if the enclosing
function is `async`, or `UP(S, T)` otherwise.
- For each `return;` statement in the block, update `T` to be `UP(Null, T)`.
- 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 typing
context `K`, and update `T` to be `UP(S, T)`.
- If the enclosing function is marked `sync*`, 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
`Iterable<K>`; let `E` be the type such that `Iterable<E>` is a
super-interface of `S`; and update `T` to be `UP(E, T)`.
- 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)`.

The **actual returned type** of the function literal is the value of `T` after
all `return` and `yield` statements in the block body have been considered.

Let `T` be the **actual returned type** of a function literal as computed above.
**actual value type** of the function literal. _The actual value type
represents the types of the actual values returned by non-generator functions,
and the values emitted by generator functions._

Let `K` be the value context schema for the function body as computed above
from the imposed return type schema.
_When we refer to the inferred type of an expression with a typing context,
it is the static type of the expression inferred using the local type inference
algorithm described below._

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 function literal is marked `async`,
then let `T` be the inferred type of the returned expression with
`FutureOr<K>` as typing context.
The actual value type is **flatten**(`T`).
- If the function literal is not marked `async`, let `T` be the inferred
type of the returned expression with typing context `K`.
The actually value type is `T`.

The actual value type of a function literal with a block body is computed as
follows.
Let `T` be `Never` if the function is a generator function,
or if every control path through the block exits the block without
reaching the end of the block, as computed by the **definite completion**
analysis specified elsewhere.
Otherwise _(the function is a non-generator function and at least
one control path reaches the end of the block)_ let `T` be `null`.

Then process relevant statements of the block, one by one in source order,
to find a value type `V` for that statement.

- If the function literal is a non-`async` non-generator function,
the relevant statements are `return;` or `return e;` statements.
* For a `return;` statement, let `V` be `Null`.
* For a `return e;` statement, let `V` be the inferred type of `e` with
typing context `K`.

- If the function literal is marked `async`, the relevant statements
are `return;` and `return e;` statements.
* For a `return;` statement, let `V` be `Null`.
* For a `return e;` statement,
then let `S` be the inferred type of `e` with typing context
`FutureOr<K>`.
Let `V` be **flatten**(`S`).

- If the function literal is marked `sync*`, the relevant statements
are `yield e;` or `yield* e;` statement.
* For a `yield e;` statement, let `V` be the inferred type of `e` with
typing context `K`.
* For a `yield* e;` statement, let `S` be the inferred type of `e` with
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

`Iterable<Object?>`, so either `S` implements `Iterable`,
or it is one of `dynamic` or `Never`._

- If the function literal is marked `async*`, the relevant statements are
`yield e;` or `yield* e;` statements.
* For a `yield e;` statement, let `V` be the inferred type of `e` with
typing context `K`.
* For a `yield* e;` statement, let `S` be the inferred type of `e` with
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

`Stream<Object?>`, so either `S` implements `Stream`,
or it is one of `dynamic` or `Never`._

After processing each relevant statement, update `T` to be **UP**(`V`, `T`).

The **actual value type** of the function literal is the value of `T` after
all relevant statements in the block body have been processed.

Let `T` be the **actual value type** of a function literal as computed above.
Let `R` be the greatest closure of the typing context `K` as computed above.

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?

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?

by the typing context, if any._

With null safety, if `R` is `void`, let `S` be `void`
lrhn marked this conversation as resolved.
Show resolved Hide resolved
_(without null-safety: no special treatment is applicable to `void`)_.

Otherwise (_if `R` is not `void`, or without null safety_),
if `T <: R` then let `S` be `T`, else let `S` be `R`.

Otherwise, if `T <: R` then let `S` be `T`. Otherwise, let `S` be `R`. The
inferred return type of the function literal is then defined as follows:
The inferred return type of the function literal is then defined as follows:

- If the function literal is marked `async` then the inferred return type is
`Future<flatten(S)>`.
`Future<S>`.
- If the function literal is marked `async*` then the inferred return type is
`Stream<S>`.
- If the function literal is marked `sync*` then the inferred return type is
`Iterable<S>`.
- Otherwise, the inferred return type is `S`.
- Otherwise, _a synchronous non-generator function_, the inferred return
type is `S`.

## Local return type inference.

Expand Down