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

Consistently use terminology "instance implementing" and "dynamic type". #3918

Closed
wants to merge 1 commit into from
Closed

Consistently use terminology "instance implementing" and "dynamic type". #3918

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
134 changes: 68 additions & 66 deletions resources/type-system/inference.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1026,15 +1026,15 @@ inference depends on the context `K`, as well as the flow analysis state._

A property of expression inference, known as _soundness_, is that when an
elaborated expression is executed, it is guaranteed either to diverge, throw an
exception, or evaluate to a value that is an _instance satisfying_ its static
type. _Instance satisfying_ is defined as follows: a value `v` is an instance
satisfying type `T` iff the runtime type of `v` is a subtype of the _extension
exception, or evaluate to a value that is an _instance implementing_ its static
type. _Instance implementing_ is defined as follows: a value `v` is an instance
Copy link
Member

@lrhn lrhn Jun 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

I think (checking ... and still think it!) that the spec uses "implements S" to mean "has S as super-interface" (or really: "is T-bounded for a T which implements S", which means having S as super-interface or is a type variable with a bound T which implements S (recurse as needed). Probably also a promoted type variable whose intersecting type implements S.)

That's different from "having as supertype" if the type is generic, so Future<int>.value(1) is an object with runtime type _Future<int> which has Future<int> as super-interface. It implements Future<int>. It does not implement Future<Object>, it just has that as a supertype.

So, (Future<int>.value(1) as Future<Object>) does not satisfy that its value's runtime type implements its static type.

For soundness, if an expression evaluates to a value, the runtime type of that value must be a subtype of the (extension-type-erased) static type of the expression. Using "implements" is likely wrong.

... there it was, in the "Superinterfaces" section:

When we say that a type $S$
\IndexCustom{implements}{type!implements a type}
another type $T$,
this means that $T$ is a superinterface of $S$,
or $S$ is $S_0$ bounded for some type $S_0$
(\ref{bindingActualsToFormals}),
and $T$ is a superinterface of $S_0$.
... snip implementing raw types ...

\commentary{%
Note that this is not the same as being a subtype.
For instance, \code{List<int>} implements \code{Iterable<int>},
but it does not implement \code{Iterable<num>}.
Similarly, \code{List<int>} implements \code{Iterable}.
Also, note that when $S$ implements $T$
where $T$ is not a subtype of \code{Null},
$S$ cannot be a subtype of \code{Null}.%
}

Copy link
Member Author

Choose a reason for hiding this comment

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

Ok, I see what you mean. Thanks for the explanation. I'm going to go ahead and abandon this PR and stick with the terminology "instance satisfying type T" in resources/type-system/inference.md.

implementing type `T` iff the dynamic type of `v` is a subtype of the _extension
type erasure_ of `T`. _So, for example, every value is considered an instance
satisfying type `dynamic`, and all values except `null` are considered an
instance satisfying type `Object`._
implementing type `dynamic`, and all values except `null` are considered an
Copy link
Member

Choose a reason for hiding this comment

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

