Static semantics v0.1

doc/definition/strong-dart.tex

Index: doc/definition/strong-dart.tex
diff --git a/doc/definition/strong-dart.tex b/doc/definition/strong-dart.tex
index 520d2bf08cddfaff8798f20b092536e83f49d204..216b476238945a8af00dcfffd647077cdd5bb1e4 100644
--- a/doc/definition/strong-dart.tex
+++ b/doc/definition/strong-dart.tex
@@ -12,37 +12,47 @@
 \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{\echeck}[2]{\kwop{check}(#1, #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{\eset}[3]{\eassign{#1.#2}{#3}}
 \newcommand{\enew}[3]{\mathbf{new}\,\TApp{#1}{#2}(#3)}
 \newcommand{\enull}{\mathbf{null}}
-\newcommand{\eprim}{\kwop{op}}
+\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{\kwextends}{\kw{extends}}
+\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}}
@@ -54,7 +64,7 @@
 
 
 \newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2}
-\newcommand{\methodDecl}[2]{\kwfun\ #1 : #2}
+\newcommand{\methodDecl}[3]{\kwfun\ #1 : \iftrans{#2 \triangleleft} #3}
 
 % statements
 \newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
@@ -70,6 +80,12 @@
 \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][]{
@@ -109,22 +125,32 @@
 \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}[4]{#1 \vdash #2.#3\, \leadsto_m\, #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}
@@ -160,6 +186,11 @@ closurized functions).
    \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 \\
@@ -168,13 +199,12 @@ closurized functions).
 %
 \text{Expressions $e$} & ::= & 
  x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&&
-   \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{e} 
+   \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 \edcall{e}{\many{e}}  \\&&
-   \alt \eload{e}{m} \alt \edload{e}{m} \alt \eload{\ethis}{x} \\&&
+   \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} \alt \echeck{e}{\tau}\\
+   \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} \\
@@ -182,7 +212,7 @@ closurized functions).
 \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{S}}}{\many{\mathit{vd}}} \\
+\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}\\
 %
@@ -207,10 +237,10 @@ 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} \\
-\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} \\
+  \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}
 \]
@@ -271,48 +301,46 @@ subtyping relation defined above.
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
 
-\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}
 
+\pagebreak
 \section*{Elaboration}
+\setboolean{show_translation}{true}
 
-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.
+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.
 
-\setboolean{show_translation}{true}
 \input{static-semantics}