Integrated deferred loading into main spec.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification \\
-{\large Version 1.4}}
+{\large Version 1.6}}
 %\author{The Dart Team}
 \begin{document}
 \maketitle
 \tableofcontents
 
 
 \newpage
 
 \pagestyle{myheadings}
 \markright{Dart Programming Language Specification}
@@ skipping 1227 matching lines @@
 Calling a redirecting factory constructor $k$ causes the constructor $k^\prime$ denoted by $type$ (respectively, $type.identifier$) to be called with the actual arguments passed to $k$, and returns the result of $k^\prime$ as the result of $k$.  The resulting constructor call is governed by the same rules as an instance creation expression using \NEW{} (\ref{instanceCreation}). 
 
 \commentary{
 It follows that if $type$ or $type.id$ are not defined, or do not refer to a class or constructor, a dynamic error occurs, as with any other undefined constructor call. The same holds if $k$ is called with fewer required parameters or more positional parameters than $k^\prime$ expects, or if $k$  is called with a named parameter that is not declared by $k^\prime$.
 }
 
 It is a compile-time error if $k$ explicitly specifies a default value for an optional parameter.\commentary{
 Default values specified in $k$ would be ignored, since it is the {\em actual} parameters that are passed to $k^\prime$. Hence, default values are disallowed.
 }
 
-It is a compile-time error if a redirecting factory constructor redirects to itself, either directly or indirectly via a sequence of redirections. %does not redirect to a non-redirecting factory constructor or to a generative constructor in a finite number of steps.
+It is a run-time error if a redirecting factory constructor redirects to itself, either directly or indirectly via a sequence of redirections. %does not redirect to a non-redirecting factory constructor or to a generative constructor in a finite number of steps.
 
 % Make this a runtime error so deferred loading works
 
 \rationale{
 If a redirecting factory $F_1$ redirects to another redirecting factory $F_2$ and $F_2$ then redirects to $F_1$, then both $F_1$ and $F_2$ are ill-defined. Such cycles are therefore illegal.
 } 
 
 
 It is a static warning if $type$ does not denote a class accessible in the current scope; if $type$ does denote such a class $C$ it is a static warning if the referenced constructor (be it $type$ or $type.id$) is not a constructor of $C$.
 
@@ skipping 225 matching lines @@
       \EXTENDS{} type
     .
 \end{grammar}
 
 %The superclass clause of a class C is processed within the enclosing scope of the static scope of C.
 %\commentary{
 %This means that in a generic class, the type parameters of the generic are available in the superclass clause.
 %} 
 
 %It is a compile-time error if  the \EXTENDS{} clause of a class $C$ includes a type expression that does not denote a class available in the lexical scope of $C$. 
-It is a compile-time error if  the \EXTENDS{} clause of a class $C$ specifies a malformed  type as a superclass.
+It is a compile-time error if  the \EXTENDS{} clause of a class $C$ specifies a malformed  type or a deferred type (\ref{staticTypes}) as a superclass.
 % too strict? Do we e want extends List<Undeclared> to work as List<dynamic>? 
 
 \commentary{ The type parameters of a generic class are available in the lexical scope of the superclass clause, potentially shadowing classes in the surrounding scope. The following code is therefore illegal and should cause a compile-time error:
 }
 
 \begin{dartCode}
 class T \{\}
 
 /* Compilation error: Attempt to subclass a type parameter */
 class G$<$T$>$ extends T \{\} 
@@ skipping 102 matching lines @@
 
 A class has a set of direct superinterfaces. This set includes the interface of its superclass and the interfaces specified in the the \IMPLEMENTS{}  clause of the class.
 % and any superinterfaces specified by interface injection (\ref{interfaceInjection}).  \Q{The latter needs to be worded carefully - when do interface injection clauses execute and in what scope?}
 
 \begin{grammar}
 {\bf interfaces:}
       \IMPLEMENTS{} typeList
     .
 \end{grammar}
 
-It is a compile-time error if  the \IMPLEMENTS{}  clause of a class $C$ specifies a type variable as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a malformed type as a superinterface  It is a compile-time error if the \IMPLEMENTS{} clause of a class $C$ specifies type \DYNAMIC{} as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a type $T$ as a superinterface more than once.
+It is a compile-time error if  the \IMPLEMENTS{}  clause of a class $C$ specifies a type variable as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a malformed type or deferred type (\ref{staticTypes}) as a superinterface  It is a compile-time error if the \IMPLEMENTS{} clause of a class $C$ specifies type \DYNAMIC{} as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a type $T$ as a superinterface more than once.
 It is a compile-time error if the superclass of a class $C$ is specified as a superinterface of $C$.
 
 \rationale{
 One might argue that it is harmless to repeat a type in the superinterface list, so why make it an error? The issue is not so much that the situation described in program source is erroneous, but that it is pointless. As such, it is an indication that the programmer may very well have meant to say something else - and that is a mistake that should be called to her or his attention.  Nevertheless, we could simply issue a warning; and perhaps we should and will. That said, problems like these are local and easily corrected on the spot, so we feel justified in taking a harder line. 
 }
 
 It is a compile-time error if the interface of a class $C$ is a superinterface of itself.
 
 Let $C$ be a concrete class that does not declare its own \code{noSuchMethod()} method.
 It is a static warning if the implicit interface of  $C$ includes an instance member $m$ of type $F$ and $C$ does not declare or inherit a corresponding non-abstract instance member $m$ of type $F'$ such that $F' <: F$. 