(Since dynamic is not an interface, you can't have it as super-interface, so you can't implement it. But everything is a subtype of dynamic because it's a top type.)

instance implementing type `Object`._

_This stands in contrast to the notion of "instance of"; a value `v` is an
instance of a type `T` only if the runtime type of `v` is __precisely__ `T`._
instance of a type `T` only if the dynamic type of `v` is __precisely__ `T`._

_The type inference rules below include informal sketches of a proof that
soundness holds for each expression type. These are non-normative, so they are
Expand All @@ -1050,18 +1050,18 @@ succintly, the syntax of Dart is extended to allow the following forms:

- Evaluate `m_1`, and let `v` denote the result.

- If `v` is an instance satisfying type `Future<T>`, then
- If `v` is an instance implementing type `Future<T>`, then
`@AWAIT_WITH_TYPE_CHECK<T>(m_1)` evaluates to `v`.

- Otherwise, let `u` be a future satisfying type `Future<T>` that will
- Otherwise, let `u` be a future implementing type `Future<T>` that will
complete to the value `v` at some later point. Then,
`@AWAIT_WITH_TYPE_CHECK<T>(m_1)` evaluates to `u`.

- _TODO(paulberry): explain why such a future is guaranteed to (soundly)
exist, by stipulating that if `T_1` is the static type of `m_1`, then `T`
must be `flatten(T_1)`, and then proving a lemma that `T_1 <:
FutureOr<flatten(T_1)>`; therefore `T_1 <: FutureOr<T>`, so in this
"otherwise" case, `v` must be an instance satisfying `T`._
"otherwise" case, `v` must be an instance implementing `T`._

- `@CONCAT(m_1, m_2, ..., m_n)`, where each `m_i` is an elaborated expression
whose static type is a subtype of `String`, represents the operation of
Expand Down Expand Up @@ -1096,10 +1096,10 @@ succintly, the syntax of Dart is extended to allow the following forms:

- `@PROMOTED_TYPE<T>(m)` represents an elaborated expression whose runtime
behavior is the same as that of `m`, but where it is known that whenever the
elaborated expression executes, the resulting value is an instance satisfying
type `T`. _This is used in situations where additional reasoning, beyond the
static type of `m`, is required to establish soundness. Wherever this
construct is used, the additional reasoning follows in italics. Note that
elaborated expression executes, the resulting value is an instance
implementing type `T`. _This is used in situations where additional reasoning,
beyond the static type of `m`, is required to establish soundness. Wherever
this construct is used, the additional reasoning follows in italics. Note that
since `m` and `@PROMOTED_TYPE<T>(m)` have the same runtime behavior,
implementations can most likely elide `@PROMOTED_TYPE<T>(m)` to `m` without
any loss of functionality, provided they are not trying to construct a proof
Expand Down Expand Up @@ -1331,7 +1331,7 @@ immediately enclosing class, enum, mixin, or extension type, or the "on" type of
the immediately enclosing extension.

_The runtime behavior of `this` is to evaluate to the target of the current
instance member invocation, which is guaranteed to be an instance satisfying
instance member invocation, which is guaranteed to be an instance implementing
this type. So soundness is satisfied._

### Logical boolean expressions
Expand Down Expand Up @@ -1361,7 +1361,7 @@ _The runtime behavior of logical boolean expressions is to evaluate to a value
equal to their first argument (in the case of a short-cut) or their second
argument (in the case of no short-cut). Since the static type of `m_1` and `m_2`
are guaranteed to be a subtype of `bool`, it follows that the the logical
boolean expression will evaluate to an instance satisfying type `bool`, so
boolean expression will evaluate to an instance implementing type `bool`, so
soundness is satisfied._

### Await expressions
Expand Down Expand Up @@ -1399,13 +1399,14 @@ are determined as follows:

- _For soundness, we must prove that whenever
`@AWAIT_WITH_TYPE_CHECK<T_2>(m_1)` evaluates `m_1` to a value `v` that is
__not__ an instance satisfying type `Future<T_2>`, that `v` __is__ an
instance satisfying type `T_2`. This is necessary to ensure that the future
created by `@AWAIT_WITH_TYPE_CHECK` will complete to a value satisfying its
type signature. Note that `v` is guaranteed to be an instance satisfying
type `T_1` (because `T_1` is the static type of `m_1`). So we can establish
soundness by assuming that `v` is an instance satisfying type `T_1` and not
an instance satisfying type `Future<T_2>`, and then considering two cases:_
__not__ an instance implementing type `Future<T_2>`, that `v` __is__ an
instance implementing type `T_2`. This is necessary to ensure that the
future created by `@AWAIT_WITH_TYPE_CHECK` will complete to a value
implementing its type signature. Note that `v` is guaranteed to be an
instance implementing type `T_1` (because `T_1` is the static type of
`m_1`). So we can establish soundness by assuming that `v` is an instance
implementing type `T_1` and not an instance implementing type `Future<T_2>`,
and then considering two cases:_

- _TODO(paulberry): it should be possible to simplify and clarify this
section once we have proven that `T <: FutureOr<flatten(T)>` for all types
Expand All @@ -1416,73 +1417,74 @@ are determined as follows:

- _If `T_1` is of the form `Null` or `dynamic`, then by the definition of
`flatten`, `T_2` must be the same as `T_1`. Therefore, `v` is an
instance satisfying type `T_2`, so soundness is satisfied._
instance implementing type `T_2`, so soundness is satisfied._

- _If `T_1` is of the form `S*` or `S?`, then by the definition of
`flatten`, `T_2` must be of the form `flatten(S)*` or `flatten(S)?`,
respectively. `null` is an instance satisfying all types ending in `*`
respectively. `null` is an instance implementing all types ending in `*`
and `?`, so soudness is satisfied._

- _Otherwise, we need to show that if `v` is a non-null instance satisfying
type `T_1`, but not an instance satisfying type `Future<T_2>`, then `v` is
an instance satisfying type `T_2`._
- _Otherwise, we need to show that if `v` is a non-null instance
implementing type `T_1`, but not an instance implementing type
`Future<T_2>`, then `v` is an instance implementing type `T_2`._

- _Substituting in the definition of `T_2`, we need to show that if `v` is a
non-null instance satisfying type `T_1`, but not an instance satisfying
type `Future<flatten(T_1)>`, then `v` is an instance satisfying type
`flatten(T_1)`. We can prove this by induction on `T_1`:_
non-null instance implementing type `T_1`, but not an instance
implementing type `Future<flatten(T_1)>`, then `v` is an instance
implementing type `flatten(T_1)`. We can prove this by induction on
`T_1`:_

- _If `T_1` is `S?`, then `flatten(T_1)` is `flatten(S)?`. We need to show
that if `v` is a non-null instance satisfying type `S?`, but not an
instance satisfying type `Future<flatten(S)?>`, then `v` is an instance
satisfying type `flatten(S)?`. Assuming `v` is a non-null instance
satisfying type `S?`, it must be a non-null instance satisfying type
`S`. Assuming `v` is not an instance satisfying type
`Future<flatten(S)?>`, it follows that `v` is not an instance satisfying
type `Future<flatten(S)>`. So we have satisfied the premise of the
induction hypothesis using `T_1 = S`, and therefore by induction, `v` is
an instance satisfying type `flatten(S)`. This in turn implies that `v`
is an instance satisfying type `flatten(S)?`._
that if `v` is a non-null instance implementing type `S?`, but not an
instance implementing type `Future<flatten(S)?>`, then `v` is an
instance implementing type `flatten(S)?`. Assuming `v` is a non-null
instance implementing type `S?`, it must be a non-null instance
implementing type `S`. Assuming `v` is not an instance implementing type
`Future<flatten(S)?>`, it follows that `v` is not an instance
implementing type `Future<flatten(S)>`. So we have satisfied the premise
of the induction hypothesis using `T_1 = S`, and therefore by induction,
`v` is an instance implementing type `flatten(S)`. This in turn implies
that `v` is an instance implementing type `flatten(S)?`._

- _(Same argument but with `?` replaced by `*`): If `T_1` is `S*`, then
`flatten(T_1)` is `flatten(S)*`. We need to show that if `v` is a
non-null instance satisfying type `S*`, but not an instance satisfying
type `Future<flatten(S)*>`, then `v` is an instance satisfying type
`flatten(S)*`. Assuming `v` is a non-null instance satisfying type `S*`,
it must be a non-null instance satisfying type `S`. Assuming `v` is not
an instance satisfying type `Future<flatten(S)*>`, it follows that `v`
is not an instance satisfying type `Future<flatten(S)>`. So we have
satisfied the premise of the induction hypothesis using `T_1 = S`, and
therefore by induction, `v` is an instance satisfying type
`flatten(S)`. This in turn implies that `v` is an instance satisfying
type `flatten(S)*`._
non-null instance implementing type `S*`, but not an instance
implementing type `Future<flatten(S)*>`, then `v` is an instance
implementing type `flatten(S)*`. Assuming `v` is a non-null instance
implementing type `S*`, it must be a non-null instance implementing type
`S`. Assuming `v` is not an instance implementing type
`Future<flatten(S)*>`, it follows that `v` is not an instance
implementing type `Future<flatten(S)>`. So we have satisfied the premise
of the induction hypothesis using `T_1 = S`, and therefore by induction,
`v` is an instance implementing type `flatten(S)`. This in turn implies
that `v` is an instance implementing type `flatten(S)*`._

- _If `T_1` is `FutureOr<S>`, then `flatten(T_1)` is `S`. We need to show
that if `v` is a non-null instance satisfying type `FutureOr<S>`, but
not an instance satisfying type `Future<S>`, then `v` is an instance
satisfying type `S`. This is trivially true, because `FutureOr<S>` is
that if `v` is a non-null instance implementing type `FutureOr<S>`, but
not an instance implementing type `Future<S>`, then `v` is an instance
implementing type `S`. This is trivially true, because `FutureOr<S>` is
the union of types `S` and `Future<S>`._

- _If `T_1 <: Future`, then `flatten(T_1)` is `S`, where `S` is a type
such that `T_1 <: Future<S>` and for all `R`, if `T_1 <: Future<R>` then
`S <: R`. We need to show that if `v` is a non-null instance satisfying
type `T_1`, but not an instance satisfying type `Future<S>`, then `v` is
an instance satisfying type `S`. Assuming `v` is a non-null instance
satisfying type `T_1`, it must also be a non-null instance satisfying
type `Future<S>` (because `T_1 <: Future<S>`). But this contradicts the
assumption that `v` is __not__ an instance satisfying type `Future<S>`,
so this case is impossible._
`S <: R`. We need to show that if `v` is a non-null instance
implementing type `T_1`, but not an instance implementing type
`Future<S>`, then `v` is an instance implementing type `S`. Assuming `v`
is a non-null instance implementing type `T_1`, it must also be a
non-null instance implementing type `Future<S>` (because `T_1 <:
Future<S>`). But this contradicts the assumption that `v` is __not__ an
instance implementing type `Future<S>`, so this case is impossible._

- _Finally, if none of the above cases are satisfied, then `flatten(T_1)`
is `T_1`. We need to show that if `v` is a non-null instance satisfying
type `T_1`, but not an instance satisfying type `Future<T_1>`, then `v`
is an instance satisfying type `T_1`. This is trivially true, since if
`v` is a non-null instance satisfying type `T_1`, it must be an instance
satisfying type `T_1`._
is `T_1`. We need to show that if `v` is a non-null instance
implementing type `T_1`, but not an instance implementing type
`Future<T_1>`, then `v` is an instance implementing type `T_1`. This is
trivially true, since if `v` is a non-null instance implementing type
`T_1`, it must be an instance implementing type `T_1`._

- Let `T` be `T_2`, and let `m` be `await m_2`. _Since `m_2` has static type
`Future<m_2>`, the value of `await m_2` must necessarily be an instance
satisfying type `T_2`, so soundness is satisfied._
implementing type `T_2`, so soundness is satisfied._

<!--

Expand Down
4 changes: 2 additions & 2 deletions specification/dartLangSpec.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7759,7 +7759,7 @@ \subsection{Super-Bounded Types}
all types of the form \code{C<$S$>}
(noting that all types must be regular-bounded
when we do not have the notion of super-bounded types).
So if we wish to allow a variable to hold any instance ``of type \code{C}''
So if we wish to allow a variable to hold any instance ``implementing type \code{C}''
Copy link
Member

Choose a reason for hiding this comment

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

So this should be
"any instance whose dynamic type is a subtype of \code{C}"

then that variable must use \code{Object} or another top type
as its type annotation,
which means that a member like \code{next} is not known to exist
Expand Down Expand Up @@ -22495,7 +22495,7 @@ \subsection{Type FutureOr}

\rationale{%
The \code{FutureOr<$T$>} type represents a case where an object can be
either an instance of the type $T$
either an instance implementing the type $T$
Copy link
Member

@lrhn lrhn Jun 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

an instance whose dynamic type is a subtype of $T$

or the type \code{Future<$T$>}.
Such cases occur naturally in asynchronous code.
The available alternative would be to use a top type (e.g., \DYNAMIC{}),
Expand Down