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

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \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
 % end of this file.
 
 \begin{document}
 \maketitle
 \tableofcontents
 
 
@@ skipping 507 matching lines @@
 
 
 
 
 
 \section{Functions}
 \LMLabel{functions}
 
 \LMHash{}
 Functions abstract over executable actions.
+% Need to fix grammar
 
 \begin{grammar}
 {\bf functionSignature:}
     metadata returnType? identifier formalParameterList
     .
     
 {\bf returnType:}
       \VOID{};
       type
     .
@@ skipping 80 matching lines @@
 \LMHash{}
 It is a compile-time error to preface a function declaration with the built-in identifier \STATIC{}.
 
 \LMHash{}
 When we say that a function $f_1$ {\em forwards} to another function $f_2$, we mean that  invoking $f_1$ causes $f_2$ to  be executed with the same arguments and/or receiver as $f_1$, and returns the result of executing $f_2$ to the caller of $f_1$, unless $f_2$ throws an exception, in which case $f_1$ throws the same exception. Furthermore, we only use the term for synthetic functions introduced by the specification.
 
 
 \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.
 
 \LMHash{}
 The formal parameter list of a function introduces a new scope known as the function's {\em formal parameter scope}. The formal parameter scope of a function $f$  is enclosed in the scope where $f$ is declared.   Every formal parameter introduces a local variable into the formal parameter scope. However, the scope of a function's signature is the function's enclosing scope, not the formal parameter scope.
 
 \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}.
+}
+
 
 %The formal parameter scope of a function maps the name of each formal parameter $p$ to the value $p$ is bound to. 
 
 % The formal parameters of a function are processed in the enclosing scope of the function. 
 % \commentary{this means that the parameters themselves may not be referenced within the formal parameter list.}
 
 \LMHash{}
 It is a compile-time error if a formal parameter is declared as a constant variable (\ref{variables}).
 
 \begin{grammar}
-{\bf formalParameterList:}`(' `)';
+
+{\bf formalParameterList:}

[Brian Wilkerson, 2015/06/21 23:32:02]

It's a little hard to tell in the review tool, but it looks like there would be
fewer changes to the grammar if formalParameterList stayed the same and we
introduced a new genericParameterList production:

genericParameterList:
  typeParameters? formalParameterList
  ;

I'd also find it (a) easier to see what's changing as a result of this DEP
(everything that's changed in the doc rather than everything that isn't changed
in the doc) and (b) easier to read the new spec after the changes are applied
(but that's just my preference and ymmv).

Also, if it stays the way it is now, I think functionTypeAlias needs to be fixed
to not allow two sets of type parameters.

[gbracha, 2015/06/23 20:26:24]

We can certainly do that. I don't want to worry about that too much right now,
because we need to fix the basics of the proposal and get a go/nogo decision
very soon.

+    typeParameters? formalValueParameterList
+   .
+   
+{\bf formalValueParameterList:}`(' `)';
  `(' normalFormalParameters ( `,'  optionalFormalParameters)? `)';
   `(' optionalFormalParameters `)'
    .
 %\end{grammar}
 %}
 
 %\begin{grammar}
 %formalParameterList:     
 %      '(' restFormalParameter? ')';
 %      '(' namedFormalParameters ')';
@@ skipping 84 matching lines @@
 If we allowed named parameters to begin with an underscore, they would be considered private and inaccessible to callers from outside the library where it was defined. If a method outside the library overrode a method with a private optional name, it would not be a subtype of the original method. The static checker would of course flag such situations, but the consequence would be that adding a private named formal would break clients outside the library in a way they could not easily correct. 
 }
 
 \subsection{Type of a Function}
 \LMLabel{typeOfAFunction}
 
 \LMHash{}
 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}. 
 
 \commentary{
 One cannot assume, based on the above, that  given a function \cd{f}, \cd{f.runtimeType} will actually be \cd{Function}, or that any two distinct function objects necessarily have the same runtime type.
 }
 
 \rationale{
 It is up to the implementation to choose an appropriate representation for functions.
@@ skipping 161 matching lines @@
 
 \LMHash{}
 It is a static warning if an instance method $m_1$ overrides an instance member $m_2$ and the type of $m_1$ is not a subtype of the type of $m_2$. It is a static warning if an instance method $m_1$ overrides an instance member $m_2$,  the signature of $m_2$ explicitly specifies a default value for a formal parameter $p$ and the signature of $m_1$ implies a different default value for $p$. It is a static warning if a class $C$ declares an instance method named $n$ and has a setter named $n=$. It is a static warning if a class $C$ declares an instance method named $n$ and an accessible static member named $n$ is declared in a superclass of $C$.
 
 % Works. If the name is public, no issue. If it's private, if a subclass has a conflicting inst var, it either is in the same lib and will be flagged, or is in another and is not an issue.
 
 
 \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:}`\~{}';
       binaryOperator;
       `[' `]' ;
       `[' `]' `='
     .
 
 {\bf binaryOperator:}multiplicativeOperator;
       additiveOperator;
@@ skipping 80 matching lines @@
 \subsection{Setters}
 \LMLabel{setters}
 
 \LMHash{}
 Setters are functions (\ref{functions}) that are used to set the values of object properties.
 
 % what about top level ones? Same for getters
 
 \begin{grammar}
 {\bf setterSignature:}