@@ skipping 145 matching lines @@
 The restriction on constructors simplifies the construction of mixin applications because the process of creating instances is simpler.
 
 The restriction on the superclass means that the type of a class  from which a mixin is derived is always implemented by any class that mixes it in. This allows us to defer the question of whether and how to express the type of the mixin independently of its superclass and super interface types.
 
 Reasonable answers exist for all these issues, but their implementation is non-trivial.
 }
 
 \subsection{Mixin Application}
 \label{mixinApplication}
 
-A mixin may be applied to a superclass, yielding a new class. Mixin application occurs when a mixin is mixed into a class declaration via its \WITH{} clause.  The mixin application may be used to extend a class per section (\ref{classes}); alternately, a class may be defined as a mixin application as described in this section.
+A mixin may be applied to a superclass, yielding a new class. Mixin application occurs when a mixin is mixed into a class declaration via its \WITH{} clause.  The mixin application may be used to extend a class per section (\ref{classes}); alternately, a class may be defined as a mixin application as described in this section.   It is a compile-time error if the \WITH{} clause of a mixin application $C$ includes a deferred type expression.
+
 
 \begin{grammar}
 {\bf  mixinApplicationClass:}
         identifier typeParameters? `='  mixinApplication `{\escapegrammar ;}' .
         
 {\bf mixinApplication:}
      type mixins interfaces? 
     .
 \end{grammar}
 
@@ skipping 303 matching lines @@
 A {\em constant expression} is an expression whose value can never change, and that can be evaluated entirely at compile time. 
 
 A constant expression is one of the following:
 \begin{itemize}
 \item A literal number (\ref{numbers}).
 \item A literal boolean (\ref{booleans}).
 \item A literal string (\ref{strings}) where any interpolated expression  (\ref{stringInterpolation}) is a compile-time constant that evaluates to a numeric, string or boolean value or to \NULL{}.
 \rationale{It would be tempting to allow string interpolation where the interpolated value is any compile-time constant.  However, this would require running the \code{toString()} method for constant objects, which could contain arbitrary code.}
 \item A literal symbol (\ref{symbols}).
 \item \NULL{} (\ref{null}).
