An attempt to add generic methods to the spec. This is just a draft for purposes of evaluation and …

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index c0b9cff01ea5ff6531cd28400c2b787e7128cc2e..7861c823ce10af0260527828d5e69607e5666536 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -6,8 +6,8 @@
 \usepackage{hyperref}
 \usepackage{lmodern}
 \newcommand{\code}[1]{{\sf #1}}
-\title{Dart Programming Language  Specification \\
-{\large Version 1.10}}
+\title{Dart Programming Language  Specification  - Generic Methods Draft\\
+{\large Version 1.11}}
 
 % For information about Location Markers (and in particular the
 % commands \LMHash and \LMLabel), see the long comment at the
@@ -535,6 +535,7 @@ Otherwise
 
 \LMHash{}
 Functions abstract over executable actions.
+% Need to fix grammar
 
 \begin{grammar}
 {\bf functionSignature:}
@@ -635,6 +636,7 @@ When we say that a function $f_1$ {\em forwards} to another function $f_2$, we m
 \subsection{Formal Parameters}
 \LMLabel{formalParameters}
 
+
 \LMHash{}
 Every function includes a {\em formal parameter list}, which consists of a list of required positional parameters (\ref{requiredFormals}), followed by any optional parameters (\ref{optionalFormals}). The optional parameters may be specified either as a set of named parameters or as a list of positional parameters, but not both.
 
@@ -644,6 +646,10 @@ The formal parameter list of a function introduces a new scope known as the func
 \LMHash{}
 The body of a function introduces a new scope known as the function's {\em  body scope}. The body scope of a function $f$  is enclosed  in the scope introduced by the formal parameter scope of $f$.
 
+\commentary {
+A function may be generic, in which case it also has formal type parameters \ref{generics}. The scope of these includes the formal parameter scope and the body scope of the function, as described in section \ref{generics}.

[Leaf, 2015/06/26 20:54:31]

Scope includes the return type too.

+}
+
 
 %The formal parameter scope of a function maps the name of each formal parameter $p$ to the value $p$ is bound to. 
 
@@ -654,7 +660,12 @@ The body of a function introduces a new scope known as the function's {\em  body
 It is a compile-time error if a formal parameter is declared as a constant variable (\ref{variables}).
 
 \begin{grammar}
-{\bf formalParameterList:}`(' `)';
+
+{\bf formalParameterList:}
+    typeParameters? formalValueParameterList
+   .
+   
+{\bf formalValueParameterList:}`(' `)';
  `(' normalFormalParameters ( `,'  optionalFormalParameters)? `)';
   `(' optionalFormalParameters `)'
    .
@@ -759,13 +770,16 @@ If we allowed named parameters to begin with an underscore, they would be consid
 If a function does not declare a return type explicitly, its return type is \DYNAMIC{} (\ref{typeDynamic}), unless it is a constructor function, in which case its return type is the immediately enclosing class.
 
 \LMHash{}
-Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and no optional parameters. Then the type of $F$ is $(T_1 ,\ldots, T_n) \rightarrow T_0$.
+Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and no optional parameters and no type parameters. Then the type of $F$ is $(T_1 ,\ldots, T_n) \rightarrow T_0$.
 
 \LMHash{}
-Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and positional optional parameters $T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$ $ p_{n+k}$. Then the type of $F$ is $(T_1 ,\ldots, T_n, [T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$  $p_{n+k}]) \rightarrow T_0$.
+Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and positional optional parameters $T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$ $ p_{n+k}$ and no type parameters. Then the type of $F$ is $(T_1 ,\ldots, T_n, [T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$  $p_{n+k}]) \rightarrow T_0$.
 
 \LMHash{}
-Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and named optional parameters $T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$ $ p_{n+k}$. Then the type of $F$ is $(T_1 ,\ldots, T_n, \{T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$  $p_{n+k}\}) \rightarrow T_0$.
+Let $F$ be a function with required formal parameters $T_1$ $p_1 \ldots, T_n$ $p_n$, return type $T_0$ and named optional parameters $T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$ $ p_{n+k}$ and no type parameters. Then the type of $F$ is $(T_1 ,\ldots, T_n, \{T_{n+1}$ $p_{n+1}, \ldots, T_{n+k}$  $p_{n+k}\}) \rightarrow T_0$.
+
+\LMHash{}
+Let $F$ be a generic function with type parameters $S_1 <: B_1 \ldots S_m <: B_m$. If, in the absence of the type parameters, $F$ would have type $\tau$, then $F$ has type $\forall S_1 <: B_1 \ldots S_m <: B_m. \tau$.
 
 \LMHash{}
 The run time type of a function object always implements the class \cd{Function}. 
@@ -947,12 +961,14 @@ It is a static warning if an instance method $m_1$ overrides an instance member
 \subsubsection{Operators}
 \LMLabel{operators}
 
+% So can one declare a generic operator? Only if inference were guaranteed. So we should ban it in the declaration?
+
 \LMHash{}
 {\em Operators} are instance methods with special names. 
 
 \begin{grammar}
 {\bf operatorSignature:}
-       returnType? \OPERATOR{} operator formalParameterList
+       returnType? \OPERATOR{} operator formalValueParameterList
        .
        
  {\bf operator:}`\~{}';
@@ -1053,7 +1069,7 @@ Setters are functions (\ref{functions}) that are used to set the values of objec
 
 \begin{grammar}
 {\bf setterSignature:}
-       returnType? \SET{} identifier formalParameterList
+       returnType? \SET{} identifier formalValueParameterList
 .
 \end{grammar}
 
@@ -1210,7 +1226,7 @@ A {\em generative constructor} consists of a constructor name, a constructor par
 
 \begin{grammar}
 {\bf constructorSignature:}
-      identifier (`{\escapegrammar .}' identifier)? formalParameterList
+      identifier (`{\escapegrammar .}' identifier)? formalValueParameterList
     .
  \end{grammar}
 
@@ -1266,7 +1282,7 @@ A generative constructor may be {\em redirecting}, in which case its only action
 
 \begin{grammar}
 {\bf redirection:}
-     `{\escapegrammar :}' \THIS{} (`{\escapegrammar .}' identifier)? arguments
+     `{\escapegrammar :}' \THIS{} (`{\escapegrammar .}' identifier)? valueArguments
     .
 \end{grammar}
 
@@ -1292,8 +1308,8 @@ An initializer list begins with a colon, and consists of a comma-separated list
     .
 
 
