pkg/dev_compiler/doc/definition/strong-dart.tex - sdk.git - Git at Google

 \documentclass[fleqn, draft]{article}
 \usepackage{proof, amsmath, amssymb, ifthen}
 \input{macros.tex}

 % types
 \newcommand{\Arrow}[3][-]{#2 \overset{#1}{\rightarrow} #3}
 \newcommand{\Bool}{\mathbf{bool}}
 \newcommand{\Bottom}{\mathbf{bottom}}
 \newcommand{\Dynamic}{\mathbf{dynamic}}
 \newcommand{\Null}{\mathbf{Null}}
 \newcommand{\Num}{\mathbf{num}}
 \newcommand{\Object}{\mathbf{Object}}
 \newcommand{\TApp}[2]{#1\mathrm{<}#2\mathrm{>}}
 \newcommand{\Type}{\mathbf{Type}}
 \newcommand{\Weak}[1]{\mathbf{\{#1\}}}
 \newcommand{\Sig}{\mathit{Sig}}
 \newcommand{\Boxed}[1]{\langle #1 \rangle}

 % expressions
 \newcommand{\eassign}[2]{#1 = #2}
 \newcommand{\eas}[2]{#1\ \mathbf{as}\ #2}
 \newcommand{\ebox}[2]{\langle#1\rangle_{#2}}
 \newcommand{\ecall}[2]{#1(#2)}
 \newcommand{\echeck}[2]{\kwop{check}(#1, #2)}
 \newcommand{\edcall}[2]{\kwop{dcall}(#1, #2)}
 \newcommand{\edload}[2]{\kwop{dload}(#1, #2)}
 \newcommand{\edo}[1]{\kwdo\{\,#1\,\}}
 \newcommand{\eff}{\mathrm{ff}}
 \newcommand{\eis}[2]{#1\ \mathbf{is}\ #2}
 \newcommand{\elabel}[1][l]{\mathit{l}}
 \newcommand{\elambda}[3]{(#1):#2 \Rightarrow #3}
 \newcommand{\eload}[2]{#1.#2}
 \newcommand{\enew}[3]{\mathbf{new}\,\TApp{#1}{#2}(#3)}
 \newcommand{\enull}{\mathbf{null}}
 \newcommand{\eobject}[2]{\kwobject_{#1} \{#2\}}
 \newcommand{\eprimapp}[2]{\ecall{#1}{#2}}
 \newcommand{\eprim}{\kwop{op}}
 \newcommand{\esend}[3]{\ecall{\eload{#1}{#2}}{#3}}
 \newcommand{\eset}[3]{\eassign{#1.#2}{#3}}
 \newcommand{\esuper}{\mathbf{super}}
 \newcommand{\ethis}{\mathbf{this}}
 \newcommand{\ethrow}{\mathbf{throw}}
 \newcommand{\ett}{\mathrm{tt}}
 \newcommand{\eunbox}[1]{{*#1}}

 % keywords
 \newcommand{\kwclass}{\kw{class}}
 \newcommand{\kwdo}{\kw{do}}
 \newcommand{\kwelse}{\kw{else}}
 \newcommand{\kwextends}{\kw{extends}}
 \newcommand{\kwfun}{\kw{fun}}
 \newcommand{\kwif}{\kw{if}}
 \newcommand{\kwin}{\kw{in}}
 \newcommand{\kwlet}{\kw{let}}
 \newcommand{\kwobject}{\kw{object}}
 \newcommand{\kwreturn}{\kw{return}}
 \newcommand{\kwthen}{\kw{then}}
 \newcommand{\kwvar}{\kw{var}}

 % declarations
 \newcommand{\dclass}[3]{\kwclass\ #1\ \kwextends\ #2\ \{#3\}}
 \newcommand{\dfun}[4]{#2(#3):#1 = #4}
 \newcommand{\dvar}[2]{\kwvar\ #1\ =\ #2}


 \newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2}
 \newcommand{\methodDecl}[3]{\kwfun\ #1 : \iftrans{#2 \triangleleft} #3}

 % statements
 \newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
 \newcommand{\sreturn}[1]{\kwreturn\ #1}

 % programs
 \newcommand{\program}[2]{\kwlet\ #1\ \kwin\ #2}

 % relational operators
 \newcommand{\sub}{\mathbin{<:}}

 % utilities
 \newcommand{\many}[1]{\overrightarrow{#1}}
 \newcommand{\alt}{\ \mathop{|}\ }
 \newcommand{\opt}[1]{[#1]}
 \newcommand{\bind}[3]{#1 \Leftarrow\, #2\ \kw{in}\ #3}

 \newcommand{\note}[1]{\textbf{NOTE:} \textit{#1}}

 %dynamic semantics
 \newcommand{\TypeError}{\mathbf{Error}}

 % inference rules
 \newcommand{\infrulem}[3][]{
   \begin{array}{c@{\ }c}
     \begin{array}{cccc}
       #2 \vspace{-2mm}
     \end{array} \\
     \hrulefill & #1 \\
     \begin{array}{l}
       #3
     \end{array}
   \end{array}
   }

 \newcommand{\axiomm}[2][]{
   \begin{array}{cc}
     \hrulefill & #1 \\
     \begin{array}{c}
       #2
     \end{array}
   \end{array}
   }

 \newcommand{\infrule}[3][]{
   \[
   \infrulem[#1]{#2}{#3}
   \]
   }

 \newcommand{\axiom}[2][]{
   \[
   \axiomm[#1]{#2}
   \]
   }

 % judgements and relations
 \newboolean{show_translation}
 \setboolean{show_translation}{false}
 \newcommand{\iftrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}{}}
 \newcommand{\ifnottrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}}

 \newcommand{\blockOk}[4]{#1 \vdash #2 \col #3\iftrans{\, \Uparrow\, #4}}
 \newcommand{\declOk}[5][]{#2 \vdash_{#1} #3 \, \Uparrow\, \iftrans{#4\, :\,} #5}
 \newcommand{\extends}[4][:]{#2[#3\ #1\ #4]}
 \newcommand{\fieldLookup}[4]{#1 \vdash #2.#3\, \leadsto_f\, #4}
 \newcommand{\methodLookup}[5]{#1 \vdash #2.#3\, \leadsto_m\, \iftrans{#4 \triangleleft} #5}
 \newcommand{\fieldAbsent}[3]{#1 \vdash #3 \notin #2}
 \newcommand{\methodAbsent}[3]{#1 \vdash #3 \notin #2}
 \newcommand{\hastype}[3]{#1 \vdash #2 \, : \, #3}
 \newcommand{\stmtOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow \iftrans{#4\, :\,} #5}
 \newcommand{\subst}[2]{[#1/#2]}
 \newcommand{\subtypeOfOpt}[5][?]{#2 \vdash\ #3 \sub^{#1} #4\, \Uparrow\, #5}
 \newcommand{\subtypeOf}[4][]{#2 \vdash\ #3 \sub^{#1} #4}
 \newcommand{\yieldsOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow\, \iftrans{#4\, :\,} #5}
 \newcommand{\programOk}[3]{#1 \vdash #2\iftrans{\, \Uparrow\, #3}}
 \newcommand{\ok}[2]{#1 \vdash #2\, \mbox{\textbf{ok}}}
 \newcommand{\overrideOk}[4]{#1 \vdash #2\,\kwextends\, #3 \Leftarrow\, #4}

 \newcommand{\down}[1]{\ensuremath{\downharpoonleft\!\!#1\!\!\downharpoonright}}
 \newcommand{\up}[1]{\ensuremath{\upharpoonleft\!\!#1\!\!\upharpoonright}}
 \newcommand{\sigof}[1]{\mathit{sigof}(#1)}
 \newcommand{\typeof}[1]{\mathit{typeof}(#1)}
 \newcommand{\sstext}[2]{\ifthenelse{\boolean{show_translation}}{#2}{#1}}

 \newcommand{\evaluatesTo}[5][]{\{#2\alt #3\}  \stepsto_{#1} \{#4 \alt #5\}}


 \title{Dart strong mode definition}

 \begin{document}

 \textbf{\large PRELIMINARY DRAFT}

 \section*{Syntax}


 Terms and types.  Note that we allow types to be optional in certain positions
 (currently function arguments and return types, and on variable declarations).
 Implicitly these are either inferred or filled in with dynamic.

 There are explicit terms for dynamic calls and loads, and for dynamic type
 checks.

 Fields can only be read or set within a method via a reference to this, so no
 dynamic set operation is required (essentially dynamic set becomes a dynamic
 call to a setter).  This just simplifies the presentation a bit.  Methods may be
 externally loaded from the object (either to call them, or to pass them as
 closurized functions).

 \[
 \begin{array}{lcl}
 \text{Type identifiers} & ::= &  C, G, T, S, \ldots \\
 %
 \text{Arrow kind ($k$)} & ::= &  +, -\\
 %
 \text{Types $\tau, \sigma$} & ::= &
  T \alt \Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \\ &&
    \alt \Bool
    \alt \Arrow[k]{\many{\tau}}{\sigma} \alt \TApp{C}{\many{\tau}} \\
 %
 \text{Ground types $\tau, \sigma$} & ::= &
  \Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \\ &&
    \alt \Bool
    \alt \Arrow[+]{\many{\Dynamic}}{\Dynamic} \alt \TApp{C}{\many{\Dynamic}} \\
 %
 \text{Optional type ($[\tau]$)} & ::= &  \_ \alt \tau \\
 %
 \text{Term identifiers} & ::= & a, b, x, y, m, n, \ldots \\
 %
 \text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{||} \ldots \\
 %
 \text{Expressions $e$} & ::= &
  x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&&
    \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{s}
    \alt \enew{C}{\many{\tau}}{} \\&&
    \alt \eprimapp{\eprim}{\many{e}} \alt \ecall{e}{\many{e}} \\&&
    \alt \eload{e}{m} \alt \eload{\ethis}{x} \\&&
    \alt \eassign{x}{e} \alt \eset{\ethis}{x}{e} \\&&
    \alt \ethrow \alt \eas{e}{\tau} \alt \eis{e}{\tau} \\
 %
 \text{Declaration ($\mathit{vd}$)} & ::= &
    \dvar{x:\opt{\tau}}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{s} \\
 %
 \text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{s_1}{s_2}
    \alt \sreturn{e} \alt s;s \\
 %
 \text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{vd}}} \\
 %
 \text{Toplevel decl ($\mathit{td}$)} & ::= & \mathit{vd} \alt \mathit{cd}\\
 %
 \text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{s}
 \end{array}
 \]


 Type contexts map type variables to their bounds.

 Class signatures describe the methods and fields in an object, along with the
 super class of the class.  There are no static methods or fields.

 The class hierararchy records the classes with their signatures.

 The term context maps term variables to their types.  I also abuse notation and
 allow for the attachment of an optional type to term contexts as follows:
 $\Gamma_\sigma$ refers to a term context within the body of a method whose class
 type is $\sigma$.

 \[
 \begin{array}{lcl}
 \text{Type context ($\Delta$)} & ::= &  \epsilon \alt \Delta, T \sub \tau \\
 \text{Class element ($\mathit{ce}$)} & ::= &
   \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
 \text{Class signature ($\Sig$)} & ::= &
   \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{ce}}} \\
 \text{Class hierarchy ($\Phi$)} & ::= &  \epsilon \alt \Phi, C\ :\ \Sig \\
 \text{Term context ($\Gamma$)} & ::= &  \epsilon \alt \Gamma, x\ :\ \tau
 \end{array}
 \]


 \section*{Subtyping}

 \subsection*{Variant Subtyping}

 We include a special kind of covariant function space to model certain dart
 idioms.  An arrow type decorated with a positive variance annotation ($+$)
 treats $\Dynamic$ in its argument list covariantly: or equivalently, it treats
 $\Dynamic$ as bottom.  This variant subtyping relation captures this special
 treatment of dynamic.

 \axiom{\subtypeOf[+]{\Phi, \Delta}{\Dynamic}{\tau}}

 \infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau} \quad \sigma \neq \Dynamic}
         {\subtypeOf[+]{\Phi, \Delta}{\sigma}{\tau}}

 \infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
         {\subtypeOf[-]{\Phi, \Delta}{\sigma}{\tau}}

 \subsection*{Invariant Subtyping}

 Regular subtyping is defined in a fairly standard way, except that generics are
 uniformly covariant, and that function argument types fall into the variant
 subtyping relation defined above.

 \axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Dynamic}}

 \axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Object}}

 \axiom{\subtypeOf{\Phi, \Delta}{\Bottom}{\tau}}

 \axiom{\subtypeOf{\Phi, \Delta}{\tau}{\tau}}

 \infrule{(S\, :\, \sigma) \in \Delta \quad
          \subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
         {\subtypeOf{\Phi, \Delta}{S}{\tau}}

 \infrule{\subtypeOf[k_1]{\Phi, \Delta}{\sigma_i}{\tau_i} \quad i \in 0, \ldots, n \quad\quad
          \subtypeOf{\Phi, \Delta}{\tau_r}{\sigma_r} \\
          \quad (k_0 = \mbox{-}) \lor (k_1 = \mbox{+})
         }
         {\subtypeOf{\Phi, \Delta}
                    {\Arrow[k_0]{\tau_0, \ldots, \tau_n}{\tau_r}}
                    {\Arrow[k_1]{\sigma_0, \ldots, \sigma_n}{\sigma_r}}}

 \infrule{\subtypeOf{\Phi, \Delta}{\tau_i}{\sigma_i} & i \in 0, \ldots, n}
         {\subtypeOf{\Phi, \Delta}
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\TApp{C}{\sigma_0, \ldots, \sigma_n}}}

 \infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}) \in \Phi \\
          \subtypeOf{\Phi, \Delta}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}}{\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
         {\subtypeOf{\Phi, \Delta}
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\TApp{G}{\sigma_0, \ldots, \sigma_m}}}


 \section*{Typing}
 \input{static-semantics}

 \pagebreak
 \section*{Elaboration}
 \setboolean{show_translation}{true}

 Elaboration is a type driven translation which maps a source Dart term to a
 translated term which corresponds to the original term with additional dynamic
 type checks inserted to reify the static unsoundness as runtime type errors.
 For the translation, we extend the source language slightly as follows.
 \[
 \begin{array}{lcl}
 \text{Expressions $e$} & ::= & \ldots
    \alt \edcall{e}{\many{e}} \alt \edload{e}{m} \alt \echeck{e}{\tau}\\
 \end{array}
 \]

 The expression language is extended with an explicitly checked dynamic call
 operation, and explicitly checked dynamic method load operation, and a runtime
 type test.  Note that while a user level cast throws an exception on failure,
 the runtime type test term introduced here produces a hard type error which
 cannot be caught programmatically.

 We also extend typing contexts slightly by adding an internal type to method signatures.
 \[
 \begin{array}{lcl}
 \text{Class element ($\mathit{ce}$)} & ::= &
   \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
 \end{array}
 \]
 A method signature of the form $\methodDecl{f}{\tau}{\sigma}$ describes a method
 whose public interface is described by $\sigma$, but which has an internal type
 $\tau$ which is a subtype of $\sigma$, but which is properly covariant in any
 type parameters.  The elaboration introduces runtime type checks to mediate
 between the two types.  This is discussed further in the translation of classes
 below.

 \input{static-semantics}


 \end{document}
	\documentclass[fleqn, draft]{article}
	\usepackage{proof, amsmath, amssymb, ifthen}
	\input{macros.tex}

	% types
	\newcommand{\Arrow}[3][-]{#2 \overset{#1}{\rightarrow} #3}
	\newcommand{\Bool}{\mathbf{bool}}
	\newcommand{\Bottom}{\mathbf{bottom}}
	\newcommand{\Dynamic}{\mathbf{dynamic}}
	\newcommand{\Null}{\mathbf{Null}}
	\newcommand{\Num}{\mathbf{num}}
	\newcommand{\Object}{\mathbf{Object}}
	\newcommand{\TApp}[2]{#1\mathrm{<}#2\mathrm{>}}
	\newcommand{\Type}{\mathbf{Type}}
	\newcommand{\Weak}[1]{\mathbf{\{#1\}}}
	\newcommand{\Sig}{\mathit{Sig}}
	\newcommand{\Boxed}[1]{\langle #1 \rangle}

	% expressions
	\newcommand{\eassign}[2]{#1 = #2}
	\newcommand{\eas}[2]{#1\ \mathbf{as}\ #2}
	\newcommand{\ebox}[2]{\langle#1\rangle_{#2}}
	\newcommand{\ecall}[2]{#1(#2)}
	\newcommand{\echeck}[2]{\kwop{check}(#1, #2)}
	\newcommand{\edcall}[2]{\kwop{dcall}(#1, #2)}
	\newcommand{\edload}[2]{\kwop{dload}(#1, #2)}
	\newcommand{\edo}[1]{\kwdo\{\,#1\,\}}
	\newcommand{\eff}{\mathrm{ff}}
	\newcommand{\eis}[2]{#1\ \mathbf{is}\ #2}
	\newcommand{\elabel}[1][l]{\mathit{l}}
	\newcommand{\elambda}[3]{(#1):#2 \Rightarrow #3}
	\newcommand{\eload}[2]{#1.#2}
	\newcommand{\enew}[3]{\mathbf{new}\,\TApp{#1}{#2}(#3)}
	\newcommand{\enull}{\mathbf{null}}
	\newcommand{\eobject}[2]{\kwobject_{#1} \{#2\}}
	\newcommand{\eprimapp}[2]{\ecall{#1}{#2}}
	\newcommand{\eprim}{\kwop{op}}
	\newcommand{\esend}[3]{\ecall{\eload{#1}{#2}}{#3}}
	\newcommand{\eset}[3]{\eassign{#1.#2}{#3}}
	\newcommand{\esuper}{\mathbf{super}}
	\newcommand{\ethis}{\mathbf{this}}
	\newcommand{\ethrow}{\mathbf{throw}}
	\newcommand{\ett}{\mathrm{tt}}
	\newcommand{\eunbox}[1]{{*#1}}

	% keywords
	\newcommand{\kwclass}{\kw{class}}
	\newcommand{\kwdo}{\kw{do}}
	\newcommand{\kwelse}{\kw{else}}
	\newcommand{\kwextends}{\kw{extends}}
	\newcommand{\kwfun}{\kw{fun}}
	\newcommand{\kwif}{\kw{if}}
	\newcommand{\kwin}{\kw{in}}
	\newcommand{\kwlet}{\kw{let}}
	\newcommand{\kwobject}{\kw{object}}
	\newcommand{\kwreturn}{\kw{return}}
	\newcommand{\kwthen}{\kw{then}}
	\newcommand{\kwvar}{\kw{var}}

	% declarations
	\newcommand{\dclass}[3]{\kwclass\ #1\ \kwextends\ #2\ \{#3\}}
	\newcommand{\dfun}[4]{#2(#3):#1 = #4}
	\newcommand{\dvar}[2]{\kwvar\ #1\ =\ #2}


	\newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2}
	\newcommand{\methodDecl}[3]{\kwfun\ #1 : \iftrans{#2 \triangleleft} #3}

	% statements
	\newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
	\newcommand{\sreturn}[1]{\kwreturn\ #1}

	% programs
	\newcommand{\program}[2]{\kwlet\ #1\ \kwin\ #2}

	% relational operators
	\newcommand{\sub}{\mathbin{<:}}

	% utilities
	\newcommand{\many}[1]{\overrightarrow{#1}}
	\newcommand{\alt}{\ \mathop{\|}\ }
	\newcommand{\opt}[1]{[#1]}
	\newcommand{\bind}[3]{#1 \Leftarrow\, #2\ \kw{in}\ #3}

	\newcommand{\note}[1]{\textbf{NOTE:} \textit{#1}}

	%dynamic semantics
	\newcommand{\TypeError}{\mathbf{Error}}

	% inference rules
	\newcommand{\infrulem}[3][]{
	\begin{array}{c@{\ }c}
	\begin{array}{cccc}
	#2 \vspace{-2mm}
	\end{array} \\
	\hrulefill & #1 \\
	\begin{array}{l}
	#3
	\end{array}
	\end{array}
	}

	\newcommand{\axiomm}[2][]{
	\begin{array}{cc}
	\hrulefill & #1 \\
	\begin{array}{c}
	#2
	\end{array}
	\end{array}
	}

	\newcommand{\infrule}[3][]{
	\[
	\infrulem[#1]{#2}{#3}
	\]
	}

	\newcommand{\axiom}[2][]{
	\[
	\axiomm[#1]{#2}
	\]
	}

	% judgements and relations
	\newboolean{show_translation}
	\setboolean{show_translation}{false}
	\newcommand{\iftrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}{}}
	\newcommand{\ifnottrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}}

	\newcommand{\blockOk}[4]{#1 \vdash #2 \col #3\iftrans{\, \Uparrow\, #4}}
	\newcommand{\declOk}[5][]{#2 \vdash_{#1} #3 \, \Uparrow\, \iftrans{#4\, :\,} #5}
	\newcommand{\extends}[4][:]{#2[#3\ #1\ #4]}
	\newcommand{\fieldLookup}[4]{#1 \vdash #2.#3\, \leadsto_f\, #4}
	\newcommand{\methodLookup}[5]{#1 \vdash #2.#3\, \leadsto_m\, \iftrans{#4 \triangleleft} #5}
	\newcommand{\fieldAbsent}[3]{#1 \vdash #3 \notin #2}
	\newcommand{\methodAbsent}[3]{#1 \vdash #3 \notin #2}
	\newcommand{\hastype}[3]{#1 \vdash #2 \, : \, #3}
	\newcommand{\stmtOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow \iftrans{#4\, :\,} #5}
	\newcommand{\subst}[2]{[#1/#2]}
	\newcommand{\subtypeOfOpt}[5][?]{#2 \vdash\ #3 \sub^{#1} #4\, \Uparrow\, #5}
	\newcommand{\subtypeOf}[4][]{#2 \vdash\ #3 \sub^{#1} #4}
	\newcommand{\yieldsOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow\, \iftrans{#4\, :\,} #5}
	\newcommand{\programOk}[3]{#1 \vdash #2\iftrans{\, \Uparrow\, #3}}
	\newcommand{\ok}[2]{#1 \vdash #2\, \mbox{\textbf{ok}}}
	\newcommand{\overrideOk}[4]{#1 \vdash #2\,\kwextends\, #3 \Leftarrow\, #4}

	\newcommand{\down}[1]{\ensuremath{\downharpoonleft\!\!#1\!\!\downharpoonright}}
	\newcommand{\up}[1]{\ensuremath{\upharpoonleft\!\!#1\!\!\upharpoonright}}
	\newcommand{\sigof}[1]{\mathit{sigof}(#1)}
	\newcommand{\typeof}[1]{\mathit{typeof}(#1)}
	\newcommand{\sstext}[2]{\ifthenelse{\boolean{show_translation}}{#2}{#1}}

	\newcommand{\evaluatesTo}[5][]{\{#2\alt #3\} \stepsto_{#1} \{#4 \alt #5\}}


	\title{Dart strong mode definition}

	\begin{document}

	\textbf{\large PRELIMINARY DRAFT}

	\section*{Syntax}


	Terms and types. Note that we allow types to be optional in certain positions
	(currently function arguments and return types, and on variable declarations).
	Implicitly these are either inferred or filled in with dynamic.

	There are explicit terms for dynamic calls and loads, and for dynamic type
	checks.

	Fields can only be read or set within a method via a reference to this, so no
	dynamic set operation is required (essentially dynamic set becomes a dynamic
	call to a setter). This just simplifies the presentation a bit. Methods may be
	externally loaded from the object (either to call them, or to pass them as
	closurized functions).

	\[
	\begin{array}{lcl}
	\text{Type identifiers} & ::= & C, G, T, S, \ldots \\
	%
	\text{Arrow kind ($k$)} & ::= & +, -\\
	%
	\text{Types $\tau, \sigma$} & ::= &
	T \alt \Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \\ &&
	\alt \Bool
	\alt \Arrow[k]{\many{\tau}}{\sigma} \alt \TApp{C}{\many{\tau}} \\
	%
	\text{Ground types $\tau, \sigma$} & ::= &
	\Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \\ &&
	\alt \Bool
	\alt \Arrow[+]{\many{\Dynamic}}{\Dynamic} \alt \TApp{C}{\many{\Dynamic}} \\
	%
	\text{Optional type ($[\tau]$)} & ::= & \_ \alt \tau \\
	%
	\text{Term identifiers} & ::= & a, b, x, y, m, n, \ldots \\
	%
	\text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{\|\|} \ldots \\
	%
	\text{Expressions $e$} & ::= &
	x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&&
	\alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{s}
	\alt \enew{C}{\many{\tau}}{} \\&&
	\alt \eprimapp{\eprim}{\many{e}} \alt \ecall{e}{\many{e}} \\&&
	\alt \eload{e}{m} \alt \eload{\ethis}{x} \\&&
	\alt \eassign{x}{e} \alt \eset{\ethis}{x}{e} \\&&
	\alt \ethrow \alt \eas{e}{\tau} \alt \eis{e}{\tau} \\
	%
	\text{Declaration ($\mathit{vd}$)} & ::= &
	\dvar{x:\opt{\tau}}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{s} \\
	%
	\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{s_1}{s_2}
	\alt \sreturn{e} \alt s;s \\
	%
	\text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{vd}}} \\
	%
	\text{Toplevel decl ($\mathit{td}$)} & ::= & \mathit{vd} \alt \mathit{cd}\\
	%
	\text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{s}
	\end{array}
	\]


	Type contexts map type variables to their bounds.

	Class signatures describe the methods and fields in an object, along with the
	super class of the class. There are no static methods or fields.

	The class hierararchy records the classes with their signatures.

	The term context maps term variables to their types. I also abuse notation and
	allow for the attachment of an optional type to term contexts as follows:
	$\Gamma_\sigma$ refers to a term context within the body of a method whose class
	type is $\sigma$.

	\[
	\begin{array}{lcl}
	\text{Type context ($\Delta$)} & ::= & \epsilon \alt \Delta, T \sub \tau \\
	\text{Class element ($\mathit{ce}$)} & ::= &
	\fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
	\text{Class signature ($\Sig$)} & ::= &
	\dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{ce}}} \\
	\text{Class hierarchy ($\Phi$)} & ::= & \epsilon \alt \Phi, C\ :\ \Sig \\
	\text{Term context ($\Gamma$)} & ::= & \epsilon \alt \Gamma, x\ :\ \tau
	\end{array}
	\]


	\section*{Subtyping}

	\subsection*{Variant Subtyping}

	We include a special kind of covariant function space to model certain dart
	idioms. An arrow type decorated with a positive variance annotation ($+$)
	treats $\Dynamic$ in its argument list covariantly: or equivalently, it treats
	$\Dynamic$ as bottom. This variant subtyping relation captures this special
	treatment of dynamic.

	\axiom{\subtypeOf[+]{\Phi, \Delta}{\Dynamic}{\tau}}

	\infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau} \quad \sigma \neq \Dynamic}
	{\subtypeOf[+]{\Phi, \Delta}{\sigma}{\tau}}

	\infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
	{\subtypeOf[-]{\Phi, \Delta}{\sigma}{\tau}}

	\subsection*{Invariant Subtyping}

	Regular subtyping is defined in a fairly standard way, except that generics are
	uniformly covariant, and that function argument types fall into the variant
	subtyping relation defined above.

	\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Dynamic}}

	\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Object}}

	\axiom{\subtypeOf{\Phi, \Delta}{\Bottom}{\tau}}

	\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\tau}}

	\infrule{(S\, :\, \sigma) \in \Delta \quad
	\subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
	{\subtypeOf{\Phi, \Delta}{S}{\tau}}

	\infrule{\subtypeOf[k_1]{\Phi, \Delta}{\sigma_i}{\tau_i} \quad i \in 0, \ldots, n \quad\quad
	\subtypeOf{\Phi, \Delta}{\tau_r}{\sigma_r} \\
	\quad (k_0 = \mbox{-}) \lor (k_1 = \mbox{+})
	}
	{\subtypeOf{\Phi, \Delta}
	{\Arrow[k_0]{\tau_0, \ldots, \tau_n}{\tau_r}}
	{\Arrow[k_1]{\sigma_0, \ldots, \sigma_n}{\sigma_r}}}

	\infrule{\subtypeOf{\Phi, \Delta}{\tau_i}{\sigma_i} & i \in 0, \ldots, n}
	{\subtypeOf{\Phi, \Delta}
	{\TApp{C}{\tau_0, \ldots, \tau_n}}
	{\TApp{C}{\sigma_0, \ldots, \sigma_n}}}

	\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}) \in \Phi \\
	\subtypeOf{\Phi, \Delta}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}}{\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
	{\subtypeOf{\Phi, \Delta}
	{\TApp{C}{\tau_0, \ldots, \tau_n}}
	{\TApp{G}{\sigma_0, \ldots, \sigma_m}}}



	\section*{Typing}
	\input{static-semantics}

	\pagebreak
	\section*{Elaboration}
	\setboolean{show_translation}{true}

	Elaboration is a type driven translation which maps a source Dart term to a
	translated term which corresponds to the original term with additional dynamic
	type checks inserted to reify the static unsoundness as runtime type errors.
	For the translation, we extend the source language slightly as follows.
	\[
	\begin{array}{lcl}
	\text{Expressions $e$} & ::= & \ldots
	\alt \edcall{e}{\many{e}} \alt \edload{e}{m} \alt \echeck{e}{\tau}\\
	\end{array}
	\]

	The expression language is extended with an explicitly checked dynamic call
	operation, and explicitly checked dynamic method load operation, and a runtime
	type test. Note that while a user level cast throws an exception on failure,
	the runtime type test term introduced here produces a hard type error which
	cannot be caught programmatically.

	We also extend typing contexts slightly by adding an internal type to method signatures.
	\[
	\begin{array}{lcl}
	\text{Class element ($\mathit{ce}$)} & ::= &
	\fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
	\end{array}
	\]
	A method signature of the form $\methodDecl{f}{\tau}{\sigma}$ describes a method
	whose public interface is described by $\sigma$, but which has an internal type
	$\tau$ which is a subtype of $\sigma$, but which is properly covariant in any
	type parameters. The elaboration introduces runtime type checks to mediate
	between the two types. This is discussed further in the translation of classes
	below.

	\input{static-semantics}


	\end{document}