-\item A qualified reference to a static constant variable (\ref{variables}). 
-\commentary {For example, If class C declares a constant static variable v, C.v is a constant. The same is true if C is accessed via a prefix p; p.C.v is a constant.
+\item A qualified reference to a static constant variable (\ref{variables}) that is not qualified by a deferred prefix. 
+\commentary {For example, If class C declares a constant static variable v, C.v is a constant. The same is true if C is accessed via a prefix p; p.C.v is a constant  unless p is a deferred prefix.
 }
 \item An identifier expression that denotes a constant variable. %CHANGE in googledoc
 \item A simple or qualified identifier denoting a class or a type alias. 
 \commentary {For example, if C is a class or typedef C is a constant, and if C is imported with a prefix p,  p.C is a constant.
 }
-\item A constant constructor invocation (\ref{const}).  
+\item A constant constructor invocation (\ref{const}) that is not qualified by a deferred prefix.  
 \item A constant list literal (\ref{lists}).
 \item A constant map literal (\ref{maps}).
-\item A simple or qualified identifier denoting a top-level function (\ref{functions}) or a static method (\ref{staticMethods}).
+\item A simple or qualified identifier denoting a top-level function (\ref{functions}) or a static method (\ref{staticMethods}) that is not qualified by a deferred prefix.
 \item A parenthesized expression \code{($e$)} where $e$ is a constant expression.
 \item An expression of the form \code{identical($e_1$, $e_2$)} where $e_1$ and $e_2$ are constant expressions  and \code{identical()} is statically bound to the predefined dart function   \code{identical()} discussed above (\ref{objectIdentity}).
 \item An expression of one of the forms  \code{$e_1$ == $e_2$} or  \code{$e_1$ != $e_2$} where $e_1$ and $e_2$ are constant expressions that evaluate to a numeric, string or boolean value or to \NULL{}.
 \item An expression of one of the forms \code{!$e$}, \code{$e_1$ \&\& $e_2$} or \code{$e_1 || e_2$}, where  $e$, $e_1$ and $e_2$ are constant expressions that evaluate to a boolean value.
 \item An expression of one of the forms \~{}$e$, $e_1$ \^{} $e_2$, \code{$e_1$ \& $e_2$}, $e_1 | e_2$, $e_1 >> e_2$ or $e_1 <<  e_2$, where  $e$, $e_1$ and $e_2$ are constant expressions that evaluate to an integer value  or to \NULL{}.
 \item An expression of one of the forms \code{$-e$},  \code{$e_1 + e_2$}, \code{$e_1$ - $e_2$}, \code{$e_1$ * $e_2$}, \code{$e_1$ / $e_2$,} \code{$e_1$ \~{}/ $e_2$},  \code{$e_1  >  e_2$}, \code{$e_1  <  e_2$}, \code{$e_1$ $>$= $e_2$}, \code{$e_1$ $<$= $e_2$} or \code{$e_1$ \% $e_2$},  where $e$, $e_1$ and $e_2$ are constant expressions that evaluate to a numeric value  or to \NULL{}.
 \item An expression of the form \code{$e_1$?$e_2$:$e3$} where where $e_1$, $e_2$ and $e_3$ are constant expressions and $e_1$ evaluates to a boolean value.
 \end{itemize}
 
 % null in all the expressions
@@ skipping 674 matching lines @@
 \item  $T$ is not a parameterized type, then for $ i \in 1 .. l$, let $V_i =  \DYNAMIC{}$.
 \item  If $T$ is  a parameterized type then let $V_i = U_i$ for $ i \in 1 .. m$.  
 \end{itemize}
 
 If $R$ is a generic with $l \ne m$ type parameters then for $ i \in 1 .. l$, let $V_i =  \DYNAMIC{}$. In any other case, let $V_i = U_i$ for $ i \in 1 .. m$.  
 
 Evaluation of $e$ proceeds as follows:
 
 First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated. 
 
+If $T$ is a deferred type with prefix $p$, then if $p$ has not been successfully loaded, a dynamic error occurs.
+
 Then, if $q$ is a non-factory constructor of an abstract class then an \code{AbstractClassInstantiationError} is thrown.
 
 If $T$  is malformed or if $T$ is a type variable a dynamic error occurs. In checked mode, if $T$ or any of its superclasses is malbounded a dynamic error occurs.
  Otherwise, if $q$ is not defined or not accessible, a \code{NoSuchMethodError} is thrown.  If $q$ has  less than $n$ positional parameters or more than $n$ required parameters, or if $q$ lacks any of the keyword parameters $\{ x_{n+1}, \ldots, x_{n+k}\}$ a \code{NoSuchMethodError} is thrown.
 
 Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), then:
 
 \commentary{Note that it this point we are assured that the number of actual type arguments match the number of formal type parameters.}
 
 A fresh instance (\ref{generativeConstructors}), $i$,  of class $R$ is allocated. For each instance variable $f$ of $i$,  if the variable declaration of $f$ has an initializer expression $e_f$, then $e_f$ is evaluated to an object $o_f$ and $f$ is bound to $o_f$. Otherwise $f$ is bound to \NULL{}.
 
 \commentary{
 Observe that \THIS{} is not in scope in $e_f$. Hence, the initialization cannot depend on other properties of the object being instantiated.
 }
 
 Next,  $q$ is executed  with \THIS{} bound to $i$,  the type parameters (if any) of $R$ bound to the actual type arguments $V_1, \ldots, V_l$ and the formal parameter bindings that resulted from the evaluation of the argument list. The result of the evaluation of $e$ is $i$.
 
 Otherwise, $q$ is a factory constructor (\ref{factories}). Then:
 
 If $q$ is a redirecting factory constructor of the form $T(p_1, \ldots, p_{n+k}) = c;$ or of the form  $T.id(p_1, \ldots, p_{n+k}) = c;$ then the result of the evaluation of $e$ is equivalent to evaluating the expression 
 
