Use more-specific instead of subtyping for type promotion; extend definition of more-specific to in…

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification \\
 {\large Draft Version 0.61}}
 \author{The Dart Team}
 \begin{document}
@@ skipping 4334 matching lines @@
 }
 %does not denote a type available in the current lexical scope. It is a %compile-time error % CHANGED
 %run-time error
 %if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters.
 
 %Note, that, in checked mode, it is a dynamic type error if a malformed type is used in a type test as specified in \ref{dynamicTypeSystem}.
 
 %It is a static warning if $T$ is malformed or malbounded.
 %does not denote a type available in the current lexical scope. 
 
-Let $v$  be a local variable or a formal parameter. An is-expression of the form \code{$v$ \IS{}! $T$} shows that $v$  has type $T$ iff $T$ is a subtype of the type $S$ of the expression $v$ and  both $T \ne \DYNAMIC{}$ and $S \ne \DYNAMIC{}$.
+Let $v$  be a local variable or a formal parameter. An is-expression of the form \code{$v$ \IS{}! $T$} shows that $v$  has type $T$ iff $T$ is more specific than the type $S$ of the expression $v$ and  both $T \ne \DYNAMIC{}$ and $S \ne \DYNAMIC{}$.
 
 The static type of an is-expression is \code{bool}. 
 %It is a static warning if if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters. 
 
 
 
 \subsection{ Type Cast}
 \label{typeCast}
 
 The {\em cast expression} ensures that an object is a member of a type.
@@ skipping 1332 matching lines @@
 A type $T$ is more specific than a type $S$, written $T << S$,  if one of the following conditions is met:
 \begin{itemize}
 \item $T$ is $S$.
 \item T is $\bot$.
 \item S is \DYNAMIC{}.
 \item $S$ is a direct supertype of $T$.
 \item $T$ is a type parameter and $S$ is the upper bound of $T$.
 \item $T$ is a type parameter and $S$ is \cd{Object}.
 \item $T$ is of the form $I<T_1, \ldots, T_n>$ and $S$ is of the form $I<S_1, \ldots, S_n>$ and:
 $T_i << S_i, 1 \le i \le n$
+\item $T$ and $S$ are both function types, and $T << S$ under the rules of section \ref{functionTypes}.
 \item $T << U$ and $U << S$.
 \end{itemize}
 
 $<<$ is a partial order on types.
 $T$ is a subtype of $S$, written $T <: S$, iff $[\bot/\DYNAMIC{}]T << S$.
 
 \rationale{
 Note that $<:$ is not a partial order on types, it is only binary relation on types. This is because $<:$ is not transitive. If it was, the subtype rule would have a cycle. For example:
 $List <: List<String>$ and $List<int> <: List$, but $List<int>$ is not a subtype of $List<String>$.
 Although $<:$ is not a partial order on types, it does contain a partial order, namely $<<$. This means that, barring raw types, intuition about classical subtype rules does apply.
@@ skipping 86 matching lines @@
 
 % ensure that Object  and dynamic may be assign dot a function type
 A function is always an instance of some class that implements the class \code{Function} and implements a \CALL{} method with the same signature as the function. All function types are subtypes of \code{Function}.
 If a type $I$ includes an instance method named \CALL{}, and the type of \CALL{} is the function type $F$, then $I$ is considered to be a subtype of $F$.  It is a static warning if a concrete class implements \cd{Function} and does not have a concrete method named \CALL{}.
 
 
 
 
 %\commentary{Need to specify how a function values dynamic type is derived from its static signature.}
 
+A function type $(T_1, \ldots T_{k}, [T_{k+1}  \ldots, T_{n+m}]) \rightarrow T$ is a more specific than the
+function type $(S_1, \ldots, S_{k+j}, [S_{k+j+1} \ldots, S_{n}]) \rightarrow S$, if all of the following conditions are met:
+\begin{enumerate}
+\item Either
+\begin{itemize}
+\item $S$ is \VOID{}, Or
+\item  $T << S$.
+\end{itemize}
+\item $\forall i \in 1 .. n, T_i << S_i$.
+\end{enumerate}
+
+
+A function type $(T_1, \ldots T_n, \{T_{x_1}$ $x_1, \ldots, T_{x_k}$ $x_k\}) \rightarrow T$ is more specific than the function type $(S_1, \ldots, S_n, \{S_{y_1}$ $y_1, \ldots, S_{y_m}$ $y_m\}) \rightarrow S$, if all of the following conditions are met:
+\begin{enumerate}
+\item Either
+\begin{itemize}
+\item $S$ is \VOID{}, Or
+\item  $T  << S$.
+\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}
+
+Furthermore, if $F$ is a function type, $F << \code{Function}$.
+
+
 \subsection{Type \DYNAMIC{}}
 \label{typeDynamic}
 
 The type  \DYNAMIC{}  denotes the unknown type. 
 
 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.
 
 \commentary{This means that given a generic declaration $G<T_1, \ldots, T_n>$, the type $G$ is equivalent to $G< \DYNAMIC{},  \ldots,  \DYNAMIC{}>$.
 }
 
@@ skipping 38 matching lines @@
 The only subtype relations that pertain to void are therefore:
 \begin{itemize}
 \item
 $\VOID{} <: \VOID{}$ (by reflexivity)
 \item
 $\bot <: \VOID{}$ (as bottom is a subtype of all types).
 \item
 $\VOID{} <:   \DYNAMIC{}$ (as  \DYNAMIC{} is a supertype of all types)
 \end{itemize}
 
+The analogous rules also hold for the $<<$ relation for  similar reasons.
+
 Hence, the static checker will issue warnings if one attempts to access a member of the result of a void method invocation (even for members of \NULL{}, such as \code{==}).  Likewise, passing the result of a void method as a parameter or assigning it to a variable will cause a warning unless the variable/formal parameter has type dynamic.
 
 On the other hand, it is possible to return the result of a void method from within a void method. One can also return \NULL{}; or a value of type \DYNAMIC{}. Returning any other result will cause a type warning. In checked mode, a dynamic type error would arise if a non-null object was returned from a void method (since no object has runtime type  \DYNAMIC{}).
 }
 
 \commentary {The name \VOID{} does not denote a \cd{Type} object.}
 
 \rationale {
 It is syntacticly illegal to use \VOID{} as an expression, and it would make no sense to do so.
 Type objects reify the runtime types of instances. No instance ever has type \VOID{}.  
@@ skipping 170 matching lines @@
 \item The names of compile time constant variables never use lower case letters. If they consist of multiple words, those words are separated by underscores. Examples: PI,  I\_AM\_A\_CONSTANT.
 \item The names of functions (including getters, setters, methods and local or library functions) and non-constant variables begin with a lowercase letter. If the name consists of multiple words, each  word (except the first) begins with an uppercase letter.  No other uppercase letters are used. Examples: camlCase, dart4TheWorld
 \item The names of types (including classes and type aliases) begin with an upper case letter.  If the name consists of multiple words, each  word  begins with an uppercase letter.  No other uppercase letters are used. Examples: CamlCase, Dart4TheWorld.
 \item The names of type variables are short (preferably single letter). Examples: T, S, K, V , E.
 \item The names of libraries or library prefixes never use upper case letters. If they consist of multiple words, those words are separated by underscores. Example: my\_favorite\_library.
 \end{itemize}
 }
 
 
 \end{document}