-       returnType? \SET{} identifier formalParameterList
+       returnType? \SET{} identifier formalValueParameterList
 .
 \end{grammar}
 
 \LMHash{}
 If no return type is specified, the return type of the setter is  \DYNAMIC{}.
 
 \LMHash{}
 A setter definition that is prefixed with the \STATIC{} modifier defines a static setter. Otherwise, it defines an instance setter. The name of a setter is  obtained by appending the  string `='  to the identifier given in its signature. The effect of a static setter declaration in class $C$ is to add an instance setter with the same name and signature to the \code{Type} object for class $C$ that forwards (\ref{functionDeclarations})  to the static setter.
 
 \commentary{Hence, a setter name can never conflict with, override or be overridden by a getter or method.}
@@ skipping 136 matching lines @@
 Iff no constructor is specified for a class $C$, it implicitly has a default constructor \code{C() : \SUPER{}() \{\}}, unless $C$ is class \code{Object}.
 
 \subsubsection{Generative Constructors}
 \LMLabel{generativeConstructors}
 
 \LMHash{}
 A {\em generative constructor} consists of a constructor name, a constructor parameter list, and either a redirect clause or an  initializer list and an optional body.
 
 \begin{grammar}
 {\bf constructorSignature:}
-      identifier (`{\escapegrammar .}' identifier)? formalParameterList
+      identifier (`{\escapegrammar .}' identifier)? formalValueParameterList
     .
  \end{grammar}
 
 \LMHash{}
 A {\em constructor parameter list} is a parenthesized, comma-separated list of formal constructor parameters. A {\em formal constructor parameter} is either a formal parameter (\ref{formalParameters}) or an initializing formal. An {\em initializing formal} has the form \code{\THIS{}.id}, where \code{id} is the name of an instance variable of the immediately enclosing class.  It is a compile-time error if \code{id} is not an instance variable of the immediately enclosing class. It is a compile-time error if an initializing formal is used by a function other than a non-redirecting generative constructor. 
 
 \LMHash{}
 If an explicit type is attached to the initializing formal, that is its static type. Otherwise, the type of an initializing formal named \code{id} is $T_{id}$, where $T_{id}$ is the type of the field named \code{id} in the immediately enclosing class. It is a static warning if the static type of \code{id} is not assignable to $T_{id}$.
 
 \LMHash{}
@@ skipping 35 matching lines @@
 
 
 \paragraph{Redirecting Constructors}
 \LMLabel{redirectingConstructors}
 
 \LMHash{}
 A generative constructor may be {\em redirecting}, in which case its only action is to invoke another generative constructor.  A redirecting constructor has no body; instead, it has a redirect clause that specifies which constructor the invocation is redirected to, and with what arguments.
 
 \begin{grammar}
 {\bf redirection:}
-     `{\escapegrammar :}' \THIS{} (`{\escapegrammar .}' identifier)? arguments
+     `{\escapegrammar :}' \THIS{} (`{\escapegrammar .}' identifier)? valueArguments
     .
 \end{grammar}
 
 % Need to specify exactly how executing a redirecting constructor works
 
 
 %\Q{We now have generative constructors with no bodies as well.}
 
 \paragraph{Initializer Lists}
 \LMLabel{initializerLists}
 
 \LMHash{}
 An initializer list begins with a colon, and consists of a comma-separated list of individual {\em initializers}. There are two kinds of initializers.
 \begin{itemize}
 \item A {\em superinitializer} identifies a {\em superconstructor} - that is, a specific  constructor of the superclass.  Execution of the superinitializer causes the initializer list of the superconstructor to be executed.
 
 \item An {\em instance variable initializer} assigns a value to an individual instance variable. 
 \end{itemize}
 
 \begin{grammar}
 {\bf initializers:}
       `{\escapegrammar :}' superCallOrFieldInitializer (`,' superCallOrFieldInitializer)*
     .
 
 
-{\bf superCallOrFieldInitializer:}\SUPER{} arguments;
-      \SUPER{} `{\escapegrammar .}' identifier arguments;
+{\bf superCallOrFieldInitializer:}\SUPER{} valueArguments;
+      \SUPER{} `{\escapegrammar .}' identifier valueArguments;
      fieldInitializer
     .
     
    {\bf  fieldInitializer:}
       (\THIS{} `{\escapegrammar .}')? identifier `=' conditionalExpression cascadeSection*
     .
 
 \end{grammar}
 
 \LMHash{}
@@ skipping 79 matching lines @@
 It is a compile-time error if class $S$ does not declare a generative constructor named $S$ (respectively $S.id$).
 
 \subsubsection{Factories}
 \LMLabel{factories}
 
 \LMHash{}
 A {\em factory} is a constructor prefaced by the built-in identifier  (\ref{identifierReference})   \FACTORY{}. 
 
 \begin{grammar}
 {\bf factoryConstructorSignature:}
-      \FACTORY{} identifier  (`{\escapegrammar .}' identifier)?  formalParameterList
+      \FACTORY{} identifier  (`{\escapegrammar .}' identifier)?  formalValueParameterList
     .
 \end{grammar}
 
 
 %The enclosing scope of a factory constructor is the static scope \ref{} of the class in which it is declared.
 
 \LMHash{}
 The {\em return type} of a factory whose signature is of the form \FACTORY{} $M$ or the form \FACTORY{} $M.id$ is $M$ if $M$ is not a generic type; otherwise the return type is  $M <T_1, \ldots, T_n>$ where $T_1, \ldots, T_n$ are the type parameters of the enclosing class
 
 \LMHash{}
@@ skipping 10 matching lines @@
 }
 
 \paragraph{Redirecting Factory Constructors}
 \LMLabel{redirectingFactoryConstructors}
 
 \LMHash{}
 A {\em redirecting factory constructor} specifies a call to a constructor of another class that is to be used whenever the redirecting constructor is called.
 
 \begin{grammar}
 {\bf redirectingFactoryConstructorSignature:}
-      \CONST{}? \FACTORY{} identifier (`{\escapegrammar .}' identifier)? formalParameterList `=' type (`{\escapegrammar .}' identifier)?
+      \CONST{}? \FACTORY{} identifier (`{\escapegrammar .}' identifier)? formalValueParameterList `=' type (`{\escapegrammar .}' identifier)?
     .
 \end{grammar}
 
 \LMHash{}
 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$.
 }
 
