blob: 216b476238945a8af00dcfffd647077cdd5bb1e4 [file] [log] [blame]
 \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}