-{\bf superCallOrFieldInitializer:}\SUPER{} arguments;
-      \SUPER{} `{\escapegrammar .}' identifier arguments;
+{\bf superCallOrFieldInitializer:}\SUPER{} valueArguments;
+      \SUPER{} `{\escapegrammar .}' identifier valueArguments;
      fieldInitializer
     .
     
@@ -1393,7 +1409,7 @@ A {\em factory} is a constructor prefaced by the built-in identifier  (\ref{iden
 
 \begin{grammar}
 {\bf factoryConstructorSignature:}
-      \FACTORY{} identifier  (`{\escapegrammar .}' identifier)?  formalParameterList
+      \FACTORY{} identifier  (`{\escapegrammar .}' identifier)?  formalValueParameterList
     .
 \end{grammar}
 
@@ -1424,7 +1440,7 @@ A {\em redirecting factory constructor} specifies a call to a constructor of ano
 
 \begin{grammar}
 {\bf redirectingFactoryConstructorSignature:}
-      \CONST{}? \FACTORY{} identifier (`{\escapegrammar .}' identifier)? formalParameterList `=' type (`{\escapegrammar .}' identifier)?
+      \CONST{}? \FACTORY{} identifier (`{\escapegrammar .}' identifier)? formalValueParameterList `=' type (`{\escapegrammar .}' identifier)?
     .
 \end{grammar}
 
@@ -1514,7 +1530,7 @@ A {\em constant constructor} may be used to create compile-time constant  (\ref{
 
 \begin{grammar}
 {\bf constantConstructorSignature:}
-      \CONST{} qualified formalParameterList
+      \CONST{} qualified formalValueParameterList
     .
 \end{grammar}
 
@@ -1982,19 +1998,25 @@ If some but not all of the $m_i, 1 \le i \le k$ are getters none of the $m_i$ ar
 
 \LMHash{}
 Otherwise, if the static types $T_1, \ldots,  T_k$ of the members $m_1, \ldots,  m_k$  are not identical, then there must be a member $m_x$ such that $T_x <: T_i, 1 \le x \le k$ for all  $i  \in 1..k$, or a static type warning occurs. The member that is inherited  is $m_x$, if it exists; otherwise:
+
+\begin{itemize} %generics
+\item If not all of the  $m_i, i \in 1..k$ are  have the same number $Y$ of type parameters, no member is inherited. \rationale{If we do allow ordinary function types to be subtypes of generic function types, we can replace the above rule and state that if they don't all have the same number of generic parameters, they have none.}
+
+\item Otherwise, 
  let $numberOfPositionals(f)$ denote the number of positional parameters of a function $f$, and let $numberOfRequiredParams(f)$ denote the number of required parameters of a function $f$. Furthermore, let $s$ denote the set of all named parameters of the $m_1, \ldots,  m_k$.  Then let 
 
 $h = max(numberOfPositionals(m_i)), $
 
 $r = min(numberOfRequiredParams(m_i)), i \in 1..k$. 
 
-\LMHash{}
-Then $I$ has a method named $n$, with $r$ required parameters of type \DYNAMIC{}, $h$  positional parameters of type \DYNAMIC{}, named parameters $s$ of type  \DYNAMIC{} and  return type  \DYNAMIC{}.  
-
+\LMHash{} %generics
+Then $I$ has a method named $n$, with $Y$ type parameters with a bound of \DYNAMIC,  $r$ required parameters of type \DYNAMIC, $h$  positional parameters of type \DYNAMIC, named parameters $s$ of type  \DYNAMIC{} and  return type  \DYNAMIC{}.  
 
+% We could be smarter about the bounds, but given that we give up on the all the other types, it seems pointless.
 
 \commentary{The only situation where the runtime would be concerned with this would be during reflection, if a mirror attempted to obtain the signature of an interface member. 
 }
+\end{itemize}
 
 \rationale{
 The current solution is a tad complex, but is robust in the face of type annotation changes.  Alternatives: (a) No member is inherited in case of conflict. (b) The first m is selected (based on order of superinterface list) (c) Inherited member chosen at random. 
@@ -2002,7 +2024,7 @@ The current solution is a tad complex, but is robust in the face of type annotat
 (a) means that the presence of an inherited member of an interface varies depending on type signatures.  (b) is sensitive to irrelevant details of the declaration and (c) is liable to give unpredictable results between implementations or even between different compilation sessions.
 }
 
-% Need warnings if overrider conflicts with overriddee either because signatures are incompatible or because done is a method and one is a getter or setter.
+% Need warnings if overrider conflicts with overriddee either because signatures are incompatible or because one is a method and one is a getter or setter.
 
 \section{Mixins}
 \LMLabel{mixins} 
@@ -2154,8 +2176,8 @@ It is also a compile-time error to subclass, mix-in or implement an enum or to e
 \section{Generics}
 \LMLabel{generics}
 
-\LMHash{}
-A class declaration (\ref{classes}) or type alias (\ref{typedef}) 
+\LMHash{} %generics
+A class declaration (\ref{classes}), type alias (\ref{typedef}) or function (\ref{functions})
 $G$ may be {\em generic}, that is, $G$ may have formal type parameters declared. A generic declaration induces a family of declarations, one for each set of actual type parameters provided in the program. 
 
 \begin{grammar}
@@ -2171,8 +2193,8 @@ $G$ may be {\em generic}, that is, $G$ may have formal type parameters declared.
 A type parameter $T$ may be suffixed with an \EXTENDS{} clause that specifies the {\em upper bound} for $T$. If no  \EXTENDS{} clause is present, the upper bound is \code{Object}.  It is a static type warning if a type parameter is a supertype of its upper bound. The bounds of type variables are a form of type annotation and have no effect on execution in production mode.

[Leaf, 2015/06/26 22:32:16]

It is a static warning if the bound of a type parameter is a universal type.

 
 \LMHash{}
-Type parameters are declared in the type-parameter scope of a class.
-The type parameters of a generic $G$ are in scope in the bounds of all of the type parameters of $G$. The type parameters of a generic class declaration $G$ are also in scope in the \EXTENDS{} and \IMPLEMENTS{} clauses of $G$ (if these exist) and in the body of $G$.   However, a type parameter is considered to be a malformed type when referenced by a static member.
+Type parameters are declared in the type-parameter scope of a class or function.
+The type parameters of a generic $G$ are in scope in the bounds of all of the type parameters of $G$. The type parameters of a generic class declaration $G$ are also in scope in the \EXTENDS{} and \IMPLEMENTS{} clauses of $G$ (if these exist) and in the body of $G$.   However, a class' type parameter is considered to be a malformed type when referenced by a static member.
 
 \rationale{
 The restriction is necessary since a type variable has no meaning in the context of a static member, because statics are shared among all instantiations of a generic. However, a type variable may be referenced from an instance initializer, even though \THIS{} is not available. 
@@ -2284,7 +2306,7 @@ Dart supports metadata which is used to attach user defined annotations to progr
 
 \begin{grammar}
 {\bf metadata:}
-      (`@' qualified ({\escapegrammar `.'} identifier)? (arguments)?)*
+      (`@' qualified ({\escapegrammar `.'} identifier)? (valueArguments)?)*
     .
 \end{grammar}
 
@@ -3193,8 +3215,15 @@ $(T_1$ $a_1, \ldots, T_n$ $a_n, \{T_{n+1}$ $x_{n+1} : d_1, \ldots,  T_{n+k}$ $x_
 is $(T_1 \ldots, T_n, \{T_{n+1}$ $x_{n+1}, \ldots, T_{n+k}$ $x_{n+k}\}) \rightarrow  Iterable{}$.
 
 \LMHash{}
+Let $F$ be a generic function literal with type parameters $S_1 <: B_1 \ldots S_m <: B_m$. If, in the absence of the type parameters, $F$ would have type $\tau$, then $F$ has type $\forall S_1 <: B_1 \ldots S_m <: B_m. \tau$.
+
+\LMHash{}
 In all of the above cases, whenever $T_i, 1 \le i \le n+k$, is not specified, it is considered to have been specified as  \DYNAMIC{}.
 
+\LMHash{} %generic
+The static type of a function literal of the form 
+$<P_1$ \EXTENDS{} $B_1, \ldots, P_l$ \EXTENDS{} $B_l> f$ is $\forall P_1 <: B_1, \ldots, P_l <: B_l. fsig$, where $fsig$ is the static type of $f$.
+
 
 \subsection{ This}
 \LMLabel{this}
@@ -3263,7 +3292,7 @@ The {\em new expression} invokes a constructor (\ref{constructors}).
 
 \begin{grammar}
 {\bf newExpression:}
-\NEW{} type (`{\escapegrammar .}' identifier)? arguments
+\NEW{} type (`{\escapegrammar .}' identifier)? valueArguments
 .
 \end{grammar}
 
@@ -3381,7 +3410,7 @@ A {\em constant object expression} invokes a constant constructor (\ref{constant
 
 \begin{grammar}
 {\bf constObjectExpression:}
-\CONST{} type ('{\escapegrammar .}' identifier)? arguments
+\CONST{} type ('{\escapegrammar .}' identifier)? valueArguments
 .
 \end{grammar}
 
@@ -3507,8 +3536,8 @@ As discussed in section \ref{errorsAndWarnings}, the handling of a suspended iso
 \subsection{ Function Invocation}
 \LMLabel{functionInvocation}
  
-\LMHash{}
-Function invocation occurs in the following cases: when a function expression  (\ref{functionExpressions}) is invoked (\ref{functionExpressionInvocation}), when a method (\ref{methodInvocation}), getter (\ref{topLevelGetterInvocation}, \ref{propertyExtraction}) or setter (\ref{assignment}) is invoked or when a constructor is invoked (either via instance creation (\ref{instanceCreation}), constructor redirection (\ref{redirectingConstructors}) or super initialization). The various kinds of function invocation differ as to how the function to be invoked, $f$,  is determined, as well as whether \THIS{} (\ref{this}) is bound. Once $f$ has been determined, the formal parameters of $f$ are bound to corresponding actual arguments. When the body of $f$ is executed it will be executed with the aforementioned bindings. 
+\LMHash{} %generics
+Function invocation occurs in the following cases: when a function expression  (\ref{functionExpressions}) is invoked (\ref{functionExpressionInvocation}), when a method (\ref{methodInvocation}), getter (\ref{topLevelGetterInvocation}, \ref{propertyExtraction}) or setter (\ref{assignment}) is invoked or when a constructor is invoked (either via instance creation (\ref{instanceCreation}), constructor redirection (\ref{redirectingConstructors}) or super initialization). The various kinds of function invocation differ as to how the function to be invoked, $f$,  is determined, as well as whether \THIS{} (\ref{this}) is bound. Once $f$ has been determined, the formal type and value parameters of $f$ are bound to corresponding actual arguments. When the body of $f$ is executed it will be executed with the aforementioned bindings. 
 
 \LMHash{}
 If $f$ is marked \ASYNC{} (\ref{functions}), then a fresh instance (\ref{generativeConstructors}) $o$ implementing the built-in class \code{Future} is associated with the invocation and immediately returned to the caller. The body of $f$ is scheduled for execution at some future time. The future $o$ will complete when $f$ terminates. The value used to complete $o$ is the current return value (\ref{return}), if it is defined, and the current exception (\ref{throw}) otherwise. 
@@ -3597,6 +3626,10 @@ Function invocation involves evaluation of the list of actual arguments to the f
 
 \begin{grammar}
 {\bf arguments:}
+      typeArguments? valueArguments
+    .
+    
+{\bf valueArguments:}
       `(' argumentList? `)'
     .
 
@@ -3629,10 +3662,26 @@ The arguments $a_1, \ldots, a_{m+l}$ are evaluated in the order they appear in t
 \LMLabel{bindingActualsToFormals}
 
 \LMHash{}
-Let $f$ be a function with $h$ required parameters,  let $p_1 \ldots p_n$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+k}$ be the optional parameters declared by $f$.
+Let $f$ be a function with $s$ type parameters, $h$ required parameters,  let $p_1 \ldots p_n$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+k}$ be the optional parameters declared by $f$.
 
 \LMHash{}
-An evaluated actual argument list $o_1 \ldots o_{m+l}$ derived from an actual argument list of the form $(a_1, \ldots, a_m, q_1: a_{m+1}, \ldots, q_l: a_{m+l})$ is bound to the formal parameters of $f$ as follows:
+An evaluated actual argument list $o_1 \ldots o_{m+l}$ derived from an actual argument list of the form $<A_1, \ldots, A_r>(a_1, \ldots, a_m, q_1: a_{m+1}, \ldots, q_l: a_{m+l})$ is bound to the formal parameters of $f$ as follows:
+
+\commentary{
+If type arguments are absent, they are taken to be \DYNAMIC. 
+
+We have two possible semantics when the number of type arguments is non-zero and differs from the number of type parameters:
+
+1. If type arguments are provided ($r \ne 0$), their number must match the number of formal type parameters.
+
+2. If there are no type parameters ($s = 0$), any type arguments are ignored. Otherwise the number of type arguments  must match the number of formal type parameters ($r = s$).
+}
+
+\LMHash{}
+If $r = 0$, the formal type parameters of $f$ are all bound to \DYNAMIC. 
+If $s = 0$ any type arguments are ignored. \rationale { This last sentence may be dropped if we choose to go with the simpler but less compatible semantics.}
+Otherwise,  $r = s$, then each formal type parameter is bound to the corresponding type argument.  

[Leaf, 2015/06/26 22:32:16]

Generic restriction: If A_i is a universal type, then it is replaced with
\DYNAMIC.

+
 
 \commentary{
 We have an argument list consisting of $m$ positional arguments and $l$ named arguments. We have a function with $h$ required parameters and $k$ optional parameters. The number of positional arguments must be at least as large as the number of required parameters, and no larger than the number of positional parameters. All named arguments must have a corresponding named parameter. You may not provide a given named argument more than once.  If an optional parameter has no corresponding argument, it gets its default value. In checked mode, all arguments must belong to subtypes of the type of their corresponding formal.
@@ -3642,20 +3691,21 @@ We have an argument list consisting of $m$ positional arguments and $l$ named ar
 If $l > 0$, then it is necessarily the case that $n = h$, because a method cannot have both optional positional parameters and named parameters.
 }
 
-
 \LMHash{}
-If  $m < h$, or $m > n$, a \cd{NoSuchMethodError} is thrown. Furthermore, each $q_i, 1 \le i \le l$,  must have a corresponding named parameter in the set $\{p_{n+1}, \ldots, p_{n +k}\}$ or a \cd{NoSuchMethodError} is thrown. Then $p_i$ is bound to $o_i, i \in 1.. m$, and $q_j$  is bound to $o_{m+j}, j \in 1.. l$.  All remaining formal parameters of $f$  are bound to their default values. 
+%If  $m < h$, or $m > n$, a \cd{NoSuchMethodError} is thrown. Furthermore, each $q_i, 1 \le i \le l$,  must have a corresponding named parameter in the set $\{p_{n+1}, \ldots, p_{n +k}\}$ or a \cd{NoSuchMethodError} is thrown. 
+Then $p_i$ is bound to $o_i, i \in 1.. m$, and $q_j$  is bound to $o_{m+j}, j \in 1.. l$.  All remaining formal parameters of $f$  are bound to their default values. 
 
 \commentary{All of these remaining parameters are necessarily optional and thus have default values.}
 
 \LMHash{}
 In checked mode, it is a dynamic type error if  $o_i$ is not \NULL{} and the actual type  (\ref{actualTypeOfADeclaration}) of $p_i$ is not a supertype of the type of $o_i, i \in 1.. m$. In checked mode, it is a dynamic type error if  $o_{m+j}$ is not \NULL{} and the actual type  (\ref{actualTypeOfADeclaration}) of $q_j$ is not a supertype of the type of $o_{m+j}, j \in 1.. l$.
+In checked mode, it is a dynamic error if $A_i, 1 \le i \le r$ is not a subtype of the actual type bound of the corresponding type parameter.
 
 \LMHash{}
 It is a compile-time error if $q_i = q_j$ for any $i \ne j$.
 
 \LMHash{}
-Let $T_i$ be the static type of $a_i$, let $S_i$ be the type of $p_i, i \in 1 .. h+k$ and let $S_q$ be the type of the named parameter $q$ of $f$.  It is a static warning if $T_j$ may not be assigned to $S_j, j \in 1..m$.  It is a static warning if $m < h$ or if $m > n$. Furthermore, each $q_i, 1 \le i \le l$,  must have a corresponding named parameter in the set $\{p_{n+1}, \ldots, p_{n +k}\}$ or a static warning occurs.  It is a static warning if $T_{m+j}$ may not be assigned to $S_{q_j}, j \in 1 .. l$.
+Let $T_i$ be the static type of $a_i$, let $S_i$ be the actual type of $p_i, i \in 1 .. h+k$ and let $S_q$ be the actual type of the named parameter $q$ of $f$.  It is a static warning if $T_j$ may not be assigned to $S_j, j \in 1..m$.  It is a static warning if $m < h$ or if $m > n$. Furthermore, each $q_i, 1 \le i \le l$,  must have a corresponding named parameter in the set $\{p_{n+1}, \ldots, p_{n +k}\}$ or a static warning occurs.  It is a static warning if $T_{m+j}$ may not be assigned to $S_{q_j}, j \in 1 .. l$.
 
 \subsubsection{ Unqualified Invocation}
 \LMLabel{unqualifiedInvocation}
@@ -3663,7 +3713,7 @@ Let $T_i$ be the static type of $a_i$, let $S_i$ be the type of $p_i, i \in 1 ..
 \LMHash{}
 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})$, 
+$id<A_1, \ldots,  A_r>(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$, 
 
 where $id$ is an identifier. 
 
@@ -3673,8 +3723,8 @@ If there exists a lexically visible declaration named $id$, let $f_{id}$ be the
 \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})$.
+Otherwise, if $f_{id}$ is a static method of the enclosing class $C$, $i$ is equivalent to $C.id<A_1, \ldots,  A_r>(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_r>(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})$.  
@@ -3687,7 +3737,7 @@ Otherwise, if $f_{id}$ is a static method of the enclosing class $C$, $i$ is equ
 Otherwise, if $i$ occurs inside a top level or static function (be it function, method, getter,  or setter) or variable initializer, evaluation of $i$ causes a \cd{NoSuchMethodError} to be thrown.
 
 \LMHash{}
-If $i$ does not occur inside a top level or static function, $i$ is equivalent to $\THIS{}.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+If $i$ does not occur inside a top level or static function, $i$ is equivalent to $\THIS{}.id<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 % Should also say:
 % It is a static warning if $i$  occurs inside a top level or static function (be it function, method, getter,  or setter) or variable initializer and there is no lexically visible declaration named $id$ in scope.
@@ -3702,7 +3752,7 @@ If $i$ does not occur inside a top level or static function, $i$ is equivalent t
 \LMHash{}
 A function expression invocation $i$ has the form 
 
-$e_f(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$, 
+$e_f<A_1, \ldots,  A_m>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$, 
 
 where $e_f$ is an expression. If $e_f$ is an identifier $id$, then $id$ must necessarily denote a local function, a library function, a library or static getter or a variable as described above, or $i$ is not considered a function expression invocation. If $e_f$ is a property extraction expression (\ref{propertyExtraction}), then $i$ is is not a function expression invocation and is instead recognized as an ordinary method invocation (\ref{ordinaryInvocation}). 
 
@@ -3713,7 +3763,7 @@ where $e_f$ is an expression. If $e_f$ is an identifier $id$, then $id$ must nec
 \LMHash{}
 Otherwise:
 
-A function expression invocation $e_f(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is equivalent to $e_f.call(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+A function expression invocation $e_f<A_1, \ldots,  A_m>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is equivalent to $e_f.call<A_1, \ldots,  A_m>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \commentary{
 The implication of this definition, and the other definitions involving the method \code{call()}, is that user defined types can be used as function values provided they define a \CALL{} method. The method \CALL{} is special in this regard. The signature of the \CALL{} method determines the signature used when using the object via the built-in invocation syntax.
@@ -3721,7 +3771,7 @@ The implication of this definition, and the other definitions involving the meth
 
 \LMHash{}
 It is a static warning if the static type $F$ of $e_f$ may not be assigned to a function type.  If $F$ is not a function type, the static type of $i$ is \DYNAMIC{}. Otherwise 
-the static type of $i$ is the declared return type of  $F$.  
+the static type of $i$ is the actual return type (\ref{actualTypeOfADeclaration})  of  $F$.  
 %\item Let $T_i$ be the static type of $a_i, i \in 1 .. n+k$. It is a static warning if $F$ is not a supertype of  $(T_1, \ldots, T_n, [T_{n+1}$ $x_{n+1}, \ldots, T_{n+k}$ $x_{n+k}]) \to \bot$.
 %\end{itemize}
 
@@ -3789,13 +3839,13 @@ An ordinary method invocation can be {\em conditional} or {\em unconditional}.
 Evaluation of a {\em conditional ordinary method invocation} $e$ of the form 
 
 \LMHash{}
-$o?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$  
+$o?.m<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$  
 
 \LMHash{}
 is equivalent to the evaluation of the expression  
 
 \LMHash{}
-$((x) => x == \NULL ? \NULL : x.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k}))(o)$. 
+$((x) => x == \NULL ? \NULL : x.m<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k}))(o)$. 
 
 \LMHash{}
 The static type of $e$ is the same as the static type of $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. Exactly the same static warnings that would be caused by $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ are also generated in the case of $o?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
@@ -3803,12 +3853,12 @@ The static type of $e$ is the same as the static type of $o.m(a_1, \ldots , a_n,
 \LMHash{}
 An {\em unconditional ordinary method invocation} $i$ has the form 
 
-$o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+$o.m<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
 Evaluation of an unconditional ordinary method invocation $i$ of the form 
 
-$o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ 
+$o.m<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ 
 
 proceeds as follows:
 
@@ -3816,23 +3866,46 @@ proceeds as follows:
 First, the expression $o$ is evaluated to a value $v_o$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $f$ be the result of looking up (\ref{methodLookup}) method $m$  in $v_o$ with respect to the current library $L$. 
 
 \LMHash{}
-Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
+Let $T_1 \ldots T_s$ be the type parameters of $f$, 
+let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
 
 \commentary{
 We have an argument list consisting of $n$ positional arguments and $k$ named arguments. We have a function with $h$ required parameters and $l$ optional parameters. The number of positional arguments must be at least as large as the number of required parameters, and no larger than the number of positional parameters. All named arguments must have a corresponding named parameter. 
+
+The argument list also contains $r$ type arguments, and the function has $s$ formal type parameters. If $r$ and $s$ are non-zero, they must match.
+
+If $r = 0$ then we simply pass in \DYNAMIC{} as described in section \ref{bindingActualsToFormals}. 
+
+If $s = 0$ then we ignore any type arguments.
+}
+
+\rationale{
+
+We have a choice between two semantics:
+
+One in which parametrically polymorphic function types are  subtypes of non-parametrically polymorphic ones, and one in which they are not. The commentary reflects the former, as it is more compatible, though harder to implement. 

[Leaf, 2015/06/26 20:54:31]

" One in which parametrically polymorphic function types are  subtypes of
non-parametrically polymorphic ones, and one in which they are not. "

I think this is backwards - we always allow universals to subtype
non-universals.  The question is whether we allow non-universals to subtype
universals.

+
+Both options are listed in the normative text below.
+To choose one option or the other here, we eliminate one of the normative lines directly below this remark, and modify the commentary as needed.
 }
 
 \LMHash{}
+If $r \ne s$ and $r \ne 0$ the method lookup has failed.
+
+\LMHash{}
+If $r \ne s$ and either $r \ne 0$ or $s \ne 0$, the method lookup has failed.
+

[Leaf, 2015/06/26 22:32:16]

Generic restriction: If A_i is a universal type, then it is replaced with
\DYNAMIC.

+
 If  $n < h$, or $n > m$, the method lookup has failed. Furthermore, each $x_i, n+1 \le i \le n+k$,  must have a corresponding named parameter in the set $\{p_{m+1}, \ldots, p_{h+l}\}$ or the method lookup also fails.  If $v_o$ is an instance of \code{Type} but $o$ is not a constant type literal, then if $m$ is a method that forwards (\ref{functionDeclarations}) to a static method, method lookup fails. Otherwise method lookup has succeeded.
 
 \LMHash{}
-If the method lookup succeeded, the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list, and with \THIS{} bound to $v_o$. The value of $i$ is the value returned after $f$ is executed.
+If the method lookup succeeded, the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list,  with \THIS{} bound to $v_o$. The value of $i$ is the value returned after $f$ is executed.
 
 \LMHash{}
 If the method lookup has failed, then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $v_o$ with respect to $L$. 
 If $v_o$ is an instance of \code{Type} but $o$ is not a constant type literal, then if $g$ is a getter that forwards to a static getter, getter lookup fails.
 If the getter lookup succeeded, let $v_g$ be the value of the getter invocation $o.m$. Then the value of $i$ is the result of invoking 
-the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}$.
+the static method \code{Function.apply()} with arguments $v_g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}, [A_1, \ldots, A_r]$.
 
 \LMHash{}
 If  getter lookup has also failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
@@ -3841,6 +3914,7 @@ If  getter lookup has also failed, then a new instance $im$  of the predefined c
 \item  \code{im.memberName} evaluates to the symbol \code{m}.
 \item \code{im.positionalArguments} evaluates to an immutable list with the same values as  \code{[$o_1, \ldots, o_n$]}.
 \item \code{im.namedArguments} evaluates to an immutable map with the same keys and values as \code{\{$x_{n+1}: o_{n+1}, \ldots, x_{n+k} : o_{n+k}$\}}.
+\item \code{im.typeArguments} evaluates to an immutable list with the same values as  \code{[$A_1, \ldots, A_r$]}. \rationale{We need to pass the actual type arguments used to \cd{noSuchMethod}, which is why we use the $A_i$.   If no argument were passed, the list will be empty (rather than being a list of $s$ occurrences of \DYNAMIC). The handler can then recognize this and  choose to use \DYNAMIC{} at its discretion.}
 \end{itemize}
 
 \LMHash{}
@@ -3850,6 +3924,7 @@ Then the method \code{noSuchMethod()} is looked up in $v_o$ and invoked with arg
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im'.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 and the result of the latter invocation is the result of evaluating $i$.
@@ -3914,14 +3989,24 @@ The present specification has not added such a construct, in the interests of si
 \LMHash{}
 A super method invocation $i$ has the form 
 
-$\SUPER{}.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+$\SUPER{}.m<A_1, \ldots,  A_r>(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
 Evaluation of $i$ proceeds as follows:
 
 \LMHash{}
 First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated  yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $S$ be the superclass of the immediately enclosing class, and let $f$ be the result of looking up method (\ref{methodLookup})  $m$ in $S$  with respect to the current library $L$. 
-Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
+Let $T_1 \ldots T_s$ be the type parameters of $f$,  let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
+
+
+\rationale{Again, we have a choice between the next two lines}
+
+\LMHash{}
+If $r \ne s$ and $r \ne 0$ the method lookup has failed.
+
+\LMHash{}
+If $r \ne s$ and either $r \ne 0$ or $s \ne 0$, the method lookup has failed.
+

[Leaf, 2015/06/26 22:32:17]

Generic restriction: If A_i is a universal type, then it is replaced with
\DYNAMIC.

 
 \LMHash{}
 If  $n < h$, or $n > m$, the method lookup has failed. Furthermore, each $x_i, n+1 \le i \le n+k$,  must have a corresponding named parameter in the set $\{p_{m+1}, \ldots, p_{h+l}\}$ or the method lookup also fails.  Otherwise method lookup has succeeded.
@@ -3931,7 +4016,7 @@ If the method lookup succeeded, the body of $f$ is executed with respect to the
 
 \LMHash{}
 If the method lookup has failed, then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $S$ with respect to $L$. If the getter lookup succeeded, let $v_g$ be the value of the getter invocation $\SUPER{}.m$. Then the value of $i$ is the result of invoking 
-the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}$.
+the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}, [A_1, \ldots, A_r]$.
  
 \LMHash{}
 If  getter lookup has also failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
@@ -3940,6 +4025,7 @@ If  getter lookup has also failed, then a new instance $im$  of the predefined c
 \item  \code{im.memberName} evaluates to the symbol \code{m}.
 \item \code{im.positionalArguments} evaluates to an immutable list with the same  values as  \code{[$o_1, \ldots, o_n$]}.
 \item \code{im.namedArguments} evaluates to an immutable map with the same keys and values as \code{\{$x_{n+1}: o_{n+1}, \ldots, x_{n+k} : o_{n+k}$\}}.
+\item \code{im.typeArguments} evaluates to an immutable list with the same values as  \code{[$A_1, \ldots, A_r$]}.
 \end{itemize}
 Then the method \code{noSuchMethod()} is looked up in $S$ and invoked on \THIS{} with argument $im$, and the result of this invocation is the result of evaluating $i$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
@@ -3947,6 +4033,7 @@ Then the method \code{noSuchMethod()} is looked up in $S$ and invoked on \THIS{}
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 and the result of this latter invocation is the result of evaluating $i$.
@@ -3956,7 +4043,7 @@ and the result of this latter invocation is the result of evaluating $i$.
 It is a compile-time error if a super method invocation occurs in a top-level function or variable initializer, in an instance variable initializer or initializer list, in class \code{Object}, in a factory constructor or in a static method or variable initializer.
 
 \LMHash{}
-It is a static type warning if $S$ does not have an accessible (\ref{privacy}) instance member named $m$ unless $S$ or a superinterface of $S$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. If $S.m$ exists, it  is a static type warning if the type $F$ of $S.m$ may not be assigned to a function type. If $S.m$ does not exist, or if $F$ is not a function type, the static type of $i$ is \DYNAMIC{}; otherwise the static type of $i$ is the declared return type of  $F$.  
+It is a static type warning if $S$ does not have an accessible (\ref{privacy}) instance member named $m$ unless $S$ or a superinterface of $S$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. If $S.m$ exists, it  is a static type warning if the type $F$ of $S.m$ may not be assigned to a function type. If $S.m$ does not exist, or if $F$ is not a function type, the static type of $i$ is \DYNAMIC{}; otherwise the static type of $i$ is the actual return type of  $F$.  
 % The following is not needed because it is specified in 'Binding Actuals to Formals"
 %Let $T_i$ be the static type of $a_i, i \in 1 .. n+k$. It is a static warning if $F$ is not a supertype of  $(T_1, \ldots, t_n, \{T_{n+1}$ $x_{n+1}, \ldots, T_{n+k}$ $x_{n+k}\}) \to \bot$.
 
@@ -4027,6 +4114,7 @@ If the getter lookup has failed, then a new instance $im$  of the predefined cla
 \item  \code{im.memberName} evaluates to the symbol \code{m}.
 \item \code{im.positionalArguments} evaluates to the value of \code{\CONST{} []}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 Then the method \code{noSuchMethod()} is looked up in $o$ and invoked  with argument $im$, and the result of this invocation is the result of evaluating $i$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on $o$ with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
@@ -4034,6 +4122,7 @@ Then the method \code{noSuchMethod()} is looked up in $o$ and invoked  with argu
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 and the result of this latter invocation is the result of evaluating $i$.
@@ -4083,6 +4172,7 @@ If the getter lookup has failed, then a new instance $im$  of the predefined cla
 \item  \code{im.memberName} evaluates to the symbol \code{m}.
 \item \code{im.positionalArguments} evaluates to the value of \code{\CONST{} []}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} 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$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
@@ -4090,6 +4180,7 @@ Then the method \code{noSuchMethod()} is looked up in $S$ and invoked  with argu
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 and the result of this latter invocation is the result of evaluating $i$.
 
@@ -4238,19 +4329,19 @@ The {\em closurization of method $f$ on object $o$} is defined to be equivalent
 \item $(a, b) \{\RETURN{}$ $u[a] = b;$\} if $f$ is named $[]=$.
 \item  
 \begin{dartCode}
-$(r_1, \ldots, r_n, \{p_1 : d_1, \ldots , p_k : d_k\})$ \{
-  \RETURN{} $ u.m(r_1, \ldots, r_n, p_1: p_1, \ldots, p_k: p_k);$
+$<T_1, \ldots,  T_s>(r_1, \ldots, r_n, \{p_1 : d_1, \ldots , p_k : d_k\})$ \{
+  \RETURN{} $ u.m<T_1, \ldots,  T_s>(r_1, \ldots, r_n, p_1: p_1, \ldots, p_k: p_k);$
 \} 
 \end{dartCode}
-if $f$ is named $m$ and has required parameters $r_1, \ldots, r_n$, and named parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
+if $f$ is named $m$ and has type parameters  $T_1, \ldots,  T_s$, required parameters $r_1, \ldots, r_n$, and named parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
 \item 
 \begin{dartCode}
-$(r_1, \ldots, r_n, [p_1 = d_1, \ldots , p_k = d_k])$\{
-  \RETURN{} $u.m(r_1, \ldots, r_n, p_1, \ldots, p_k)$;
+$<T_1, \ldots,  T_s>(r_1, \ldots, r_n, [p_1 = d_1, \ldots , p_k = d_k])$\{
+  \RETURN{} $u.m<T_1, \ldots,  T_s>(r_1, \ldots, r_n, p_1, \ldots, p_k)$;
 \}
 \end{dartCode}
 
-if $f$ is named $m$ and has required parameters $r_1, \ldots, r_n$, and optional positional parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
+if $f$ is named $m$ and has  type parameters  $T_1, \ldots,  T_s$, required parameters $r_1, \ldots, r_n$, and optional positional parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
 \end{itemize}
 
 \LMHash{}
@@ -4353,19 +4444,19 @@ The {\em closurization of method $f$ with respect to superclass $S$} is defined
 \item $(a, b) \{\RETURN{}$ $\SUPER[a] = b;$\} if $f$ is named $[]=$.
 \item  
 \begin{dartCode}
-$(r_1, \ldots, r_n, \{p_1 : d_1, \ldots , p_k : d_k\})$ \{
+$<T_1, \ldots,  T_s>(r_1, \ldots, r_n, \{p_1 : d_1, \ldots , p_k : d_k\})$ \{
   \RETURN{} \SUPER$.m(r_1, \ldots, r_n, p_1: p_1, \ldots, p_k: p_k);$
 \} 
 \end{dartCode}
-if $f$ is named $m$ and has required parameters $r_1, \ldots, r_n$, and named parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
+if $f$ is named $m$ and has  type parameters  $T_1, \ldots,  T_s$, required parameters $r_1, \ldots, r_n$, and named parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
 \item 
 \begin{dartCode}
-$(r_1, \ldots, r_n, [p_1 = d_1, \ldots , p_k = d_k])$\{
+$<T_1, \ldots,  T_s>(r_1, \ldots, r_n, [p_1 = d_1, \ldots , p_k = d_k])$\{
   \RETURN{} \SUPER$.m(r_1, \ldots, r_n, p_1, \ldots, p_k)$;
 \}
 \end{dartCode}
 
-if $f$ is named $m$ and has required parameters $r_1, \ldots, r_n$, and optional positional parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
+if $f$ is named $m$ and has type parameters  $T_1, \ldots,  T_s$,  required parameters $r_1, \ldots, r_n$, and optional positional parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
 \end{itemize}
 
 \LMHash{}
@@ -4447,6 +4538,7 @@ If the setter lookup has failed, then a new instance $im$  of the predefined cla
 \item  \code{im.memberName} evaluates to the symbol \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{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 \LMHash{}
@@ -4457,6 +4549,7 @@ However, if the implementation found cannot be invoked with a single positional
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 \LMHash{}
@@ -4491,6 +4584,7 @@ If the setter lookup has failed, then a new instance $im$  of the predefined cla
 \item  \code{im.memberName} evaluates to the symbol \code{v=}.
 \item \code{im.positionalArguments} evaluates to an immutable list with the same values as \code{[$o$]}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 \LMHash{}
@@ -4501,6 +4595,7 @@ However, if the implementation found cannot be invoked with a single positional
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
+\item \code{im.typeArguments} evaluates to the value of \code{\CONST{} []}.
 \end{itemize}
 
 \LMHash{}
@@ -5016,7 +5111,6 @@ A postfix expression of the form \code{$v$++}, where $v$ is an identifier, is eq
 
 \rationale{The above ensures that if $v$ is a field, the getter gets called exactly once. Likewise in the cases below. 
 }
-%what about e?.x++ 
 
 \LMHash{}
 A postfix expression of the form \code{$C.v$ ++} is equivalent to 
@@ -6907,8 +7001,12 @@ A URI of the form \code{dart:$s$} is interpreted as a reference to a system libr
 \LMHash{}
 A URI of the form \code{package:$s$} is interpreted in an implementation specific manner.
 
+\commentary{ 
+This location will often be the location of the root library presented to the Dart compiler. However, implementations may supply means to override or replace this choice.
+}
+
 \rationale{
-The intent is that, during development, Dart programmers can rely on a package manager to find elements of their program. 
+The intent is that, during development, Dart programmers can rely on a package manager to find elements of their program.
 }
 
 \LMHash{}
@@ -7207,6 +7305,9 @@ For example, assigning a value of static type Object to a variable with static t
 \subsection{Function Types}
 \LMLabel{functionTypes}
 
+\subsubsection{Ordinary Function Types}
+\LMLabel{ordinaryFunctionTypes}
+
 \LMHash{}
 Function types come in two variants: 
 \begin{enumerate}
@@ -7323,6 +7424,41 @@ A function type $(T_1, \ldots T_n, \{T_{x_1}$ $x_1, \ldots, T_{x_k}$ $x_k\}) \ri
 \LMHash{}
 Furthermore, if $F$ is a function type, $F << \code{Function}$.
 
+\subsubsection{Generic Function Types}
+\LMLabel{genericFunctionTypes} %generics
+
+
+ A generic function type has the form $\forall T_1 <: B_1, \ldots, T_k <: B_k. F$ where $F$  is an ordinary function type.
+ 
+ Let  $G_1 = \forall S_1 <: B_1, \ldots, S_k <: B_k. F_1$ and $G_2 = \forall T_1 <: C_1, \ldots, T_k <: C_k. F_2$.  Then $G_1 <: G_2$ iff $B_i <: C_i$ and $F_1 <: [S_i/T_i] F_2, i \in 1 .. k$.
+ 
+ \rationale{
+ The rule is covariant, in keeping with Dart's other rules for generics, and for the same reasons.
+
+}
+ 
+ A generic function type $G = \forall T_1 <: B_1, \ldots, T_k <: B_k. F$ is a subtype of an ordinary function type $F'$  iff $[\DYNAMIC/T_i] F <: F', i \in 1 .. k$.
+ 
+ \rationale{
+ It is essential that a generic function may be used without the arguments. Dart, by design, never insists on the use of type information. So even if a function is declared with type parameters, users of the function must be free to call it without type arguments. 
+ 
+Even if we did not insist on the former point on principle, there are many functions in the Dart libraries that would benefit from the use of type parameters.  If these are to be changed, it is also crucial for compatibility that their callers may continue to use them without type arguments. 
+ 
+In light of the broad arguments given in the two preceding paragraphs, we can now explain the above type rule in detail. When used without actual type arguments, the generic function will use type \DYNAMIC{} as the default value for its type parameters. Hence, if we substitute \DYNAMIC{} for all uses of the formal type parameters in the generic function type and the resulting function type is a subtype of an ordinary function type, we are assured the generic function can be used in place of the non-generic one.
+}
+
+{\bf Hypothetical:}
+
+An ordinary function $F$ is a subtype of a generic function $G = \forall T_1 <: B_1, \ldots, T_k <: B_k. F'$  iff $F <: [B_i/T_i] F'$.
+
+\rationale{
+
+It would be extremely attractive to have this rule, allowing ordinary functions to be used where generic functions are expected. The motivation here would also be compatibility. If an existing method were converted to be generic, subclasses and implementors would no longer be valid. At the very least, their declarations would now provoke warnings.  Worse, if existing uses of such APIs evolved to pass actual type arguments, the code would crash.
+
+This leads to the proposed rule above. 
+ }
+ 
+
 
 \subsection{Type \DYNAMIC{}}
 \LMLabel{typeDynamic}
@@ -7471,7 +7607,7 @@ The least upper bound relation is symmetric and reflexive.
 
 \LMHash{}
 The least upper bound of a function type and an interface type $T$ is the least upper bound of \cd{Function} and $T$.
-Let $F$ and $G$ be function types. If $F$ and $G$ differ in their number of required parameters, then the least upper bound of $F$ and $G$ is \cd{Function}.  Otherwise:
+Let $F$ and $G$ be function types. If $F$ and $G$ differ in their number of required parameters, then the least upper bound of $F$ and $G$ is \cd{Function}. Otherwise:
 \begin{itemize}
 \item If 
 
@@ -7496,7 +7632,7 @@ $(L_1 \ldots L_r) \longrightarrow L_0$
 
 where $L_i$ 
 is the least upper bound of $T_i$ and $S_i, i \in 0..r$.
-\item If 
+\item If  
 
 $F= (T_1 \ldots T_r, \{T_{r+1}$  $p_{r+1}, \ldots, T_f$ $p_f\}) \longrightarrow T_0$,  
 
@@ -7508,6 +7644,36 @@ the least upper bound of $F$ and $G$ is
 $(L_1 \ldots L_r, \{ X_m$ $x_m, \ldots, X_n$ $x_n\}) \longrightarrow L_0$ 
 
 where $L_i$ is the least upper bound of $T_i$ and $S_i, i \in 0..r$ 
+
+\item If
+
+$F = \forall P_1 <: B_1, \ldots, P_n <: B_m. fsig$
+
+$G = \forall Q_1 <: C_1, \ldots, Q_n <: C_m. gsig$
+
+then
+the least upper bound of $F$ and $G$ is
+$\forall R_1 <: L_1, \ldots, R_n <: L_n. lsig$ where
+$L_i$ is the least upper bound of $[R_j/P_j]_{j=1}^{i}B_i$ and $[R_j/Q_j]_{j=1}^{i}C_i, i \in 1..n$ and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$.

[Leaf, 2015/06/26 20:54:31]

I think there's still a small problem here at the boundary: in computing the LUB
for B_i and C_i, what is the bound for R_i?  This formulation either implies
some sort of horrible fixed point (finding L_i uses L_i as the bound on R_i
while computing L_i), or else uses no bound?  I think that while computing L_i,
the bound to use should be B_i, given the covariant rule.  So this would
suggest:

the least upper bound of $F$ and $G$ is $\forall R_1 <: [R_1/P_1]L_1, \ldots,
R_n <: [R_n/P_n]L_n. lsig$ where $L_i$ is the least upper bound of
$[R_j/P_j]_{j=1}^{i-1}B_i$ and $[R_j/Q_j]_{j=1}^{i-1}[P_i/Q_i]C_i, i \in 1..n$
and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$.

Or perhaps better:

the least upper bound of $F$ and $G$ is $\forall R_1 <: L_1, \ldots, R_n <: L_n.
lsig$ where $L_i$ is $[R_i/P_i]M_i$ and $M_i$ is the least upper bound of
$[R_j/P_j]_{j=1}^{i-1}B_i$ and $[R_j/Q_j]_{j=1}^{i-1}[P_i/Q_i]C_i, i \in 1..n$
and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$.

+
+
+\item If
+
+$F = \forall P_1 <: B_1, \ldots, P_n <: B_m. fsig$
+
+$G = \forall Q_1 <: C_1, \ldots, Q_m <: C_m. gsig$
+
+where $n \ne m$, then
+the least upper bound of $F$ and $G$ is the least upper bound of
+$[B_i/P_i]fsig, i \in 1..n$ and $[C_j/Q_j]gsig, j \in 1..m$.
+
+\item
+$F = \forall P_1 <: B_1, \ldots, P_m <: B_m. fsig$
+
+$G = gsig$
+ then
+the least upper bound of $F$ and $G$ is the least upper bound of $[B_i/P_i]fsig, i \in 1..n$ and $gsig$.
+
 \end{itemize}