Consistently use terminology "instance implementing" and "dynamic type". #3918
Conversation
In the code review discussion #3850 (comment), we agreed to use the terminology "instance satisfying type T" to mean "instance whose runtime type is T or a subtype thereof", and I made the necessary changes to `resources/type-system/inference.md`. However, after digging through `dartLangSpec.tex`, it appears that the terminology we were already using in the spec for this concept is "instance implementing type T". This commit modifies `resources/type-system/inference.md` to match the spec terminology. It also fixes two places in the spec where we were incorrectly saying "instance of type T", but we meant "instance implementing type T". Furthermore, the spec consistently uses the term "dynamic type of `v`" for the concept that we informally refer to as the "runtime type of `v`", so this commit updates `resources/type-system/inference.md` to follow the spec convention.
(I really want to use "runtime type of |
| 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 |
There was a problem hiding this comment.
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}.% }
There was a problem hiding this comment.
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.
| 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 |
There was a problem hiding this comment.
(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.)
| @@ -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}'' | |||
There was a problem hiding this comment.
So this should be
"any instance whose dynamic type is a subtype of \code{C}"
| @@ -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$ | |||
There was a problem hiding this comment.
an instance whose dynamic type is a subtype of $T$
In the code review discussion
#3850 (comment), we agreed to use the terminology "instance satisfying type T" to mean "instance whose runtime type is T or a subtype thereof", and I made the necessary changes to
resources/type-system/inference.md. However, after digging throughdartLangSpec.tex, it appears that the terminology we were already using in the spec for this concept is "instance implementing type T". This commit modifiesresources/type-system/inference.mdto match the spec terminology.It also fixes two places in the spec where we were incorrectly saying "instance of type T", but we meant "instance implementing type T".
Furthermore, the spec consistently uses the term "dynamic type of
v" for the concept that we informally refer to as the "runtime type ofv", so this commit updatesresources/type-system/inference.mdto follow the spec convention.Contribution guidelines:
dart format.Note that many Dart repos have a weekly cadence for reviewing PRs - please allow for some latency before initial review feedback.