Index: doc/definition/strong-dart.tex |
diff --git a/doc/definition/strong-dart.tex b/doc/definition/strong-dart.tex |
index 3da3ca40c7dced4a19b35d7a9e898b4cb51c728f..520d2bf08cddfaff8798f20b092536e83f49d204 100644 |
--- a/doc/definition/strong-dart.tex |
+++ b/doc/definition/strong-dart.tex |
@@ -1,8 +1,9 @@ |
-\documentclass[fleqn]{article} |
-\usepackage{proof, amsmath} |
+\documentclass[fleqn, draft]{article} |
+\usepackage{proof, amsmath, amssymb, ifthen} |
+\input{macros.tex} |
% types |
-\newcommand{\Arrow}[2]{#1 \rightarrow #2} |
+\newcommand{\Arrow}[3][-]{#2 \overset{#1}{\rightarrow} #3} |
\newcommand{\Bool}{\mathbf{bool}} |
\newcommand{\Bottom}{\mathbf{bottom}} |
\newcommand{\Dynamic}{\mathbf{dynamic}} |
@@ -13,37 +14,48 @@ |
\newcommand{\Type}{\mathbf{Type}} |
% expressions |
-\newcommand{\eapp}[2]{#1(#2)} |
-\newcommand{\eas}[2]{#1\ \mathbf{as}\ #2} |
\newcommand{\eassign}[2]{#1 = #2} |
+\newcommand{\eas}[2]{#1\ \mathbf{as}\ #2} |
+\newcommand{\echeck}[2]{\kwop{check}(#1, #2)} |
+\newcommand{\ecall}[2]{#1(#2)} |
+\newcommand{\edcall}[2]{\kwop{dcall}(#1, #2)} |
+\newcommand{\edload}[2]{\kwop{dload}(#1, #2)} |
\newcommand{\eff}{\mathrm{ff}} |
\newcommand{\eis}[2]{#1\ \mathbf{is}\ #2} |
-\newcommand{\elambda}[2]{(#1) \Rightarrow #2} |
+\newcommand{\elambda}[3]{(#1):#2 \Rightarrow #3} |
+\newcommand{\eload}[2]{#1.#2} |
+\newcommand{\eset}[3]{\eassign{#1.#2}{#3}} |
\newcommand{\enew}[3]{\mathbf{new}\,\TApp{#1}{#2}(#3)} |
\newcommand{\enull}{\mathbf{null}} |
-\newcommand{\eprimapp}[2]{\eapp{#1}{#2}} |
-\newcommand{\eproj}[2]{#1.#2} |
-\newcommand{\esend}[3]{\eapp{\eproj{#1}{#2}}{#3}} |
+\newcommand{\eprim}{\kwop{op}} |
+\newcommand{\eprimapp}[2]{\ecall{#1}{#2}} |
+\newcommand{\esend}[3]{\ecall{\eload{#1}{#2}}{#3}} |
\newcommand{\esuper}{\mathbf{super}} |
\newcommand{\ethis}{\mathbf{this}} |
+\newcommand{\ethrow}{\mathbf{throw}} |
\newcommand{\ett}{\mathrm{tt}} |
% keywords |
-\newcommand{\kwclass}{\mathbf{class}} |
-\newcommand{\kwextends}{\mathbf{extends}} |
-\newcommand{\kwelse}{\mathbf{else}} |
-\newcommand{\kwif}{\mathbf{if}} |
-\newcommand{\kwin}{\mathbf{in}} |
-\newcommand{\kwlet}{\mathbf{let}} |
-\newcommand{\kwreturn}{\mathbf{return}} |
-\newcommand{\kwthen}{\mathbf{then}} |
-\newcommand{\kwvar}{\mathbf{var}} |
+\newcommand{\kwclass}{\kw{class}} |
+\newcommand{\kwextends}{\kw{extends}} |
+\newcommand{\kwelse}{\kw{else}} |
+\newcommand{\kwfun}{\kw{fun}} |
+\newcommand{\kwif}{\kw{if}} |
+\newcommand{\kwin}{\kw{in}} |
+\newcommand{\kwlet}{\kw{let}} |
+\newcommand{\kwreturn}{\kw{return}} |
+\newcommand{\kwthen}{\kw{then}} |
+\newcommand{\kwvar}{\kw{var}} |
% declarations |
\newcommand{\dclass}[3]{\kwclass\ #1\ \kwextends\ #2\ \{#3\}} |
-\newcommand{\dfun}[4]{#1\ #2(#3)\ #4} |
+\newcommand{\dfun}[4]{#2(#3):#1 = #4} |
\newcommand{\dvar}[2]{\kwvar\ #1\ =\ #2} |
+ |
+\newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2} |
+\newcommand{\methodDecl}[2]{\kwfun\ #1 : #2} |
+ |
% statements |
\newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3} |
\newcommand{\sreturn}[1]{\kwreturn\ #1} |
@@ -52,106 +64,256 @@ |
\newcommand{\program}[2]{\kwlet\ #1\ \kwin\ #2} |
% relational operators |
-\newcommand{\sub}{\mathop{<:}} |
+\newcommand{\sub}{\mathbin{<:}} |
% utilities |
\newcommand{\many}[1]{\overrightarrow{#1}} |
\newcommand{\alt}{\ \mathop{|}\ } |
+\newcommand{\opt}[1]{[#1]} |
% inference rules |
-\newcommand{\axiom}[1]{\infer{#1}{}} |
-\newcommand{\infrule}[2]{\infer{#2}{#1}} |
+\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}{}} |
-% relations |
+\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}[4]{#1 \vdash #2.#3\, \leadsto_m\, #4} |
+\newcommand{\hastype}[3]{#1 \vdash #2 \, : \, #3} |
+\newcommand{\stmtOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow \iftrans{#4\, :\,} #5} |
\newcommand{\subst}[2]{[#1/#2]} |
-\newcommand{\subtypeOf}[3]{#1 \vdash\ #2 \sub\ #3} |
+\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{\sstext}[2]{\ifthenelse{\boolean{show_translation}}{#2}{#1}} |
+ |
+ |
\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{\many{\tau}}{\sigma} \alt \TApp{C}{\many{\tau}} \\ |
+ 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{Optional type ($[\tau]$)} & ::= & \_ \alt \tau \\ |
% |
\text{Term identifiers} & ::= & a, b, x, y, m, n, \ldots \\ |
% |
\text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{||} \ldots \\ |
% |
-\text{lhs ($l$)} & ::= & x \alt \eproj{e}{m} \\ |
-% |
\text{Expressions $e$} & ::= & |
- x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \alt \esuper |
- \alt \elambda{\many{x:\tau}}{e} \alt \enew{C}{\many{\tau}}{\many{e}} \\&& |
- \alt \eprimapp{\phi}{\many{e}} \alt \eapp{e}{\many{e}} |
- \alt \eproj{e}{m} \alt \eassign{l}{e} \\&& |
- \alt \eas{e}{\tau} \alt \eis{e}{\tau} \\ |
+ x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&& |
+ \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{e} |
+ \alt \enew{C}{\many{\tau}}{} \\&& |
+ \alt \eprimapp{\eprim}{\many{e}} \alt \ecall{e}{\many{e}} |
+ \alt \edcall{e}{\many{e}} \\&& |
+ \alt \eload{e}{m} \alt \edload{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} \alt \echeck{e}{\tau}\\ |
% |
\text{Declaration ($\mathit{vd}$)} & ::= & |
- \dvar{x}{e} \alt \dvar{x:\tau}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{b} \\ |
+ \dvar{x:\opt{\tau}}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{s} \\ |
% |
-\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{b_1}{b_2} |
+\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{s_1}{s_2} |
\alt \sreturn{e} \alt s;s \\ |
% |
-\text{Blocks ($b$)} & ::= & \{s;\} \\ |
-% |
\text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{vd}}} \\ |
% |
\text{Toplevel decl ($\mathit{td}$)} & ::= & \mathit{vd} \alt \mathit{cd}\\ |
% |
-\text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{b} |
+\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{Class signature ($\mathit{Sig}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{x:\tau}} \\ |
-\text{Type context ($\Delta$)} & ::= & \epsilon \alt \Delta, X \sub \tau \\ |
-\text{Class hierarchy ($\Phi$)} & ::= & \epsilon \alt \Phi, C\ :\ \mathit{Sig} |
+\text{Type context ($\Delta$)} & ::= & \epsilon \alt \Delta, T \sub \tau \\ |
+\text{Class element ($\mathit{ce}$)} & ::= & |
+ \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau} \\ |
+\text{Class signature ($\mathit{Sig}$)} & ::= & |
+ \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{ce}}} \\ |
+\text{Class hierarchy ($\Phi$)} & ::= & \epsilon \alt \Phi, C\ :\ \mathit{Sig} \\ |
+\text{Term context ($\Gamma$)} & ::= & \epsilon \alt \Gamma, x\ :\ \tau |
\end{array} |
\] |
\section*{Subtyping} |
-\[ |
-\begin{array}{ccc} |
-\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{\Delta = \extends[\sub]{\Delta'}{S}{\sigma} & |
+ |
+\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{\Phi, \Delta}{\sigma_i}{\tau_i} & i \in 0, \ldots, n & |
- \subtypeOf{\Phi, \Delta}{\tau_r}{\sigma_r}} |
+ {\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{\tau_0, \ldots, \tau_n}{\tau_r}} |
- {\Arrow{\sigma_0, \ldots, \sigma_n}{\sigma_r}}} \\\\ |
-% |
+ {\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{\Phi = \extends{\Phi'}{C}{\dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}} \\ |
+ {\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}}} |
-\end{array} |
-\] |
+ |
+\section*{Field and Method lookup} |
+ |
+\subsection*{Field lookup} |
+ |
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\ |
+ \fieldDecl{x}{\tau} \in \many{\mathit{ce}} |
+ } |
+ {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}} |
+ } |
+ |
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad x \notin \many{\mathit{ce}} \\ |
+ \fieldLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{x}{\tau} |
+ } |
+ {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}} |
+ } |
+ |
+\subsection*{Method lookup} |
+ |
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\ |
+ \methodDecl{m}{\tau} \in \many{\mathit{ce}} |
+ } |
+ {\methodLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}} |
+ } |
+ |
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad m \notin \many{\mathit{ce}} \\ |
+ \methodLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{m}{\tau} |
+ } |
+ {\methodLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}} |
+ } |
+ |
+ |
+ |
+\section*{Typing} |
+\input{static-semantics} |
+ |
+\section*{Elaboration} |
+ |
+These are the same rules, extended with a translated term which corresponds to |
+the original term with the additional dynamic type checks inserted to reify the |
+static unsoundness as runtime type errors. |
+ |
+\setboolean{show_translation}{true} |
+\input{static-semantics} |
+ |
\end{document} |