@@ skipping 69 matching lines @@
 
 
 \subsubsection{Constant Constructors}
 \LMLabel{constantConstructors}
 
 \LMHash{}
 A {\em constant constructor} may be used to create compile-time constant  (\ref{constants}) objects. A constant constructor is prefixed by the reserved word \CONST{}. 
 
 \begin{grammar}
 {\bf constantConstructorSignature:}
-      \CONST{} qualified formalParameterList
+      \CONST{} qualified formalValueParameterList
     .
 \end{grammar}
 
 
 %\commentary{Spell out subtleties: a constant constructor call within the initializer of a constant constructor is treated as a  ordinary constructor call (a new), because the arguments cannot be assumed constant anymore. In practice, this means two versions are compiled and analyzed. One for new and one for const.}
 
 % \Q{How to specify?}
 
 \commentary{All the work of a constant constructor must be handled via its initializers.}
 
@@ skipping 447 matching lines @@
 % tighten definition? do we need chain as for classes?  Definition for interface override?
 
 \LMHash{}
 However, if the above rules would cause multiple members $m_1, \ldots,  m_k$ with the same name $n$ to be inherited (because identically named members existed in several superinterfaces) then at most one member is inherited. 
 
 \LMHash{}
 If some but not all of the $m_i, 1 \le i \le k$ are getters none of the $m_i$ are inherited, and a static warning is issued.
 
 \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. 
 
 (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} 
 
 
 \LMHash{}
 A mixin describes the difference between a class and its superclass. A mixin is always derived from an existing class declaration. 
 
 \LMHash{}
 It is a compile-time error if a declared or derived mixin refers to \SUPER{}. It is a compile-time error if a declared or derived mixin explicitly declares a constructor. It is a compile-time error if a mixin is derived from a class whose superclass is not \code{Object}.
@@ skipping 131 matching lines @@
 \}
 \end{dartCode}
 
 \commentary {
 It is also a compile-time error to subclass, mix-in or implement an enum or to explicitly instantiate an enum.  These restrictions are given in normative form in sections \ref{superclasses}, \ref{superinterfaces}, \ref{mixinApplication} and \ref{instanceCreation} as appropriate.
 }
 
 \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}
 {\bf typeParameter:}
      metadata identifier (\EXTENDS{} type)?
     .
 {\bf typeParameters:}
      `<' typeParameter (`,' typeParameter)* `>'
     .
 \end{grammar}
 
 \LMHash{}
 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.
 
 \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. 
 }
 
 \commentary{
 Because type parameters are in scope in their bounds, we support F-bounded quantification (if you don't know what that is, don't ask). This enables typechecking code such as:
 }
 
 \begin{dartCode}
@@ skipping 91 matching lines @@
 
 
 \section{Metadata}
 \LMLabel{metadata}
 
 \LMHash{}
 Dart supports metadata which is used to attach user defined annotations to program structures.  
 
 \begin{grammar}
 {\bf metadata:}