-$[V_1,  \ldots, V_m/T_1,  \ldots, T_m]($\code{\NEW{} $c(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k}))$}.
+$[V_1,  \ldots, V_m/T_1,  \ldots, T_m]($\code{\NEW{} $c(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k}))$}.  If evaluation of $q$ causes $q$ to be re-evaluated cyclically, a runtime error occurs.
+
 
 Otherwise, the body of $q$ is executed with respect to the bindings that resulted from the evaluation of the argument list and the type parameters (if any) of $q$ bound to the actual type arguments $V_1, \ldots, V_l$ resulting in an object $i$. The result of the evaluation of $e$ is $i$.
 
 It is a static warning if $q$ is a constructor of an abstract class and $q$ is not a factory constructor.
 
 \commentary{The above gives precise meaning to the idea that instantiating an abstract class leads to a warning. 
 A similar clause applies to constant object creation in the next section.
 } 
 
 \rationale{In particular, a factory constructor can be declared in an abstract class and used safely, as it will either produce a valid instance or lead to a warning inside its own declaration.
@@ skipping 20 matching lines @@
 \begin{grammar}
 {\bf constObjectExpression:}
 \CONST{} type ('{\escapegrammar .}' identifier)? arguments
 .
 \end{grammar}
 
 Let $e$ be a constant object expression of the form  
 
 \CONST{} $T.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ 
 
-or the form  \CONST{} $T(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. It is a compile-time error if $T$ does not denote a class accessible in the current scope. 
+or the form  \CONST{} $T(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. It is a compile-time error if $T$ does not denote a class accessible in the current scope.  It is a compile-time error if $T$ is a deferred type (\ref{staticTypes}).
 
 \commentary{In particular, $T$ may not be a type variable.}
 
 If $T$ is a parameterized type, it is a compile-time error if $T$ includes a type variable among its type arguments.
 
 If $e$ is of the form \CONST{} $T.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ it is a compile-time error if $T.id$ is not the name of a constant constructor declared by the type $T$. If $e$ is of the form  \CONST{} $T(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ it is a compile-time error if the type $T$ does not declare a constant constructor with the same name as the declaration of $T$. 
 
 In all of the above cases, it is a compile-time error if $a_i,  i\in 1 .. n + k$, is not a compile-time constant expression.
 
 %If $T$ is a parameterized type (\ref{parameterizedTypes}) $S<U_1,  \ldots, U_m>$, let $R = S$.  It is a compile-time error if $T$ is is malformed. If $T$ is not a parameterized type, let $R = T$.
@@ skipping 248 matching lines @@
 
 \subsubsection{ Unqualified Invocation}
 \label{unqualifiedInvocation}
 
 An unqualified function invocation $i$ has the form 
 
 $id(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$, 
 
 where $id$ is an identifier or an identifier qualified with a library prefix. 
 
+If $id$ is qualified with a deferred prefix $p$ and $p$ has not been successfully loaded, then:
+\begin{itemize}
+\item
+If the invocation has the form $p$\code{.loadLibrary()} then an attempt to load the library represented by the prefix $p$ is initiated as discussed in section \ref{imports}. 
+\item
+ Otherwise, a \code{NoSuchMethodError} is thrown.
+ \end{itemize}
+
 If there exists a lexically visible declaration named $id$, let $f_{id}$ be the innermost such declaration. Then:
 \begin{itemize}
 \item
  If $f_{id}$ is a local function, a library function, a library or static getter or a variable then $i$ is interpreted as a function expression invocation (\ref{functionExpressionInvocation}).
  \item
 Otherwise, if $f_{id}$ is a static method of the enclosing class $C$, $i$ is equivalent to $C.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 \item Otherwise, $f_{id}$ is considered equivalent to the ordinary method invocation $\THIS{}.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 \end{itemize}
 
 %Otherwise, if there is an accessible (\ref{privacy}) static method named $id$ declared in a superclass $S$ of the immediately enclosing class $C$ then i is equivalent to the static method invocation $S.id(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$.  
@@ skipping 137 matching lines @@
 Note that the absence of $C.m$ is statically detectable. Nevertheless, we choose not to define this situation as an error.  The goal is to allow coding to proceed in the order that suits the developer rather than eagerly insisting on consistency. The warnings are given statically at compile-time to help developers catch errors. However, developers need not correct these problems immediately in order to make progress.
 }
 
 \commentary{
 Note the requirement that $C$ {\em declare} the method. This means that static methods declared in superclasses of $C$ cannot be invoked via $C$.
 }
 
 
 Evaluation of $i$ proceeds as follows:
 
-If $C$ does not declare a static method or getter $m$ then the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated, after which a \code{NoSuchMethodError} is thrown. 
+If $C$ is a deferred type  (\ref{staticTypes}) with prefix $p$, and $p$ has not been successfully loaded, or
+if $C$ does not declare a static method or getter $m$ then the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated, after which a \code{NoSuchMethodError} is thrown. 
 
 Otherwise, evaluation proceeds as follows:
 \begin{itemize}
 \item
 If the member $m$ declared by $C$ is a getter, then $i$ is equivalent to the expression $(C.m)(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. 
 \item Otherwise, let $f$ be the the method $m$ declared in class $C$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated.
 The body of $f$ is then executed with respect to the bindings that resulted from the evaluation of the argument list. The value of $i$ is the value returned after the body of $f$ is executed.
 \end{itemize}
 
 It is a static type warning if the type $F$ of $C.m$ may not be assigned to a function type.  If $F$ is not a function type, or if $C.m$ does not exist, the static type of $i$ is \DYNAMIC{}. Otherwise 
@@ skipping 105 matching lines @@
 
 If the getter lookup has failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
 \begin{itemize}
 \item  \code{im.isGetter} evaluates to \code{\TRUE{}}.
 \item  \code{im.memberName} evaluates to \code{'m'}.
 \item \code{im.positionalArguments} evaluates to the value of \code{\CONST{} []}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 Then the method \code{noSuchMethod()} is looked up in $S$ and invoked  with argument $im$, and the result of this invocation is the result of evaluating $i$.
 
+
+
 It is a static type warning if $S$ does not have a getter named $m$.  The static type of $i$ is the declared return type of $S.m$, if $S.m$ exists; otherwise the static type of $i$  is  \DYNAMIC{}. 
 
+Evaluation of a getter invocation of the form $p.C.v$, where $p$ is a deferred prefix, proceeds as follows:
+
+If $p$ has been successfully loaded, the assignment is evaluated exactly like the invocation $K.v$, where $K$ denotes the top level member $C$ of the library represented by $p$. Otherwise a \code{NoSuchMethodError} is thrown.
+
+
+Evaluation of a top-level getter invocation $i$ of the form $p.m$, where $p$ is a deferred prefix and  $m$ is an identifier, proceeds as follows:
+
+If $p$ has been successfully loaded, the invocation is evaluated exactly like the invocation $w$, where $w$ denotes the top level member named $m$ of the library represented by $p$. Otherwise a \code{NoSuchMethodError} is thrown.
  
 
 
 \subsection{ Assignment}
 \label{assignment}
 
 An assignment changes the value associated with a mutable variable or property.
 
 \begin{grammar}
 {\bf assignmentOperator:}`=' ;
@@ skipping 54 matching lines @@
 If the setter lookup has failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
 \begin{itemize}
 \item  \code{im.isSetter} evaluates to \code{\TRUE{}}.
 \item  \code{im.memberName} evaluates to \code{'v='}.
 \item \code{im.positionalArguments} evaluates to an immutable list with the same values as \code{[$o_2$]}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 
 Then the method \code{noSuchMethod()} is looked up in $o_1$ and invoked  with argument $im$. The value of the assignment expression is $o_2$ irrespective of whether setter lookup has failed or succeeded.
 
+Evaluation of an assignment of the form $p.v \code{=} e$, where $p$ is a deferred prefix, proceeds as follows:
+
+If $p$ has been successfully loaded, the assignment is evaluated exactly like the assignment $w \code{=} e$, where $w$ denotes the top level member named $v$ of the library represented by $p$. Otherwise, $e$ is evaluated and then a \code{NoSuchMethodError} is thrown.
+
+Evaluation of an assignment of the form $p.C.v \code{=} e$, where $p$ is a deferred prefix, proceeds as follows:
+
+If $p$ has been successfully loaded, the assignment is evaluated exactly like the assignment $K.v = e$, where $K$ denotes the top level member $C$ of the library represented by $p$. Otherwise $e$ is evaluated and then a \code{NoSuchMethodError} is thrown.
+
 In checked mode, it is a dynamic type error if $o_2$ is not \NULL{} and the interface of the class of $o_2$ is not a subtype of the actual type of $e_1.v$.
 
 Let $T$ be the static type of $e_1$. It is a static type warning if $T$ does not have an accessible instance setter named $v=$ unless $T$ or a superinterface of $T$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. It is a static type warning if the static type of $e_2$ may not be assigned to $T$.   The static type of the expression $e_1v$ \code{=} $e_2$ is the static type of $e_2$.
 
 Evaluation of an assignment of the form $e_1[e_2]$ \code{=} $e_3$ is equivalent to the evaluation of the expression \code{(a, i, e)\{a.[]=(i, e); \RETURN{} e; \} ($e_1, e_2, e_3$)}.  The static type of the expression $e_1[e_2]$ \code{=} $e_3$ is the static type of $e_3$.
 
 % Should we add: It is a dynamic error if $e_1$ evaluates to an  constant list or map.
 
 It is as static warning if an assignment of the form $v = e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer and there is neither a local variable declaration with name $v$  nor setter declaration with name $v=$ in the lexical scope enclosing the assignment.
 
 
 
 \subsubsection{Compound Assignment}
 \label{compoundAssignment}
 
 A compound assignment of the form $v$ $op\code{=} e$ is equivalent to $v \code{=} v$ $op$ $e$. A compound assignment of the form $C.v$ $op \code{=} e$ is equivalent to $C.v \code{=} C.v$ $op$ $e$. A compound assignment of the form $e_1.v$ $op = e_2$ is equivalent to \code{((x) $=>$ x.v = x.v $op$ $e_2$)($e_1$)} where $x$ is a variable that is not used in $e_2$. A compound assignment of the form  $e_1[e_2]$ $op\code{=} e_3$ is equivalent to 
-\code{((a, i) $=>$ a[i] = a[i] $op$ $e_3$)($e_1, e_2$)} where $a$ and $i$ are a variables that are not used in $e_3$. 
+\code{((a, i) $=>$ a[i] = a[i] $op$ $e_3$)($e_1, e_2$)} where $a$ and $i$ are a variables that are not used in $e_3$. A compound assignment of the form $p.v$ $op\code{=} e$, where $p$ is a deferred prefix,  is equivalent to $p.v \code{=} p.v$ $op$ $e$. A compound assignment of the form $p.C.v$ $op\code{=} e$, where $p$ is a deferred prefix,  is equivalent to $p.C.v \code{=} p.C.v$ $op$ $e$.
+
 
 \begin{grammar}
 {\bf compoundAssignmentOperator:}`*=';
       `/=';
       `\~{}/=';
       `\%=';
       `+=';
       `-=';
       `{\escapegrammar \lt \lt}=';
        `{\escapegrammar \gt \gt}=';
@@ skipping 528 matching lines @@
  .
  
  
 {\bf isOperator:}
 \IS{} `!'?
     .
  \end{grammar}
  
  Evaluation of the is-expression \code{$e$ \IS{} $T$} proceeds as follows:
 
-The expression $e$ is evaluated to a value $v$. Then, if $T$ is malformed, a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the is-expression evaluates to true. Otherwise it evaluates to false.
+The expression $e$ is evaluated to a value $v$. Then, if $T$ is a malformed or deferred type (\ref{staticTypes}), a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the is-expression evaluates to true. Otherwise it evaluates to false.
 
 \commentary{It follows that \code{$e$ \IS{} Object} is always true. This makes sense in a language where everything is an object. 
 
 Also note that \code{\NULL{} \IS{} $T$} is false unless $T = \code{Object}$, $T = \code{\DYNAMIC{}}$ or $T = \code{Null}$.  The former two are useless, as is anything of the form \code{$e$ \IS{} Object} or \code{$e$ \IS{} \DYNAMIC{}}.  Users should test for a null value directly rather than via type tests.
 }
 
 The is-expression \code{$e$ \IS{}! $T$} is equivalent to \code{!($e$ \IS{} $T$)}.
 
 % Add flow dependent types
 
@@ skipping 24 matching lines @@
  .
  
  
 {\bf asOperator:}
 \AS{}
     .
  \end{grammar}
  
  Evaluation of the cast expression \code{$e$ \AS{} $T$} proceeds as follows:
 
-The expression $e$ is evaluated to a value $v$. Then, if $T$ is malformed, a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the cast expression evaluates to $v$. Otherwise, if $v$ is \NULL{}, the cast expression evaluates to $v$. 
+The expression $e$ is evaluated to a value $v$. Then, if $T$ is a malformed or deferred type (\ref{staticTypes}), a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the cast expression evaluates to $v$. Otherwise, if $v$ is \NULL{}, the cast expression evaluates to $v$. 
 In all other cases,  a \code{CastError} is thrown.
  
 The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$. 
 
 
 \section{Statements}
 \label{statements}
 
  \begin{grammar}
 {\bf statements:}
@@ skipping 367 matching lines @@
  it is a compile-time error if the expressions $e_k$ are not compile-time constants for all  $k \in 1..n$.  It is a compile-time error if the values of the expressions $e_k$ are not either:
  \begin{itemize}
  \item instances of the same class $C$, for all $k \in 1..n$,  or 
  \item instances of a class that implements \cd{int}, for all $k \in 1..n$,  or 
  \item instances of a class that implements \cd{String}, for all $k \in 1..n$. 
  \end{itemize}
  
 \commentary{In other words,  all the expressions in the cases evaluate to constants of the exact same user defined class or are of certain known types.  Note that the values of the expressions are known at compile-time, and are independent of any static type annotations.
 }
 
-It is a compile-time error if the class $C$ has an implementation of the operator $==$ other than the one inherited from \code{Object} unless the value of the expression is a string, an integer, literal symbol or the result of invoking a constant constructor class \cd{Symbol}.
+It is a compile-time error if the class $C$ has an implementation of the operator $==$ other than the one inherited from \code{Object} unless the value of the expression is a string, an integer, literal symbol or the result of invoking a constant constructor of class \cd{Symbol}.
  
  \rationale{
  The prohibition on user defined equality allows us to implement the switch efficiently for user defined types. We could formulate matching in terms of identity instead with the same efficiency. However, if a type defines an equality operator, programmers would find it quite surprising that equal objects did not match.
  
  }
 
 \commentary{
 The \SWITCH{}  statement should only be used in very limited situations (e.g., interpreters or scanners).  
 }
 
@@ skipping 138 matching lines @@
  \item
 A set of \ON{}-\CATCH{} clauses, each of which specifies  (either explicitly or implicitly) the type of exception object to be handled, one or two exception parameters and a block statement.
 \item
 A \FINALLY{} clause, which consists of a block statement. 
 \end{enumerate}
 
 \rationale{
 The syntax is designed to be upward compatible with existing Javascript programs. The \ON{} clause can be omitted, leaving what looks like a Javascript catch clause.
 }
 
-An \ON{}-\CATCH{} clause of the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$}  {\em matches} an object $o$  if the type of $o$ is a subtype of $T$.  If $T$ is a malformed type, then performing a match causes a run time error.
+An \ON{}-\CATCH{} clause of the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$}  {\em matches} an object $o$  if the type of $o$ is a subtype of $T$.  If $T$ is a malformed or deferred type  (\ref{staticTypes}), then performing a match causes a run time error.
 
 \commentary {
-It is of course a static warning if $T$ is a malformed type (\ref{staticTypes}).
+It is of course a static warning if $T$ is a deferred or malformed type.
 }
 
 An \ON{}-\CATCH{} clause of the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$} introduces a new scope $CS$ in which local variables specified by $p_1$ and $p_2$ are defined. The statement $s$ is enclosed within $CS$.
 
 
 An \ON{}-\CATCH{} clause of the form  \code{\ON{} $T$ \CATCH{} ($p_1$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$} where $p_2$ is an identifier that does not occur anywhere else in the program. 
 
 
 An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p$) $s$}. An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p_1, p_2$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p_1, p_2$) $s$}
 
