Type Type

Author: eernstg

specification/dartLangSpec.tex

@@ -836,10 +836,13 @@ \section{Overview}
   Type annotations declare the types of
   variables and functions (including methods and constructors).
 \item
-  %% TODO(eernst): Change when integrating instantiate-to-bounds.md.
   Type annotations may be omitted, in which case they are generally
-  filled in with the type \DYNAMIC{}
+  filled in using type inference, or using the type \DYNAMIC{}
   (\ref{typeDynamic}).
+  \commentary{%
+  Type inference will be specified in a future version of this document
+  (\ref{overview}).%
+  }
 \end{enumerate}%
 }
 
@@ -3446,9 +3449,8 @@ \subsubsection{The Operator `=='}
   which was originally obtained by evaluation of a literal symbol or
   a constant invocation of a constructor of the \code{Symbol} class
   has a primitive operator \lit{==}.
-\item Every instance of type \code{Type}
-  which was originally obtained by evaluating a constant type literal
-  (\ref{dynamicTypeSystem})
+\item Every instance of type \code{Type} which is a reified type
+  (\ref{typeType})
   has a primitive operator \lit{==}.
 \item An instance $o$ has a primitive operator \lit{==}
   if the dynamic type of $o$ is a class $C$,
@@ -7654,12 +7656,7 @@ \subsection{Instantiation to Bound}
 For instance, with the declaration \code{Type listType() => List;},
 evaluation of the raw type expression \code{List} in the body yields
 an instance of class \code{Type} reifying \code{List<dynamic>},
-because \code{List} is subject to instantiation to bound.
-Note that \code{List<dynamic>} is not syntactically an expression,
-but it is still possible to get access to
-a \code{Type} instance reifying \code{List<dynamic>}
-without instantiation to bound,
-because it can be the value of a type variable.%
+because \code{List} is subject to instantiation to bound.%
 }
 
 \rationale{%
@@ -8374,7 +8371,9 @@ \subsection{Constants}
   a mixin or a type alias that is not qualified by a deferred prefix,
   is a potentially constant and constant expression.
   \commentary{%
-    The constant expression always evaluates to a \code{Type} object.
+    The constant expression always evaluates to a \code{Type} object
+    which is a reified type
+    (\ref{typeType}).
     For example, if $C$ is the name of a class or type alias,
     the expression \code{$C$} is a constant,
     and if $C$ is imported with a prefix $p$, \code{$p$.$C$} is
@@ -17327,7 +17326,8 @@ \subsection{Identifier Reference}
 \item
   If $D$ is a class, mixin, or type alias,
   the value of $e$ is an object implementing the class \code{Type}
-  which reifies the corresponding type.
+  which reifies the corresponding type
+  (\ref{typeType}).
 \item
   If $D$ is a type parameter $X$ then the value of $e$ is
   the value of the actual type argument corresponding to $X$
@@ -20917,41 +20917,6 @@ \subsection{Dynamic Type System}
 (\ref{actualTypes}).%
 }
 
-\LMHash{}%
-When types are reified as instances of the built-in class \code{Type},
-those objects override the \lit{==} operator
-inherited from the \code{Object} class, so that
-two \code{Type} objects are equal according to operator \lit{==}
-if{}f the corresponding types are subtypes of each other.
-
-\commentary{%
-For example, the \code{Type} objects for the types
-\DYNAMIC{} and \code{Object} are equal to each other
-and hence \code{dynamic\,==\,Object} must evaluate to \TRUE.
-No constraints are imposed on the built-in function \code{identical},
-so \code{identical(dynamic, Object)} may be \TRUE{} or \FALSE.
-
-Similarly, \code{Type} instances for distinct type alias declarations
-declaring a name for the same function type are equal:%
-}
-
-\begin{dartCode}
-\TYPEDEF{} F = \VOID{} \FUNCTION{}<X>(X);
-\TYPEDEF{} G = \VOID{} \FUNCTION{}<Y>(Y);
-\\
-\VOID{} main() \{
-  assert(F == G);
-\}
-\end{dartCode}
-
-\LMHash{}%
-\commentary{%
-Instances of \code{Type} can be obtained in various ways,
-for example by using reflection,
-by reading the \code{runtimeType} of an object,
-or by evaluating a \emph{type literal} expression.%
-}
-
 \LMHash{}%
 An expression is a \emph{type literal} if it is an identifier,
 or a qualified identifier,
@@ -22836,7 +22801,7 @@ \subsection{Type Never}
 }
 
 
-\subsection{Type \code{Null}}
+\subsection{Type Null}
 \LMLabel{typeNull}
 
 \LMHash{}%
@@ -22882,6 +22847,109 @@ \subsection{Type \code{Null}}
 }
 
 
+\subsection{Type Type}
+\LMLabel{typeType}
+
+\LMHash{}%
+The Dart runtime supports a very limited kind of introspective reflection
+for all programs
+(\commentary{%
+that is, without including any reflection support mechanisms,
+e.g., importing \code{dart:mirrors},
+or using reflection related code generation%
+}).
+In particular, evaluation of a type literal as an expression yields
+an object whose run-time type is a subtype of the built-in type \code{Type}.
+System libraries may deliver such objects as well
+(\commentary{e.g., the method \code{runtimeType} on \code{Object}}).
+If an object $o$ is obtained in this manner
+as a reification of the Dart type $T$,
+we say that $o$ is a \Index{reified type},
+and we say that $o$ \IndexCustom{reifies}{type!reifies} $T$.
+
+%% TODO(eernst): Define "same type" in one location in this spec, use it here.
+\LMHash{}%
+A reified type identifies the underlying Dart type in the sense that
+it supports equality tests with other reified types as follows.
+Let $o_1$ and $o_2$ be reified types that reify $S_1$ respectively $S_2$,
+and let $o_3$ be an object which is not a reified type.
+Let $U_j$ be the transitive alias expansion of $S_j$, for $j \in 1 .. 3$,
+and let $v_j$ be a fresh variable whose value is $o_j$, for $j \in 1 .. 3$.
+It is then guaranteed that \code{$v_1$ == $v_2$} if{}f
+\NormalizedTypeOf{$U_1$} and \NormalizedTypeOf{$U_2$}
+are syntactically equal,
+up to equivalence of bound variables
+and up to designations of the same type using different syntax
+(\commentary{e.g., \code{C} and \code{prefix.C} may denote the same type}).
+Conversely, \code{$v_1$ == $v_3$} will yield false.
+
+\commentary{%
+Note that we do not equate primitive top types.
+For example,
+reified types reifying \code{List<\VOID>} and \code{List<\DYNAMIC>}
+are not equal.
+However, a type variable which is declared by a function type
+is treated as if it were consistently renamed to a fresh name,
+thus making types identical if possible
+(also known as alpha equivalence).
+For example:%
+}
+
+\begin{dartCode}
+\TYPEDEF{} F = \VOID{} \FUNCTION{}<X>(X);
+\TYPEDEF{} G = \VOID{} \FUNCTION{}<Y>(Y);
+\\
+\VOID{} main() \{
+  print(F == G); // \comment{Prints 'true'.}
+\}
+\end{dartCode}
+
+\commentary{%
+Note that reified types have a primitive operator \lit{==}
+(\ref{theOperatorEqualsEquals}).
+This property cannot be assumed for arbitrary expressions of type \code{Type}.
+For instance, we can declare
+\code{\CLASS\,\,MyType\,\,\EXTENDS\,\,Type \{\ldots\}}
+and override operator \lit{==}.%
+}
+
+\LMHash{}%
+Let $e_1$ and $e_2$ be constant expressions
+(\ref{constants})
+evaluating to $o_1$ respectively $o_2$,
+which are reified types reifying the Dart types $S_1$ respecively $S_2$.
+Let $v_1$ and $v_2$ be fresh variables bound to $o_1$ respectively $o_2$
+We then have \code{identical($v_1$, $v_2$)} if{}f
+\code{$S_1$\,\,==\,\,$S_2$}.
+
+\commentary{%
+In other words, constant reified types are canonicalized.
+For runtime implementations which implement identity by choosing a
+canonical representative for the equivalence class of equal instances,
+the choice of what type object to canonicalize to is not
+observable in the language.
+}
+
+\rationale{%
+As mentioned at the beginning of this section,
+reified types support a very limited kind of introspective reflection.
+In particular, we can compare reified types for equality,
+and in the case where two reified types are equal
+it is known that they reify types which are subtypes of each other
+(that is, they are ``the same type'' with respect to subtyping).
+But we cannot compare reified types for any inequality, that is,
+we cannot determine whether one is a subtype of the other.
+It is also impossible to deconstruct a reified type.
+E.g., we cannot obtain the reified type for \code{$T$}
+by performing operations on a given reified type for \code{List<$T$>}.
+This design was chosen in order to ensure that Dart programs
+do not incur the substantial implications in terms of
+program size and run-time performance
+that are very difficult to avoid
+when a more powerful form of reflection is supported.%
+}
+
+
 \subsection{Function Types}
 \LMLabel{functionTypes}
 
@@ -22934,7 +23002,7 @@ \subsection{Function Types}
 }
 
 
-\subsection{Type \FUNCTION}
+\subsection{Type Function}
 \LMLabel{functionType}
 
 \LMHash{}%
@@ -22975,7 +23043,7 @@ \subsection{Type \FUNCTION}
 }
 
 
-\subsection{Type \DYNAMIC}
+\subsection{Type dynamic}
 \LMLabel{typeDynamic}
 
 \LMHash{}%
@@ -24105,44 +24173,20 @@ \subsubsection{Null promotion}
 These are extended as per
 [separate proposal](https://github.com/dart-lang/language/blob/master/resources/type-system/flow-analysis.md).
 
-\subsubsection{Runtime type equality operator}
-
-!!!TODO!!!
-
-Two objects $T_1$ and $T_2$ which are instances of \code{Type} (that
-is, runtime type objects) are considered equal if and only if the
-runtime type objects $T_1$ and $T_2$ corresponds to the types $S_1$
-and $S_2$ respectively, and the normal forms \NormalizedTypeOf{$S_1$}
-and \NormalizedTypeOf{$S_2$} are syntactically equal up to equivalence
-of bound variables. Note that we do not equate primitive top types.
-\code{List<\VOID>} and \code{List<\DYNAMIC>} are still considered
-distinct runtime type objects.  Note that we also do not equate
-function types which differ in the placement of \REQUIRED{} on
-parameter types.
-
-\subsubsection{Constant evaluation and canonicalization}
-
-\paragraph{Type literals}
-
-Two constant type literals $T_1$ and $T_2$ compare as identical if they
-are equal using the definition of runtime type equality specified above.
-
-For runtime implementations which implement identity by choosing a
-canonical representative for the equivalence class of equal instances,
-the choice of what type object to canonicalize to is not
-observable in the language.
 
 \paragraph{Constant instances}
 
-Any two
-instances which are otherwise identical except for their generic type arguments
-shall be considered identical if those generic type arguments compare equal
-using the definition of runtime type object equality defined above.  That is,
-comparison (or canonicalization) of constant instances of generic classes is
-performed relative to the normal forms of their generic type arguments.
-Hence, an instance of
-\code{$C$<$T_0$>} compares identical to \code{C<$T_1$>} if $T_0$ and $T_1$ have the same normal form
-(up to the identity of bound variables), and the objects are otherwise
+!!!TODO!!!
+
+Any two instances which are otherwise identical except for their
+generic type arguments shall be considered identical if those generic
+type arguments compare equal using the definition of runtime type
+object equality defined above.  That is, comparison (or
+canonicalization) of constant instances of generic classes is
+performed relative to the normal forms of their generic type
+arguments.  Hence, an instance of \code{$C$<$T_0$>} compares identical
+to \code{C<$T_1$>} if $T_0$ and $T_1$ have the same normal form (up to
+the identity of bound variables), and the objects are otherwise
 identical.
 
 Implementations of the Dart runtime semantics rely on canonicalization of