-      (`@' qualified ({\escapegrammar `.'} identifier)? (arguments)?)*
+      (`@' qualified ({\escapegrammar `.'} identifier)? (valueArguments)?)*
     .
 \end{grammar}
 
 \LMHash{}
 Metadata consists of a series of annotations, each of which begin with the character @, followed by  a constant expression that starts with an identifier. It is a compile time error if the expression is not one of the following:
 \begin{itemize}
 \item A reference to a compile-time constant variable.
 \item A call to a constant constructor.
 \end{itemize}
 
@@ skipping 888 matching lines @@
 is $(T_1 \ldots, T_n, \{T_{n+1}$ $x_{n+1}, \ldots, T_{n+k}$ $x_{n+k}\}) \rightarrow  Stream{}$.
 
 \LMHash{}
 The static type of a function literal of the form  
 
 $(T_1$ $a_1, \ldots, T_n$ $a_n, \{T_{n+1}$ $x_{n+1} : d_1, \ldots,  T_{n+k}$ $x_{n+k} : d_k\})$ $\SYNC*{}$ $\{s\}$
  
 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}
 
 \LMHash{}
 The reserved word \THIS{} denotes the target of the current instance member invocation.
 
 \begin{grammar}
 {\bf thisExpression:}
       \THIS{}
@@ skipping 48 matching lines @@
 
 
 \subsubsection{ New}
 \LMLabel{new}
 
 \LMHash{}
 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}
 
 \LMHash{}
 Let $e$ be a new expression of the form  
 
 \NEW{} $T.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ or the form  
 
 \NEW{} $T(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. 
 
@@ skipping 97 matching lines @@
 
 
 \subsubsection{ Const}
 \LMLabel{const}
 
 \LMHash{}
 A {\em constant object expression} invokes a constant constructor (\ref{constantConstructors}). 
 
 \begin{grammar}
 {\bf constObjectExpression:}
-\CONST{} type ('{\escapegrammar .}' identifier)? arguments
+\CONST{} type ('{\escapegrammar .}' identifier)? valueArguments
 .
 \end{grammar}
 
 \LMHash{}
 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.  It is a compile-time error if $T$ is a deferred type (\ref{staticTypes}).
 
@@ skipping 105 matching lines @@
 
 \commentary{
 As discussed in section \ref{errorsAndWarnings}, the handling of a suspended isolate is the responsibility of the embedder.
 }
 
 
 
 \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. 
 
 \LMHash{}
 If $f$ is marked \ASYNC* (\ref{functions}), then a fresh instance $s$ implementing the built-in class \code{Stream} is associated with the invocation and immediately returned. When $s$ is listened to, execution of the body of $f$ will begin.  When $f$ terminates:
 \begin{itemize}
 \item If the current return value is defined then, if $s$ has been canceled then its cancellation future is completed with \NULL{} (\ref{null}). 
 \item If the current exception $x$ is defined:
   \begin{itemize}
@@ skipping 68 matching lines @@
 
 
 \subsubsection{ Actual Argument List Evaluation}
 \LMLabel{actualArguments}
 
 \LMHash{}
 Function invocation involves evaluation of the list of actual arguments to the function and binding of the results to the function's formal parameters.
 
 \begin{grammar}
 {\bf arguments:}
+      typeArguments? valueArguments
+    .
+    
+{\bf valueArguments:}

[Brian Wilkerson, 2015/06/21 23:32:02]

I think the same is true here, that it would result in fewer changes that are
easier to proof-read if 'arguments' stayed the same and we introduced a new
genericArguments production. (In fact, if I'm counting correctly, there might
only be one or two references to the new production and you might want to just
inline it. But I could easily be off in my counts.)

       `(' argumentList? `)'
     .
 
 {\bf argumentList:}namedArgument (`,' namedArgument)*;
   %    expressionList ',' spreadArgument;
       expressionList (`,' namedArgument)*
 %      spreadArgument
     .
 
 {\bf namedArgument:}
@@ skipping 12 matching lines @@
 The arguments $a_1, \ldots, a_{m+l}$ are evaluated in the order they appear in the program, yielding objects $o_1, \ldots, o_{m+l}$.
 
 \commentary{Simply stated, an argument list consisting of $m$ positional arguments and $l$ named arguments is evaluated from left to right.
 }
 
 
 \subsubsection{ Binding Actuals to Formals}
 \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 \DYNAMIC. 

[Leaf, 2015/06/16 23:23:10]

s.b "to be \DYNAMIC"

[gbracha, 2015/06/18 20:05:59]

Done.

+
+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 ($r = 0$), any type arguments are ignored. Otherwise the number of type arguments  must match the number of formal type parameters ($r = s$).

[Leaf, 2015/06/16 23:23:10]

s.b. ($s = 0$) ?

[gbracha, 2015/06/18 20:05:58]

No, why? This specifically describes the semantics where any number of type
arguments may be  passed.

[Leaf, 2015/06/23 01:59:59]

I think the ($r = 0$) should be ($s = 0) because r is the number of type
arguments (not the number of type parameters), and the text is referring to the
number of type parameters.  That is, if there are no type parameters (s = 0)
then any number (r) of type arguments are allowed.  No?

[gbracha, 2015/06/23 20:26:24]

Yes. I thought r = 0 was supposed to replace r = s and was puzzled. Should have
looked higher up.

+}
+
+\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.  
+
 
 \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.
 }
 
 \commentary{
 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}
 
 \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. 
 
 \LMHash{}
 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})$.
+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})$.  
 
 %\rationale{
 %Unqualified access to static methods of superclasses is inconsistent with the idea that static methods are not inherited. It is not particularly necessary and  may be restricted in future versions.
 %}
 
 \LMHash{}
 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.
 
 
 
 
 
 \subsubsection{ Function Expression Invocation}
 \LMLabel{functionExpressionInvocation}
 
 \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}). 
 
 \commentary{
 \code{$a.b(x)$} is parsed as a method invocation of method \code{$b()$} on object \code{$a$}, not as an invocation of getter \code{$b$} on \code{$a$} followed by a function call \code{$(a.b)(x)$}.  If a method or getter \code{$b$} exists, the two will be equivalent. However, if \code{$b$} is not defined on \code{$a$}, the resulting invocation of \code{noSuchMethod()} would differ.  The \code{Invocation} passed to \code{noSuchMethod()} would describe a call to a method \code{$b$} with argument \code{$x$} in the former case, and a call to a getter \code{$b$} (with no arguments) in the latter.
 }
 
 \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.
 }
 
 \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}
 
 \subsection{ Lookup}
 \LMLabel{lookup}
 
 \subsubsection{Method Lookup}
 \LMLabel{methodLookup}
 
 \LMHash{}
@@ skipping 47 matching lines @@
 \subsubsection{Ordinary Invocation}
 \LMLabel{ordinaryInvocation}
 
 \LMHash{}
 An ordinary method invocation can be {\em conditional} or {\em unconditional}.
 
 \LMHash{}
 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})$.
 
 \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:
 
 \LMHash{}
 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 below. 
+
+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. 
+
+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.
+
+
 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]$.

[Leaf, 2015/06/16 23:23:10]

s.b "with arguments $v_g, " ?

[gbracha, 2015/06/18 20:05:58]

Done.

[Leaf, 2015/06/16 23:23:10]

I think there's a small issue with expressing this in terms of Function.apply
here since not all types are allowed to appear in expressions contexts (e.g. if
A_1 is List<int>).  This applies in the NSM case and the corresponding super
call cases below as well.

[gbracha, 2015/06/18 20:05:59]