@@ skipping 314 matching lines @@
 The {\em public namespace} of library $L$ is the mapping that maps the simple name of each public top-level member $m$ of $L$ to $m$. 
 The scope of a library $L$ consists of the names introduced by all top-level declarations declared in $L$, and the names added by $L$'s imports (\ref{imports}).
 
 
 \subsection{Imports}
 \label{imports}
 
 An {\em import} specifies a library to be used in the scope of another library. 
 \begin{grammar}
 {\bf libraryImport:}
-   metadata \IMPORT{}  uri (\AS{} identifier)?  combinator* `{\escapegrammar ;}'
+   metadata importSpecification
     .
-    
+ 
+ {\bf importSpecification:}
+    \IMPORT{}  uri (\AS{} identifier)?  combinator* `{\escapegrammar ;}';
+     \IMPORT{}  uri \DEFERRED{} \AS{} identifier  combinator* `{\escapegrammar ;}'
+    .
+       
 {\bf combinator:}\SHOW{} identifierList;
 \HIDE{} identifierList
     .
     
     {\bf identifierList:}
       identifier (, identifier)*
  \end{grammar}
  
 
-An import specifies a URI $x$ where the declaration of an imported library is to be found. It is a compile-time error if  the specified URI does not refer to a library declaration.  The interpretation of URIs is described in section \ref{uris} below.
+An import specifies a URI $x$ where the declaration of an imported library is to be found. 
+
+Imports may be {\em deferred} or {\em immediate}. A deferred import is distinguished by the appearance of the built-in identifier \DEFERRED{} after the URI. Any import that is not deferred is immediate.
+
+It is a compile-time error if  the specified URI of an immediate import does not refer to a library declaration.  The interpretation of URIs is described in section \ref{uris} below.
+
+It is a static warning if the specified URI of a deferred import does not refer to a library declaration.
+
+\rationale{
+ One cannot detect the problem at compile time because compilation often occurs during execution and  one does not know what the URI refers to.  However the development environment should detect the problem.
+ }
+
  
 The {\em current library} is the library currently being compiled. The import modifies the  namespace of the current library in a manner that is determined by the imported library and by the optional elements of  the import.
      
-An import directive $I$ may optionally include:
-\begin{itemize}
-\item A prefix clause of the form \AS{} \code{Id} used to prefix names imported by $I$.
-\item Namespace combinator clauses used to restrict the set of names imported by $I$. Currently, two namespace combinators are supported: \HIDE{} and \SHOW{}.
-\end{itemize}
+An immediate import directive $I$ may optionally include a prefix clause of the form \AS{} \code{Id} used to prefix names imported by $I$. A deferred import must include a prefix clause or a compile time error occurs. It is a compile-time error if a prefix used in a deferred import is used in another import clause.
+
+An import directive $I$ may optionally include a namespace combinator clauses used to restrict the set of names imported by $I$. Currently, two namespace combinators are supported: \HIDE{} and \SHOW{}.
 
 Let $I$ be an import directive that refers to a URI via the string $s_1$. Evaluation of $I$  proceeds as follows:
 
-First,
+If $I$ is a deferred import, no evaluation takes place. Instead, the following names are added to the scope of $L$:
+\begin{itemize}
+\item
+The name of the prefix, $p$ denoting a deferred prefix declaration.
+\item
+The name \code{$p$.loadLibrary}, denoting a top level function with no arguments, whose semantics are described below.
+\end{itemize}
+ 
+A deferred prefix $p$ may be loaded explicitly via the function call \code{$p$.loadLibrary}, which returns a future $f$. The effect of the call is to cause an immediate import $IÕ$ to be executed at some future time, where $IÕ$ is is derived from $I$ by eliding the word \DEFERRED{} and adding a \HIDE{} \code{loadLibrary}  combinator clause. When $IÕ$ executes without error, $f$ completes successfully. If $IÕ$ executes without error, we say that the call to \code{$p$.loadLibrary} has succeeded, otherwise we say the call has failed.
+
+After a call succeeds, the names $p$ and \code{$p$.loadLibrary} remain in the top-level scope of $L$, and so it is possible to call \code{loadLibrary} again. If a call fails, nothing happens, and one again has the option to call \code{loadLibrary} again. Whether a repeated call to \code{loadLibrary} succeeds will vary as described below.
+
+The effect of a repeated call to \code{$p$.loadLibrary} is as follows:
+\begin{itemize}
+\item
+If another call to \code{$p$.loadLibrary} has already succeeded, the repeated call also succeeds. 
+Otherwise,
+\item
+If another call to  to \code{$p$.loadLibrary} has failed:
+\begin{itemize}
+\item
+If the failure is due to a compilation error, the repeated call fails for the same reason.
+\item
+If the failure is due to other causes, the repeated call behaves as if no previous call had been made.
+\end{itemize}
+\end{itemize}
+
+\commentary{
+In other words, one can retry a deferred load after a network failure or because a file is absent, but once one finds some content and loads it, one can no longer reload.
+
+We do not specify what value the future returned resolves to.
+}
+
+If $I$ is an immediate import then, first
 
  \begin{itemize}
  \item
 If  the URI that is the value of $s_1$ has not yet been accessed by an import or export (\ref{exports}) directive  in the current isolate then the contents of the URI  are compiled to yield a library $B$. \commentary{Because libraries may have mutually recursive imports, care must be taken to avoid an infinite regress.
 }
 \item Otherwise, the contents of the URI denoted by $s_1$ have been compiled into a library $B$ within the current isolate.
 \end{itemize}
 
 
 Let $NS_0$ be the exported namespace (\ref{exports}) of $B$. Then, for each combinator clause $C_i, i \in 1..n$ in $I$:
@@ skipping 291 matching lines @@
 %  \item Let $T_i$ be the type parameters of $G$ (if any) and let $B_i$ be the bound of $T_i,  i \in 1.. n$, and $S_i$ is not a subtype of $[S_1,  \ldots, S_n/T_1, \ldots, T_n]B_i,   i \in 1.. n$. 
 %  \end{itemize}
 \end{itemize}
 
  Any use of a malformed  type gives rise to a static warning. A malformed type is then interpreted as \DYNAMIC{} by the static type checker and the runtime unless explicitly specified otherwise.
   
  \rationale{
 This ensures that the developer is spared a series of cascading warnings as the malformed type interacts with other types.
 }
 
+A type $T$ is deferred iff it is of the form $p.T$ where $p$ is a deferred prefix.
+It is a static warning to use a deferred type in a type annotation, type test, type cast or as a type parameter. However, all other static warnings must be issued under the assumption that all deferred libraries have successfully been loaded.
+
 
 \subsubsection{Type Promotion}
 \label{typePromotion}
 
 The static type system ascribes a static type to every expression.  In some cases, the types of local variables and formal parameters may be promoted from their declared types based on control flow. 
 
 We say that a variable $v$ is known to have type $T$ whenever we allow the type of $v$ to be promoted. The exact circumstances when type promotion is allowed are given in the relevant sections of the specification (\ref{logicalBooleanExpressions}, \ref{conditional} and \ref{if}).
 
 Type promotion for a variable $v$ is allowed only when we can deduce that such promotion is valid based on an analysis of certain boolean expressions. In such cases, we say that the boolean expression $b$ shows that $v$ has type $T$. As a rule, for all variables $v$ and types $T$, a boolean expression does not show that $v$ has type $T$. Those situations where an expression does show that a variable has a type are mentioned explicitly in the relevant sections of this specification (\ref{typeTest} and \ref{logicalBooleanExpressions}).
 
 
 \subsection{Dynamic Type System}
 \label{dynamicTypeSystem}
 
 A Dart implementation must support execution in both {\em production mode} and {\em checked mode}.  Those dynamic checks specified as occurring specifically in checked mode must be performed iff the code is executed in checked mode.
 
+\commentary{
+Note that this is the case even if the deferred type belongs to a prefix that has already been loaded. This is regrettable, since it strongly discourages the use of type annotations that involve deferred types because Dart programmers use checked mode much of the time.
+
+In practice, many scenarios involving deferred loading involve deferred loading of classes that implement eagerly loaded interfaces, so the situation is often less onerous than it seems. The current semantics were adopted based on considerations of ease of implementation.
+
+Clearly, if a deferred type has not yet been loaded, it is impossible to do a correct subtype test involving it, and one would expect a dynamic failure, as is the case with type tests and casts. By the same token, one would expect checked mode to work seamlessly once a type had been loaded. We hope to adopt these semantics in the future; such a change would be upwardly compatible.
+
+}
+
 %It is a run-time type error to access an undeclared type outside .
 
 %It is a dynamic type error if a malformed type is used in a subtype test.  
-In checked mode, it is a dynamic type error if a malformed or malbounded (\ref{parameterizedTypes}) 
+In checked mode, it is a dynamic type error if a deferred, malformed or malbounded (\ref{parameterizedTypes}) 
 type is used in a subtype test.  
 
 %In production mode, an undeclared type is treated as an instance of type \DYNAMIC{}. 
 
 \commentary{Consider the following program}
 
 \begin{dartCode}
 \TYPEDEF{} F(bool x);
 f(foo x) $=>$ x;
 main() \{
@@ skipping 565 matching lines @@
 \item The names of compile time constant variables never use lower case letters. If they consist of multiple words, those words are separated by underscores. Examples: PI,  I\_AM\_A\_CONSTANT.
 \item The names of functions (including getters, setters, methods and local or library functions) and non-constant variables begin with a lowercase letter. If the name consists of multiple words, each  word (except the first) begins with an uppercase letter.  No other uppercase letters are used. Examples: camlCase, dart4TheWorld
 \item The names of types (including classes and type aliases) begin with an upper case letter.  If the name consists of multiple words, each  word  begins with an uppercase letter.  No other uppercase letters are used. Examples: CamlCase, Dart4TheWorld.
 \item The names of type variables are short (preferably single letter). Examples: T, S, K, V , E.
 \item The names of libraries or library prefixes never use upper case letters. If they consist of multiple words, those words are separated by underscores. Example: my\_favorite\_library.
 \end{itemize}
 }
 
 
 \end{document}