Yes and no. I'm not saying this is the call Function.apply(v_g, ... [A1, ...,
Ar]). I'm saying the function got invoked with those values. They do exist
(e.g., new List<int>().runtimeType). You can argue that the list [A1, .., Ar]
isn't really valid, and I should say something like a list with the elements A1,
..., Ar in that order.

But section 5 already gives license to such abuse of notation. So I think I'm in
the clear.

[Leaf, 2015/06/23 01:59:59]

Ok.

 \LMHash{}
 If  getter lookup has also failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
 \begin{itemize}
 \item  \code{im.isMethod} evaluates to \code{\TRUE{}}.
 \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$ rather than the $V_i$.  If no argument were passed, the handler can choose to use \DYNAMIC{} at its discretion.}

[Leaf, 2015/06/16 23:23:10]

What are the $V_i$? I looked in the surrounding text but didn't find a place
they were introduced, did I miss it somewhere?

[gbracha, 2015/06/18 20:05:59]

There used to be V_i, representing the type arguments passed in practice (e.g.,
using dynamic when no arguments are present.  I eventually centralized that in
section 16.14.2 and eliminated the V_i in the process. I forgot to clean up this
rationale. Will rephrase.

 \end{itemize}
 
 \LMHash{}
 Then the method \code{noSuchMethod()} is looked up in $v_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 $v_o$ with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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$.
 
 \rationale {
 It is possible to bring about such a situation by overriding \code{noSuchMethod()} with the wrong number of arguments:}
 
 \begin{code}
 \CLASS{} Perverse \{
     noSuchMethod(x,y) =$>$ x + y;
@@ skipping 44 matching lines @@
 
 The present specification has not added such a construct, in the interests of simplicity and rapid language evolution. However, Dart implementations may experiment with such constructs, as noted in section \ref{ecmaConformance}.
 }
 
 \subsubsection{Super Invocation}
 \LMLabel{superInvocation}
 
 \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.
+
 
 \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.
 
 \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 the current value of \THIS{}. 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 $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 :
 \begin{itemize}
 \item  \code{im.isMethod} evaluates to \code{\TRUE{}}.
 \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}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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$.
 
 
 \LMHash{}
 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$.
 
 
 
 
 \subsubsection{Sending Messages}
 \LMLabel{sendingMessages}
 
 \LMHash{}
@@ skipping 50 matching lines @@
 Otherwise, $i$ is a getter invocation.  Let $f$ be the result of looking up
 (\ref{getterAndSetterLookup}) getter (\ref{getters}) $m$ in $o$  with respect to $L$. If $o$ is an instance of \code{Type} but $e$ is not a constant type literal, then if $f$ is a getter that forwards  to a static getter,  getter lookup fails. Otherwise, the body of $f$ is executed with \THIS{} bound to $o$.  The value of $i$ is the result returned by the call to the getter function. 
 
 \LMHash{}
 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 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}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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$.
 
 \LMHash{}
 It is a compile-time error if $m$ is a member of class \cd{Object} and $e$ is either a prefix object (\ref{imports}) or a constant type literal.
 
 \commentary {
 This precludes \code{int.toString} but not \code{(int).toString} because in the latter case, $e$ is a parenthesized expression.
 }
@@ skipping 29 matching lines @@
 \LMHash{}
  Otherwise, $i$ is a getter invocation.  Let $f$ be the result of  looking up getter $m$ in $S$  with respect to $L$.  The body of $f$  is executed with \THIS{} bound to the current value of  \THIS{}.  The value of $i$ is the result returned by the call to the getter function. 
 
 \LMHash{}
 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 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}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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$.
 
 \LMHash{}
 It is a static type warning if $S$ does not have an accessible instance method or getter named $m$.  
 
 The static type of $i$ is:
 \begin{itemize}
 \item The declared return type of $S.m$, if $S$ has an accessible instance getter named $m$.
 \item The static type of function $S.m$ if $S$ has an accessible instance method named $m$.
@@ skipping 128 matching lines @@
 \LMHash{}
 Let $o$ be an object, and let $u$ be a fresh final variable bound to $o$.
 The {\em closurization of method $f$ on object $o$} is defined to be equivalent to:
 \begin{itemize}
 \item $(a) \{\RETURN{}$ $u$ $op$ $a;$\} if $f$ is named $op$ and $op$ is one of  \code{$<$, $>$, $<$=, $>$=, ==,  -, +, /, \~{}/, *, \%, $|$, \^{}, \&, $<<$, $>>$} (this precludes closurization of unary -).
 \item $() \{\RETURN{}$ \~{} $u;$\} if $f$ is named \~{}.
 \item $(a) \{\RETURN{}$ $u[a];$\} if $f$ is named $[]$.
 \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\})$ \{
+$<T_1, \ldots,  T_s>(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);$
 \} 

[Leaf, 2015/06/16 23:23:10]

Is it intentional that the type parameters are dropped here?  This seems wrong 
- why allow closurization if the types just get dropped?

[gbracha, 2015/06/18 20:05:59]

No, it's not intentional. It's called a bug. Fixed.

[Leaf, 2015/06/23 01:59:59]

Well you know, one man's bug is another man's feature... :)

 \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{} $u.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}
 

[Leaf, 2015/06/16 23:23:10]

If I'm reading this correctly, neither the closurization rules nor the
application rules allow for partial applications of generic functions (e.g. var
intId = id<int>; where id is the polymorphic identity).  Did I miss something? 
If not, is this intentional?  My sense was that allowing this would be useful
for a number of different reasons, and I don't think it substantially adds to
the implementation complexity. 

[gbracha, 2015/06/18 20:05:58]

Yes, that is correct. We should discuss where you find this useful. 

[Leaf, 2015/06/23 02:00:00]

My original DEP proposal used this a fair bit in the examples.  Basically, I
think it gives a way to reduce the syntactic noise in the absence of inference. 
Any place that you need to instantiate something more than once, you can easily
bind the instantiation so you don't have to repeat it.  It's a small thing, but
the implementation cost should be very low (it's just another form of
closurization) and I think it provides some nice expressiveness.  

[gbracha, 2015/06/23 20:26:24]

Ok, we can discuss.

 \LMHash{}
 Except that iff  \code{identical($o_1, o_2$)}  then  \cd{$o_1\#m$ == $o_2\#m$},  \cd{$o_1.m$ == $o_2.m$}, \cd{$o_1\#m$ == $o_2.m$} and  \cd{$o_1.m$ == $o_2\#m$}.
 %\item The static type of the property extraction is the static type of function $T.m$, where $T$ is the static type of $e$, if $T.m$ is defined. Otherwise the static type of $e.m$ is \DYNAMIC{}.
 
 \LMHash{}
 The {\em closurization of getter $f$ on object $o$} is defined to be equivalent to \cd{()\{\RETURN{} u.m;\}} if $f$ is named $m$, except that iff  \code{identical($o_1, o_2$)} then  \cd{$o_1\#m$ == $o_2\#m$}.
 
 \LMHash{}
 The {\em closurization of setter $f$ on object $o$} is defined to be equivalent to \cd{(a)\{\RETURN{} u.m = a;\}} if $f$ is named $m=$, except that iff  \code{identical($o_1, o_2$)} then \cd{$o_1\#m=$ == $o_2\#m=$}.
 
@@ skipping 80 matching lines @@
 The {\em closurization of method $f$ with respect to superclass $S$} is defined to be equivalent to:
 
 \LMHash{}
 \begin{itemize}
 \item $(a) \{\RETURN{}$ \SUPER{} $op$ $a;$\} if $f$ is named $op$ and $op$ is one of  \code{$<$, $>$, $<$=, $>$=, ==,  -, +, /, \~{}/, *, \%, $|$, \^{}, \&, $<<$, $>>$}.
 \item $() \{\RETURN{}$ \~{}\SUPER;\} if $f$ is named \~{}.
 \item $(a) \{\RETURN{}$ $\SUPER[a];$\} if $f$ is named $[]$.
 \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{}
 Except that iff two closurizations were created by code declared in the same class with identical bindings of \THIS{} then  \cd{\SUPER$_1\#m$ == \SUPER$_2\#m$},  \cd{\SUPER$_1.m$ == \SUPER$_2.m$}, \cd{\SUPER$_1\#m$ == \SUPER$_2.m$} and  \cd{\SUPER$_1.m$ == \SUPER$_2\#m$}.
 
 
 \LMHash{}
 The {\em closurization of getter $f$  with respect to superclass $S$} is defined to be equivalent to \cd{()\{\RETURN{} \SUPER.m;\}} if $f$ is named $m$, except that iff two closurizations were created by code declared in the same class with identical bindings of \THIS{} then  \cd{\SUPER$_1\#m$ == \SUPER$_2\#m$}.
 
 \LMHash{}
@@ skipping 61 matching lines @@
 \LMHash{}
 The expression $e_1$ is evaluated to an object $o_1$. Then, the expression $e_2$  is evaluated to an object $o_2$. Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $o_1$ with respect to the current library.  If $o_1$ is an instance of \code{Type} but $e_1$ is not a constant type literal, then if $v=$ is a setter that forwards (\ref{functionDeclarations}) to a static setter, setter lookup fails. Otherwise, the body  of $v=$ is executed with its formal parameter bound to $o_2$ and \THIS{} bound to $o_1$. 
 
 \LMHash{}
 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 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{}
 Then the method \code{noSuchMethod()} is looked up in $o_1$ and invoked  with argument $im$. 
 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_1$ with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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{}
 The value of the assignment expression is $o_2$ irrespective of whether setter lookup has failed or succeeded.
 
 \LMHash{}
 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$.
 
 \LMHash{}
 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 either:
@@ skipping 14 matching lines @@
 Let $S$ be the superclass of the immediately enclosing class.
 The expression $e$ is evaluated to an object $o$.  Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $S$ with respect to the current library.  The body  of $v=$ is executed with its formal parameter bound to $o$ and \THIS{} bound to \THIS{}. 
 
 \LMHash{}
 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 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{}
 Then the method \code{noSuchMethod()} is looked up in $S$ and invoked  with argument $im$. 
 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}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \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{}
 The value of the assignment expression is $o$ irrespective of whether setter lookup has failed or succeeded.
 
 \LMHash{}
 In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of $S.v$.
 
 \LMHash{}
 It is a static type warning if $S$ does not have an accessible instance setter named $v=$ 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}. 
@@ skipping 495 matching lines @@
  \end{grammar}
  
 \LMHash{}
  A {\em postfix expression} is either a primary expression, a function, method or getter invocation, or an invocation of a postfix operator on an expression $e$.
 
 \LMHash{}
 A postfix expression of the form \code{$v$++}, where $v$ is an identifier, is equivalent to \code{()\{var r = $v$; $v$ = r + 1; return r\}()}.
 
 \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 
 
 \code{()\{var r = $C.v$; $C.v$ = r + 1; return r\}()}.
 
 \LMHash{}
 A postfix expression of the form \code{$e_1.v$++} is equivalent to 
 
 \code{(x)\{var r = x.v; x.v = r + 1; \RETURN{} r\}($e_1$)}.
@@ skipping 1870 matching lines @@
  \rationale{
  The interpretation of URIs is mostly left to the surrounding computing environment. For example, if Dart is running in a web browser, that browser will likely interpret some URIs. While it might seem attractive to specify, say, that URIs are interpreted with respect to a standard such as IETF RFC 3986, in practice this will usually depend on the browser and cannot be relied upon.
  }
  
 \LMHash{}
 A URI of the form \code{dart:$s$} is interpreted as a reference to a system library (\ref{imports}) $s$. 
  
 \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{}
 Otherwise, any relative URI is interpreted as relative to the the location of the current library. All further interpretation of URIs is implementation dependent. 
 
 \commentary{This means it is dependent on the embedder.}
 
 
 \section{Types}
 \LMLabel{types}
@@ skipping 278 matching lines @@
 An interface type $T$ may be assigned to a type $S$, written  $T \Longleftrightarrow S$, iff either $T <: S$ or $S <: T$. 
 
 \rationale{This rule may surprise readers accustomed to conventional typechecking. The intent of the $\Longleftrightarrow$ relation is not to ensure that an assignment is correct. Instead, it aims to only flag assignments that are almost certain to be erroneous, without precluding assignments that may work. 
 
 For example, assigning a value of static type Object to a variable with static type String, while not guaranteed to be correct, might be fine if the runtime value happens to be a string.
 }
 
 \subsection{Function Types}
 \LMLabel{functionTypes}
 
+\subsubsection{Ordinary Function Types}
+\LMLabel{ordinaryFunctionTypes}
+
 \LMHash{}
 Function types come in two variants: 
 \begin{enumerate}
 \item
 The types of functions that only have positional parameters.  These have the general form $(T_1, \ldots, T_n, [T_{n+1} \ldots, T_{n+k}]) \rightarrow T$.
 \item
 The types of functions with named  parameters. These have the general form $(T_1, \ldots, T_n, \{T_{x_1}$ $x_1 \ldots, T_{x_k}$ $x_k\}) \rightarrow T$.
 \end{enumerate}
 
 %$(T_1, \ldots T_n) \rightarrow T$ is a subtype of  $(S_1, \ldots, S_n, ) \rightarrow S$, if all of the following conditions are met:
@@ skipping 96 matching lines @@
 \end{itemize}
 \item $\forall i \in 1 .. n, T_i << S_i$.
 \item $k \ge m$ and $y_i \in \{x_1,  \ldots, x_k\}, i \in 1 .. m$.
 %\{x_1,  \ldots, x_k\}$ is a superset of $\{y_1,  \ldots, y_m\}$.
 \item For all $y_i \in \{y_1,  \ldots, y_m\}, y_i = x_j \Rightarrow T_j << S_i$
 \end{enumerate}
 
 \LMHash{}
 Furthermore, if $F$ is a function type, $F << \code{Function}$.
 
+\subsubsection{Generic Function Types}

[Leaf, 2015/06/16 23:23:10]

This is missing the treatment of assignability and more specific than, which I
think become necessary if we move to a non-prenex system (as I believe this
draft spec proposes).

+\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{

[Leaf, 2015/06/16 23:23:10]

Just as an aside, I think this is a fairly natural rule from a technical
perspective as well.  If you take the view that subtyping is entailment, then
the \forall t.\tau is naturally a subtype of \tau with \sigma substituted for t
(that is, a universal entails any of its instantiations).  I believe that the
substitution of dynamic for the T_i essentially implements this: rather than
search for the exact instantiation, we simply check that the instantiation with
dynamic is a subtype.  If it is, then there is * some* instantiation and we're
happy.  If it's not, I believe that the Dart type system is structured such that
no instantiation would work.  

[gbracha, 2015/06/18 20:05:58]

That's an interesting point. AFIK, most type systems with universal
quantification and subtyping don't take this path though.  Not that it matters,
but do you know of counter examples? I haven't looked at this since the Java
generics days.

[Leaf, 2015/06/23 01:59:59]

I don't know specifically with object subtyping.  I think I first got this
interpretation from Frank Pfenning and Rowan Davies.  They were working on
intersection types, and hence had a notion of subtyping and as I recall this
kind of fit naturally into what they were doing.  I could ping Frank about it,
see if he knows anything interested and related.  It's not all that different
from the more standard type inference driven instantiation in practice, except
that you don't need to actually produce the instantiation type - just show that
there is one.  The difference isn't very relevant in languages without reified
types though.  

Of course, in languages like ML with HM type inference, you can just use a
generic in a monomorphic context and it will be implicitly instantiated, so it
feels awfully similar to the programmer.  ML signature matching also has this
property - you can ascribe a signature with a monomorphic type for a function to
a structure containing a polymorphic function if it can be instantiated
appropriately.  The whole signature matching thing always smelled very
subtyping-ish to me - not sure if there are any really good reasons it wasn't
expressed that way.

+ 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. 

[Leaf, 2015/06/16 23:23:10]

Double comma after "principle".

[gbracha, 2015/06/18 20:05:59]

Done.

+ 
+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.

[Leaf, 2015/06/16 23:23:10]

I agree with the motivation for wanting this, but i seems to me that this is
solving a short term problem (transitioning libraries to use generic method) at
a long term cost to the language (surprising behavior, implementation
complexity).

Essentially, this rule makes the "dynamic" type definable: for any type S,

    \forall(T).() => T <: () => S  // since S <==> dynamic (or Object) for any S
    () => S <: \forall(T).() => T  // since S <==> Object for any S

Put another way, you essentially lose all typechecking with universal types: any
function type of the right arity is going to be assignable to a universal type
with Object bounds.  Universal types with concrete bounds will be a little more
restricted.

This also means that every method must be prepared to accept any number of type
parameters and silently ignore them, since every method can be called as a
generic method.

Overall, this seems like a large cost to pay for a small benefit.  It's true
that it allows implementors of genericized interfaces to ignore the change
(though they may still break in checked mode), but a small extra burden on the
subset of library writers who don't want to use generics seems small compared to
the cost of making universal types fairly meaningless as types.

[gbracha, 2015/06/18 20:05:58]

Yes, I realize it's rather costly. The choice is however, rather stark. A
significant incompatibility vs. an expensive and somewhat lobotomized type
system. If you view the benefit of generics as a error checking, you may find
this especially disturbing. I am hardly interested in that, and much more in
benefits to name completion etc.  If *I* were to do generic methods, I'd go for
compatibility. But I agree this is very disturbing.

[Leaf, 2015/06/23 01:59:59]

Fair enough.  I obviously fall in the error checking camp, and it does blow a
pretty big hole in the system.  A possible compromise would be to only allow
this in method overriding (where most of the incompatibility is), but that feels
kind of ad hoc.  

+
+This leads to the proposed rule above. 
+ }
+ 
+
 
 \subsection{Type \DYNAMIC{}}
 \LMLabel{typeDynamic}
 
 \LMHash{}
 The type  \DYNAMIC{}  denotes the unknown type. 
 
 \LMHash{}
 If no static type annotation has been provided the type system assumes the declaration has the unknown type. If a generic type is used but type arguments are not provided, then the  type arguments default to the unknown type.
 
@@ skipping 128 matching lines @@
 The least upper bound of \VOID{} and any type $T \ne \DYNAMIC{}$ is \VOID{}.
 Let $U$ be a type variable with upper bound $B$. The least upper bound of $U$ and a type $T$ is the least upper bound of $B$ and $T$. 
 
 \LMHash{}
 The least upper bound relation is symmetric and reflexive.
 
 % Function types
 
 \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 
 
 $F= (T_1 \ldots T_r, [T_{r+1}, \ldots, T_n]) \longrightarrow T_0$, 
 
 $G= (S_1 \ldots S_r, [S_{r+1}, \ldots, S_k]) \longrightarrow S_0$ 
 
 where $k \le n$ then the least upper bound of $F$ and $G$ is 
 
 $(L_1 \ldots L_r, [L_{r+1}, \ldots, L_k]) \longrightarrow L_0$ 
 
 where $L_i$ is the least upper bound of $T_i$ and $S_i, i \in 0..k$.
 \item If 
 
 $F= (T_1 \ldots T_r, [T_{r+1}, \ldots, T_n]) \longrightarrow T_0$,
 
 $G= (S_1 \ldots S_r, \{ \ldots \}) \longrightarrow S_0$ 
 
 then the least upper bound of $F$ and $G$ is 
 
 $(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$,  
 
 $G= (S_1 \ldots S_r, \{ S_{r+1}$  $q_{r+1}, \ldots, S_g$ $q_g\}) \longrightarrow S_0$ 
 
 then let $\{x_m, \ldots x_n\}  = \{p_{r+1}, \ldots, p_f\} \cap \{q_{r+1}, \ldots, q_g\}$ and let $X_j$ be the least upper bound of the types of $x_j$ in $F$ and $G, j \in m..n$. Then
 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

[Leaf, 2015/06/16 23:23:10]

I think this is wrong.  It's not symmetric, and I think it gives the wrong
answers.  Consider finding the LUB of:

\forall T <: int . int => int
\forall S <: String . S => S

LUB[int, String] is Object

LUB[int => int, T => T] where T <: int is int => int

so the LUB we compute is \forall T <: Object. int => int.

But if we switch the order of the inputs, we end up using S <: String for the
variable, and computing

\forall S <: Object. Object => Object

Unless I'm misconstruing something?  I think each successive recursive LUB needs
to use the LUB computed for the previously encountered bounds, rather than the
original bounds.  Then we have:

LUB[int => int, Q => Q] where Q <: Object is Object => Object

and we get a LUB which has the presumably desired property that each of the
inputs is a subtype of the output, and which (at least for this example) seems
to be symmetric.

[gbracha, 2015/06/18 20:05:59]

Yes, the asymmetry is a problem. 

[Leaf, 2015/06/23 01:59:59]

I think a reasonable definition might be to define it inductively: 

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 the least upper bound
of $F = \forall P_2 <: B_2, \ldots, P_n <: B_m. fsig$ and $[P_1/Q_1]\forall Q_2
<: C_2, \ldots, Q_n <: C_m. gsig$
with the bound of $P_1$ set to $L_1$ where $L_1$ is the least upper bound of
$B_1$ and $[P_1/Q_1]C_1$

with the obvious base case when $n=0$.

WDYT?

+
+$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 P_1 <: L_1, \ldots, P_n <: L_n. lsig$ where
+$L_i$ is the least upper bound of $B_i$ and $[P_i/Q_i]C_i, i \in 1..n$ and $lsig$ is the least upper bound of $fsig$ and $[P_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}
 
 
 \section{Reference}
 \LMLabel{reference}
 
 \subsection{Lexical Rules}
 \LMLabel{lexicalRules}
 
 \LMHash{}
@@ skipping 276 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------